%%% Assignment 6 %%% Out: Mon 29 Oct %%% Due: Mon 5 Nov % % This assignment is to be turned in on paper. % % % 1. Equality. % % A type X is said to be infinite if % there is an operation f : X -> X on it that is: % % - injective, i.e. fx = fy implies x = y, % % - not surjective, i.e. it's not the case that % for every y there is some x with y = fx. % % Prove formally that the type of natural numbers is infinite. % Specifically, give natural deduction proofs of the following: % % x : nat, y : nat |- sx = sy => x = y % % x : nat |- ~(sx = 0) % % Finally, assign terms and give the proof terms for these proofs. % % % 2. The predicate Even(n). % % Implement the predicate Even(n) on natural numbers % by giving formation, introduction, and elimination rules % following the pattern of m = n . % % Prove, from your rules, that 4 is even, and that 3 is not. % % % 3. Induction. % % Prove informally, by induction, that sn + sn is always greater than sn. % % How much of your proof can be formalized in our current system? % Indicate which steps are justified by our rules, and which are not. % % % 4. Quantifiers. % % Give a natural deduction proof of the following proposition: % % (?x:t. !y:t . A(x,y)) => (!y:t. ?x:t . A(x,y)) % % Do you think the converse of the above can be proved? % Justify your answer. % %%% %%% %%%