%%% 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.
%
%%%
%%%
%%%