diff options
| author | Landon D. C. Elkind | 2021-02-14 18:50:50 -0700 |
|---|---|---|
| committer | GitHub | 2021-02-14 18:50:50 -0700 |
| commit | d2cf655a8a37fb83b1c407a10054be4f6839587c (patch) | |
| tree | b4423de954cc286f7e326a2755f2b55b5eaec1bf /PL.v | |
| parent | 3b834485e5a3627c4bc07f47c7a5e8b9ab27bea6 (diff) | |
Proof of *5.7 now follows PM sketch
Diffstat (limited to 'PL.v')
| -rw-r--r-- | PL.v | 1894 |
1 files changed, 997 insertions, 897 deletions
@@ -6,9 +6,9 @@ Import Unicode.Utf8. for the propositional calculus in *1.*) Axiom Impl1_01 : ∀ P Q : Prop, - (P → Q) = (~P ∨ Q). + (P → Q) = (¬P ∨ Q). (*This is a definition in Principia: there → is a - defined sign and ∨, ~ are primitive ones. So + defined sign and ∨, ¬ are primitive ones. So we will use this axiom to switch between disjunction and implication.*) @@ -44,10 +44,10 @@ Import No1. (*We proceed to the deductions of of Principia.*) Theorem Abs2_01 : ∀ P : Prop, - (P → ~P) → ~P. + (P → ¬P) → ¬P. Proof. intros P. - specialize Taut1_2 with (~P). - replace (~P ∨ ~P) with (P → ~P). + specialize Taut1_2 with (¬P). + replace (¬P ∨ ¬P) with (P → ¬P). apply MP1_1. apply Impl1_01. Qed. @@ -55,19 +55,19 @@ Qed. Theorem Simp2_02 : ∀ P Q : Prop, Q → (P → Q). Proof. intros P Q. - specialize Add1_3 with (~P) Q. - replace (~P ∨ Q) with (P → Q). + specialize Add1_3 with (¬P) Q. + replace (¬P ∨ Q) with (P → Q). apply (MP1_1 Q (P → Q)). apply Impl1_01. Qed. Theorem Transp2_03 : ∀ P Q : Prop, - (P → ~Q) → (Q → ~P). + (P → ¬Q) → (Q → ¬P). Proof. intros P Q. - specialize Perm1_4 with (~P) (~Q). - replace (~P ∨ ~Q) with (P → ~Q). - replace (~Q ∨ ~P) with (Q → ~P). - apply (MP1_1 (P → ~Q) (Q → ~P)). + specialize Perm1_4 with (¬P) (¬Q). + replace (¬P ∨ ¬Q) with (P → ¬Q). + replace (¬Q ∨ ¬P) with (Q → ¬P). + apply (MP1_1 (P → ¬Q) (Q → ¬P)). apply Impl1_01. apply Impl1_01. Qed. @@ -75,11 +75,11 @@ Qed. Theorem Comm2_04 : ∀ P Q R : Prop, (P → (Q → R)) → (Q → (P → R)). Proof. intros P Q R. - specialize Assoc1_5 with (~P) (~Q) R. - replace (~Q ∨ R) with (Q → R). - replace (~P ∨ (Q → R)) with (P → (Q → R)). - replace (~P ∨ R) with (P → R). - replace (~Q ∨ (P → R)) with (Q → (P → R)). + specialize Assoc1_5 with (¬P) (¬Q) R. + replace (¬Q ∨ R) with (Q → R). + replace (¬P ∨ (Q → R)) with (P → (Q → R)). + replace (¬P ∨ R) with (P → R). + replace (¬Q ∨ (P → R)) with (Q → (P → R)). apply (MP1_1 (P → Q → R) (Q → P → R)). apply Impl1_01. apply Impl1_01. @@ -90,9 +90,9 @@ Qed. Theorem Syll2_05 : ∀ P Q R : Prop, (Q → R) → ((P → Q) → (P → R)). Proof. intros P Q R. - specialize Sum1_6 with (~P) Q R. - replace (~P ∨ Q) with (P → Q). - replace (~P ∨ R) with (P → R). + specialize Sum1_6 with (¬P) Q R. + replace (¬P ∨ Q) with (P → Q). + replace (¬P ∨ R) with (P → R). apply (MP1_1 (Q → R) ((P → Q) → (P → R))). apply Impl1_01. apply Impl1_01. @@ -135,41 +135,43 @@ Proof. intros P. Qed. Theorem n2_1 : ∀ P : Prop, - (~P) ∨ P. + (¬P) ∨ P. Proof. intros P. specialize Id2_08 with P. - replace (~P ∨ P) with (P → P). + replace (¬P ∨ P) with (P → P). apply MP1_1. apply Impl1_01. Qed. Theorem n2_11 : ∀ P : Prop, - P ∨ ~P. + P ∨ ¬P. Proof. intros P. - specialize Perm1_4 with (~P) P. + specialize Perm1_4 with (¬P) P. intros Perm1_4. specialize n2_1 with P. intros n2_1. + apply (MP1_1 (¬P∨P) (P∨¬P)). apply Perm1_4. apply n2_1. Qed. Theorem n2_12 : ∀ P : Prop, - P → ~~P. + P → ¬¬P. Proof. intros P. - specialize n2_11 with (~P). + specialize n2_11 with (¬P). intros n2_11. rewrite Impl1_01. apply n2_11. Qed. Theorem n2_13 : ∀ P : Prop, - P ∨ ~~~P. + P ∨ ¬¬¬P. Proof. intros P. - specialize Sum1_6 with P (~P) (~~~P). + specialize Sum1_6 with P (¬P) (¬¬¬P). intros Sum1_6. - specialize n2_12 with (~P). + specialize n2_12 with (¬P). intros n2_12. + apply (MP1_1 (¬P→¬¬¬P) ((P∨¬P)→(P∨¬¬¬P))). apply Sum1_6. apply n2_12. specialize n2_11 with P. @@ -178,31 +180,32 @@ Proof. intros P. Qed. Theorem n2_14 : ∀ P : Prop, - ~~P → P. + ¬¬P → P. Proof. intros P. - specialize Perm1_4 with P (~~~P). + specialize Perm1_4 with P (¬¬¬P). intros Perm1_4. specialize n2_13 with P. intros n2_13. rewrite Impl1_01. + apply (MP1_1 (P∨¬¬¬P) (¬¬¬P∨P)). apply Perm1_4. apply n2_13. Qed. Theorem Transp2_15 : ∀ P Q : Prop, - (~P → Q) → (~Q → P). + (¬P → Q) → (¬Q → P). Proof. intros P Q. - specialize Syll2_05 with (~P) Q (~~Q). + specialize Syll2_05 with (¬P) Q (¬¬Q). intros Syll2_05a. specialize n2_12 with Q. intros n2_12. - specialize Transp2_03 with (~P) (~Q). + specialize Transp2_03 with (¬P) (¬Q). intros Transp2_03. - specialize Syll2_05 with (~Q) (~~P) P. + specialize Syll2_05 with (¬Q) (¬¬P) P. intros Syll2_05b. - specialize Syll2_05 with (~P → Q) (~P → ~~Q) (~Q → ~~P). + specialize Syll2_05 with (¬P → Q) (¬P → ¬¬Q) (¬Q → ¬¬P). intros Syll2_05c. - specialize Syll2_05 with (~P → Q) (~Q → ~~P) (~Q → P). + specialize Syll2_05 with (¬P → Q) (¬Q → ¬¬P) (¬Q → P). intros Syll2_05d. apply Syll2_05d. apply Syll2_05b. @@ -211,6 +214,7 @@ Proof. intros P Q. apply n2_14. apply Syll2_05c. apply Transp2_03. + apply (MP1_1 (Q→¬¬Q) ((¬P→Q)→(¬P→¬¬Q))). apply Syll2_05a. apply n2_12. Qed. @@ -227,13 +231,13 @@ Ltac MP H1 H2 := end. Theorem Transp2_16 : ∀ P Q : Prop, - (P → Q) → (~Q → ~P). + (P → Q) → (¬Q → ¬P). Proof. intros P Q. specialize n2_12 with Q. intros n2_12a. - specialize Syll2_05 with P Q (~~Q). + specialize Syll2_05 with P Q (¬¬Q). intros Syll2_05a. - specialize Transp2_03 with P (~Q). + specialize Transp2_03 with P (¬Q). intros Transp2_03a. MP n2_12a Syll2_05a. Syll Syll2_05a Transp2_03a S. @@ -241,13 +245,13 @@ Proof. intros P Q. Qed. Theorem Transp2_17 : ∀ P Q : Prop, - (~Q → ~P) → (P → Q). + (¬Q → ¬P) → (P → Q). Proof. intros P Q. - specialize Transp2_03 with (~Q) P. + specialize Transp2_03 with (¬Q) P. intros Transp2_03a. specialize n2_14 with Q. intros n2_14a. - specialize Syll2_05 with P (~~Q) Q. + specialize Syll2_05 with P (¬¬Q) Q. intros Syll2_05a. MP n2_14a Syll2_05a. Syll Transp2_03a Syll2_05a S. @@ -255,14 +259,14 @@ Proof. intros P Q. Qed. Theorem n2_18 : ∀ P : Prop, - (~P → P) → P. + (¬P → P) → P. Proof. intros P. specialize n2_12 with P. intro n2_12a. - specialize Syll2_05 with (~P) P (~~P). + specialize Syll2_05 with (¬P) P (¬¬P). intro Syll2_05a. MP Syll2_05a n2_12. - specialize Abs2_01 with (~P). + specialize Abs2_01 with (¬P). intros Abs2_01a. Syll Syll2_05a Abs2_01a Sa. specialize n2_14 with P. @@ -283,22 +287,22 @@ Proof. intros P Q. Qed. Theorem n2_21 : ∀ P Q : Prop, - ~P → (P → Q). + ¬P → (P → Q). Proof. intros P Q. - specialize n2_2 with (~P) Q. + specialize n2_2 with (¬P) Q. intros n2_2a. specialize Impl1_01 with P Q. intros Impl1_01a. - replace (~P∨Q) with (P→Q) in n2_2a. + replace (¬P∨Q) with (P→Q) in n2_2a. apply n2_2a. Qed. Theorem n2_24 : ∀ P Q : Prop, - P → (~P → Q). + P → (¬P → Q). Proof. intros P Q. specialize n2_21 with P Q. intros n2_21a. - specialize Comm2_04 with (~P) P Q. + specialize Comm2_04 with (¬P) P Q. intros Comm2_04a. apply Comm2_04a. apply n2_21a. @@ -309,20 +313,20 @@ Theorem n2_25 : ∀ P Q : Prop, Proof. intros P Q. specialize n2_1 with (P ∨ Q). intros n2_1a. - specialize Assoc1_5 with (~(P∨Q)) P Q. + specialize Assoc1_5 with (¬(P∨Q)) P Q. intros Assoc1_5a. MP Assoc1_5a n2_1a. - replace (~(P∨Q)∨Q) with (P∨Q→Q) in Assoc1_5a. + replace (¬(P∨Q)∨Q) with (P∨Q→Q) in Assoc1_5a. apply Assoc1_5a. apply Impl1_01. Qed. Theorem n2_26 : ∀ P Q : Prop, - ~P ∨ ((P → Q) → Q). + ¬P ∨ ((P → Q) → Q). Proof. intros P Q. - specialize n2_25 with (~P) Q. + specialize n2_25 with (¬P) Q. intros n2_25a. - replace (~P∨Q) with (P→Q) in n2_25a. + replace (¬P∨Q) with (P→Q) in n2_25a. apply n2_25a. apply Impl1_01. Qed. @@ -332,7 +336,7 @@ Theorem n2_27 : ∀ P Q : Prop, Proof. intros P Q. specialize n2_26 with P Q. intros n2_26a. - replace (~P∨((P→Q)→Q)) with (P→(P→Q)→Q) in n2_26a. + replace (¬P∨((P→Q)→Q)) with (P→(P→Q)→Q) in n2_26a. apply n2_26a. apply Impl1_01. Qed. @@ -464,11 +468,11 @@ Proof. intros P Q. Qed. Theorem n2_42 : ∀ P Q : Prop, - (~P ∨ (P → Q)) → (P → Q). + (¬P ∨ (P → Q)) → (P → Q). Proof. intros P Q. - specialize n2_4 with (~P) Q. + specialize n2_4 with (¬P) Q. intros n2_4a. - replace (~P∨Q) with (P→Q) in n2_4a. + replace (¬P∨Q) with (P→Q) in n2_4a. apply n2_4a. apply Impl1_01. Qed. @@ -477,13 +481,13 @@ Theorem n2_43 : ∀ P Q : Prop, Proof. intros P Q. specialize n2_42 with P Q. intros n2_42a. - replace (~P ∨ (P→Q)) with (P→(P→Q)) in n2_42a. + replace (¬P ∨ (P→Q)) with (P→(P→Q)) in n2_42a. apply n2_42a. apply Impl1_01. Qed. Theorem n2_45 : ∀ P Q : Prop, - ~(P ∨ Q) → ~P. + ¬(P ∨ Q) → ¬P. Proof. intros P Q. specialize n2_2 with P Q. intros n2_2a. @@ -494,7 +498,7 @@ Proof. intros P Q. Qed. Theorem n2_46 : ∀ P Q : Prop, - ~(P ∨ Q) → ~Q. + ¬(P ∨ Q) → ¬Q. Proof. intros P Q. specialize Add1_3 with P Q. intros Add1_3a. @@ -505,76 +509,76 @@ Proof. intros P Q. Qed. Theorem n2_47 : ∀ P Q : Prop, - ~(P ∨ Q) → (~P ∨ Q). + ¬(P ∨ Q) → (¬P ∨ Q). Proof. intros P Q. specialize n2_45 with P Q. intros n2_45a. - specialize n2_2 with (~P) Q. + specialize n2_2 with (¬P) Q. intros n2_2a. Syll n2_45a n2_2a S. apply S. Qed. Theorem n2_48 : ∀ P Q : Prop, - ~(P ∨ Q) → (P ∨ ~Q). + ¬(P ∨ Q) → (P ∨ ¬Q). Proof. intros P Q. specialize n2_46 with P Q. intros n2_46a. - specialize Add1_3 with P (~Q). + specialize Add1_3 with P (¬Q). intros Add1_3a. Syll n2_46a Add1_3a S. apply S. Qed. Theorem n2_49 : ∀ P Q : Prop, - ~(P ∨ Q) → (~P ∨ ~Q). + ¬(P ∨ Q) → (¬P ∨ ¬Q). Proof. intros P Q. specialize n2_45 with P Q. intros n2_45a. - specialize n2_2 with (~P) (~Q). + specialize n2_2 with (¬P) (¬Q). intros n2_2a. Syll n2_45a n2_2a S. apply S. Qed. Theorem n2_5 : ∀ P Q : Prop, - ~(P → Q) → (~P → Q). + ¬(P → Q) → (¬P → Q). Proof. intros P Q. - specialize n2_47 with (~P) Q. + specialize n2_47 with (¬P) Q. intros n2_47a. - replace (~P∨Q) with (P→Q) in n2_47a. - replace (~~P∨Q) with (~P→Q) in n2_47a. + replace (¬P∨Q) with (P→Q) in n2_47a. + replace (¬¬P∨Q) with (¬P→Q) in n2_47a. apply n2_47a. apply Impl1_01. apply Impl1_01. Qed. Theorem n2_51 : ∀ P Q : Prop, - ~(P → Q) → (P → ~Q). + ¬(P → Q) → (P → ¬Q). Proof. intros P Q. - specialize n2_48 with (~P) Q. + specialize n2_48 with (¬P) Q. intros n2_48a. - replace (~P∨Q) with (P→Q) in n2_48a. - replace (~P∨~Q) with (P→~Q) in n2_48a. + replace (¬P∨Q) with (P→Q) in n2_48a. + replace (¬P∨¬Q) with (P→¬Q) in n2_48a. apply n2_48a. apply Impl1_01. apply Impl1_01. Qed. Theorem n2_52 : ∀ P Q : Prop, - ~(P → Q) → (~P → ~Q). + ¬(P → Q) → (¬P → ¬Q). Proof. intros P Q. - specialize n2_49 with (~P) Q. + specialize n2_49 with (¬P) Q. intros n2_49a. - replace (~P∨Q) with (P→Q) in n2_49a. - replace (~~P∨~Q) with (~P→~Q) in n2_49a. + replace (¬P∨Q) with (P→Q) in n2_49a. + replace (¬¬P∨¬Q) with (¬P→¬Q) in n2_49a. apply n2_49a. apply Impl1_01. apply Impl1_01. Qed. Theorem n2_521 : ∀ P Q : Prop, - ~(P→Q)→(Q→P). + ¬(P→Q)→(Q→P). Proof. intros P Q. specialize n2_52 with P Q. intros n2_52a. @@ -585,44 +589,44 @@ Proof. intros P Q. Qed. Theorem n2_53 : ∀ P Q : Prop, - (P ∨ Q) → (~P → Q). + (P ∨ Q) → (¬P → Q). Proof. intros P Q. specialize n2_12 with P. intros n2_12a. - specialize n2_38 with Q P (~~P). + specialize n2_38 with Q P (¬¬P). intros n2_38a. MP n2_38a n2_12a. - replace (~~P∨Q) with (~P→Q) in n2_38a. + replace (¬¬P∨Q) with (¬P→Q) in n2_38a. apply n2_38a. apply Impl1_01. Qed. Theorem n2_54 : ∀ P Q : Prop, - (~P → Q) → (P ∨ Q). + (¬P → Q) → (P ∨ Q). Proof. intros P Q. specialize n2_14 with P. intros n2_14a. - specialize n2_38 with Q (~~P) P. + specialize n2_38 with Q (¬¬P) P. intros n2_38a. MP n2_38a n2_12a. - replace (~~P∨Q) with (~P→Q) in n2_38a. + replace (¬¬P∨Q) with (¬P→Q) in n2_38a. apply n2_38a. apply Impl1_01. Qed. Theorem n2_55 : ∀ P Q : Prop, - ~P → ((P ∨ Q) → Q). + ¬P → ((P ∨ Q) → Q). Proof. intros P Q. specialize n2_53 with P Q. intros n2_53a. - specialize Comm2_04 with (P∨Q) (~P) Q. + specialize Comm2_04 with (P∨Q) (¬P) Q. intros Comm2_04a. MP n2_53a Comm2_04a. apply Comm2_04a. Qed. Theorem n2_56 : ∀ P Q : Prop, - ~Q → ((P ∨ Q) → P). + ¬Q → ((P ∨ Q) → P). Proof. intros P Q. specialize n2_55 with Q P. intros n2_55a. @@ -636,27 +640,27 @@ Proof. intros P Q. Qed. Theorem n2_6 : ∀ P Q : Prop, - (~P→Q) → ((P → Q) → Q). + (¬P→Q) → ((P → Q) → Q). Proof. intros P Q. - specialize n2_38 with Q (~P) Q. + specialize n2_38 with Q (¬P) Q. intros n2_38a. specialize Taut1_2 with Q. intros Taut1_2a. - specialize Syll2_05 with (~P∨Q) (Q∨Q) Q. + specialize Syll2_05 with (¬P∨Q) (Q∨Q) Q. intros Syll2_05a. MP Syll2_05a Taut1_2a. Syll n2_38a Syll2_05a S. - replace (~P∨Q) with (P→Q) in S. + replace (¬P∨Q) with (P→Q) in S. apply S. apply Impl1_01. Qed. Theorem n2_61 : ∀ P Q : Prop, - (P → Q) → ((~P → Q) → Q). + (P → Q) → ((¬P → Q) → Q). Proof. intros P Q. specialize n2_6 with P Q. intros n2_6a. - specialize Comm2_04 with (~P→Q) (P→Q) Q. + specialize Comm2_04 with (¬P→Q) (P→Q) Q. intros Comm2_04a. MP Comm2_04a n2_6a. apply Comm2_04a. @@ -685,26 +689,26 @@ Proof. intros P Q. Qed. Theorem n2_63 : ∀ P Q : Prop, - (P ∨ Q) → ((~P ∨ Q) → Q). + (P ∨ Q) → ((¬P ∨ Q) → Q). Proof. intros P Q. specialize n2_62 with P Q. intros n2_62a. - replace (~P∨Q) with (P→Q). + replace (¬P∨Q) with (P→Q). apply n2_62a. apply Impl1_01. Qed. Theorem n2_64 : ∀ P Q : Prop, - (P ∨ Q) → ((P ∨ ~Q) → P). + (P ∨ Q) → ((P ∨ ¬Q) → P). Proof. intros P Q. specialize n2_63 with Q P. intros n2_63a. specialize Perm1_4 with P Q. intros Perm1_4a. Syll n2_63a Perm1_4a Ha. - specialize Syll2_06 with (P∨~Q) (~Q∨P) P. + specialize Syll2_06 with (P∨¬Q) (¬Q∨P) P. intros Syll2_06a. - specialize Perm1_4 with P (~Q). + specialize Perm1_4 with P (¬Q). intros Perm1_4b. MP Syll2_06a Perm1_4b. Syll Syll2_06a Ha S. @@ -712,12 +716,12 @@ Proof. intros P Q. Qed. Theorem n2_65 : ∀ P Q : Prop, - (P → Q) → ((P → ~Q) → ~P). + (P → Q) → ((P → ¬Q) → ¬P). Proof. intros P Q. - specialize n2_64 with (~P) Q. + specialize n2_64 with (¬P) Q. intros n2_64a. - replace (~P∨Q) with (P→Q) in n2_64a. - replace (~P∨~Q) with (P→~Q) in n2_64a. + replace (¬P∨Q) with (P→Q) in n2_64a. + replace (¬P∨¬Q) with (P→¬Q) in n2_64a. apply n2_64a. apply Impl1_01. apply Impl1_01. @@ -728,12 +732,12 @@ Theorem n2_67 : ∀ P Q : Prop, Proof. intros P Q. specialize n2_54 with P Q. intros n2_54a. - specialize Syll2_06 with (~P→Q) (P∨Q) Q. + specialize Syll2_06 with (¬P→Q) (P∨Q) Q. intros Syll2_06a. MP Syll2_06a n2_54a. specialize n2_24 with P Q. intros n2_24. - specialize Syll2_06 with P (~P→Q) Q. + specialize Syll2_06 with P (¬P→Q) Q. intros Syll2_06b. MP Syll2_06b n2_24a. Syll Syll2_06b Syll2_06a S. @@ -743,9 +747,9 @@ Qed. Theorem n2_68 : ∀ P Q : Prop, ((P → Q) → Q) → (P ∨ Q). Proof. intros P Q. - specialize n2_67 with (~P) Q. + specialize n2_67 with (¬P) Q. intros n2_67a. - replace (~P∨Q) with (P→Q) in n2_67a. + replace (¬P∨Q) with (P→Q) in n2_67a. specialize n2_54 with P Q. intros n2_54a. Syll n2_67a n2_54a S. @@ -801,21 +805,21 @@ Qed. Theorem n2_75 : ∀ P Q R : Prop, (P ∨ Q) → ((P ∨ (Q → R)) → (P ∨ R)). Proof. intros P Q R. - specialize n2_74 with P (~Q) R. + specialize n2_74 with P (¬Q) R. intros n2_74a. specialize n2_53 with Q P. intros n2_53a. Syll n2_53a n2_74a Sa. - specialize n2_31 with P (~Q) R. + specialize n2_31 with P (¬Q) R. intros n2_31a. - specialize Syll2_06 with (P∨(~Q)∨R)((P∨(~Q))∨R) (P∨R). + specialize Syll2_06 with (P∨(¬Q)∨R)((P∨(¬Q))∨R) (P∨R). intros Syll2_06a. MP Syll2_06a n2_31a. Syll Sa Syll2_06a Sb. specialize Perm1_4 with P Q. intros Perm1_4a. (*not cited*) Syll Perm1_4a Sb Sc. - replace (~Q∨R) with (Q→R) in Sc. + replace (¬Q∨R) with (Q→R) in Sc. apply Sc. apply Impl1_01. Qed. @@ -834,11 +838,11 @@ Qed. Theorem n2_77 : ∀ P Q R : Prop, (P → (Q → R)) → ((P → Q) → (P → R)). Proof. intros P Q R. - specialize n2_76 with (~P) Q R. + specialize n2_76 with (¬P) Q R. intros n2_76a. - replace (~P∨(Q→R)) with (P→Q→R) in n2_76a. - replace (~P∨Q) with (P→Q) in n2_76a. - replace (~P∨R) with (P→R) in n2_76a. + replace (¬P∨(Q→R)) with (P→Q→R) in n2_76a. + replace (¬P∨Q) with (P→Q) in n2_76a. + replace (¬P∨R) with (P→R) in n2_76a. apply n2_76a. apply Impl1_01. apply Impl1_01. @@ -846,14 +850,14 @@ Proof. intros P Q R. Qed. Theorem n2_8 : ∀ Q R S : Prop, - (Q ∨ R) → ((~R ∨ S) → (Q ∨ S)). + (Q ∨ R) → ((¬R ∨ S) → (Q ∨ S)). Proof. intros Q R S. specialize n2_53 with R Q. intros n2_53a. specialize Perm1_4 with Q R. intros Perm1_4a. Syll Perm1_4a n2_53a Ha. - specialize n2_38 with S (~R) Q. + specialize n2_38 with S (¬R) Q. intros n2_38a. Syll H n2_38a Hb. apply Hb. @@ -874,11 +878,11 @@ Proof. intros P Q R S. Qed. Theorem n2_82 : ∀ P Q R S : Prop, - (P ∨ Q ∨ R)→((P ∨ ~R ∨ S)→(P ∨ Q ∨ S)). + (P ∨ Q ∨ R)→((P ∨ ¬R ∨ S)→(P ∨ Q ∨ S)). Proof. intros P Q R S. specialize n2_8 with Q R S. intros n2_8a. - specialize n2_81 with P (Q∨R) (~R∨S) (Q∨S). + specialize n2_81 with P (Q∨R) (¬R∨S) (Q∨S). intros n2_81a. MP n2_81a n2_8a. apply n2_81a. @@ -887,15 +891,15 @@ Qed. Theorem n2_83 : ∀ P Q R S : Prop, (P→(Q→R))→((P→(R→S))→(P→(Q→S))). Proof. intros P Q R S. - specialize n2_82 with (~P) (~Q) R S. + specialize n2_82 with (¬P) (¬Q) R S. intros n2_82a. - replace (~Q∨R) with (Q→R) in n2_82a. - replace (~P∨(Q→R)) with (P→Q→R) in n2_82a. - replace (~R∨S) with (R→S) in n2_82a. - replace (~P∨(R→S)) with (P→R→S) in n2_82a. - replace (~Q∨S) with (Q→S) in n2_82a. - replace (~Q∨S) with (Q→S) in n2_82a. - replace (~P∨(Q→S)) with (P→Q→S) in n2_82a. + replace (¬Q∨R) with (Q→R) in n2_82a. + replace (¬P∨(Q→R)) with (P→Q→R) in n2_82a. + replace (¬R∨S) with (R→S) in n2_82a. + replace (¬P∨(R→S)) with (P→R→S) in n2_82a. + replace (¬Q∨S) with (Q→S) in n2_82a. + replace (¬Q∨S) with (Q→S) in n2_82a. + replace (¬P∨(Q→S)) with (P→Q→S) in n2_82a. apply n2_82a. apply Impl1_01. apply Impl1_01. @@ -919,15 +923,15 @@ Proof. intros P Q R. specialize Syll2_05 with (P∨Q) (P∨R) R. intros Syll2_05a. Syll n2_55a Syll2_05a Ha. - specialize n2_83 with (~P) ((P∨Q)→(P∨R)) ((P∨Q)→R) (Q→R). + specialize n2_83 with (¬P) ((P∨Q)→(P∨R)) ((P∨Q)→R) (Q→R). intros n2_83a. MP n2_83a Ha. - specialize Comm2_04 with (~P) (P∨Q→P∨R) (Q→R). + specialize Comm2_04 with (¬P) (P∨Q→P∨R) (Q→R). intros Comm2_04a. Syll Ha Comm2_04a Hb. specialize n2_54 with P (Q→R). intros n2_54a. - specialize Simp2_02 with (~P) ((P∨Q→R)→(Q→R)). + specialize Simp2_02 with (¬P) ((P∨Q→R)→(Q→R)). intros Simp2_02a. (*Not cited*) (*Greg's suggestion per the BRS list on June 25, 2017.*) MP Syll2_06a Simp2_02a. @@ -939,11 +943,11 @@ Qed. Theorem n2_86 : ∀ P Q R : Prop, ((P → Q) → (P → R)) → (P → (Q → R)). Proof. intros P Q R. - specialize n2_85 with (~P) Q R. + specialize n2_85 with (¬P) Q R. intros n2_85a. - replace (~P∨Q) with (P→Q) in n2_85a. - replace (~P∨R) with (P→R) in n2_85a. - replace (~P∨(Q→R)) with (P→Q→R) in n2_85a. + replace (¬P∨Q) with (P→Q) in n2_85a. + replace (¬P∨R) with (P→R) in n2_85a. + replace (¬P∨(Q→R)) with (P→Q→R) in n2_85a. apply n2_85a. apply Impl1_01. apply Impl1_01. @@ -958,19 +962,19 @@ Import No1. Import No2. Axiom Prod3_01 : ∀ P Q : Prop, - (P ∧ Q) = ~(~P ∨ ~Q). + (P ∧ Q) = ¬(¬P ∨ ¬Q). Axiom Abb3_02 : ∀ P Q R : Prop, (P → Q → R) = (P → Q) ∧ (Q → R). Theorem Conj3_03 : ∀ P Q : Prop, P → Q → (P∧Q). Proof. intros P Q. - specialize n2_11 with (~P∨~Q). intros n2_11a. - specialize n2_32 with (~P) (~Q) (~(~P ∨ ~Q)). intros n2_32a. + specialize n2_11 with (¬P∨¬Q). intros n2_11a. + specialize n2_32 with (¬P) (¬Q) (¬(¬P ∨ ¬Q)). intros n2_32a. MP n2_32a n2_11a. - replace (~(~P∨~Q)) with (P∧Q) in n2_32a. - replace (~Q ∨ (P∧Q)) with (Q→(P∧Q)) in n2_32a. - replace (~P ∨ (Q → (P∧Q))) with (P→Q→(P∧Q)) in n2_32a. + replace (¬(¬P∨¬Q)) with (P∧Q) in n2_32a. + replace (¬Q ∨ (P∧Q)) with (Q→(P∧Q)) in n2_32a. + replace (¬P ∨ (Q → (P∧Q))) with (P→Q→(P∧Q)) in n2_32a. apply n2_32a. apply Impl1_01. apply Impl1_01. @@ -986,9 +990,9 @@ Ltac Conj H1 H2 := end. Theorem n3_1 : ∀ P Q : Prop, - (P ∧ Q) → ~(~P ∨ ~Q). + (P ∧ Q) → ¬(¬P ∨ ¬Q). Proof. intros P Q. - replace (~(~P∨~Q)) with (P∧Q). + replace (¬(¬P∨¬Q)) with (P∧Q). specialize Id2_08 with (P∧Q). intros Id2_08a. apply Id2_08a. @@ -996,9 +1000,9 @@ Proof. intros P Q. Qed. Theorem n3_11 : ∀ P Q : Prop, - ~(~P ∨ ~Q) → (P ∧ Q). + ¬(¬P ∨ ¬Q) → (P ∧ Q). Proof. intros P Q. - replace (~(~P∨~Q)) with (P∧Q). + replace (¬(¬P∨¬Q)) with (P∧Q). specialize Id2_08 with (P∧Q). intros Id2_08a. apply Id2_08a. @@ -1006,35 +1010,35 @@ Proof. intros P Q. Qed. Theorem n3_12 : ∀ P Q : Prop, - (~P ∨ ~Q) ∨ (P ∧ Q). + (¬P ∨ ¬Q) ∨ (P ∧ Q). Proof. intros P Q. - specialize n2_11 with (~P∨~Q). + specialize n2_11 with (¬P∨¬Q). intros n2_11a. - replace (~(~P∨~Q)) with (P∧Q) in n2_11a. + replace (¬(¬P∨¬Q)) with (P∧Q) in n2_11a. apply n2_11a. apply Prod3_01. Qed. Theorem n3_13 : ∀ P Q : Prop, - ~(P ∧ Q) → (~P ∨ ~Q). + ¬(P ∧ Q) → (¬P ∨ ¬Q). Proof. intros P Q. specialize n3_11 with P Q. intros n3_11a. - specialize Transp2_15 with (~P∨~Q) (P∧Q). + specialize Transp2_15 with (¬P∨¬Q) (P∧Q). intros Transp2_15a. MP Transp2_15a n3_11a. apply Transp2_15a. Qed. Theorem n3_14 : ∀ P Q : Prop, - (~P ∨ ~Q) → ~(P ∧ Q). + (¬P ∨ ¬Q) → ¬(P ∧ Q). Proof. intros P Q. specialize n3_1 with P Q. intros n3_1a. - specialize Transp2_16 with (P∧Q) (~(~P∨~Q)). + specialize Transp2_16 with (P∧Q) (¬(¬P∨¬Q)). intros Transp2_16a. MP Transp2_16a n3_1a. - specialize n2_12 with (~P∨~Q). + specialize n2_12 with (¬P∨¬Q). intros n2_12a. Syll n2_12a Transp2_16a S. apply S. @@ -1045,11 +1049,11 @@ Theorem n3_2 : ∀ P Q : Prop, Proof. intros P Q. specialize n3_12 with P Q. intros n3_12a. - specialize n2_32 with (~P) (~Q) (P∧Q). + specialize n2_32 with (¬P) (¬Q) (P∧Q). intros n2_32a. MP n3_32a n3_12a. - replace (~Q ∨ P ∧ Q) with (Q→P∧Q) in n2_32a. - replace (~P ∨ (Q → P ∧ Q)) with (P→Q→P∧Q) in n2_32a. + replace (¬Q ∨ P ∧ Q) with (Q→P∧Q) in n2_32a. + replace (¬P ∨ (Q → P ∧ Q)) with (P→Q→P∧Q) in n2_32a. apply n2_32a. apply Impl1_01. apply Impl1_01. @@ -1071,7 +1075,7 @@ Theorem n3_22 : ∀ P Q : Prop, Proof. intros P Q. specialize n3_13 with Q P. intros n3_13a. - specialize Perm1_4 with (~Q) (~P). + specialize Perm1_4 with (¬Q) (¬P). intros Perm1_4a. Syll n3_13a Perm1_4a Ha. specialize n3_14 with P Q. @@ -1084,11 +1088,11 @@ Proof. intros P Q. Qed. Theorem n3_24 : ∀ P : Prop, - ~(P ∧ ~P). + ¬(P ∧ ¬P). Proof. intros P. - specialize n2_11 with (~P). + specialize n2_11 with (¬P). intros n2_11a. - specialize n3_14 with P (~P). + specialize n3_14 with P (¬P). intros n3_14a. MP n3_14a n2_11a. apply n3_14a. @@ -1099,23 +1103,21 @@ Theorem Simp3_26 : ∀ P Q : Prop, Proof. intros P Q. specialize Simp2_02 with Q P. intros Simp2_02a. - replace (P→(Q→P)) with (~P∨(Q→P)) in Simp2_02a. - replace (Q→P) with (~Q∨P) in Simp2_02a. - specialize n2_31 with (~P) (~Q) P. + replace (P→(Q→P)) with (¬P∨(Q→P)) in Simp2_02a. + replace (Q→P) with (¬Q∨P) in Simp2_02a. + specialize n2_31 with (¬P) (¬Q) P. intros n2_31a. MP n2_31a Simp2_02a. - specialize n2_53 with (~P∨~Q) P. + specialize n2_53 with (¬P∨¬Q) P. intros n2_53a. MP n2_53a Simp2_02a. - replace (~(~P∨~Q)) with (P∧Q) in n2_53a. + replace (¬(¬P∨¬Q)) with (P∧Q) in n2_53a. apply n2_53a. apply Prod3_01. - replace (~Q∨P) with (Q→P). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. - replace (~P∨(Q→P)) with (P→Q→P). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. Qed. Theorem Simp3_27 : ∀ P Q : Prop, @@ -1132,43 +1134,55 @@ Qed. Theorem Exp3_3 : ∀ P Q R : Prop, ((P ∧ Q) → R) → (P → (Q → R)). Proof. intros P Q R. - specialize Transp2_15 with (~P∨~Q) R. + specialize Id2_08 with ((P∧Q)→R). + intros Id2_08a. (*This theorem isn't needed.*) + replace (((P ∧ Q) → R) → ((P ∧ Q) → R)) with + (((P ∧ Q) → R) → (¬(¬P ∨ ¬Q) → R)) in Id2_08a. + specialize Transp2_15 with (¬P∨¬Q) R. intros Transp2_15a. - specialize Comm2_04 with (~R) P (~Q). + Syll Id2_08a Transp2_15a Sa. + specialize Id2_08 with (¬R → (¬P ∨ ¬Q)). + intros Id2_08b. (*This theorem isn't needed.*) + Syll Sa Id2_08b Sb. + replace (¬P ∨ ¬Q) with (P → ¬Q) in Sb. + specialize Comm2_04 with (¬R) P (¬Q). intros Comm2_04a. - replace (P → ~Q) with (~P ∨ ~Q) in Comm2_04a. - Syll Transp2_15a Comm2_04a Sa. + Syll Sb Comm2_04a Sc. specialize Transp2_17 with Q R. intros Transp2_17a. - specialize Syll2_05 with P (~R→~Q) (Q→R). + specialize Syll2_05 with P (¬R → ¬Q) (Q → R). intros Syll2_05a. MP Syll2_05a Transp2_17a. - Syll Sa Syll2_05a Sb. - replace (~(~P ∨ ~Q)) with (P ∧ Q) in Sb. - apply Sb. - apply Prod3_01. - replace (~P∨~Q) with (P→~Q). + Syll Sa Syll2_05a Sd. + apply Sd. + rewrite <- Impl1_01. + reflexivity. + rewrite Prod3_01. reflexivity. - apply Impl1_01. Qed. -(*The proof sketch cites Id2_08, but - we did not seem to need it.*) Theorem Imp3_31 : ∀ P Q R : Prop, (P → (Q → R)) → (P ∧ Q) → R. Proof. intros P Q R. - specialize n2_31 with (~P) (~Q) R. + specialize Id2_08 with (P → (Q → R)). + intros Id2_08a. (*This use of Id2_08 is redundant.*) + replace ((P → (Q → R))→(P → (Q → R))) with + ((P → (Q → R))→(¬P ∨ (Q → R))) in Id2_08a. + replace (¬P ∨ (Q → R)) with + (¬P ∨ (¬Q ∨ R)) in Id2_08a. + specialize n2_31 with (¬P) (¬Q) R. intros n2_31a. - specialize n2_53 with (~P∨~Q) R. + Syll Id2_08a n2_31a Sa. + specialize n2_53 with (¬P∨¬Q) R. intros n2_53a. - Syll n2_31a n2_53a S. - replace (~Q∨R) with (Q→R) in S. - replace (~P∨(Q→R)) with (P→Q→R) in S. - replace (~(~P∨~Q)) with (P∧Q) in S. - apply S. + replace (¬(¬P∨¬Q)) with (P∧Q) in n2_53a. + Syll n2_31a n2_53a Sb. + apply Sb. apply Prod3_01. - apply Impl1_01. - apply Impl1_01. + rewrite Impl1_01. + reflexivity. + rewrite <- Impl1_01. + reflexivity. Qed. (*The proof sketch cites Id2_08, but we did not seem to need it.*) @@ -1207,17 +1221,17 @@ Proof. intros P Q. Qed. Theorem Transp3_37 : ∀ P Q R : Prop, - (P ∧ Q → R) → (P ∧ ~R → ~Q). + (P ∧ Q → R) → (P ∧ ¬R → ¬Q). Proof. intros P Q R. specialize Transp2_16 with Q R. intros Transp2_16a. - specialize Syll2_05 with P (Q→R) (~R→~Q). + specialize Syll2_05 with P (Q→R) (¬R→¬Q). intros Syll2_05a. MP Syll2_05a Transp2_16a. specialize Exp3_3 with P Q R. intros Exp3_3a. Syll Exp3_3a Syll2_05a Sa. - specialize Imp3_31 with P (~R) (~Q). + specialize Imp3_31 with P (¬R) (¬Q). intros Imp3_31a. Syll Sa Imp3_31a Sb. apply Sb. @@ -1228,16 +1242,15 @@ Theorem n3_4 : ∀ P Q : Prop, Proof. intros P Q. specialize n2_51 with P Q. intros n2_51a. - specialize Transp2_15 with (P→Q) (P→~Q). + specialize Transp2_15 with (P→Q) (P→¬Q). intros Transp2_15a. MP Transp2_15a n2_51a. - replace (P→~Q) with (~P∨~Q) in Transp2_15a. - replace (~(~P∨~Q)) with (P∧Q) in Transp2_15a. + replace (P→¬Q) with (¬P∨¬Q) in Transp2_15a. + replace (¬(¬P∨¬Q)) with (P∧Q) in Transp2_15a. apply Transp2_15a. apply Prod3_01. - replace (~P∨~Q) with (P→~Q). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. Qed. Theorem n3_41 : ∀ P Q R : Prop, @@ -1282,12 +1295,12 @@ Qed. Theorem n3_44 : ∀ P Q R : Prop, (Q → P) ∧ (R → P) → (Q ∨ R → P). Proof. intros P Q R. - specialize Syll3_33 with (~Q) R P. + specialize Syll3_33 with (¬Q) R P. intros Syll3_33a. specialize n2_6 with Q P. intros n2_6a. Syll Syll3_33a n2_6a Sa. - specialize Exp3_3 with (~Q→R) (R→P) ((Q→P)→P). + specialize Exp3_3 with (¬Q→R) (R→P) ((Q→P)→P). intros Exp3_3a. MP Exp3_3a Sa. specialize Comm2_04 with (R→P) (Q→P) P. @@ -1296,12 +1309,12 @@ Proof. intros P Q R. specialize Imp3_31 with (Q→P) (R→P) P. intros Imp3_31a. Syll Sb Imp3_31a Sc. - specialize Comm2_04 with (~Q→R) ((Q→P)∧(R→P)) P. + specialize Comm2_04 with (¬Q→R) ((Q→P)∧(R→P)) P. intros Comm2_04b. MP Comm2_04b Sc. specialize n2_53 with Q R. intros n2_53a. - specialize Syll2_06 with (Q∨R) (~Q→R) P. + specialize Syll2_06 with (Q∨R) (¬Q→R) P. intros Syll2_06a. MP Syll2_06a n2_53a. Syll Comm2_04b Syll2_06a Sd. @@ -1311,24 +1324,25 @@ Qed. Theorem Fact3_45 : ∀ P Q R : Prop, (P → Q) → (P ∧ R) → (Q ∧ R). Proof. intros P Q R. - specialize Syll2_06 with P Q (~R). + specialize Syll2_06 with P Q (¬R). intros Syll2_06a. - specialize Transp2_16 with (Q→~R) (P→~R). + specialize Transp2_16 with (Q→¬R) (P→¬R). intros Transp2_16a. - Syll Syll2_06a Transp2_16a S. - replace (P→~R) with (~P∨~R) in S. - replace (Q→~R) with (~Q∨~R) in S. - replace (~(~P∨~R)) with (P∧R) in S. - replace (~(~Q∨~R)) with (Q∧R) in S. - apply S. + Syll Syll2_06a Transp2_16a Sa. + specialize Id2_08 with (¬(P→R)→¬(Q→¬R)). + intros Id2_08a. + Syll Sa Id2_08a Sb. + replace (P→¬R) with (¬P∨¬R) in Sb. + replace (Q→¬R) with (¬Q∨¬R) in Sb. + replace (¬(¬P∨¬R)) with (P∧R) in Sb. + replace (¬(¬Q∨¬R)) with (Q∧R) in Sb. + apply Sb. apply Prod3_01. apply Prod3_01. - replace (~Q∨~R) with (Q→~R). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. - replace (~P∨~R) with (P→~R). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. Qed. Theorem n3_47 : ∀ P Q R S : Prop, @@ -1356,11 +1370,23 @@ Proof. intros P Q R S. intros Syll2_05b. MP Syll2_05b n3_22b. Syll Sc Syll2_05b Sd. + clear Simp3_26a. clear Fact3_45a. clear Sa. + clear n3_22a. clear Fact3_45b. + clear Syll2_05a. clear Simp3_27a. + clear Sc. clear n3_22b. clear Syll2_05b. + Conj Sb Sd. + split. + apply Sb. + apply Sd. specialize n2_83 with ((P→R)∧(Q→S)) (P∧Q) (Q∧R) (R∧S). - intros n2_83a. - MP n2_83a Sb. - MP n2_83 Sd. - apply n2_83a. + intros n2_83a. (*This with MP works, but it omits Conj3_03.*) + specialize Imp3_31 with (((P→R)∧(Q→S))→((P∧Q)→(Q∧R))) + (((P→R)∧(Q→S))→((Q∧R)→(R∧S))) + (((P→R)∧(Q→S))→((P∧Q)→(R∧S))). + intros Imp3_31a. + MP Imp3_31a n2_83a. + MP Imp3_31a H. + apply Imp3_31a. Qed. Theorem n3_48 : ∀ P Q R S : Prop, @@ -1419,7 +1445,7 @@ Ltac Equiv H1 := end. Theorem Transp4_1 : ∀ P Q : Prop, - (P → Q) ↔ (~Q → ~P). + (P → Q) ↔ (¬Q → ¬P). Proof. intros P Q. specialize Transp2_16 with P Q. intros Transp2_16a. @@ -1435,7 +1461,7 @@ Proof. intros P Q. Qed. Theorem Transp4_11 : ∀ P Q : Prop, - (P ↔ Q) ↔ (~P ↔ ~Q). + (P ↔ Q) ↔ (¬P ↔ ¬Q). Proof. intros P Q. specialize Transp2_16 with P Q. intros Transp2_16a. @@ -1445,16 +1471,16 @@ Proof. intros P Q. split. apply Transp2_16a. apply Transp2_16b. - specialize n3_47 with (P→Q) (Q→P) (~Q→~P) (~P→~Q). + specialize n3_47 with (P→Q) (Q→P) (¬Q→¬P) (¬P→¬Q). intros n3_47a. MP n3_47 H. - specialize n3_22 with (~Q → ~P) (~P → ~Q). + specialize n3_22 with (¬Q → ¬P) (¬P → ¬Q). intros n3_22a. Syll n3_47a n3_22a Sa. replace ((P → Q) ∧ (Q → P)) with (P↔Q) in Sa. - replace ((~P → ~Q) ∧ (~Q → ~P)) with (~P↔~Q) in Sa. + replace ((¬P → ¬Q) ∧ (¬Q → ¬P)) with (¬P↔¬Q) in Sa. clear Transp2_16a. clear H. clear Transp2_16b. - clear n3_22a. clear n3_47a. + clear n3_22a. clear n3_47a. specialize Transp2_17 with Q P. intros Transp2_17a. specialize Transp2_17 with P Q. @@ -1463,7 +1489,7 @@ Proof. intros P Q. split. apply Transp2_17a. apply Transp2_17b. - specialize n3_47 with (~P→~Q) (~Q→~P) (Q→P) (P→Q). + specialize n3_47 with (¬P→¬Q) (¬Q→¬P) (Q→P) (P→Q). intros n3_47a. MP n3_47a H. specialize n3_22 with (Q→P) (P→Q). @@ -1472,7 +1498,7 @@ Proof. intros P Q. clear Transp2_17a. clear Transp2_17b. clear H. clear n3_47a. clear n3_22a. replace ((P → Q) ∧ (Q → P)) with (P↔Q) in Sb. - replace ((~P → ~Q) ∧ (~Q → ~P)) with (~P↔~Q) in Sb. + replace ((¬P → ¬Q) ∧ (¬Q → ¬P)) with (¬P↔¬Q) in Sb. Conj Sa Sb. split. apply Sa. @@ -1487,7 +1513,7 @@ Proof. intros P Q. Qed. Theorem n4_12 : ∀ P Q : Prop, - (P ↔ ~Q) ↔ (Q ↔ ~P). + (P ↔ ¬Q) ↔ (Q ↔ ¬P). Proof. intros P Q. specialize Transp2_03 with P Q. intros Transp2_03a. @@ -1497,7 +1523,7 @@ Theorem n4_12 : ∀ P Q : Prop, split. apply Transp2_03a. apply Transp2_15a. - specialize n3_47 with (P→~Q) (~Q→P) (Q→~P) (~P→Q). + specialize n3_47 with (P→¬Q) (¬Q→P) (Q→¬P) (¬P→Q). intros n3_47a. MP n3_47a H. specialize Transp2_03 with Q P. @@ -1508,30 +1534,23 @@ Theorem n4_12 : ∀ P Q : Prop, split. apply Transp2_03b. apply Transp2_15b. - specialize n3_47 with (Q→~P) (~P→Q) (P→~Q) (~Q→P). + specialize n3_47 with (Q→¬P) (¬P→Q) (P→¬Q) (¬Q→P). intros n3_47b. MP n3_47b H0. - clear Transp2_03a. clear Transp2_15a. clear H. clear - Transp2_03b. clear Transp2_15b. clear H0. - replace ((P → ~Q) ∧ (~Q → P)) with (P↔~Q) in n3_47a. - replace ((Q → ~P) ∧ (~P → Q)) with (Q↔~P) in n3_47a. - replace ((P → ~Q) ∧ (~Q → P)) with (P↔~Q) in n3_47b. - replace ((Q → ~P) ∧ (~P → Q)) with (Q↔~P) in n3_47b. + clear Transp2_03a. clear Transp2_15a. clear H. + clear Transp2_03b. clear Transp2_15b. clear H0. Conj n3_47a n3_47b. split. apply n3_47a. apply n3_47b. - Equiv H. + rewrite <- Equiv4_01 in H. + rewrite <- Equiv4_01 in H. + rewrite <- Equiv4_01 in H. apply H. - apply Equiv4_01. - apply Equiv4_01. - apply Equiv4_01. - apply Equiv4_01. - apply Equiv4_01. Qed. Theorem n4_13 : ∀ P : Prop, - P ↔ ~~P. + P ↔ ¬¬P. Proof. intros P. specialize n2_12 with P. intros n2_12a. @@ -1547,11 +1566,11 @@ Theorem n4_13 : ∀ P : Prop, Qed. Theorem n4_14 : ∀ P Q R : Prop, - ((P ∧ Q) → R) ↔ ((P ∧ ~R) → ~Q). + ((P ∧ Q) → R) ↔ ((P ∧ ¬R) → ¬Q). Proof. intros P Q R. specialize Transp3_37 with P Q R. intros Transp3_37a. -specialize Transp3_37 with P (~R) (~Q). +specialize Transp3_37 with P (¬R) (¬Q). intros Transp3_37b. Conj Transp3_37a Transp3_37b. split. apply Transp3_37a. @@ -1560,8 +1579,8 @@ specialize n4_13 with Q. intros n4_13a. specialize n4_13 with R. intros n4_13b. -replace (~~Q) with Q in H. -replace (~~R) with R in H. +replace (¬¬Q) with Q in H. +replace (¬¬R) with R in H. Equiv H. apply H. apply Equiv4_01. @@ -1572,31 +1591,31 @@ apply n4_13a. Qed. Theorem n4_15 : ∀ P Q R : Prop, - ((P ∧ Q) → ~R) ↔ ((Q ∧ R) → ~P). + ((P ∧ Q) → ¬R) ↔ ((Q ∧ R) → ¬P). Proof. intros P Q R. - specialize n4_14 with Q P (~R). + specialize n4_14 with Q P (¬R). intros n4_14a. specialize n3_22 with Q P. intros n3_22a. - specialize Syll2_06 with (Q∧P) (P∧Q) (~R). + specialize Syll2_06 with (Q∧P) (P∧Q) (¬R). intros Syll2_06a. MP Syll2_06a n3_22a. specialize n4_13 with R. intros n4_13a. - replace (~~R) with R in n4_14a. + replace (¬¬R) with R in n4_14a. rewrite Equiv4_01 in n4_14a. - specialize Simp3_26 with ((Q ∧ P → ~R) → Q ∧ R → ~P) - ((Q ∧ R → ~P) → Q ∧ P → ~R). + specialize Simp3_26 with ((Q ∧ P → ¬R) → Q ∧ R → ¬P) + ((Q ∧ R → ¬P) → Q ∧ P → ¬R). intros Simp3_26a. MP Simp3_26a n4_14a. Syll Syll2_06a Simp3_26a Sa. - specialize Simp3_27 with ((Q ∧ P → ~R) → Q ∧ R → ~P) - ((Q ∧ R → ~P) → Q ∧ P → ~R). + specialize Simp3_27 with ((Q ∧ P → ¬R) → Q ∧ R → ¬P) + ((Q ∧ R → ¬P) → Q ∧ P → ¬R). intros Simp3_27a. MP Simp3_27a n4_14a. specialize n3_22 with P Q. intros n3_22b. - specialize Syll2_06 with (P∧Q) (Q∧P) (~R). + specialize Syll2_06 with (P∧Q) (Q∧P) (¬R). intros Syll2_06b. MP Syll2_06b n3_22b. Syll Syll2_06b Simp3_27a Sb. @@ -1775,21 +1794,21 @@ Qed. Proof. intros P Q R. specialize n4_15 with P Q R. intros n4_15a. - specialize Transp4_1 with P (~(Q ∧ R)). + specialize Transp4_1 with P (¬(Q ∧ R)). intros Transp4_1a. - replace (~~(Q ∧ R)) with (Q ∧ R) in Transp4_1a. - replace (Q ∧ R→~P) with (P→~(Q ∧ R)) in n4_15a. - specialize Transp4_11 with (P ∧ Q → ~R) (P → ~(Q ∧ R)). + replace (¬¬(Q ∧ R)) with (Q ∧ R) in Transp4_1a. + replace (Q ∧ R→¬P) with (P→¬(Q ∧ R)) in n4_15a. + specialize Transp4_11 with (P ∧ Q → ¬R) (P → ¬(Q ∧ R)). intros Transp4_11a. - replace ((P ∧ Q → ~R) ↔ (P → ~(Q ∧ R))) with - (~(P ∧ Q → ~R) ↔ ~(P → ~(Q ∧ R))) in n4_15a. - replace (P ∧ Q → ~R) with - (~(P ∧ Q ) ∨ ~R) in n4_15a. - replace (P → ~(Q ∧ R)) with - (~P ∨ ~(Q ∧ R)) in n4_15a. - replace (~(~(P ∧ Q) ∨ ~R)) with + replace ((P ∧ Q → ¬R) ↔ (P → ¬(Q ∧ R))) with + (¬(P ∧ Q → ¬R) ↔ ¬(P → ¬(Q ∧ R))) in n4_15a. + replace (P ∧ Q → ¬R) with + (¬(P ∧ Q ) ∨ ¬R) in n4_15a. + replace (P → ¬(Q ∧ R)) with + (¬P ∨ ¬(Q ∧ R)) in n4_15a. + replace (¬(¬(P ∧ Q) ∨ ¬R)) with ((P ∧ Q) ∧ R) in n4_15a. - replace (~(~P ∨ ~(Q ∧ R))) with + replace (¬(¬P ∨ ¬(Q ∧ R))) with (P ∧ (Q ∧ R )) in n4_15a. apply n4_15a. apply Prod3_01. @@ -1798,8 +1817,8 @@ Qed. reflexivity. rewrite Impl1_01. reflexivity. - replace (~(P ∧ Q → ~R) ↔ ~(P → ~(Q ∧ R))) with - ((P ∧ Q → ~R) ↔ (P → ~(Q ∧ R))). + replace (¬(P ∧ Q → ¬R) ↔ ¬(P → ¬(Q ∧ R))) with + ((P ∧ Q → ¬R) ↔ (P → ¬(Q ∧ R))). reflexivity. apply EqBi. apply Transp4_11a. @@ -1812,12 +1831,10 @@ Qed. Qed. (*Note that the actual proof uses n4_12, but that transposition involves transforming a - biconditional into a conditional. This way - of doing it - using Transp4_1 to transpose a - conditional and then applying n4_13 to - double negate - is easier without a derived - rule for replacing a biconditional with one - of its equivalent implications.*) + biconditional into a conditional. This theorem + may be a misprint. Using Transp4_1 to transpose + a conditional and then applying n4_13 to double + negate does secure the desired formula, though.*) Theorem n4_33 : ∀ P Q R : Prop, (P ∨ (Q ∨ R)) ↔ ((P ∨ Q) ∨ R). @@ -2132,10 +2149,10 @@ Proof. intros P Q R. split. apply n2_53a. apply n2_53b. - specialize n3_47 with (P ∨ Q) (P ∨ R) (~P → Q) (~P → R). + specialize n3_47 with (P ∨ Q) (P ∨ R) (¬P → Q) (¬P → R). intros n3_47a. MP n3_47a H0. - specialize Comp3_43 with (~P) Q R. + specialize Comp3_43 with (¬P) Q R. intros Comp3_43b. Syll n3_47a Comp3_43b Sa. specialize n2_54 with P (Q∧R). @@ -2154,23 +2171,23 @@ Proof. intros P Q R. Qed. Theorem n4_42 : ∀ P Q : Prop, - P ↔ ((P ∧ Q) ∨ (P ∧ ~Q)). + P ↔ ((P ∧ Q) ∨ (P ∧ ¬Q)). Proof. intros P Q. - specialize n3_21 with P (Q ∨ ~Q). + specialize n3_21 with P (Q ∨ ¬Q). intros n3_21a. specialize n2_11 with Q. intros n2_11a. MP n3_21a n2_11a. - specialize Simp3_26 with P (Q ∨ ~Q). + specialize Simp3_26 with P (Q ∨ ¬Q). intros Simp3_26a. clear n2_11a. Conj n3_21a Simp3_26a. split. apply n3_21a. apply Simp3_26a. Equiv H. - specialize n4_4 with P Q (~Q). + specialize n4_4 with P Q (¬Q). intros n4_4a. - replace (P ∧ (Q ∨ ~Q)) with P in n4_4a. + replace (P ∧ (Q ∨ ¬Q)) with P in n4_4a. apply n4_4a. apply EqBi. apply H. @@ -2178,39 +2195,40 @@ Proof. intros P Q. Qed. Theorem n4_43 : ∀ P Q : Prop, - P ↔ ((P ∨ Q) ∧ (P ∨ ~Q)). + P ↔ ((P ∨ Q) ∧ (P ∨ ¬Q)). Proof. intros P Q. specialize n2_2 with P Q. intros n2_2a. - specialize n2_2 with P (~Q). + specialize n2_2 with P (¬Q). intros n2_2b. Conj n2_2a n2_2b. split. apply n2_2a. apply n2_2b. - specialize Comp3_43 with P (P∨Q) (P∨~Q). + specialize Comp3_43 with P (P∨Q) (P∨¬Q). intros Comp3_43a. MP Comp3_43a H. specialize n2_53 with P Q. intros n2_53a. - specialize n2_53 with P (~Q). + specialize n2_53 with P (¬Q). intros n2_53b. Conj n2_53a n2_53b. split. apply n2_53a. apply n2_53b. - specialize n3_47 with (P∨Q) (P∨~Q) (~P→Q) (~P→~Q). + specialize n3_47 with (P∨Q) (P∨¬Q) (¬P→Q) (¬P→¬Q). intros n3_47a. MP n3_47a H0. - specialize n2_65 with (~P) Q. + specialize n2_65 with (¬P) Q. intros n2_65a. - replace (~~P) with P in n2_65a. - specialize Imp3_31 with (~P → Q) (~P → ~Q) (P). + replace (¬¬P) with P in n2_65a. + specialize Imp3_31 with (¬P → Q) (¬P → ¬Q) (P). intros Imp3_31a. MP Imp3_31a n2_65a. Syll n3_47a Imp3_31a Sa. - clear n2_2a. clear n2_2b. clear H. clear n2_53a. clear n2_53b. - clear H0. clear n2_65a. clear n3_47a. clear Imp3_31a. + clear n2_2a. clear n2_2b. clear H. clear n2_53a. + clear n2_53b. clear H0. clear n2_65a. + clear n3_47a. clear Imp3_31a. Conj Comp3_43a Sa. split. apply Comp3_43a. @@ -2277,34 +2295,34 @@ Theorem n4_45 : ∀ P Q : Prop, Qed. Theorem n4_5 : ∀ P Q : Prop, - P ∧ Q ↔ ~(~P ∨ ~Q). + P ∧ Q ↔ ¬(¬P ∨ ¬Q). Proof. intros P Q. specialize n4_2 with (P ∧ Q). intros n4_2a. rewrite Prod3_01. - replace (~(~P ∨ ~Q)) with (P ∧ Q). + replace (¬(¬P ∨ ¬Q)) with (P ∧ Q). apply n4_2a. apply Prod3_01. Qed. Theorem n4_51 : ∀ P Q : Prop, - ~(P ∧ Q) ↔ (~P ∨ ~Q). + ¬(P ∧ Q) ↔ (¬P ∨ ¬Q). Proof. intros P Q. specialize n4_5 with P Q. intros n4_5a. - specialize n4_12 with (P ∧ Q) (~P ∨ ~Q). + specialize n4_12 with (P ∧ Q) (¬P ∨ ¬Q). intros n4_12a. - replace ((P∧Q ↔ ~(~P∨~Q))↔(~P∨~Q ↔ ~(P∧Q))) with - ((P∧Q ↔ ~(~P∨~Q)) = (~P∨~Q ↔ ~(P∧Q))) in n4_12a. - replace (P ∧ Q ↔ ~(~P ∨ ~Q)) with - (~P ∨ ~Q ↔ ~(P ∧ Q)) in n4_5a. - replace (~P ∨ ~Q ↔ ~(P ∧ Q)) with - (~(P ∧ Q) ↔ (~P ∨ ~Q)) in n4_5a. + replace ((P∧Q ↔ ¬(¬P∨¬Q))↔(¬P∨¬Q ↔ ¬(P∧Q))) with + ((P∧Q ↔ ¬(¬P∨¬Q)) = (¬P∨¬Q ↔ ¬(P∧Q))) in n4_12a. + replace (P ∧ Q ↔ ¬(¬P ∨ ¬Q)) with + (¬P ∨ ¬Q ↔ ¬(P ∧ Q)) in n4_5a. + replace (¬P ∨ ¬Q ↔ ¬(P ∧ Q)) with + (¬(P ∧ Q) ↔ (¬P ∨ ¬Q)) in n4_5a. apply n4_5a. - specialize n4_21 with (~(P ∧ Q)) (~P ∨ ~Q). + specialize n4_21 with (¬(P ∧ Q)) (¬P ∨ ¬Q). intros n4_21a. apply EqBi. - specialize n4_21 with (~(P∧Q)) (~P ∨ ~Q). + specialize n4_21 with (¬(P∧Q)) (¬P ∨ ¬Q). intros n4_21b. apply n4_21b. apply EqBi. @@ -2312,11 +2330,11 @@ Theorem n4_51 : ∀ P Q : Prop, Qed. Theorem n4_52 : ∀ P Q : Prop, - (P ∧ ~Q) ↔ ~(~P ∨ Q). + (P ∧ ¬Q) ↔ ¬(¬P ∨ Q). Proof. intros P Q. - specialize n4_5 with P (~Q). + specialize n4_5 with P (¬Q). intros n4_5a. - replace (~~Q) with Q in n4_5a. + replace (¬¬Q) with Q in n4_5a. apply n4_5a. specialize n4_13 with Q. intros n4_13a. @@ -2325,20 +2343,20 @@ Theorem n4_52 : ∀ P Q : Prop, Qed. Theorem n4_53 : ∀ P Q : Prop, - ~(P ∧ ~Q) ↔ (~P ∨ Q). + ¬(P ∧ ¬Q) ↔ (¬P ∨ Q). Proof. intros P Q. specialize n4_52 with P Q. intros n4_52a. - specialize n4_12 with (P ∧ ~Q) ((~P ∨ Q)). + specialize n4_12 with (P ∧ ¬Q) ((¬P ∨ Q)). intros n4_12a. - replace ((P∧~Q ↔ ~(~P∨Q))↔(~P∨Q ↔ ~(P∧~Q))) with - ((P∧~Q ↔ ~(~P∨Q)) = (~P∨Q ↔ ~(P∧~Q))) in n4_12a. - replace (P ∧ ~Q ↔ ~(~P ∨ Q)) with - (~P ∨ Q ↔ ~(P ∧ ~Q)) in n4_52a. - replace (~P ∨ Q ↔ ~(P ∧ ~Q)) with - (~(P ∧ ~Q) ↔ (~P ∨ Q)) in n4_52a. + replace ((P∧¬Q ↔ ¬(¬P∨Q))↔(¬P∨Q ↔ ¬(P∧¬Q))) with + ((P∧¬Q ↔ ¬(¬P∨Q)) = (¬P∨Q ↔ ¬(P∧¬Q))) in n4_12a. + replace (P ∧ ¬Q ↔ ¬(¬P ∨ Q)) with + (¬P ∨ Q ↔ ¬(P ∧ ¬Q)) in n4_52a. + replace (¬P ∨ Q ↔ ¬(P ∧ ¬Q)) with + (¬(P ∧ ¬Q) ↔ (¬P ∨ Q)) in n4_52a. apply n4_52a. - specialize n4_21 with (~(P ∧ ~Q)) (~P ∨ Q). + specialize n4_21 with (¬(P ∧ ¬Q)) (¬P ∨ Q). intros n4_21a. apply EqBi. apply n4_21a. @@ -2347,48 +2365,51 @@ Theorem n4_53 : ∀ P Q : Prop, Qed. Theorem n4_54 : ∀ P Q : Prop, - (~P ∧ Q) ↔ ~(P ∨ ~Q). + (¬P ∧ Q) ↔ ¬(P ∨ ¬Q). Proof. intros P Q. - specialize n4_5 with (~P) Q. + specialize n4_5 with (¬P) Q. intros n4_5a. specialize n4_13 with P. intros n4_13a. - replace (~~P) with P in n4_5a. + replace (¬¬P) with P in n4_5a. apply n4_5a. apply EqBi. apply n4_13a. Qed. Theorem n4_55 : ∀ P Q : Prop, - ~(~P ∧ Q) ↔ (P ∨ ~Q). + ¬(¬P ∧ Q) ↔ (P ∨ ¬Q). Proof. intros P Q. specialize n4_54 with P Q. intros n4_54a. - specialize n4_12 with (~P ∧ Q) (P ∨ ~Q). + specialize n4_12 with (¬P ∧ Q) (P ∨ ¬Q). intros n4_12a. - replace (~P ∧ Q ↔ ~(P ∨ ~Q)) with - (P ∨ ~Q ↔ ~(~P ∧ Q)) in n4_54a. - replace (P ∨ ~Q ↔ ~(~P ∧ Q)) with - (~(~P ∧ Q) ↔ (P ∨ ~Q)) in n4_54a. + replace (¬P ∧ Q ↔ ¬(P ∨ ¬Q)) with + (P ∨ ¬Q ↔ ¬(¬P ∧ Q)) in n4_54a. + replace (P ∨ ¬Q ↔ ¬(¬P ∧ Q)) with + (¬(¬P ∧ Q) ↔ (P ∨ ¬Q)) in n4_54a. apply n4_54a. - specialize n4_21 with (~(~P ∧ Q)) (P ∨ ~Q). - intros n4_21a. + specialize n4_21 with (¬(¬P ∧ Q)) (P ∨ ¬Q). + intros n4_21a. (*Not cited*) apply EqBi. apply n4_21a. - replace ((~P ∧ Q ↔ ~(P ∨ ~Q)) ↔ (P ∨ ~Q ↔ ~(~P ∧ Q))) with - ((~P ∧ Q ↔ ~(P ∨ ~Q)) = (P ∨ ~Q ↔ ~(~P ∧ Q))) in n4_12a. - rewrite n4_12a. - reflexivity. apply EqBi. + replace ((P∨¬Q↔¬(¬P∧Q))↔(¬P∧Q↔¬(P∨¬Q))) + with ((¬P∧Q↔¬(P∨¬Q))↔(P∨¬Q↔¬(¬P∧Q))). + apply n4_12a. apply EqBi. + specialize n4_21 with (P∨¬Q↔¬(¬P∧Q)) + (¬P∧Q↔¬(P∨¬Q)). + intros n4_21b. + apply n4_21. Qed. Theorem n4_56 : ∀ P Q : Prop, - (~P ∧ ~Q) ↔ ~(P ∨ Q). + (¬P ∧ ¬Q) ↔ ¬(P ∨ Q). Proof. intros P Q. - specialize n4_54 with P (~Q). + specialize n4_54 with P (¬Q). intros n4_54a. - replace (~~Q) with Q in n4_54a. + replace (¬¬Q) with Q in n4_54a. apply n4_54a. apply EqBi. specialize n4_13 with Q. @@ -2397,94 +2418,94 @@ Theorem n4_56 : ∀ P Q : Prop, Qed. Theorem n4_57 : ∀ P Q : Prop, - ~(~P ∧ ~Q) ↔ (P ∨ Q). + ¬(¬P ∧ ¬Q) ↔ (P ∨ Q). Proof. intros P Q. specialize n4_56 with P Q. intros n4_56a. - specialize n4_12 with (~P ∧ ~Q) (P ∨ Q). + specialize n4_12 with (¬P ∧ ¬Q) (P ∨ Q). intros n4_12a. - replace (~P ∧ ~Q ↔ ~(P ∨ Q)) with - (P ∨ Q ↔ ~(~P ∧ ~Q)) in n4_56a. - replace (P ∨ Q ↔ ~(~P ∧ ~Q)) with - (~(~P ∧ ~Q) ↔ P ∨ Q) in n4_56a. + replace (¬P ∧ ¬Q ↔ ¬(P ∨ Q)) with + (P ∨ Q ↔ ¬(¬P ∧ ¬Q)) in n4_56a. + replace (P ∨ Q ↔ ¬(¬P ∧ ¬Q)) with + (¬(¬P ∧ ¬Q) ↔ P ∨ Q) in n4_56a. apply n4_56a. - specialize n4_21 with (~(~P ∧ ~Q)) (P ∨ Q). + specialize n4_21 with (¬(¬P ∧ ¬Q)) (P ∨ Q). intros n4_21a. apply EqBi. apply n4_21a. - replace ((~P∧~Q↔~(P∨Q))↔(P∨Q↔~(~P∧~Q))) with - ((P∨Q↔~(~P∧~Q))↔(~P∧~Q↔~(P∨Q))) in n4_12a. + replace ((¬P∧¬Q↔¬(P∨Q))↔(P∨Q↔¬(¬P∧¬Q))) with + ((P∨Q↔¬(¬P∧¬Q))↔(¬P∧¬Q↔¬(P∨Q))) in n4_12a. apply EqBi. apply n4_12a. apply EqBi. specialize n4_21 with - (P ∨ Q ↔ ~(~P ∧ ~Q)) (~P ∧ ~Q ↔ ~(P ∨ Q)). + (P ∨ Q ↔ ¬(¬P ∧ ¬Q)) (¬P ∧ ¬Q ↔ ¬(P ∨ Q)). intros n4_21b. apply n4_21b. Qed. Theorem n4_6 : ∀ P Q : Prop, - (P → Q) ↔ (~P ∨ Q). + (P → Q) ↔ (¬P ∨ Q). Proof. intros P Q. - specialize n4_2 with (~P∨ Q). + specialize n4_2 with (¬P∨ Q). intros n4_2a. rewrite Impl1_01. apply n4_2a. Qed. Theorem n4_61 : ∀ P Q : Prop, - ~(P → Q) ↔ (P ∧ ~Q). + ¬(P → Q) ↔ (P ∧ ¬Q). Proof. intros P Q. specialize n4_6 with P Q. intros n4_6a. - specialize Transp4_11 with (P→Q) (~P∨Q). + specialize Transp4_11 with (P→Q) (¬P∨Q). intros Transp4_11a. specialize n4_52 with P Q. intros n4_52a. - replace ((P → Q) ↔ ~P ∨ Q) with - (~(P → Q) ↔ ~(~P ∨ Q)) in n4_6a. - replace (~(~P ∨ Q)) with (P ∧ ~Q) in n4_6a. + replace ((P → Q) ↔ ¬P ∨ Q) with + (¬(P → Q) ↔ ¬(¬P ∨ Q)) in n4_6a. + replace (¬(¬P ∨ Q)) with (P ∧ ¬Q) in n4_6a. apply n4_6a. apply EqBi. apply n4_52a. - replace (((P→Q)↔~P∨Q)↔(~(P→Q)↔~(~P∨Q))) with - ((~(P→Q)↔~(~P∨Q))↔((P→Q)↔~P∨Q)) in Transp4_11a. + replace (((P→Q)↔¬P∨Q)↔(¬(P→Q)↔¬(¬P∨Q))) with + ((¬(P→Q)↔¬(¬P∨Q))↔((P→Q)↔¬P∨Q)) in Transp4_11a. apply EqBi. apply Transp4_11a. apply EqBi. - specialize n4_21 with (~(P→Q)↔~(~P∨Q)) - ((P→Q)↔(~P∨Q)). + specialize n4_21 with (¬(P→Q)↔¬(¬P∨Q)) + ((P→Q)↔(¬P∨Q)). intros n4_21a. apply n4_21a. Qed. Theorem n4_62 : ∀ P Q : Prop, - (P → ~Q) ↔ (~P ∨ ~Q). + (P → ¬Q) ↔ (¬P ∨ ¬Q). Proof. intros P Q. - specialize n4_6 with P (~Q). + specialize n4_6 with P (¬Q). intros n4_6a. apply n4_6a. Qed. Theorem n4_63 : ∀ P Q : Prop, - ~(P → ~Q) ↔ (P ∧ Q). + ¬(P → ¬Q) ↔ (P ∧ Q). Proof. intros P Q. specialize n4_62 with P Q. intros n4_62a. - specialize Transp4_11 with (P → ~Q) (~P ∨ ~Q). + specialize Transp4_11 with (P → ¬Q) (¬P ∨ ¬Q). intros Transp4_11a. specialize n4_5 with P Q. intros n4_5a. - replace (~(~P ∨ ~Q)) with (P ∧ Q) in Transp4_11a. - replace ((P → ~Q) ↔ ~P ∨ ~Q) with - ((~(P → ~Q) ↔ P ∧ Q)) in n4_62a. + replace (¬(¬P ∨ ¬Q)) with (P ∧ Q) in Transp4_11a. + replace ((P → ¬Q) ↔ ¬P ∨ ¬Q) with + ((¬(P → ¬Q) ↔ P ∧ Q)) in n4_62a. apply n4_62a. - replace (((P→~Q)↔~P∨~Q)↔(~(P→~Q)↔P∧Q)) with - ((~(P→~Q)↔P∧Q)↔((P→~Q)↔~P∨~Q)) in Transp4_11a. + replace (((P→¬Q)↔¬P∨¬Q)↔(¬(P→¬Q)↔P∧Q)) with + ((¬(P→¬Q)↔P∧Q)↔((P→¬Q)↔¬P∨¬Q)) in Transp4_11a. apply EqBi. apply Transp4_11a. specialize n4_21 with - (~(P → ~Q) ↔ P ∧ Q) ((P → ~Q) ↔ ~P ∨ ~Q). + (¬(P → ¬Q) ↔ P ∧ Q) ((P → ¬Q) ↔ ¬P ∨ ¬Q). intros n4_21a. apply EqBi. apply n4_21a. @@ -2493,7 +2514,7 @@ Theorem n4_63 : ∀ P Q : Prop, Qed. Theorem n4_64 : ∀ P Q : Prop, - (~P → Q) ↔ (P ∨ Q). + (¬P → Q) ↔ (P ∨ Q). Proof. intros P Q. specialize n2_54 with P Q. intros n2_54a. @@ -2509,65 +2530,67 @@ Theorem n4_64 : ∀ P Q : Prop, Qed. Theorem n4_65 : ∀ P Q : Prop, - ~(~P → Q) ↔ (~P ∧ ~Q). + ¬(¬P → Q) ↔ (¬P ∧ ¬Q). Proof. intros P Q. specialize n4_64 with P Q. intros n4_64a. - specialize Transp4_11 with(~P → Q) (P ∨ Q). + specialize Transp4_11 with(¬P → Q) (P ∨ Q). intros Transp4_11a. specialize n4_56 with P Q. intros n4_56a. - replace (((~P→Q)↔P∨Q)↔(~(~P→Q)↔~(P∨Q))) with - ((~(~P→Q)↔~(P∨Q))↔((~P→Q)↔P∨Q)) in Transp4_11a. - replace ((~P → Q) ↔ P ∨ Q) with - (~(~P → Q) ↔ ~(P ∨ Q)) in n4_64a. - replace (~(P ∨ Q)) with (~P ∧ ~Q) in n4_64a. + replace (((¬P→Q)↔P∨Q)↔(¬(¬P→Q)↔¬(P∨Q))) with + ((¬(¬P→Q)↔¬(P∨Q))↔((¬P→Q)↔P∨Q)) in Transp4_11a. + replace ((¬P → Q) ↔ P ∨ Q) with + (¬(¬P → Q) ↔ ¬(P ∨ Q)) in n4_64a. + replace (¬(P ∨ Q)) with (¬P ∧ ¬Q) in n4_64a. apply n4_64a. apply EqBi. apply n4_56a. apply EqBi. apply Transp4_11a. apply EqBi. - specialize n4_21 with (~(~P → Q)↔~(P ∨ Q)) - ((~P → Q)↔(P ∨ Q)). + specialize n4_21 with (¬(¬P → Q)↔¬(P ∨ Q)) + ((¬P → Q)↔(P ∨ Q)). intros n4_21a. apply n4_21a. Qed. Theorem n4_66 : ∀ P Q : Prop, - (~P → ~Q) ↔ (P ∨ ~Q). + (¬P → ¬Q) ↔ (P ∨ ¬Q). Proof. intros P Q. - specialize n4_64 with P (~Q). + specialize n4_64 with P (¬Q). intros n4_64a. apply n4_64a. Qed. Theorem n4_67 : ∀ P Q : Prop, - ~(~P → ~Q) ↔ (~P ∧ Q). + ¬(¬P → ¬Q) ↔ (¬P ∧ Q). Proof. intros P Q. specialize n4_66 with P Q. intros n4_66a. - specialize Transp4_11 with (~P → ~Q) (P ∨ ~Q). + specialize Transp4_11 with (¬P → ¬Q) (P ∨ ¬Q). intros Transp4_11a. - replace ((~P → ~Q) ↔ P ∨ ~Q) with - (~(~P → ~Q) ↔ ~(P ∨ ~Q)) in n4_66a. + replace ((¬P → ¬Q) ↔ P ∨ ¬Q) with + (¬(¬P → ¬Q) ↔ ¬(P ∨ ¬Q)) in n4_66a. specialize n4_54 with P Q. intros n4_54a. - replace (~(P ∨ ~Q)) with (~P ∧ Q) in n4_66a. + replace (¬(P ∨ ¬Q)) with (¬P ∧ Q) in n4_66a. apply n4_66a. apply EqBi. apply n4_54a. - replace (((~P→~Q)↔P∨~Q)↔(~(~P→~Q)↔~(P∨~Q))) with - ((~(~P→~Q)↔~(P∨~Q))↔((~P→~Q)↔P∨~Q)) in Transp4_11a. + replace (((¬P→¬Q)↔P∨¬Q)↔(¬(¬P→¬Q)↔¬(P∨¬Q))) with + ((¬(¬P→¬Q)↔¬(P∨¬Q))↔((¬P→¬Q)↔P∨¬Q)) in Transp4_11a. apply EqBi. apply Transp4_11a. apply EqBi. - specialize n4_21 with (~(~P → ~Q)↔~(P ∨ ~Q)) - ((~P → ~Q)↔(P ∨ ~Q)). + specialize n4_21 with (¬(¬P → ¬Q)↔¬(P ∨ ¬Q)) + ((¬P → ¬Q)↔(P ∨ ¬Q)). intros n4_21a. apply n4_21a. Qed. + (*Return to this proof.*) + (*We did get one half of the ↔.*) Theorem n4_7 : ∀ P Q : Prop, (P → Q) ↔ (P → (P ∧ Q)). Proof. intros P Q. @@ -2635,39 +2658,39 @@ Theorem n4_72 : ∀ P Q : Prop, Proof. intros P Q. specialize Transp4_1 with P Q. intros Transp4_1a. - specialize n4_71 with (~Q) (~P). + specialize n4_71 with (¬Q) (¬P). intros n4_71a. Conj Transp4_1a n4_71a. split. apply Transp4_1a. apply n4_71a. specialize n4_22 with - (P→Q) (~Q→~P) (~Q↔~Q ∧ ~P). + (P→Q) (¬Q→¬P) (¬Q↔¬Q ∧ ¬P). intros n4_22a. MP n4_22a H. - specialize n4_21 with (~Q) (~Q ∧ ~P). + specialize n4_21 with (¬Q) (¬Q ∧ ¬P). intros n4_21a. Conj n4_22a n4_21a. split. apply n4_22a. apply n4_21a. specialize n4_22 with - (P→Q) (~Q ↔ ~Q ∧ ~P) (~Q ∧ ~P ↔ ~Q). + (P→Q) (¬Q ↔ ¬Q ∧ ¬P) (¬Q ∧ ¬P ↔ ¬Q). intros n4_22b. MP n4_22b H0. - specialize n4_12 with (~Q ∧ ~P) (Q). + specialize n4_12 with (¬Q ∧ ¬P) (Q). intros n4_12a. Conj n4_22b n4_12a. split. apply n4_22b. apply n4_12a. specialize n4_22 with - (P → Q) ((~Q ∧ ~P) ↔ ~Q) (Q ↔ ~(~Q ∧ ~P)). + (P → Q) ((¬Q ∧ ¬P) ↔ ¬Q) (Q ↔ ¬(¬Q ∧ ¬P)). intros n4_22c. MP n4_22b H0. specialize n4_57 with Q P. intros n4_57a. - replace (~(~Q ∧ ~P)) with (Q ∨ P) in n4_22c. + replace (¬(¬Q ∧ ¬P)) with (Q ∨ P) in n4_22c. specialize n4_31 with P Q. intros n4_31a. replace (Q ∨ P) with (P ∨ Q) in n4_22c. @@ -2675,11 +2698,11 @@ Theorem n4_72 : ∀ P Q : Prop, apply EqBi. apply n4_31a. apply EqBi. - replace (~(~Q ∧ ~P) ↔ Q ∨ P) with - (Q ∨ P ↔~(~Q ∧ ~P)) in n4_57a. + replace (¬(¬Q ∧ ¬P) ↔ Q ∨ P) with + (Q ∨ P ↔¬(¬Q ∧ ¬P)) in n4_57a. apply n4_57a. apply EqBi. - specialize n4_21 with (Q ∨ P) (~(~Q ∧ ~P)). + specialize n4_21 with (Q ∨ P) (¬(¬Q ∧ ¬P)). intros n4_21b. apply n4_21b. Qed. @@ -2703,7 +2726,7 @@ Theorem n4_73 : ∀ P Q : Prop, Qed. Theorem n4_74 : ∀ P Q : Prop, - ~P → (Q ↔ (P ∨ Q)). + ¬P → (Q ↔ (P ∨ Q)). Proof. intros P Q. specialize n2_21 with P Q. intros n2_21a. @@ -2724,11 +2747,11 @@ Theorem n4_74 : ∀ P Q : Prop, Theorem n4_76 : ∀ P Q R : Prop, ((P → Q) ∧ (P → R)) ↔ (P → (Q ∧ R)). Proof. intros P Q R. - specialize n4_41 with (~P) Q R. + specialize n4_41 with (¬P) Q R. intros n4_41a. - replace (~P ∨ Q) with (P→Q) in n4_41a. - replace (~P ∨ R) with (P→R) in n4_41a. - replace (~P ∨ Q ∧ R) with (P → Q ∧ R) in n4_41a. + replace (¬P ∨ Q) with (P→Q) in n4_41a. + replace (¬P ∨ R) with (P→R) in n4_41a. + replace (¬P ∨ Q ∧ R) with (P → Q ∧ R) in n4_41a. replace ((P → Q ∧ R) ↔ (P → Q) ∧ (P → R)) with ((P → Q) ∧ (P → R) ↔ (P → Q ∧ R)) in n4_41a. apply n4_41a. @@ -2746,61 +2769,34 @@ Theorem n4_77 : ∀ P Q R : Prop, Proof. intros P Q R. specialize n3_44 with P Q R. intros n3_44a. - specialize Id2_08 with (Q ∨ R → P). - intros Id2_08a. (*Not cited*) - replace ((Q ∨ R → P) → (Q ∨ R → P)) with - ((Q ∨ R → P) → (~(Q ∨ R) ∨ P)) in Id2_08a. - replace (~(Q ∨ R)) with (~Q ∧ ~R) in Id2_08a. - replace (~Q ∧ ~R ∨ P) with - ((~Q ∨ P) ∧ (~R ∨ P)) in Id2_08a. - replace (~Q ∨ P) with (Q → P) in Id2_08a. - replace (~R ∨ P) with (R → P) in Id2_08a. - Conj n3_44a Id2_08a. + specialize n2_2 with Q R. + intros n2_2a. + specialize Add1_3 with Q R. + intros Add1_3a. + specialize Syll2_06 with Q (Q ∨ R) P. + intros Syll2_06a. + MP Syll2_06a n2_2a. + specialize Syll2_06 with R (Q ∨ R) P. + intros Syll2_06b. + MP Syll2_06b Add1_3a. + Conj Syll2_06a Syll2_06b. + split. + apply Syll2_06a. + apply Syll2_06b. + specialize Comp3_43 with ((Q ∨ R)→P) + (Q→P) (R→P). + intros Comp3_43a. + MP Comp3_43a H. + clear n2_2a. clear Add1_3a. clear H. + clear Syll2_06a. clear Syll2_06b. + Conj n3_44a Comp3_43a. split. apply n3_44a. - apply Id2_08a. + apply Comp3_43a. Equiv H. apply H. apply Equiv4_01. - apply Impl1_01. - apply Impl1_01. - specialize n4_41 with P (~Q) (~R). - intros n4_41a. (*Not cited*) - replace (P ∨ ~Q) with - (~Q ∨ P) in n4_41a. - replace (P ∨ ~R) with - (~R ∨ P) in n4_41a. - replace (P ∨ ~Q ∧ ~R) with (~Q ∧ ~R ∨ P) in n4_41a. - replace (~Q ∧ ~R ∨ P ↔ (~Q ∨ P) ∧ (~R ∨ P)) with - ((~Q ∨ P) ∧ (~R ∨ P) ↔ ~Q ∧ ~R ∨ P) in n4_41a. - apply EqBi. - apply n4_41a. - apply EqBi. - specialize n4_21 - with ((~Q ∨ P) ∧ (~R ∨ P)) (~Q ∧ ~R ∨ P). - intros n4_21a. (*Not cited*) - apply n4_21a. - specialize n4_31 with (~Q ∧ ~R) P. - intros n4_31a. (*Not cited*) - apply EqBi. - apply n4_31a. - specialize n4_31 with (~R) P. - intros n4_31b. (*Not cited*) - apply EqBi. - apply n4_31b. - specialize n4_31 with (~Q) P. - intros n4_31c. (*Not cited*) - apply EqBi. - apply n4_31c. (*Not cited*) - apply EqBi. - specialize n4_56 with Q R. - intros n4_56a. (*Not cited*) - apply n4_56a. - replace (~(Q ∨ R) ∨ P) with (Q∨R→P). - reflexivity. - apply Impl1_01. (*Not cited*) Qed. - (*Proof sketch cites Add1_3 + n2_2.*) Theorem n4_78 : ∀ P Q R : Prop, ((P → Q) ∨ (P → R)) ↔ (P → (Q ∨ R)). @@ -2808,63 +2804,61 @@ Theorem n4_78 : ∀ P Q R : Prop, specialize n4_2 with ((P→Q) ∨ (P → R)). intros n4_2a. replace (((P→Q)∨(P→R))↔((P→Q)∨(P→R))) with - (((P → Q) ∨ (P → R))↔((~P ∨ Q) ∨ ~P ∨ R)) in n4_2a. - specialize n4_33 with (~P) Q (~P ∨ R). + (((P → Q) ∨ (P → R))↔((¬P ∨ Q) ∨ ¬P ∨ R)) in n4_2a. + specialize n4_33 with (¬P) Q (¬P ∨ R). intros n4_33a. - replace ((~P ∨ Q) ∨ ~P ∨ R) with - (~P ∨ Q ∨ ~P ∨ R) in n4_2a. - specialize n4_31 with (~P) Q. + replace ((¬P ∨ Q) ∨ ¬P ∨ R) with + (¬P ∨ Q ∨ ¬P ∨ R) in n4_2a. + specialize n4_31 with (¬P) Q. intros n4_31a. - specialize n4_37 with (~P∨Q) (Q ∨ ~P) R. + specialize n4_37 with (¬P∨Q) (Q ∨ ¬P) R. intros n4_37a. MP n4_37a n4_31a. - replace (Q ∨ ~P ∨ R) with - ((Q ∨ ~P) ∨ R) in n4_2a. - replace ((Q ∨ ~P) ∨ R) with - ((~P ∨ Q) ∨ R) in n4_2a. - specialize n4_33 with (~P) (~P∨Q) R. + replace (Q ∨ ¬P ∨ R) with + ((Q ∨ ¬P) ∨ R) in n4_2a. + replace ((Q ∨ ¬P) ∨ R) with + ((¬P ∨ Q) ∨ R) in n4_2a. + specialize n4_33 with (¬P) (¬P∨Q) R. intros n4_33b. - replace (~P ∨ (~P ∨ Q) ∨ R) with - ((~P ∨ (~P ∨ Q)) ∨ R) in n4_2a. - specialize n4_25 with (~P). + replace (¬P ∨ (¬P ∨ Q) ∨ R) with + ((¬P ∨ (¬P ∨ Q)) ∨ R) in n4_2a. + specialize n4_25 with (¬P). intros n4_25a. specialize n4_37 with - (~P) (~P ∨ ~P) (Q ∨ R). + (¬P) (¬P ∨ ¬P) (Q ∨ R). intros n4_37b. MP n4_37b n4_25a. - replace (~P ∨ ~P ∨ Q) with - ((~P ∨ ~P) ∨ Q) in n4_2a. - replace (((~P ∨ ~P) ∨ Q) ∨ R) with - ((~P ∨ ~P) ∨ Q ∨ R) in n4_2a. - replace ((~P ∨ ~P) ∨ Q ∨ R) with - ((~P) ∨ (Q ∨ R)) in n4_2a. - replace (~P ∨ Q ∨ R) with + replace (¬P ∨ ¬P ∨ Q) with + ((¬P ∨ ¬P) ∨ Q) in n4_2a. + replace (((¬P ∨ ¬P) ∨ Q) ∨ R) with + ((¬P ∨ ¬P) ∨ Q ∨ R) in n4_2a. + replace ((¬P ∨ ¬P) ∨ Q ∨ R) with + ((¬P) ∨ (Q ∨ R)) in n4_2a. + replace (¬P ∨ Q ∨ R) with (P → (Q ∨ R)) in n4_2a. apply n4_2a. apply Impl1_01. apply EqBi. apply n4_37b. apply Abb2_33. - replace ((~P ∨ ~P) ∨ Q) with (~P ∨ ~P ∨ Q). + replace ((¬P ∨ ¬P) ∨ Q) with (¬P ∨ ¬P ∨ Q). reflexivity. apply Abb2_33. - replace ((~P ∨ ~P ∨ Q) ∨ R) with - (~P ∨ (~P ∨ Q) ∨ R). + replace ((¬P ∨ ¬P ∨ Q) ∨ R) with + (¬P ∨ (¬P ∨ Q) ∨ R). reflexivity. apply EqBi. apply n4_33b. apply EqBi. apply n4_37a. - replace ((Q ∨ ~P) ∨ R) with (Q ∨ ~P ∨ R). + replace ((Q ∨ ¬P) ∨ R) with (Q ∨ ¬P ∨ R). reflexivity. apply Abb2_33. apply EqBi. apply n4_33a. - replace (~P ∨ Q) with (P→Q). - replace (~P ∨ R) with (P→R). + rewrite <- Impl1_01. + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. - apply Impl1_01. Qed. Theorem n4_79 : ∀ P Q R : Prop, @@ -2879,46 +2873,74 @@ Theorem n4_79 : ∀ P Q R : Prop, apply Transp4_1a. apply Transp4_1b. specialize n4_39 with - (Q→P) (R→P) (~P→~Q) (~P→~R). + (Q→P) (R→P) (¬P→¬Q) (¬P→¬R). intros n4_39a. MP n4_39a H. - specialize n4_78 with (~P) (~Q) (~R). + specialize n4_78 with (¬P) (¬Q) (¬R). intros n4_78a. - replace ((~P → ~Q) ∨ (~P → ~R)) with - (~P → ~Q ∨ ~R) in n4_39a. - specialize Transp4_1 with (~P) (~Q ∨ ~R). - intros Transp4_1c. - replace (~P → ~Q ∨ ~R) with - (~(~Q ∨ ~R) → ~~P) in n4_39a. - replace (~(~Q ∨ ~R)) with - (Q ∧ R) in n4_39a. - replace (~~P) with P in n4_39a. + rewrite Equiv4_01 in n4_78a. + specialize Simp3_26 with + (((¬P→¬Q)∨(¬P→¬R))→(¬P→(¬Q∨¬R))) + ((¬P→(¬Q∨¬R))→((¬P→¬Q)∨(¬P→¬R))). + intros Simp3_26a. + MP Simp3_26a n4_78a. + specialize Transp2_15 with P (¬Q∨¬R). + intros Transp2_15a. + specialize Simp3_27 with + (((¬P→¬Q)∨(¬P→¬R))→(¬P→(¬Q∨¬R))) + ((¬P→(¬Q∨¬R))→((¬P→¬Q)∨(¬P→¬R))). + intros Simp3_27a. + MP Simp3_27a n4_78a. + specialize Transp2_15 with (¬Q∨¬R) P. + intros Transp2_15b. + specialize Syll2_06 with ((¬P→¬Q)∨(¬P→¬R)) + (¬P→(¬Q∨¬R)) (¬(¬Q∨¬R)→P). + intros Syll2_06a. + MP Syll2_06a Simp3_26a. + MP Syll2_06a Transp2_15a. + specialize Syll2_06 with (¬(¬Q∨¬R)→P) + (¬P→(¬Q∨¬R)) ((¬P→¬Q)∨(¬P→¬R)). + intros Syll2_06b. + MP Syll2_06b Trans2_15b. + MP Syll2_06b Simp3_27a. + Conj Syll2_06a Syll2_06b. + split. + apply Syll2_06a. + apply Syll2_06b. + Equiv H0. + clear Transp4_1a. clear Transp4_1b. clear H. + clear Simp3_26a. clear Syll2_06b. clear n4_78a. + clear Transp2_15a. clear Simp3_27a. + clear Transp2_15b. clear Syll2_06a. + Conj n4_39a H0. + split. apply n4_39a. - specialize n4_13 with P. - intros n4_13a. - apply EqBi. - apply n4_13a. - apply Prod3_01. - replace (~(~Q ∨ ~R) → ~~P) with - (~P → ~Q ∨ ~R). - reflexivity. - apply EqBi. - apply Transp4_1c. - replace (~P → ~Q ∨ ~R) with - ((~P → ~Q) ∨ (~P → ~R)). - reflexivity. - apply EqBi. - apply n4_78a. + apply H0. + specialize n4_22 with ((Q→P)∨(R→P)) + ((¬P→¬Q)∨(¬P→¬R)) (¬(¬Q∨¬R)→P). + intros n4_22a. + MP n4_22a H. + specialize n4_2 with (¬(¬Q∨¬R)→P). + intros n4_2a. + Conj n4_22a n4_2a. + split. + apply n4_22a. + apply n4_2a. + specialize n4_22 with ((Q→P)∨(R→P)) + (¬(¬Q∨¬R)→P) (¬(¬Q∨¬R)→P). + intros n4_22b. + MP n4_22b H1. + rewrite <- Prod3_01 in n4_22b. + apply n4_22b. + apply Equiv4_01. Qed. - (*The proof sketch cites Transp2_15, but we did - not need Transp2_15 as a lemma here.*) Theorem n4_8 : ∀ P : Prop, - (P → ~P) ↔ ~P. + (P → ¬P) ↔ ¬P. Proof. intros P. specialize Abs2_01 with P. intros Abs2_01a. - specialize Simp2_02 with P (~P). + specialize Simp2_02 with P (¬P). intros Simp2_02a. Conj Abs2_01a Simp2_02a. split. @@ -2930,11 +2952,11 @@ Theorem n4_8 : ∀ P : Prop, Qed. Theorem n4_81 : ∀ P : Prop, - (~P → P) ↔ P. + (¬P → P) ↔ P. Proof. intros P. specialize n2_18 with P. intros n2_18a. - specialize Simp2_02 with (~P) P. + specialize Simp2_02 with (¬P) P. intros Simp2_02a. Conj n2_18a Simp2_02a. split. @@ -2946,26 +2968,26 @@ Theorem n4_81 : ∀ P : Prop, Qed. Theorem n4_82 : ∀ P Q : Prop, - ((P → Q) ∧ (P → ~Q)) ↔ ~P. + ((P → Q) ∧ (P → ¬Q)) ↔ ¬P. Proof. intros P Q. specialize n2_65 with P Q. intros n2_65a. - specialize Imp3_31 with (P→Q) (P→~Q) (~P). + specialize Imp3_31 with (P→Q) (P→¬Q) (¬P). intros Imp3_31a. MP Imp3_31a n2_65a. specialize n2_21 with P Q. intros n2_21a. - specialize n2_21 with P (~Q). + specialize n2_21 with P (¬Q). intros n2_21b. Conj n2_21a n2_21b. split. apply n2_21a. apply n2_21b. - specialize Comp3_43 with (~P) (P→Q) (P→~Q). + specialize Comp3_43 with (¬P) (P→Q) (P→¬Q). intros Comp3_43a. MP Comp3_43a H. - clear n2_65a. clear n2_21a. clear n2_21b. - clear H. + clear n2_65a. clear n2_21a. + clear n2_21b. clear H. Conj Imp3_31a Comp3_43a. split. apply Imp3_31a. @@ -2976,26 +2998,26 @@ Theorem n4_82 : ∀ P Q : Prop, Qed. Theorem n4_83 : ∀ P Q : Prop, - ((P → Q) ∧ (~P → Q)) ↔ Q. + ((P → Q) ∧ (¬P → Q)) ↔ Q. Proof. intros P Q. specialize n2_61 with P Q. intros n2_61a. - specialize Imp3_31 with (P→Q) (~P→Q) (Q). + specialize Imp3_31 with (P→Q) (¬P→Q) (Q). intros Imp3_31a. MP Imp3_31a n2_61a. specialize Simp2_02 with P Q. intros Simp2_02a. - specialize Simp2_02 with (~P) Q. + specialize Simp2_02 with (¬P) Q. intros Simp2_02b. Conj Simp2_02a Simp2_02b. split. apply Simp2_02a. apply Simp2_02b. - specialize Comp3_43 with Q (P→Q) (~P→Q). + specialize Comp3_43 with Q (P→Q) (¬P→Q). intros Comp3_43a. MP Comp3_43a H. - clear n2_61a. clear Simp2_02a. clear Simp2_02b. - clear H. + clear n2_61a. clear Simp2_02a. + clear Simp2_02b. clear H. Conj Imp3_31a Comp3_43a. split. apply Imp3_31a. @@ -3071,8 +3093,7 @@ Theorem n4_86 : ∀ P Q R : Prop, specialize Exp3_3 with (P↔Q) (Q↔R) (P↔R). intros Exp3_3b. MP Exp3_3b n4_22b. - clear n4_22a. - clear n4_22b. + clear n4_22a. clear n4_22b. replace (Q↔P) with (P↔Q) in Exp3_3a. Conj Exp3_3a Exp3_3b. split. @@ -3187,11 +3208,11 @@ Theorem n5_1 : ∀ P Q : Prop, Qed. Theorem n5_11 : ∀ P Q : Prop, - (P → Q) ∨ (~P → Q). + (P → Q) ∨ (¬P → Q). Proof. intros P Q. specialize n2_5 with P Q. intros n2_5a. - specialize n2_54 with ((P → Q)) (~P → Q). + specialize n2_54 with (P → Q) (¬P → Q). intros n2_54a. MP n2_54a n2_5a. apply n2_54a. @@ -3200,11 +3221,11 @@ Theorem n5_11 : ∀ P Q : Prop, but this may be a misprint.*) Theorem n5_12 : ∀ P Q : Prop, - (P → Q) ∨ (P → ~Q). + (P → Q) ∨ (P → ¬Q). Proof. intros P Q. specialize n2_51 with P Q. intros n2_51a. - specialize n2_54 with ((P → Q)) (P → ~Q). + specialize n2_54 with ((P → Q)) (P → ¬Q). intros n2_54a. MP n2_54a n2_5a. apply n2_54a. @@ -3217,18 +3238,16 @@ Theorem n5_13 : ∀ P Q : Prop, Proof. intros P Q. specialize n2_521 with P Q. intros n2_521a. - replace (~(P → Q) → Q → P) with - (~~(P → Q) ∨ (Q → P)) in n2_521a. - replace (~~(P→Q)) with (P→Q) in n2_521a. + replace (¬(P → Q) → Q → P) with + (¬¬(P → Q) ∨ (Q → P)) in n2_521a. + replace (¬¬(P→Q)) with (P→Q) in n2_521a. apply n2_521a. apply EqBi. specialize n4_13 with (P→Q). intros n4_13a. (*Not cited*) apply n4_13a. - replace (~~(P → Q) ∨ (Q → P)) with - (~(P → Q) → Q → P). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. Qed. Theorem n5_14 : ∀ P Q R : Prop, @@ -3242,78 +3261,76 @@ Theorem n5_14 : ∀ P Q R : Prop, specialize n2_21 with Q R. intros n2_21a. Syll Transp2_16a n2_21a Sa. - replace (~(P→Q)→(Q→R)) with - (~~(P→Q)∨(Q→R)) in Sa. - replace (~~(P→Q)) with (P→Q) in Sa. + replace (¬(P→Q)→(Q→R)) with + (¬¬(P→Q)∨(Q→R)) in Sa. + replace (¬¬(P→Q)) with (P→Q) in Sa. apply Sa. apply EqBi. specialize n4_13 with (P→Q). intros n4_13a. apply n4_13a. - replace (~~(P→Q)∨(Q→R)) with - (~(P→Q)→(Q→R)). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. Qed. Theorem n5_15 : ∀ P Q : Prop, - (P ↔ Q) ∨ (P ↔ ~Q). + (P ↔ Q) ∨ (P ↔ ¬Q). Proof. intros P Q. specialize n4_61 with P Q. intros n4_61a. - replace (~(P → Q) ↔ P ∧ ~Q) with - ((~(P→Q)→P∧~Q)∧((P∧~Q)→~(P→Q))) in n4_61a. + replace (¬(P → Q) ↔ P ∧ ¬Q) with + ((¬(P→Q)→P∧¬Q)∧((P∧¬Q)→¬(P→Q))) in n4_61a. specialize Simp3_26 with - (~(P → Q) → P ∧ ~Q) ((P ∧ ~Q) → ~(P → Q)). + (¬(P → Q) → P ∧ ¬Q) ((P ∧ ¬Q) → ¬(P → Q)). intros Simp3_26a. MP Simp3_26a n4_61a. - specialize n5_1 with P (~Q). + specialize n5_1 with P (¬Q). intros n5_1a. Syll Simp3_26a n5_1a Sa. - specialize n2_54 with (P→Q) (P ↔ ~Q). + specialize n2_54 with (P→Q) (P ↔ ¬Q). intros n2_54a. MP n2_54a Sa. specialize n4_61 with Q P. intros n4_61b. - replace ((~(Q → P)) ↔ (Q ∧ ~P)) with - (((~(Q→P))→(Q∧~P))∧((Q∧~P)→(~(Q→P)))) in n4_61b. + replace ((¬(Q → P)) ↔ (Q ∧ ¬P)) with + (((¬(Q→P))→(Q∧¬P))∧((Q∧¬P)→(¬(Q→P)))) in n4_61b. specialize Simp3_26 with - (~(Q → P)→ (Q ∧ ~P)) ((Q ∧ ~P)→ (~(Q → P))). + (¬(Q → P)→ (Q ∧ ¬P)) ((Q ∧ ¬P)→ (¬(Q → P))). intros Simp3_26b. MP Simp3_26b n4_61b. - specialize n5_1 with Q (~P). + specialize n5_1 with Q (¬P). intros n5_1b. Syll Simp3_26b n5_1b Sb. specialize n4_12 with P Q. intros n4_12a. - replace (Q↔~P) with (P↔~Q) in Sb. - specialize n2_54 with (Q→P) (P↔~Q). + replace (Q↔¬P) with (P↔¬Q) in Sb. + specialize n2_54 with (Q→P) (P↔¬Q). intros n2_54b. MP n2_54b Sb. clear n4_61a. clear Simp3_26a. clear n5_1a. clear n2_54a. clear n4_61b. clear Simp3_26b. clear n5_1b. clear n4_12a. clear n2_54b. - replace (~(P → Q) → P ↔ ~Q) with - (~~(P → Q) ∨ (P ↔ ~Q)) in Sa. - replace (~~(P→Q)) with (P→Q) in Sa. - replace (~(Q → P) → (P ↔ ~Q)) with - (~~(Q → P) ∨ (P ↔ ~Q)) in Sb. - replace (~~(Q→P)) with (Q→P) in Sb. + replace (¬(P → Q) → P ↔ ¬Q) with + (¬¬(P → Q) ∨ (P ↔ ¬Q)) in Sa. + replace (¬¬(P→Q)) with (P→Q) in Sa. + replace (¬(Q → P) → (P ↔ ¬Q)) with + (¬¬(Q → P) ∨ (P ↔ ¬Q)) in Sb. + replace (¬¬(Q→P)) with (Q→P) in Sb. Conj Sa Sb. split. apply Sa. apply Sb. - specialize n4_41 with (P↔~Q) (P→Q) (Q→P). + specialize n4_41 with (P↔¬Q) (P→Q) (Q→P). intros n4_41a. - replace ((P → Q) ∨ (P ↔ ~Q)) with - ((P ↔ ~Q) ∨ (P → Q)) in H. - replace ((Q → P) ∨ (P ↔ ~Q)) with - ((P ↔ ~Q) ∨ (Q → P)) in H. - replace (((P↔~Q)∨(P→Q))∧((P↔~Q)∨(Q→P))) with - ((P ↔ ~Q) ∨ (P → Q) ∧ (Q → P)) in H. + replace ((P → Q) ∨ (P ↔ ¬Q)) with + ((P ↔ ¬Q) ∨ (P → Q)) in H. + replace ((Q → P) ∨ (P ↔ ¬Q)) with + ((P ↔ ¬Q) ∨ (Q → P)) in H. + replace (((P↔¬Q)∨(P→Q))∧((P↔¬Q)∨(Q→P))) with + ((P ↔ ¬Q) ∨ (P → Q) ∧ (Q → P)) in H. replace ((P→Q) ∧ (Q → P)) with (P↔Q) in H. - replace ((P ↔ ~Q) ∨ (P ↔ Q)) with - ((P ↔ Q) ∨ (P ↔ ~Q)) in H. + replace ((P ↔ ¬Q) ∨ (P ↔ Q)) with + ((P ↔ Q) ∨ (P ↔ ¬Q)) in H. apply H. apply EqBi. apply n4_31. @@ -3328,18 +3345,14 @@ Theorem n5_15 : ∀ P Q : Prop, specialize n4_13 with (Q→P). intros n4_13a. apply n4_13a. - replace (~~(Q → P) ∨ (P ↔ ~Q)) with - (~(Q → P) → (P ↔ ~Q)). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. apply EqBi. specialize n4_13 with (P→Q). intros n4_13b. apply n4_13b. - replace (~~(P → Q) ∨ (P ↔ ~Q)) with - (~(P → Q) → P ↔ ~Q). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. apply EqBi. apply n4_12a. apply Equiv4_01. @@ -3347,32 +3360,32 @@ Theorem n5_15 : ∀ P Q : Prop, Qed. Theorem n5_16 : ∀ P Q : Prop, - ~((P ↔ Q) ∧ (P ↔ ~Q)). + ¬((P ↔ Q) ∧ (P ↔ ¬Q)). Proof. intros P Q. - specialize Simp3_26 with ((P→Q)∧ (P → ~Q)) (Q→P). + specialize Simp3_26 with ((P→Q)∧ (P → ¬Q)) (Q→P). intros Simp3_26a. - specialize Id2_08 with ((P ↔ Q) ∧ (P → ~Q)). + specialize Id2_08 with ((P ↔ Q) ∧ (P → ¬Q)). intros Id2_08a. - replace (((P → Q) ∧ (P → ~Q)) ∧ (Q → P)) with - ((P→Q)∧((P→~Q)∧(Q→P))) in Simp3_26a. - replace ((P → ~Q) ∧ (Q → P)) with - ((Q → P) ∧ (P → ~Q)) in Simp3_26a. - replace ((P→Q) ∧ (Q → P)∧ (P → ~Q)) with - (((P→Q) ∧ (Q → P)) ∧ (P → ~Q)) in Simp3_26a. + replace (((P → Q) ∧ (P → ¬Q)) ∧ (Q → P)) with + ((P→Q)∧((P→¬Q)∧(Q→P))) in Simp3_26a. + replace ((P → ¬Q) ∧ (Q → P)) with + ((Q → P) ∧ (P → ¬Q)) in Simp3_26a. + replace ((P→Q) ∧ (Q → P)∧ (P → ¬Q)) with + (((P→Q) ∧ (Q → P)) ∧ (P → ¬Q)) in Simp3_26a. replace ((P → Q) ∧ (Q → P)) with (P↔Q) in Simp3_26a. Syll Id2_08a Simp3_26a Sa. specialize n4_82 with P Q. intros n4_82a. - replace ((P → Q) ∧ (P → ~Q)) with (~P) in Sa. + replace ((P → Q) ∧ (P → ¬Q)) with (¬P) in Sa. specialize Simp3_27 with - (P→Q) ((Q→P)∧ (P → ~Q)). + (P→Q) ((Q→P)∧ (P → ¬Q)). intros Simp3_27a. - replace ((P→Q) ∧ (Q → P)∧ (P → ~Q)) with - (((P→Q) ∧ (Q → P)) ∧ (P → ~Q)) in Simp3_27a. + replace ((P→Q) ∧ (Q → P)∧ (P → ¬Q)) with + (((P→Q) ∧ (Q → P)) ∧ (P → ¬Q)) in Simp3_27a. replace ((P → Q) ∧ (Q → P)) with (P↔Q) in Simp3_27a. - specialize Syll3_33 with Q P (~Q). + specialize Syll3_33 with Q P (¬Q). intros Syll3_33a. Syll Simp3_27a Syll2_06a Sb. specialize Abs2_01 with Q. @@ -3386,128 +3399,124 @@ Theorem n5_16 : ∀ P Q : Prop, apply Sa. apply Sc. specialize Comp3_43 with - ((P ↔ Q) ∧ (P → ~Q)) (~P) (~Q). + ((P ↔ Q) ∧ (P → ¬Q)) (¬P) (¬Q). intros Comp3_43a. MP Comp3_43a H. specialize n4_65 with Q P. intros n4_65a. - replace (~Q ∧ ~P) with (~P ∧ ~Q) in n4_65a. - replace (~P ∧ ~Q) with - (~(~Q→P)) in Comp3_43a. + replace (¬Q ∧ ¬P) with (¬P ∧ ¬Q) in n4_65a. + replace (¬P ∧ ¬Q) with + (¬(¬Q→P)) in Comp3_43a. specialize Exp3_3 with - (P↔Q) (P→~Q) (~(~Q→P)). + (P↔Q) (P→¬Q) (¬(¬Q→P)). intros Exp3_3a. MP Exp3_3a Comp3_43a. - replace ((P→~Q)→~(~Q→P)) with - (~(P→~Q)∨~(~Q→P)) in Exp3_3a. - specialize n4_51 with (P→~Q) (~Q→P). + replace ((P→¬Q)→¬(¬Q→P)) with + (¬(P→¬Q)∨¬(¬Q→P)) in Exp3_3a. + specialize n4_51 with (P→¬Q) (¬Q→P). intros n4_51a. - replace (~(P → ~Q) ∨ ~(~Q → P)) with - (~((P → ~Q) ∧ (~Q → P))) in Exp3_3a. - replace ((P→~Q) ∧ (~Q → P)) with - (P↔~Q) in Exp3_3a. - replace ((P↔Q)→~(P↔~Q)) with - (~(P↔Q)∨~(P↔~Q)) in Exp3_3a. - specialize n4_51 with (P↔Q) (P↔~Q). + replace (¬(P → ¬Q) ∨ ¬(¬Q → P)) with + (¬((P → ¬Q) ∧ (¬Q → P))) in Exp3_3a. + replace ((P→¬Q) ∧ (¬Q → P)) with + (P↔¬Q) in Exp3_3a. + replace ((P↔Q)→¬(P↔¬Q)) with + (¬(P↔Q)∨¬(P↔¬Q)) in Exp3_3a. + specialize n4_51 with (P↔Q) (P↔¬Q). intros n4_51b. - replace (~(P ↔ Q) ∨ ~(P ↔ ~Q)) with - (~((P ↔ Q) ∧ (P ↔ ~Q))) in Exp3_3a. + replace (¬(P ↔ Q) ∨ ¬(P ↔ ¬Q)) with + (¬((P ↔ Q) ∧ (P ↔ ¬Q))) in Exp3_3a. apply Exp3_3a. apply EqBi. apply n4_51b. - replace (~(P ↔ Q) ∨ ~(P ↔ ~Q)) with - (P ↔ Q → ~(P ↔ ~Q)). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. apply Equiv4_01. apply EqBi. apply n4_51a. - replace (~(P → ~Q) ∨ ~(~Q → P)) with - ((P → ~Q) → ~(~Q → P)). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. apply EqBi. apply n4_65a. apply EqBi. - specialize n4_3 with (~P) (~Q). + specialize n4_3 with (¬P) (¬Q). intros n4_3a. apply n4_3a. apply Equiv4_01. apply EqBi. - specialize n4_32 with (P→Q) (Q→P) (P→~Q). + specialize n4_32 with (P→Q) (Q→P) (P→¬Q). intros n4_32a. apply n4_32a. - replace (~P) with ((P → Q) ∧ (P → ~Q)). + replace (¬P) with ((P → Q) ∧ (P → ¬Q)). reflexivity. apply EqBi. apply n4_82a. apply Equiv4_01. apply EqBi. - specialize n4_32 with (P→Q) (Q→P) (P→~Q). + specialize n4_32 with (P→Q) (Q→P) (P→¬Q). intros n4_32b. apply n4_32b. apply EqBi. - specialize n4_3 with (Q→P) (P→~Q). + specialize n4_3 with (Q→P) (P→¬Q). intros n4_3b. apply n4_3b. - replace ((P → Q) ∧ (P → ~Q) ∧ (Q → P)) with - (((P → Q) ∧ (P → ~Q)) ∧ (Q → P)). + replace ((P → Q) ∧ (P → ¬Q) ∧ (Q → P)) with + (((P → Q) ∧ (P → ¬Q)) ∧ (Q → P)). reflexivity. apply EqBi. - specialize n4_32 with (P→Q) (P→~Q) (Q→P). + specialize n4_32 with (P→Q) (P→¬Q) (Q→P). intros n4_32a. apply n4_32a. Qed. Theorem n5_17 : ∀ P Q : Prop, - ((P ∨ Q) ∧ ~(P ∧ Q)) ↔ (P ↔ ~Q). + ((P ∨ Q) ∧ ¬(P ∧ Q)) ↔ (P ↔ ¬Q). Proof. intros P Q. specialize n4_64 with Q P. intros n4_64a. - specialize n4_21 with (Q∨P) (~Q→P). + specialize n4_21 with (Q∨P) (¬Q→P). intros n4_21a. - replace ((~Q→P)↔(Q∨P)) with - ((Q∨P)↔(~Q→P)) in n4_64a. + replace ((¬Q→P)↔(Q∨P)) with + ((Q∨P)↔(¬Q→P)) in n4_64a. replace (Q∨P) with (P∨Q) in n4_64a. specialize n4_63 with P Q. intros n4_63a. - replace (~(P → ~Q) ↔ P ∧ Q) with - (P ∧ Q ↔ ~(P → ~Q)) in n4_63a. - specialize Transp4_11 with (P∧Q) (~(P→~Q)). + replace (¬(P → ¬Q) ↔ P ∧ Q) with + (P ∧ Q ↔ ¬(P → ¬Q)) in n4_63a. + specialize Transp4_11 with (P∧Q) (¬(P→¬Q)). intros Transp4_11a. - replace (~~(P→~Q)) with - (P→~Q) in Transp4_11a. - replace (P ∧ Q ↔ ~(P → ~Q)) with - (~(P ∧ Q) ↔ (P → ~Q)) in n4_63a. + replace (¬¬(P→¬Q)) with + (P→¬Q) in Transp4_11a. + replace (P ∧ Q ↔ ¬(P → ¬Q)) with + (¬(P ∧ Q) ↔ (P → ¬Q)) in n4_63a. clear Transp4_11a. clear n4_21a. Conj n4_64a n4_63a. split. apply n4_64a. apply n4_63a. specialize n4_38 with - (P ∨ Q) (~(P ∧ Q)) (~Q → P) (P → ~Q). + (P ∨ Q) (¬(P ∧ Q)) (¬Q → P) (P → ¬Q). intros n4_38a. MP n4_38a H. - replace ((~Q→P) ∧ (P → ~Q)) with - (~Q↔P) in n4_38a. - specialize n4_21 with P (~Q). + replace ((¬Q→P) ∧ (P → ¬Q)) with + (¬Q↔P) in n4_38a. + specialize n4_21 with P (¬Q). intros n4_21b. - replace (~Q↔P) with (P↔~Q) in n4_38a. + replace (¬Q↔P) with (P↔¬Q) in n4_38a. apply n4_38a. apply EqBi. apply n4_21b. apply Equiv4_01. - replace (~(P ∧ Q) ↔ (P → ~Q)) with - (P ∧ Q ↔ ~(P → ~Q)). + replace (¬(P ∧ Q) ↔ (P → ¬Q)) with + (P ∧ Q ↔ ¬(P → ¬Q)). reflexivity. apply EqBi. apply Transp4_11a. apply EqBi. - specialize n4_13 with (P→~Q). + specialize n4_13 with (P→¬Q). intros n4_13a. apply n4_13a. apply EqBi. - specialize n4_21 with (P ∧ Q) (~(P→~Q)). + specialize n4_21 with (P ∧ Q) (¬(P→¬Q)). intros n4_21b. apply n4_21b. apply EqBi. @@ -3519,7 +3528,7 @@ Theorem n5_17 : ∀ P Q : Prop, Qed. Theorem n5_18 : ∀ P Q : Prop, - (P ↔ Q) ↔ ~(P ↔ ~Q). + (P ↔ Q) ↔ ¬(P ↔ ¬Q). Proof. intros P Q. specialize n5_15 with P Q. intros n5_15a. @@ -3529,43 +3538,43 @@ Theorem n5_18 : ∀ P Q : Prop, split. apply n5_15a. apply n5_16a. - specialize n5_17 with (P↔Q) (P↔~Q). + specialize n5_17 with (P↔Q) (P↔¬Q). intros n5_17a. - replace ((P ↔ Q) ↔ ~(P ↔ ~Q)) with - (((P↔Q)∨(P↔~Q))∧~((P↔Q)∧(P↔~Q))). + replace ((P ↔ Q) ↔ ¬(P ↔ ¬Q)) with + (((P↔Q)∨(P↔¬Q))∧¬((P↔Q)∧(P↔¬Q))). apply H. apply EqBi. apply n5_17a. Qed. Theorem n5_19 : ∀ P : Prop, - ~(P ↔ ~P). + ¬(P ↔ ¬P). Proof. intros P. specialize n5_18 with P P. intros n5_18a. specialize n4_2 with P. intros n4_2a. - replace (~(P↔~P)) with (P↔P). + replace (¬(P↔¬P)) with (P↔P). apply n4_2a. apply EqBi. apply n5_18a. Qed. Theorem n5_21 : ∀ P Q : Prop, - (~P ∧ ~Q) → (P ↔ Q). + (¬P ∧ ¬Q) → (P ↔ Q). Proof. intros P Q. - specialize n5_1 with (~P) (~Q). + specialize n5_1 with (¬P) (¬Q). intros n5_1a. specialize Transp4_11 with P Q. intros Transp4_11a. - replace (~P↔~Q) with (P↔Q) in n5_1a. + replace (¬P↔¬Q) with (P↔Q) in n5_1a. apply n5_1a. apply EqBi. apply Transp4_11a. Qed. Theorem n5_22 : ∀ P Q : Prop, - ~(P ↔ Q) ↔ ((P ∧ ~Q) ∨ (Q ∧ ~P)). + ¬(P ↔ Q) ↔ ((P ∧ ¬Q) ∨ (Q ∧ ¬P)). Proof. intros P Q. specialize n4_61 with P Q. intros n4_61a. @@ -3576,13 +3585,13 @@ Theorem n5_22 : ∀ P Q : Prop, apply n4_61a. apply n4_61b. specialize n4_39 with - (~(P → Q)) (~(Q → P)) (P ∧ ~Q) (Q ∧ ~P). + (¬(P → Q)) (¬(Q → P)) (P ∧ ¬Q) (Q ∧ ¬P). intros n4_39a. MP n4_39a H. specialize n4_51 with (P→Q) (Q→P). intros n4_51a. - replace (~(P → Q) ∨ ~(Q → P)) with - (~((P → Q) ∧ (Q → P))) in n4_39a. + replace (¬(P → Q) ∨ ¬(Q → P)) with + (¬((P → Q) ∧ (Q → P))) in n4_39a. replace ((P → Q) ∧ (Q → P)) with (P↔Q) in n4_39a. apply n4_39a. @@ -3592,54 +3601,56 @@ Theorem n5_22 : ∀ P Q : Prop, Qed. Theorem n5_23 : ∀ P Q : Prop, - (P ↔ Q) ↔ ((P ∧ Q) ∨ (~P ∧ ~Q)). + (P ↔ Q) ↔ ((P ∧ Q) ∨ (¬P ∧ ¬Q)). Proof. intros P Q. specialize n5_18 with P Q. intros n5_18a. - specialize n5_22 with P (~Q). + specialize n5_22 with P (¬Q). intros n5_22a. - specialize n4_13 with Q. - intros n4_13a. - replace (~(P↔~Q)) with - ((P ∧ ~~Q) ∨ (~Q ∧ ~P)) in n5_18a. - replace (~~Q) with Q in n5_18a. - replace (~Q ∧ ~P) with (~P ∧ ~Q) in n5_18a. + Conj n5_18a n5_22a. + split. apply n5_18a. + apply n5_22a. + specialize n4_22 with (P↔Q) (¬(P↔¬Q)) + (P ∧ ¬¬Q ∨ ¬Q ∧ ¬P). + intros n4_22a. + MP n4_22a H. + replace (¬¬Q) with Q in n4_22a. + replace (¬Q ∧ ¬P) with (¬P ∧ ¬Q) in n4_22a. + apply n4_22a. apply EqBi. - specialize n4_3 with (~P) (~Q). + specialize n4_3 with (¬P) (¬Q). intros n4_3a. - apply n4_3a. (*with (~P) (~Q)*) + apply n4_3a. (*with (¬P) (¬Q)*) apply EqBi. + specialize n4_13 with Q. + intros n4_13a. apply n4_13a. - replace (P∧~~Q∨~Q∧~P) with (~(P↔~Q)). - reflexivity. - apply EqBi. - apply n5_22a. Qed. - (*The proof sketch in Principia offers n4_36, - but we found it far simpler to to use n4_3.*) + (*The proof sketch in Principia offers n4_36. + This seems to be a misprint. We used n4_3.*) Theorem n5_24 : ∀ P Q : Prop, - ~((P ∧ Q) ∨ (~P ∧ ~Q)) ↔ ((P ∧ ~Q) ∨ (Q ∧ ~P)). + ¬((P ∧ Q) ∨ (¬P ∧ ¬Q)) ↔ ((P ∧ ¬Q) ∨ (Q ∧ ¬P)). Proof. intros P Q. specialize n5_22 with P Q. intros n5_22a. specialize n5_23 with P Q. intros n5_23a. - replace ((P↔Q)↔((P∧ Q) ∨(~P ∧ ~Q))) with - ((~(P↔Q)↔~((P∧ Q)∨(~P ∧ ~Q)))) in n5_23a. - replace (~(P↔Q)) with - (~((P ∧ Q) ∨ (~P ∧ ~Q))) in n5_22a. + replace ((P↔Q)↔((P∧ Q) ∨(¬P ∧ ¬Q))) with + ((¬(P↔Q)↔¬((P∧ Q)∨(¬P ∧ ¬Q)))) in n5_23a. + replace (¬(P↔Q)) with + (¬((P ∧ Q) ∨ (¬P ∧ ¬Q))) in n5_22a. apply n5_22a. - replace (~((P ∧ Q)∨(~P ∧ ~Q))) with (~(P↔Q)). + replace (¬((P ∧ Q)∨(¬P ∧ ¬Q))) with (¬(P↔Q)). reflexivity. apply EqBi. apply n5_23a. - replace (~(P ↔ Q) ↔ ~(P ∧ Q ∨ ~P ∧ ~Q)) with - ((P ↔ Q) ↔ P ∧ Q ∨ ~P ∧ ~Q). + replace (¬(P ↔ Q) ↔ ¬(P ∧ Q ∨ ¬P ∧ ¬Q)) with + ((P ↔ Q) ↔ P ∧ Q ∨ ¬P ∧ ¬Q). reflexivity. specialize Transp4_11 with - (P↔Q) (P ∧ Q ∨ ~P ∧ ~Q). + (P↔Q) (P ∧ Q ∨ ¬P ∧ ¬Q). intros Transp4_11a. apply EqBi. apply Transp4_11a. (*Not cited*) @@ -3842,8 +3853,8 @@ Theorem n5_36 : ∀ P Q : Prop, apply EqBi. apply n5_32a. Qed. - (*The proof sketch cites Ass3_35 and n4_38, but - the sketch was indecipherable.*) + (*The proof sketch cites Ass3_35 and n4_38, + but the sketch was indecipherable.*) Theorem n5_4 : ∀ P Q : Prop, (P → (P → Q)) ↔ (P → Q). @@ -3921,57 +3932,65 @@ Theorem n5_44 : ∀ P Q R : Prop, Proof. intros P Q R. specialize n4_76 with P Q R. intros n4_76a. - replace ((P→Q)∧(P→R)↔(P→Q∧R)) with - (((P→Q)∧(P→R)→(P→Q∧R)) - ∧ - ((P→Q∧R)→(P→Q)∧(P→R))) in n4_76a. + rewrite Equiv4_01 in n4_76a. specialize Simp3_26 with - ((P→Q)∧(P→R)→(P→Q∧R)) - ((P→Q∧R)→(P→Q)∧(P→R)). - intros Simp3_26a. (*Not cited*) + (((P→Q)∧(P→R))→(P→(Q∧R))) + ((P→(Q∧R))→((P→Q)∧(P→R))). + intros Simp3_26a. MP Simp3_26a n4_76a. - specialize Exp3_3 with (P→Q) (P→R) (P→Q∧R). - intros Exp3_3a. (*Not cited*) - MP Exp3_3a Simp3_26a. specialize Simp3_27 with - ((P→Q)∧(P→R)→(P→Q∧R)) - ((P→Q∧R)→(P→Q)∧(P→R)). - intros Simp3_27a. (*Not cited*) + (((P→Q)∧(P→R))→(P→(Q∧R))) + ((P→(Q∧R))→((P→Q)∧(P→R))). + intros Simp3_27a. MP Simp3_27a n4_76a. - specialize Simp3_26 with (P→R) (P→Q). + specialize Simp3_27 with (P→Q) (P→Q∧R). + intros Simp3_27d. + Syll Simp3_27d Simp3_27a Sa. + specialize n5_3 with (P→Q) (P→R) (P→(Q∧R)). + intros n5_3a. + rewrite Equiv4_01 in n5_3a. + specialize Simp3_26 with + ((((P→Q)∧(P→R))→(P→(Q∧R)))→ + (((P→Q)∧(P→R))→((P→Q)∧(P→(Q∧R))))) + ((((P→Q)∧(P→R))→((P→Q)∧(P→(Q∧R)))) + →(((P→Q)∧(P→R))→(P→(Q∧R)))). intros Simp3_26b. - replace ((P→Q)∧(P→R)) with - ((P→R)∧(P→Q)) in Simp3_27a. - Syll Simp3_27a Simp3_26b Sa. - specialize Simp2_02 with (P→Q) ((P→Q∧R)→P→R). - intros Simp2_02a. (*Not cited*) - MP Simp2_02a Sa. - clear Sa. clear Simp3_26b. clear Simp3_26a. - clear n4_76a. clear Simp3_27a. - Conj Exp3_3a Simp2_02a. + MP Simp3_26b n5_3a. + specialize Simp3_27 with + ((((P→Q)∧(P→R))→(P→(Q∧R)))→ + (((P→Q)∧(P→R))→((P→Q)∧(P→(Q∧R))))) + ((((P→Q)∧(P→R))→((P→Q)∧(P→(Q∧R)))) + →(((P→Q)∧(P→R))→(P→(Q∧R)))). + intros Simp3_27b. + MP Simp3_27b n5_3a. + MP Simp3_26a Simp3_26b. + MP Simp3_27a Simp3_27b. + clear n4_76a. clear Simp3_26a. clear Simp3_27a. + clear Simp3_27b. clear Simp3_27d. clear n5_3a. + Conj Simp3_26b Sa. split. - apply Exp3_3a. - apply Simp2_02a. - specialize n4_76 with (P→Q) - ((P→R)→(P→(Q∧R))) ((P→(Q∧R))→(P→R)). - intros n4_76b. (*Second use not indicated*) - replace - (((P→Q)→(P→R)→P→Q∧R)∧((P→Q)→(P→Q∧R)→P→R)) - with - ((P→Q)→((P→R)→P→Q∧R)∧((P→Q∧R)→P→R)) in H. - replace (((P→R)→P→Q∧R)∧((P→Q∧R)→P→R)) with - ((P→R)↔(P→Q∧R)) in H. - apply H. - apply Equiv4_01. - replace ((P→Q)→((P→R)→P→Q∧R)∧((P→Q∧R)→P→R)) with - (((P→Q)→(P→R)→P→Q∧R)∧((P→Q)→(P→Q∧R)→P→R)). - reflexivity. - apply EqBi. - apply n4_76b. + apply Sa. + apply Simp3_26b. + Equiv H. + specialize n5_32 with (P→Q) (P→R) (P→(Q∧R)). + intros n5_32a. + rewrite Equiv4_01 in n5_32a. + specialize Simp3_27 with + (((P → Q) → (P → R) ↔ (P → Q ∧ R)) + → (P → Q) ∧ (P → R) ↔ (P → Q) ∧ (P → Q ∧ R)) + ((P → Q) ∧ (P → R) ↔ (P → Q) ∧ (P → Q ∧ R) + → (P → Q) → (P → R) ↔ (P → Q ∧ R)). + intros Simp3_27c. + MP Simp3_27c n5_32a. + replace (((P→Q)∧(P→(Q∧R)))↔((P→Q)∧(P→R))) + with (((P→Q)∧(P→R))↔((P→Q)∧(P→(Q∧R)))) in H. + MP Simp3_27c H. + apply Simp3_27c. + specialize n4_21 with + ((P→Q)∧(P→R)) ((P→Q)∧(P→(Q∧R))). + intros n4_21a. apply EqBi. - specialize n4_3 with (P→R) (P→Q). - intros n4_3a. - apply n4_3a. (*Not cited*) + apply n4_21a. apply Equiv4_01. Qed. @@ -4095,19 +4114,19 @@ Theorem n5_54 : ∀ P Q : Prop, intros Transp4_11a. replace (Q∧P) with (P∧Q) in n4_44a. replace (Q↔Q∨P∧Q) with - (~Q↔~(Q∨P∧Q)) in n4_44a. - replace (~Q) with (~(Q∨P∧Q)) in Transp2_16a. - replace (~(Q∨P∧Q)) with - (~Q∧~(P∧Q)) in Transp2_16a. - specialize n5_1 with (~Q) (~(P∧Q)). + (¬Q↔¬(Q∨P∧Q)) in n4_44a. + replace (¬Q) with (¬(Q∨P∧Q)) in Transp2_16a. + replace (¬(Q∨P∧Q)) with + (¬Q∧¬(P∧Q)) in Transp2_16a. + specialize n5_1 with (¬Q) (¬(P∧Q)). intros n5_1a. Syll Transp2_16a n5_1a Sa. - replace (~(P↔P∧Q)→(~Q↔~(P∧Q))) with - (~~(P↔P∧Q)∨(~Q↔~(P∧Q))) in Sa. - replace (~~(P↔P∧Q)) with (P↔P∧Q) in Sa. + replace (¬(P↔P∧Q)→(¬Q↔¬(P∧Q))) with + (¬¬(P↔P∧Q)∨(¬Q↔¬(P∧Q))) in Sa. + replace (¬¬(P↔P∧Q)) with (P↔P∧Q) in Sa. specialize Transp4_11 with Q (P∧Q). intros Transp4_11b. - replace (~Q↔~(P∧Q)) with (Q↔(P∧Q)) in Sa. + replace (¬Q↔¬(P∧Q)) with (Q↔(P∧Q)) in Sa. replace (Q↔(P∧Q)) with ((P∧Q)↔Q) in Sa. replace (P↔(P∧Q)) with ((P∧Q)↔P) in Sa. apply Sa. @@ -4125,19 +4144,17 @@ Theorem n5_54 : ∀ P Q : Prop, specialize n4_13 with (P ↔ (P∧Q)). intros n4_13a. (*Not cited*) apply n4_13a. - replace (~~(P↔P∧Q)∨(~Q↔~(P∧Q))) with - (~(P↔P∧Q)→~Q↔~(P∧Q)). + rewrite <- Impl1_01. (*Not cited*) reflexivity. - apply Impl1_01. (*Not cited*) apply EqBi. specialize n4_56 with Q (P∧Q). intros n4_56a. (*Not cited*) apply n4_56a. - replace (~(Q∨P∧Q)) with (~Q). + replace (¬(Q∨P∧Q)) with (¬Q). reflexivity. apply EqBi. apply n4_44a. - replace (~Q↔~(Q∨P∧Q)) with (Q↔Q∨P∧Q). + replace (¬Q↔¬(Q∨P∧Q)) with (Q↔Q∨P∧Q). reflexivity. apply EqBi. apply Transp4_11a. @@ -4164,9 +4181,9 @@ Theorem n5_55 : ∀ P Q : Prop, intros Transp2_15a. (*Not cited*) MP Transp2_15a n4_74a. Syll Transp2_15a Sa Sb. - replace (~(Q↔(P∨Q))→(P↔(P∨Q))) with - (~~(Q↔(P∨Q))∨(P↔(P∨Q))) in Sb. - replace (~~(Q↔(P∨Q))) with (Q↔(P∨Q)) in Sb. + replace (¬(Q↔(P∨Q))→(P↔(P∨Q))) with + (¬¬(Q↔(P∨Q))∨(P↔(P∨Q))) in Sb. + replace (¬¬(Q↔(P∨Q))) with (Q↔(P∨Q)) in Sb. replace (Q↔(P∨Q)) with ((P∨Q)↔Q) in Sb. replace (P↔(P∨Q)) with ((P∨Q)↔P) in Sb. replace ((P∨Q↔Q)∨(P∨Q↔P)) with @@ -4188,10 +4205,8 @@ Theorem n5_55 : ∀ P Q : Prop, specialize n4_13 with (Q ↔ P ∨ Q). intros n4_13a. (*Not cited*) apply n4_13a. - replace (~~(Q↔P∨Q)∨(P↔P∨Q)) with - (~(Q↔P∨Q)→P↔P∨Q). + rewrite <- Impl1_01. reflexivity. - apply Impl1_01. apply EqBi. specialize n4_31 with P Q. intros n4_31b. @@ -4219,28 +4234,28 @@ Theorem n5_55 : ∀ P Q : Prop, Qed. Theorem n5_6 : ∀ P Q R : Prop, - ((P ∧ ~Q) → R) ↔ (P → (Q ∨ R)). + ((P ∧ ¬Q) → R) ↔ (P → (Q ∨ R)). Proof. intros P Q R. - specialize n4_87 with P (~Q) R. + specialize n4_87 with P (¬Q) R. intros n4_87a. specialize n4_64 with Q R. intros n4_64a. specialize n4_85 with P Q R. intros n4_85a. - replace (((P∧~Q→R)↔(P→~Q→R))↔((~Q→P→R)↔(~Q∧P→R))) + replace (((P∧¬Q→R)↔(P→¬Q→R))↔((¬Q→P→R)↔(¬Q∧P→R))) with - ((((P∧~Q→R)↔(P→~Q→R))→((~Q→P→R)↔(~Q∧P→R))) + ((((P∧¬Q→R)↔(P→¬Q→R))→((¬Q→P→R)↔(¬Q∧P→R))) ∧ - ((((~Q→P→R)↔(~Q∧P→R)))→(((P∧~Q→R)↔(P→~Q→R))))) + ((((¬Q→P→R)↔(¬Q∧P→R)))→(((P∧¬Q→R)↔(P→¬Q→R))))) in n4_87a. specialize Simp3_27 with - (((P∧~Q→R)↔(P→~Q→R)→(~Q→P→R)↔(~Q∧P→R))) - (((~Q→P→R)↔(~Q∧P→R)→(P∧~Q→R)↔(P→~Q→R))). + (((P∧¬Q→R)↔(P→¬Q→R)→(¬Q→P→R)↔(¬Q∧P→R))) + (((¬Q→P→R)↔(¬Q∧P→R)→(P∧¬Q→R)↔(P→¬Q→R))). intros Simp3_27a. MP Simp3_27a n4_87a. - specialize Imp3_31 with (~Q) P R. + specialize Imp3_31 with (¬Q) P R. intros Imp3_31a. - specialize Exp3_3 with (~Q) P R. + specialize Exp3_3 with (¬Q) P R. intros Exp3_3a. Conj Imp3_31a Exp3_3a. split. @@ -4248,9 +4263,9 @@ Theorem n5_6 : ∀ P Q R : Prop, apply Exp3_3a. Equiv H. MP Simp3_27a H. - replace (~Q→R) with (Q∨R) in Simp3_27a. + replace (¬Q→R) with (Q∨R) in Simp3_27a. apply Simp3_27a. - replace (Q ∨ R) with (~Q → R). + replace (Q ∨ R) with (¬Q → R). reflexivity. apply EqBi. apply n4_64a. @@ -4259,22 +4274,22 @@ Theorem n5_6 : ∀ P Q R : Prop, Qed. Theorem n5_61 : ∀ P Q : Prop, - ((P ∨ Q) ∧ ~Q) ↔ (P ∧ ~Q). + ((P ∨ Q) ∧ ¬Q) ↔ (P ∧ ¬Q). Proof. intros P Q. specialize n4_74 with Q P. intros n4_74a. - specialize n5_32 with (~Q) P (Q∨P). + specialize n5_32 with (¬Q) P (Q∨P). intros n5_32a. - replace (~Q → P ↔ Q ∨ P) with - (~Q ∧ P ↔ ~Q ∧ (Q ∨ P)) in n4_74a. - replace (~Q∧P) with (P∧~Q) in n4_74a. - replace (~Q∧(Q∨P)) with ((Q∨P)∧~Q) in n4_74a. - replace (Q∨P) with (P∨Q) in n4_74a. - replace (P ∧ ~Q ↔ (P ∨ Q) ∧ ~Q) with - ((P ∨ Q) ∧ ~Q ↔ P ∧ ~Q) in n4_74a. + replace (¬Q → P ↔ Q ∨ P) with + (¬Q ∧ P ↔ ¬Q ∧ (Q ∨ P)) in n4_74a. + replace (¬Q ∧ P) with (P ∧ ¬Q) in n4_74a. + replace (¬Q ∧ (Q ∨ P)) with ((Q ∨ P) ∧ ¬Q) in n4_74a. + replace (Q ∨ P) with (P ∨ Q) in n4_74a. + replace (P ∧ ¬Q ↔ (P ∨ Q) ∧ ¬Q) with + ((P ∨ Q) ∧ ¬Q ↔ P ∧ ¬Q) in n4_74a. apply n4_74a. apply EqBi. - specialize n4_21 with ((P∨Q)∧~Q) (P∧~Q). + specialize n4_21 with ((P ∨ Q) ∧ ¬Q) (P ∧ ¬Q). intros n4_21a. (*Not cited*) apply n4_21a. apply EqBi. @@ -4282,35 +4297,35 @@ Theorem n5_61 : ∀ P Q : Prop, intros n4_31a. (*Not cited*) apply n4_31a. apply EqBi. - specialize n4_3 with (Q∨P) (~Q). + specialize n4_3 with (Q ∨ P) (¬Q). intros n4_3a. (*Not cited*) apply n4_3a. apply EqBi. - specialize n4_3 with P (~Q). + specialize n4_3 with P (¬Q). intros n4_3b. (*Not cited*) apply n4_3b. - replace (~Q ∧ P ↔ ~Q ∧ (Q ∨ P)) with - (~Q → P ↔ Q ∨ P). + replace (¬Q ∧ P ↔ ¬Q ∧ (Q ∨ P)) with + (¬Q → P ↔ Q ∨ P). reflexivity. apply EqBi. apply n5_32a. Qed. Theorem n5_62 : ∀ P Q : Prop, - ((P ∧ Q) ∨ ~Q) ↔ (P ∨ ~Q). + ((P ∧ Q) ∨ ¬Q) ↔ (P ∨ ¬Q). Proof. intros P Q. specialize n4_7 with Q P. intros n4_7a. - replace (Q→P) with (~Q∨P) in n4_7a. - replace (Q→(Q∧P)) with (~Q∨(Q∧P)) in n4_7a. - replace (~Q∨(Q∧P)) with ((Q∧P)∨~Q) in n4_7a. - replace (~Q∨P) with (P∨~Q) in n4_7a. + replace (Q→P) with (¬Q∨P) in n4_7a. + replace (Q→(Q∧P)) with (¬Q∨(Q∧P)) in n4_7a. + replace (¬Q∨(Q∧P)) with ((Q∧P)∨¬Q) in n4_7a. + replace (¬Q∨P) with (P∨¬Q) in n4_7a. replace (Q∧P) with (P∧Q) in n4_7a. - replace (P ∨ ~Q ↔ P ∧ Q ∨ ~Q) with - (P ∧ Q ∨ ~Q ↔ P ∨ ~Q) in n4_7a. + replace (P ∨ ¬Q ↔ P ∧ Q ∨ ¬Q) with + (P ∧ Q ∨ ¬Q ↔ P ∨ ¬Q) in n4_7a. apply n4_7a. apply EqBi. - specialize n4_21 with (P ∧ Q ∨ ~Q) (P ∨ ~Q). + specialize n4_21 with (P ∧ Q ∨ ¬Q) (P ∨ ¬Q). intros n4_21a. (*Not cited*) apply n4_21a. apply EqBi. @@ -4318,49 +4333,41 @@ Theorem n5_62 : ∀ P Q : Prop, intros n4_3a. (*Not cited*) apply n4_3a. apply EqBi. - specialize n4_31 with P (~Q). + specialize n4_31 with P (¬Q). intros n4_31a. (*Not cited*) apply n4_31a. apply EqBi. - specialize n4_31 with (Q ∧ P) (~Q). + specialize n4_31 with (Q ∧ P) (¬Q). intros n4_31b. (*Not cited*) apply n4_31b. - replace (~Q ∨ Q ∧ P) with (Q → Q ∧ P). + rewrite <- Impl1_01. reflexivity. - apply EqBi. - specialize n4_6 with Q (Q∧P). - intros n4_6a. (*Not cited*) - apply n4_6a. - replace (~Q ∨ P) with (Q → P). + rewrite <- Impl1_01. reflexivity. - apply EqBi. - specialize n4_6 with Q P. - intros n4_6b. (*Not cited*) - apply n4_6b. Qed. Theorem n5_63 : ∀ P Q : Prop, - (P ∨ Q) ↔ (P ∨ (~P ∧ Q)). + (P ∨ Q) ↔ (P ∨ (¬P ∧ Q)). Proof. intros P Q. - specialize n5_62 with Q (~P). + specialize n5_62 with Q (¬P). intros n5_62a. - replace (~~P) with P in n5_62a. + replace (¬¬P) with P in n5_62a. replace (Q ∨ P) with (P ∨ Q) in n5_62a. - replace ((Q∧~P)∨P) with (P∨(Q∧~P)) in n5_62a. - replace (P ∨ Q ∧ ~P ↔ P ∨ Q) with - (P ∨ Q ↔ P ∨ Q ∧ ~P) in n5_62a. - replace (Q∧~P) with (~P∧Q) in n5_62a. + replace ((Q∧¬P)∨P) with (P∨(Q∧¬P)) in n5_62a. + replace (P ∨ Q ∧ ¬P ↔ P ∨ Q) with + (P ∨ Q ↔ P ∨ Q ∧ ¬P) in n5_62a. + replace (Q∧¬P) with (¬P∧Q) in n5_62a. apply n5_62a. apply EqBi. - specialize n4_3 with (~P) Q. + specialize n4_3 with (¬P) Q. intros n4_3a. apply n4_3a. (*Not cited*) apply EqBi. - specialize n4_21 with (P∨Q) (P∨(Q∧~P)). + specialize n4_21 with (P∨Q) (P∨(Q∧¬P)). intros n4_21a. (*Not cited*) apply n4_21a. apply EqBi. - specialize n4_31 with P (Q∧~P). + specialize n4_31 with P (Q∧¬P). intros n4_31a. (*Not cited*) apply n4_31a. apply EqBi. @@ -4376,89 +4383,168 @@ Theorem n5_63 : ∀ P Q : Prop, Theorem n5_7 : ∀ P Q R : Prop, ((P ∨ R) ↔ (Q ∨ R)) ↔ (R ∨ (P ↔ Q)). Proof. intros P Q R. - specialize n5_32 with (~R) (~P) (~Q). - intros n5_32a. (*Not cited*) - replace (~R∧~P) with (~(R∨P)) in n5_32a. - replace (~R∧~Q) with (~(R∨Q)) in n5_32a. - replace ((~(R∨P))↔(~(R∨Q))) with - ((R∨P)↔(R∨Q)) in n5_32a. - replace ((~P)↔(~Q)) with (P↔Q) in n5_32a. - replace (~R→(P↔Q)) with - (~~R∨(P↔Q)) in n5_32a. - replace (~~R) with R in n5_32a. - replace (R∨P) with (P∨R) in n5_32a. - replace (R∨Q) with (Q∨R) in n5_32a. - replace ((R∨(P↔Q))↔(P∨R↔Q∨R)) with - ((P∨R↔Q∨R)↔(R∨(P↔Q))) in n5_32a. - apply n5_32a. (*Not cited*) - apply EqBi. - specialize n4_21 with ((P∨R)↔(Q∨R)) (R∨(P↔Q)). - intros n4_21a. - apply n4_21a. (*Not cited*) + specialize n4_74 with R P. + intros n4_74a. + specialize n4_74 with R Q. + intros n4_74b. (*Greg's suggestion*) + Conj n4_74a n4_74b. + split. + apply n4_74a. + apply n4_74b. + specialize Comp3_43 with + (¬R) (P↔R∨P) (Q↔R∨Q). + intros Comp3_43a. + MP Comp3_43a H. + specialize n4_22 with P (R∨P) (R∨Q). + intros n4_22a. + specialize n4_22 with P (R∨Q) Q. + intros n4_22b. + specialize Exp3_3 with (P↔(R∨Q)) + ((R∨Q)↔Q) (P↔Q). + intros Exp3_3a. + MP Exp3_3a n4_22b. + Syll n4_22a Exp3_3a Sa. + specialize Imp3_31 with ((P↔(R∨P))∧ + ((R ∨ P) ↔ (R ∨ Q))) ((R∨Q)↔Q) (P↔Q). + intros Imp3_31a. + MP Imp3_31a Sa. + replace (((P↔(R∨P))∧((R ∨ P) ↔ + (R ∨ Q))) ∧ ((R∨Q)↔Q)) with + ((P↔(R∨P))∧(((R ∨ P) ↔ + (R ∨ Q)) ∧ ((R∨Q)↔Q))) in Imp3_31a. + replace ((R ∨ P ↔ R ∨ Q) ∧ (R ∨ Q ↔ Q)) with + ((R ∨ Q ↔ Q) ∧ (R ∨ P ↔ R ∨ Q)) in Imp3_31a. + replace ((P↔(R∨P)) ∧ + ((R ∨ Q ↔ Q) ∧ (R ∨ P ↔ R ∨ Q))) with + (((P↔(R∨P)) ∧ (R ∨ Q ↔ Q)) ∧ + (R ∨ P ↔ R ∨ Q)) in Imp3_31a. + specialize Exp3_3 with + ((P↔(R∨P))∧(R∨Q↔Q)) + (R ∨ P ↔ R ∨ Q) (P ↔ Q). + intros Exp3_3b. + MP Exp3_3b Imp3_31a. + replace (Q↔R∨Q) with (R∨Q↔Q) in Comp3_43a. + Syll Comp3_43a Exp3_3b Sb. + replace (R∨P) with (P∨R) in Sb. + replace (R∨Q) with (Q∨R) in Sb. + specialize Imp3_31 with (¬R) (P∨R↔Q∨R) (P↔Q). + intros Imp3_31b. + MP Imp3_31b Sb. + replace (¬R ∧ (P ∨ R ↔ Q ∨ R)) with + ((P ∨ R ↔ Q ∨ R) ∧ ¬R) in Imp3_31b. + specialize Exp3_3 with + (P ∨ R ↔ Q ∨ R) (¬R) (P ↔ Q). + intros Exp3_3c. + MP Exp3_3c Imp3_31b. + replace (¬R→(P↔Q)) with + (¬¬R∨(P↔Q)) in Exp3_3c. + replace (¬¬R) with R in Exp3_3c. + specialize Add1_3 with P R. + intros Add1_3a. + specialize Add1_3 with Q R. + intros Add1_3b. + Conj Add1_3a Add1_3b. + split. + apply Add1_3a. + apply Add1_3b. + specialize Comp3_43 with (R) (P∨R) (Q∨R). + intros Comp3_43b. + MP Comp3_43b H0. + specialize n5_1 with (P ∨ R) (Q ∨ R). + intros n5_1a. + Syll Comp3_43b n5_1a Sc. + specialize n4_37 with P Q R. + intros n4_37a. + Conj Sc n4_37a. + split. + apply Sc. + apply n4_37a. + specialize n4_77 with (P ∨ R ↔ Q ∨ R) + R (P↔Q). + intros n4_77a. + rewrite Equiv4_01 in n4_77a. + specialize Simp3_26 with + ((R → P ∨ R ↔ Q ∨ R) ∧ + (P ↔ Q → P ∨ R ↔ Q ∨ R) + → R ∨ (P ↔ Q) → P ∨ R ↔ Q ∨ R) + ((R ∨ (P ↔ Q) → P ∨ R ↔ Q ∨ R) + → (R → P ∨ R ↔ Q ∨ R) ∧ + (P ↔ Q → P ∨ R ↔ Q ∨ R)). + intros Simp3_26a. + MP Simp3_26 n4_77a. + MP Simp3_26a H1. + clear n4_77a. clear H1. clear n4_37a. clear Sa. + clear n5_1a. clear Comp3_43b. clear H0. + clear Add1_3a. clear Add1_3b. clear H. clear Imp3_31b. + clear n4_74a. clear n4_74b. clear Comp3_43a. + clear Imp3_31a. clear n4_22a. clear n4_22b. + clear Exp3_3a. clear Exp3_3b. clear Sb. clear Sc. + Conj Exp3_3c Simp3_26a. + split. + apply Exp3_3c. + apply Simp3_26a. + Equiv H. + apply H. + apply Equiv4_01. apply EqBi. - specialize n4_31 with Q R. - intros n4_31a. (*Not cited*) - apply n4_31a. + apply n4_13. (*With R*) + rewrite <- Impl1_01. (*With (¬R) (P↔Q)*) + reflexivity. apply EqBi. - specialize n4_31 with P R. - intros n4_31b. (*Not cited*) - apply n4_31b. + apply n4_3. (*With (R ∨ Q ↔ R ∨ P) (¬R)*) apply EqBi. - specialize n4_13 with R. - intros n4_13a. (*Not cited*) - apply n4_13a. - replace (~~R∨(P↔Q)) with (~R→P↔Q). - reflexivity. - apply Impl1_01. (*Not cited*) + apply n4_31. (*With P R*) apply EqBi. - specialize Transp4_11 with P Q. - intros Transp4_11a. (*Not cited*) - apply Transp4_11a. + apply n4_31. (*With Q R*) apply EqBi. - specialize Transp4_11 with (R ∨ P) (R ∨ Q). - intros Transp4_11a. (*Not cited*) - apply Transp4_11a. - replace (~(R∨Q)) with (~R∧~Q). - reflexivity. + apply n4_21. (*With (P ∨ R) (Q ∨ R)*) apply EqBi. - specialize n4_56 with R Q. - intros n4_56a. (*Not cited*) - apply n4_56a. - replace (~(R∨P)) with (~R∧~P). - reflexivity. + apply n4_32. (*With (P ↔ R ∨ P) (R ∨ Q ↔ Q) (R ∨ P ↔ R ∨ Q)*) apply EqBi. - specialize n4_56 with R P. - intros n4_56b. (*Not cited*) - apply n4_56b. - Qed. - (*The proof sketch was indecipherable, but an - easy proof was available through n5_32.*) + apply n4_3. (*With (R ∨ Q ↔ Q) (R ∨ P ↔ R ∨ Q)*) + apply EqBi. + apply n4_21. (*To commute the biconditional.*) + apply n4_32. (*With (P ↔ R ∨ P) (R ∨ P ↔ R ∨ Q) (R ∨ Q ↔ Q)*) +Qed. Theorem n5_71 : ∀ P Q R : Prop, - (Q → ~R) → (((P ∨ Q) ∧ R) ↔ (P ∧ R)). + (Q → ¬R) → (((P ∨ Q) ∧ R) ↔ (P ∧ R)). Proof. intros P Q R. - specialize n4_4 with R P Q. - intros n4_4a. specialize n4_62 with Q R. intros n4_62a. specialize n4_51 with Q R. intros n4_51a. - replace (~Q∨~R) with (~(Q∧R)) in n4_62a. - replace ((Q→~R)↔~(Q∧R)) with - (((Q→~R)→~(Q∧R)) - ∧ - (~(Q∧R)→(Q→~R))) in n4_62a. + specialize n4_21 with (¬(Q∧R)) (¬Q∨¬R). + intros n4_21a. + rewrite Equiv4_01 in n4_21a. specialize Simp3_26 with - ((Q→~R)→~(Q∧R)) (~(Q∧R)→(Q→~R)). + ((¬(Q∧R)↔(¬Q∨¬R))→((¬Q∨¬R)↔¬(Q∧R))) + (((¬Q∨¬R)↔¬(Q∧R))→(¬(Q∧R)↔(¬Q∨¬R))). intros Simp3_26a. - MP Simp3_26a n4_62a. + MP Simp3_26a n4_21a. + MP Simp3_26a n4_51a. + clear n4_21a. clear n4_51a. + Conj n4_62a Simp3_26a. + split. + apply n4_62a. + apply Simp3_26a. + specialize n4_22 with + (Q→¬R) (¬Q∨¬R) (¬(Q∧R)). + intros n4_22a. + MP n4_22a H. + replace ((Q→¬R)↔¬(Q∧R)) with + (((Q→¬R)→¬(Q∧R)) + ∧ + (¬(Q∧R)→(Q→¬R))) in n4_22a. + specialize Simp3_26 with + ((Q→¬R)→¬(Q∧R)) (¬(Q∧R)→(Q→¬R)). + intros Simp3_26b. + MP Simp3_26b n4_22a. specialize n4_74 with (Q∧R) (P∧R). intros n4_74a. Syll Simp3_26a n4_74a Sa. - replace (R∧P) with (P∧R) in n4_4a. - replace (R∧Q) with (Q∧R) in n4_4a. replace ((P∧R)∨(Q∧R)) with - ((Q∧R)∨(P∧R)) in n4_4a. + ((Q∧R)∨(P∧R)) in Sa. replace ((Q∧R)∨(P∧R)) with (R∧(P∨Q)) in Sa. replace (R∧(P∨Q)) with ((P∨Q)∧R) in Sa. replace ((P∧R)↔((P∨Q)∧R)) with @@ -4473,22 +4559,29 @@ Theorem n5_71 : ∀ P Q R : Prop, intros n4_3a. apply n4_3a. (*Not cited*) apply EqBi. + specialize n4_4 with R P Q. + intros n4_4a. + replace ((Q∧R)∨(P∧R)) with ((P∧R)∨(Q∧R)). + replace (Q ∧ R) with (R ∧ Q). + replace (P ∧ R) with (R ∧ P). apply n4_4a. (*Not cited*) apply EqBi. - specialize n4_31 with (Q∧R) (P∧R). - intros n4_31a. (*Not cited*) - apply n4_31a. - apply EqBi. - specialize n4_3 with Q R. - intros n4_3a. (*Not cited*) + specialize n4_3 with R P. + intros n4_3a. apply n4_3a. apply EqBi. - specialize n4_3 with P R. - intros n4_3b. (*Not cited*) + specialize n4_3 with R Q. + intros n4_3b. apply n4_3b. - apply Equiv4_01. apply EqBi. - apply n4_51a. + specialize n4_31 with (P∧R) (Q∧R). + intros n4_31a. (*Not cited*) + apply n4_31a. + apply EqBi. + specialize n4_31 with (Q∧R) (P∧R). + intros n4_31b. (*Not cited*) + apply n4_31b. + apply Equiv4_01. Qed. Theorem n5_74 : ∀ P Q R : Prop, @@ -4507,8 +4600,8 @@ Theorem n5_74 : ∀ P Q R : Prop, (P→Q→R) (P→R→Q). intros n4_38a. MP n4_38a H. - replace (((P→Q)→(P→R))∧((P→R)→(P→Q))) with - ((P→Q)↔(P→R)) in n4_38a. + replace (((P→Q)→(P→R))∧((P→R)→(P→Q))) + with ((P→Q)↔(P→R)) in n4_38a. specialize n4_76 with P (Q→R) (R→Q). intros n4_76a. replace ((Q→R)∧(R→Q)) with (Q↔R) in n4_76a. @@ -4518,7 +4611,8 @@ Theorem n5_74 : ∀ P Q R : Prop, ((P→(Q↔R))↔((P→Q)↔(P→R))) in n4_38a. apply n4_38a. apply EqBi. - specialize n4_21 with (P→Q↔R) ((P→Q)↔(P→R)). + specialize n4_21 with (P→Q↔R) + ((P→Q)↔(P→R)). intros n4_21a. (*Not cited*) apply n4_21a. replace (P→Q↔R) with ((P→Q→R)∧(P→R→Q)). @@ -4530,27 +4624,30 @@ Theorem n5_74 : ∀ P Q R : Prop, Qed. Theorem n5_75 : ∀ P Q R : Prop, - ((R → ~Q) ∧ (P ↔ Q ∨ R)) → ((P ∧ ~Q) ↔ R). + ((R → ¬Q) ∧ (P ↔ Q ∨ R)) → ((P ∧ ¬Q) ↔ R). Proof. intros P Q R. specialize n5_6 with P Q R. intros n5_6a. - replace ((P∧~Q→R)↔(P→Q∨R)) with - (((P∧~Q→R)→(P→Q∨R)) - ∧ - ((P→Q∨R)→(P∧~Q→R))) in n5_6a. + replace ((P∧¬Q→R)↔(P→Q∨R)) with + (((P∧¬Q→R)→(P→Q∨R)) ∧ + ((P→Q∨R)→(P∧¬Q→R))) in n5_6a. specialize Simp3_27 with - ((P∧~Q→R)→(P→Q∨R)) ((P→Q∨R)→(P∧~Q→R)). + ((P∧¬Q→R)→(P→Q∨R)) + ((P→Q∨R)→(P∧¬Q→R)). intros Simp3_27a. MP Simp3_27a n5_6a. - specialize Simp3_26 with (P→(Q∨R)) ((Q∨R)→P). + specialize Simp3_26 with + (P→(Q∨R)) ((Q∨R)→P). intros Simp3_26a. replace ((P→(Q∨R))∧((Q∨R)→P)) with (P↔(Q∨R)) in Simp3_26a. Syll Simp3_26a Simp3_27a Sa. - specialize Simp3_27 with (R→~Q) (P↔(Q∨R)). + specialize Simp3_27 with + (R→¬Q) (P↔(Q∨R)). intros Simp3_27b. Syll Simp3_27b Sa Sb. - specialize Simp3_27 with (P→(Q∨R)) ((Q∨R)→P). + specialize Simp3_27 with + (P→(Q∨R)) ((Q∨R)→P). intros Simp3_27c. replace ((P→(Q∨R))∧((Q∨R)→P)) with (P↔(Q∨R)) in Simp3_27c. @@ -4561,33 +4658,36 @@ Theorem n5_75 : ∀ P Q R : Prop, specialize Simp3_27 with (Q→P) (R→P). intros Simp3_27d. Syll Sa Simp3_27d Sd. - specialize Simp3_26 with (R→~Q) (P↔(Q∨R)). + specialize Simp3_26 with (R→¬Q) (P↔(Q∨R)). intros Simp3_26b. Conj Sd Simp3_26b. split. apply Sd. apply Simp3_26b. specialize Comp3_43 with - ((R→~Q)∧(P↔(Q∨R))) (R→P) (R→~Q). + ((R→¬Q)∧(P↔(Q∨R))) (R→P) (R→¬Q). intros Comp3_43a. MP Comp3_43a H. - specialize Comp3_43 with R P (~Q). + specialize Comp3_43 with R P (¬Q). intros Comp3_43b. Syll Comp3_43a Comp3_43b Se. - clear n5_6a. clear Simp3_27a. clear Simp3_27b. - clear Simp3_27c. clear Simp3_27d. clear Simp3_26a. - clear Simp3_26b. clear Comp3_43a. clear Comp3_43b. - clear Sa. clear Sc. clear Sd. clear H. clear n4_77a. + clear n5_6a. clear Simp3_27a. + clear Simp3_27c. clear Simp3_27d. + clear Simp3_26a. clear Comp3_43b. + clear Simp3_26b. clear Comp3_43a. + clear Sa. clear Sc. clear Sd. clear H. + clear n4_77a. clear Simp3_27b. Conj Sb Se. split. apply Sb. apply Se. specialize Comp3_43 with - ((R→~Q)∧(P↔Q∨R)) (P∧~Q→R) (R→P∧~Q). + ((R→¬Q)∧(P↔Q∨R)) + (P∧¬Q→R) (R→P∧¬Q). intros Comp3_43c. MP Comp3_43c H. - replace ((P∧~Q→R)∧(R→P∧~Q)) with - (P∧~Q↔R) in Comp3_43c. + replace ((P∧¬Q→R)∧(R→P∧¬Q)) with + (P∧¬Q↔R) in Comp3_43c. apply Comp3_43c. apply Equiv4_01. apply EqBi. |