%%% Assignment 1 %%% Out: Wednesday Sep 5 %%% Due: Monday Sep 17 %%% Author : Brigitte Pientka proof a : (A & (B & C)) => (A & B) = begin [A & (B & C); % 1 Assumption A; % 2 AndE1 1 B & C; % 3 AndE2 1 B; % 4 AndE1 3 A & B ]; % 5 AndI 2, 4 (A & (B & C)) => (A & B) % 6 ImpI 1,5 end; proof b : (A => B) => ((B => C) => (A => C)) = begin [A => B; % 1 Assumption [B => C; % 2 Assumption [A; % 3 Assumption B; % 4 ImpE 1, 3 C]; % 5 ImpE 3 4 A => C]; % 6 ImpI 3, 5 (B => C) => (A => C)]; % 7 ImpI 2, 6 (A => B) => (B => C) => (A => C); % 8 ImpI 1, 7 end; proof c : ((A => B) & (A | C)) => (B | C) = begin [((A => B) & (A | C)); % 1 Assumption A => B; % 2 AndE1 1 A | C; % 3 AndE2 2 [A; % 4 Assumption (OrE(1)) B; % 5 ImpE 2,4 B | C]; % 6 OrE(1) [C; % 7 Assumption (OrE(2)) B | C]; % 8 OrI2 B | C]; % 9 OrE ((A => B) & (A | C)) => (B | C); % 10 ImpI 1,9 end; proof da : (A => (A => F)) => (A => F) = begin [A => (A => F); % 1 Assumption (from ImpI ) [A; % 2 Assumption (from ImpI on ~A) A => F; % 3 ImpE 1, 2 F]; % 4 Imp A => F; ]; (A => (A => F)) => (A => F); end; proof d : (A => ~ A) => ~ A = begin [A => ~ A; % 1 Assumption [A; % 2 Assumption ~ A; % 3 ImpE 2 F]; % 4 ImpE 2 ~ A; % 5 ImpI ]; (A => ~ A) => ~ A; % 6 ImpI end; proof e : (~ A & ~ B) => ~ (A | B) = begin [~ A & ~ B; ~ A; ~ B; [A | B; [A; F]; [B; F]; F]; ~ (A | B)]; (~ A & ~ B) => ~ (A | B); end; proof f : A <=> A = begin [A; A]; A => A; A <=> A; end; proof g : (A <=> T) <=> A = begin [A; [T; A]; T => A; [A; T]; A => T; A <=> T]; A => (A <=> T); [A <=> T; A => T; T => A; T; A]; (A <=> T) => A; (A <=> T) <=> A; end; proof h: ((A & B) => C) <=> (A => (B => C)) = begin [A => (B => C); [A & B; A; B; (B => C); C]; (A & B) => C]; (A => (B => C)) => ((A & B) => C); [(A & B) => C; [A; [B; A & B; C]; B => C]; A => (B => C)]; ((A & B) => C) => (A => (B => C)); ((A & B) => C) <=> (A => (B => C)); end;