%{ Recitation 2 (Sep 5, 2012) Introduction to Tutch and & or | true T false F implication => not ~ Invoke `tutch -v filename` for justifications of each step. }% proof contraction : A & A => A = begin [ A & A; % brackets indicate scope of assumption A & A A ]; % from this assumption, we can conclude A (via and-elimination) A & A => A; % implication-introduction end; proof trueContr : A => A & T = begin [ A; % assuming A... T; % T-introduction A & T ]; % and-introduction A => A & T; end; proof orComm : A | B => B | A = begin [ A | B; % or-elimination [ A; B | A ]; % or-elimination, branch 1 [ B; B | A ]; % or-elimination, branch 2 B | A ]; % or-elimination, conclusion A | B => B | A; end; proof drop : A => B => A = begin [ A; [ B; A ]; B => A ]; A => B => A; end; proof impDef : (~A | B) => A => B = begin [ ~A | B; [ A; [ ~A ; F; B ]; [ B ; B ]; B ]; A => B ]; (~A | B) => A => B; end; proof compose : (A => B) => (B => C) => (A => C) = begin [ A => B; [ B => C; [ A; B; % by A => B C ]; % by B => C A => C ]; (B => C) => (A => C) ]; (A => B) => (B => C) => (A => C); end; proof curry : (A & B => C) => (A => B => C) = begin [ A & B => C; [ A; [ B; A & B; C ]; B => C ]; A => B => C ]; (A & B => C) => (A => B => C); end; proof uncurry : (A => B => C) => (A & B => C) = begin [ A => B => C; [ A & B; A; B => C; B; C ]; A & B => C ]; (A => B => C) => (A & B => C); end; proof dnLem : ~~(A | ~A) = begin [ ~(A | ~A); [ A; A | ~A; F ]; ~A; A | ~A; F ]; ~~(A | ~A); end; proof tne : ~~~A => ~A = begin [ ~~~A; [ A; [ ~A; F ]; ~~A; F ]; ~A ]; ~~~A => ~A; end;