Principia Mathematica Data PROGRAM BY Dan J. O'Leary Copyright (c) 1982 Daniel J. O'Leary Re-entered with changes by Dennis J. Darland Copyright (C) 2017 Dennis J. Darland This file is part of Dan J. O'Leary's proof checker for PM It is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. It is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with it. If not, see . PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.01 12/29/2017 15:50:08 *1.01 Cpq=ANpq Df. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.1 12/29/2017 15:50:08 *1.1 Anything implied by a true elementary proposition is true. Pp. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.11 12/29/2017 15:50:08 *1.11 When Ux can be asserted, where x is a real variable, and CUxVx can be asserted, where x is a real variablr, then Vx can be asserted, where x is a real variable. Pp. Since I do not have access to Greek letters I have let U stand in for phi and V stand in for psi here, and subsequently. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.2 12/29/2017 15:50:08 *1.2 CAppp Pp. (Taut) PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.3 12/29/2017 15:50:08 *1.3 CqApq Pp. (Add) PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.4 12/29/2017 15:50:08 *1.4 CApqAqp Pp. (Perm) PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.4.1 12/29/2017 15:50:08 *1.4.1 CCApqArqCApqAqr PROOF ABBREVIATION *1.4.1+Prop PROOF 1 CCApqArqCApqAqr *1.4.1 This is here to make *3.48 work. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.4.2 12/29/2017 15:50:08 *1.4.2 CCAqrAsrCAqrArs PROOF ABBREVIATION *1.4.2+Prop PROOF 1 CCAqrAsrCAqrArs *1.4.2 This is here to make *3.48 work. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.5 12/29/2017 15:50:08 *1.5 CApAqrAqApr Pp. (Assoc) PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.6 12/29/2017 15:50:08 *1.6 CCqrCApqApr Pp. (Sum) PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.7 12/29/2017 15:50:08 *1.7 If p is an elementary proposition, then Np is an elementary proposition. Pp. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.71 12/29/2017 15:50:08 *1.71 If p and q are elementary propositions, Apq is an elementary proposition. Pp. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *1.72 12/29/2017 15:50:08 *1.72 If Up and Vp are elementary propositional functions which take elementary propositions as arguments, AUpVp is an elementary propositional function. Pp. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.01 12/29/2017 15:50:08 *2.01 CCpNpNp (Abs) PROOF ABBREVIATION *1.2 p/Np+(1) (1)+*1.01 q/Np;*2.01 PROOF 1 CAppp *1.2 (Taut) p/Np (1) 2 CANpNpNp SUB Cpq=ANpq Df. *1.01 q/Np CpNp=ANpNp Df. 3 CCpNpNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.02 12/29/2017 15:50:08 *2.02 CqCpq (Simp) PROOF ABBREVIATION *1.3 p/Np+(1) (1)+*1.01;*2.02 PROOF 1 CqApq *1.3 (Add) p/Np (1) 2 CqANpq SUB Cpq=ANpq Df. *1.01 3 CqCpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.03 12/29/2017 15:50:08 *2.03 CCpNqCqNp (Transp) PROOF ABBREVIATION *1.4 p/Np, q/Nq+(1) (1)+*1.01 q/Nq;*1.01 p/q, q/Np;*2.03 PROOF 1 CApqAqp *1.4 (Perm) p/Np, q/Nq (1) 2 CANpNqANqNp SUB Cpq=ANpq Df. *1.01 q/Nq CpNq=ANpNq Df. 3 CCpNqANqNp REP Cpq=ANpq Df. *1.01 p/q, q/Np CqNp=ANqNp Df. 4 CCpNqCqNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.04 12/29/2017 15:50:08 *2.04 CCpCqrCqCpr (Comm) PROOF ABBREVIATION *1.5 p/Np, q/Nq+(1) (1)+*1.01 p/q, q/r;*1.01 q/Cqr;*1.01 q/r;*1.01 p/q, q/Cpr;*2.04 PROOF 1 CApAqrAqApr *1.5 (Assoc) p/Np, q/Nq (1) 2 CANpANqrANqANpr SUB Cpq=ANpq Df. *1.01 p/q, q/r Cqr=ANqr Df. 3 CANpCqrANqANpr REP Cpq=ANpq Df. *1.01 q/Cqr CpCqr=ANpCqr Df. 4 CCpCqrANqANpr REP Cpq=ANpq Df. *1.01 q/r Cpr=ANpr Df. 5 CCpCqrANqCpr REP Cpq=ANpq Df. *1.01 p/q, q/Cpr CqCpr=ANqCpr Df. 6 CCpCqrCqCpr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.05 12/29/2017 15:50:08 *2.05 CCqrCCpqCpr (Syll) PROOF ABBREVIATION *1.6 p/Np+(1) (1)+*1.01;*1.01 q/r;*2.05 PROOF 1 CCqrCApqApr *1.6 (Sum) p/Np (1) 2 CCqrCANpqANpr SUB Cpq=ANpq Df. *1.01 3 CCqrCCpqANpr REP Cpq=ANpq Df. *1.01 q/r Cpr=ANpr Df. 4 CCqrCCpqCpr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.06 12/29/2017 15:50:08 *2.06 CCpqCCqrCpr (Syll) PROOF ABBREVIATION *2.04 p/Cqr, q/Cpq, r/Cpr+(1) *2.05+(2) (1)+C(2)-*2.06 PROOF 1 CCpCqrCqCpr *2.04 (Comm) p/Cqr, q/Cpq, r/Cpr (1) 2 CCCqrCCpqCprCCpqCCqrCpr SUB (2) 3 CCqrCCpqCpr *2.05 (Syll) 4 CCpqCCqrCpr MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.07 12/29/2017 15:50:08 *2.07 CpApp PROOF ABBREVIATION *1.3 q/p+*2.07 PROOF 1 CqApq *1.3 (Add) q/p 2 CpApp SUB This introduces a typographical convention which is explained in PM following the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.08 12/29/2017 15:50:08 *2.08 Cpp (Id) PROOF ABBREVIATION *2.05 q/App, r/p+(1) *1.2+(2) (1)+C(2)-(3) *2.07+(4) (3)+C(4)-*2.08 PROOF 1 CCqrCCpqCpr *2.05 (Syll) q/App, r/p (1) 2 CCApppCCpAppCpp SUB (2) 3 CAppp *1.2 (Taut) (3) 4 CCpAppCpp MP: 2, 3 (4) 5 CpApp *2.07 6 Cpp MP: 4, 5 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.1 12/29/2017 15:50:08 *2.1 ANpp PROOF ABBREVIATION *2.08+*1.01 q/p;*2.1 PROOF 1 Cpp *2.08 (Id) Cpq=ANpq Df. *1.01 q/p Cpp=ANpp Df. 2 ANpp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.11 12/29/2017 15:50:08 *2.11 ApNp PROOF ABBREVIATION *1.4 p/Np, q/p+(1) (1)+C*2.1-*2.11 PROOF 1 CApqAqp *1.4 (Perm) p/Np, q/p (1) 2 CANppApNp SUB 3 ANpp *2.1 4 ApNp MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.12 12/29/2017 15:50:08 *2.12 CpNNp PROOF ABBREVIATION *2.11 p/Np+(1) (1)+*1.01 q/NNp;*2.12 PROOF 1 ApNp *2.11 p/Np (1) 2 ANpNNp SUB Cpq=ANpq Df. *1.01 q/NNp CpNNp=ANpNNp Df. 3 CpNNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.13 12/29/2017 15:50:08 *2.13 ApNNNp PROOF ABBREVIATION *1.6 q/Np, r/NNNp+(1) *2.12 p/Np+(2) (1)+C(2)-(3) (3)+C*2.11-*2.13 PROOF 1 CCqrCApqApr *1.6 (Sum) q/Np, r/NNNp (1) 2 CCNpNNNpCApNpApNNNp SUB 3 CpNNp *2.12 p/Np (2) 4 CNpNNNp SUB (3) 5 CApNpApNNNp MP: 2, 4 6 ApNp *2.11 7 ApNNNp MP: 5, 6 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.14 12/29/2017 15:50:08 *2.14 CNNpp PROOF ABBREVIATION *1.4 q/NNNp+(1) (1)+C*2.13-(2) (2)+*1.01 p/NNp, q/p;*2.14 PROOF 1 CApqAqp *1.4 (Perm) q/NNNp (1) 2 CApNNNpANNNpp SUB 3 ApNNNp *2.13 (2) 4 ANNNpp MP: 2, 3 Cpq=ANpq Df. *1.01 p/NNp, q/p CNNpp=ANNNpp Df. 5 CNNpp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.15 12/29/2017 15:50:08 *2.15 CCNpqCNqp PROOF ABBREVIATION *2.05 p/Np, r/NNq+(1) *2.12 p/q+(2) (1)+C(2)-(3) *2.03 p/Np, q/Nq+(4) *2.05 p/Nq, q/NNp, r/p+(5) (5)+C*2.14-(6) *2.05 p/CNpq, q/CNpNNq, r/CNqNNp+(7) (7)+C(4)-(8) (8)+C(3)-(9) *2.05 p/CNpq, q/CNqNNp, r/CNqp+(10) (10)+C(6)-(11) (11)+C(9)-*2.15 PROOF 1 CCqrCCpqCpr *2.05 (Syll) p/Np, r/NNq (1) 2 CCqNNqCCNpqCNpNNq SUB 3 CpNNp *2.12 p/q (2) 4 CqNNq SUB (3) 5 CCNpqCNpNNq MP: 2, 4 6 CCpNqCqNp *2.03 (Transp) p/Np, q/Nq (4) 7 CCNpNNqCNqNNp SUB 8 CCqrCCpqCpr *2.05 (Syll) p/Nq, q/NNp, r/p (5) 9 CCNNppCCNqNNpCNqp SUB 10 CNNpp *2.14 (6) 11 CCNqNNpCNqp MP: 9, 10 12 CCqrCCpqCpr *2.05 (Syll) p/CNpq, q/CNpNNq, r/CNqNNp (7) 13 CCCNpNNqCNqNNpCCCNpqCNpNNqCCNpqCNqNNp SUB (8) 14 CCCNpqCNpNNqCCNpqCNqNNp MP: 13, 7 (9) 15 CCNpqCNqNNp MP: 14, 5 16 CCqrCCpqCpr *2.05 (Syll) p/CNpq, q/CNqNNp, r/CNqp (10) 17 CCCNqNNpCNqpCCCNpqCNqNNpCCNpqCNqp SUB (11) 18 CCCNpqCNqNNpCCNpqCNqp MP: 17, 11 19 CCNpqCNqp MP: 18, 15 The note on the proof of *2.15 introduces a new demonstration paradigm. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.16 12/29/2017 15:50:08 *2.16 CCpqCNqNp PROOF ABBREVIATION *2.05 r/NNq+C*2.12 p/q-(1) *2.03 q/Nq+(2) *2.06 p/Cpq, q/CpNNq, r/CNqNp+C(1)-C(2)-Prop PROOF 1 CCqrCCpqCpr *2.05 (Syll) r/NNq 2 CCqNNqCCpqCpNNq SUB 3 CpNNp *2.12 p/q 4 CqNNq SUB (1) 5 CCpqCpNNq MP: 2, 4 6 CCpNqCqNp *2.03 (Transp) q/Nq (2) 7 CCpNNqCNqNp SUB 8 CCpqCCqrCpr *2.06 (Syll) p/Cpq, q/CpNNq, r/CNqNp 9 CCCpqCpNNqCCCpNNqCNqNpCCpqCNqNp SUB 10 CCCpNNqCNqNpCCpqCNqNp MP: 9, 5 11 CCpqCNqNp MP: 10, 7 This is the first use of Syll as a typographical convention. Syll in square brackets is applied to (1) and (2). PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.17 12/29/2017 15:50:08 *2.17 CCNqNpCpq (Transp) PROOF ABBREVIATION *2.03 p/Nq, q/p+(1) *2.05 q/NNq, r/q+C*2.14 p/q-(2) *2.06 p/CNqNp, q/CpNNq, r/Cpq+C(1)-C(2)-Prop PROOF 1 CCpNqCqNp *2.03 (Transp) p/Nq, q/p (1) 2 CCNqNpCpNNq SUB 3 CCqrCCpqCpr *2.05 (Syll) q/NNq, r/q 4 CCNNqqCCpNNqCpq SUB 5 CNNpp *2.14 p/q 6 CNNqq SUB (2) 7 CCpNNqCpq MP: 4, 6 8 CCpqCCqrCpr *2.06 (Syll) p/CNqNp, q/CpNNq, r/Cpq 9 CCCNqNpCpNNqCCCpNNqCpqCCNqNpCpq SUB 10 CCCpNNqCpqCCNqNpCpq MP: 9, 2 11 CCNqNpCpq MP: 10, 7 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.18 12/29/2017 15:50:08 *2.18 CCNppp PROOF ABBREVIATION *2.05 p/Np, q/p, r/NNp+C*2.12-(1) *2.01 p/Np+(2) *2.06 p/CNpp, q/CNpNNp, r/NNp+C(1)-C(2)-C(2)-(3) *2.14+(4) *2.06 p/CNpp, q/NNp, r/p+C(3)-C(4)-Prop PROOF 1 CCqrCCpqCpr *2.05 (Syll) p/Np, q/p, r/NNp 2 CCpNNpCCNppCNpNNp SUB 3 CpNNp *2.12 (1) 4 CCNppCNpNNp MP: 2, 3 5 CCpNpNp *2.01 (Abs) p/Np (2) 6 CCNpNNpNNp SUB 7 CCpqCCqrCpr *2.06 (Syll) p/CNpp, q/CNpNNp, r/NNp 8 CCCNppCNpNNpCCCNpNNpNNpCCNppNNp SUB 9 CCCNpNNpNNpCCNppNNp MP: 8, 4 10 CCNppNNp MP: 9, 6 (3) 11 CCNppNNp MP: 9, 6 (4) 12 CNNpp *2.14 13 CCpqCCqrCpr *2.06 (Syll) p/CNpp, q/NNp, r/p 14 CCCNppNNpCCNNppCCNppp SUB 15 CCNNppCCNppp MP: 14, 11 16 CCNppp MP: 15, 12 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.2 12/29/2017 15:50:08 *2.2 CpApq PROOF ABBREVIATION *1.3 p/q, q/p+(1) *1.4 p/q, q/p+(2) *2.06 q/Aqp, r/Apq+C(1)-C(2)-Prop PROOF 1 CqApq *1.3 (Add) p/q, q/p (1) 2 CpAqp SUB 3 CApqAqp *1.4 (Perm) p/q, q/p (2) 4 CAqpApq SUB 5 CCpqCCqrCpr *2.06 (Syll) q/Aqp, r/Apq 6 CCpAqpCCAqpApqCpApq SUB 7 CCAqpApqCpApq MP: 6, 2 8 CpApq MP: 7, 4 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.21 12/29/2017 15:50:08 *2.21 CNpCpq PROOF ABBREVIATION *2.2 p/Np+*1.01;Prop PROOF 1 CpApq *2.2 p/Np 2 CNpANpq SUB Cpq=ANpq Df. *1.01 3 CNpCpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.24 12/29/2017 15:50:08 *2.24 CpCNpq PROOF ABBREVIATION *2.04 p/Np, q/p, r/q+C*2.21-Prop PROOF 1 CCpCqrCqCpr *2.04 (Comm) p/Np, q/p, r/q 2 CCNpCpqCpCNpq SUB 3 CNpCpq *2.21 4 CpCNpq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.25 12/29/2017 15:50:08 *2.25 ApCApqq PROOF ABBREVIATION *1.5 p/NApq, q/p, r/q+C*2.1 p/Apq-*1.01 p/Apq;Prop PROOF 1 CApAqrAqApr *1.5 (Assoc) p/NApq, q/p, r/q 2 CANApqApqApANApqq SUB 3 ANpp *2.1 p/Apq 4 ANApqApq SUB 5 ApANApqq MP: 2, 4 Cpq=ANpq Df. *1.01 p/Apq CApqq=ANApqq Df. 6 ApCApqq REP This introduces a proof paradigm. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.26 12/29/2017 15:50:08 *2.26 ANpCCpqq PROOF ABBREVIATION *2.25 p/Np+*1.01;Prop PROOF 1 ApCApqq *2.25 p/Np 2 ANpCANpqq SUB Cpq=ANpq Df. *1.01 3 ANpCCpqq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.27 12/29/2017 15:50:08 *2.27 CpCCpqq PROOF ABBREVIATION *2.26+*1.01 q/CCpqq;Prop PROOF 1 ANpCCpqq *2.26 Cpq=ANpq Df. *1.01 q/CCpqq CpCCpqq=ANpCCpqq Df. 2 CpCCpqq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.3 12/29/2017 15:50:08 *2.3 CApAqrApArq PROOF ABBREVIATION *1.6 q/Aqr, r/Arq+C*1.4 p/q, q/r-Prop PROOF 1 CCqrCApqApr *1.6 (Sum) q/Aqr, r/Arq 2 CCAqrArqCApAqrApArq SUB 3 CApqAqp *1.4 (Perm) p/q, q/r 4 CAqrArq SUB 5 CApAqrApArq MP: 2, 4 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.31 12/29/2017 15:50:08 *2.31 CApAqrAApqr PROOF ABBREVIATION *2.06 p/ApAqr, q/ApArq, r/ArApq+(1) *2.3+(2) (1)+C(2)-(3) *1.5 q/r, r/q+(4) (3)+C(4)-(5) *2.06 p/ApAqr, q/ArApq, r/AApqr+(6) (6)+C(5)-(7) *1.4 p/r, q/Apq+(8) (7)+C(8)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/ApAqr, q/ApArq, r/ArApq (1) 2 CCApAqrApArqCCApArqArApqCApAqrArApq SUB (2) 3 CApAqrApArq *2.3 (3) 4 CCApArqArApqCApAqrArApq MP: 2, 3 5 CApAqrAqApr *1.5 (Assoc) q/r, r/q (4) 6 CApArqArApq SUB (5) 7 CApAqrArApq MP: 4, 6 8 CCpqCCqrCpr *2.06 (Syll) p/ApAqr, q/ArApq, r/AApqr (6) 9 CCApAqrArApqCCArApqAApqrCApAqrAApqr SUB (7) 10 CCArApqAApqrCApAqrAApqr MP: 9, 7 11 CApqAqp *1.4 (Perm) p/r, q/Apq (8) 12 CArApqAApqr SUB 13 CApAqrAApqr MP: 10, 12 The proof paradigm in the remark would be written as follows in the present notation: *2.06 p/a, q/b, r/c+(1) THM+(2) (1)+C(2)-(3) THM+(4) (3)+C(4)-(5) *2.06 p/a, q/c, r/d+(6) (6)+C(5)-(7) THM+(8) (7)+C(8)-Prop. Where THM is some previously proved theorem or a substitution instance of some previously proved theorem. Prop is the proposition to be proved. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.32 12/29/2017 15:50:08 *2.32 CAApqrApAqr PROOF ABBREVIATION *2.06 p/AApqr, q/ArApq, r/ApArq+(1) *1.4 p/Apq, q/r+(2) (1)+C(2)-(3) *1.5 p/r, q/p, r/q+(4) (3)+C(4)-(5) *2.06 p/AApqr, q/ApArq, r/ApAqr+(6) (6)+C(5)-(7) *2.3 q/r, r/q+(8) (7)+C(8)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/AApqr, q/ArApq, r/ApArq (1) 2 CCAApqrArApqCCArApqApArqCAApqrApArq SUB 3 CApqAqp *1.4 (Perm) p/Apq, q/r (2) 4 CAApqrArApq SUB (3) 5 CCArApqApArqCAApqrApArq MP: 2, 4 6 CApAqrAqApr *1.5 (Assoc) p/r, q/p, r/q (4) 7 CArApqApArq SUB (5) 8 CAApqrApArq MP: 5, 7 9 CCpqCCqrCpr *2.06 (Syll) p/AApqr, q/ApArq, r/ApAqr (6) 10 CCAApqrApArqCCApArqApAqrCAApqrApAqr SUB (7) 11 CCApArqApAqrCAApqrApAqr MP: 10, 8 12 CApAqrApArq *2.3 q/r, r/q (8) 13 CApArqApAqr SUB 14 CAApqrApAqr MP: 11, 13 There are two minor typographical errors in the demonstration. The first and second line should each end with a dot. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.33 12/29/2017 15:50:08 *2.33 REDUNDANT Pp. This definition is redundant in the notation system used here. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.36 12/29/2017 15:50:08 *2.36 CCqrCApqArp PROOF ABBREVIATION *2.05 p/Apq, q/Apr, r/Arp+C*1.4 q/r-(1) *1.6+(2) *2.05 p/Cqr, q/CApqApr, r/CApqArp+C(1)-C(2)-Prop PROOF 1 CCqrCCpqCpr *2.05 (Syll) p/Apq, q/Apr, r/Arp 2 CCAprArpCCApqAprCApqArp SUB 3 CApqAqp *1.4 (Perm) q/r 4 CAprArp SUB (1) 5 CCApqAprCApqArp MP: 2, 4 (2) 6 CCqrCApqApr *1.6 (Sum) 7 CCqrCCpqCpr *2.05 (Syll) p/Cqr, q/CApqApr, r/CApqArp 8 CCCApqAprCApqArpCCCqrCApqAprCCqrCApqArp SUB 9 CCCqrCApqAprCCqrCApqArp MP: 8, 5 10 CCqrCApqArp MP: 9, 6 This should also be called SUM. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.37 12/29/2017 15:50:08 *2.37 CCqrCAqpApr PROOF ABBREVIATION *2.06 p/Aqp, q/Apq, r/Apr+C*1.4 p/q, q/p-(1) *1.6+(2) *2.05 p/Cqr, q/CApqApr, r/CAqpApr+C(1)-C(2)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/Aqp, q/Apq, r/Apr 2 CCAqpApqCCApqAprCAqpApr SUB 3 CApqAqp *1.4 (Perm) p/q, q/p 4 CAqpApq SUB (1) 5 CCApqAprCAqpApr MP: 2, 4 (2) 6 CCqrCApqApr *1.6 (Sum) 7 CCqrCCpqCpr *2.05 (Syll) p/Cqr, q/CApqApr, r/CAqpApr 8 CCCApqAprCAqpAprCCCqrCApqAprCCqrCAqpApr SUB 9 CCCqrCApqAprCCqrCAqpApr MP: 8, 5 10 CCqrCAqpApr MP: 9, 6 This should also be called SUM. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.38 12/29/2017 15:50:08 *2.38 CCqrCAqpArp PROOF ABBREVIATION *2.05 p/Aqp, q/Apr, r/Arp+C*1.4 q/r-(1) *1.6+SE(*1.4:*1.4 p/q, q/p);(2) *2.05 p/Cqr, q/CAqpApr, r/CAqpArp+C(1)-C(2)-Prop PROOF 1 CCqrCCpqCpr *2.05 (Syll) p/Aqp, q/Apr, r/Arp 2 CCAprArpCCAqpAprCAqpArp SUB 3 CApqAqp *1.4 (Perm) q/r 4 CAprArp SUB (1) 5 CCAqpAprCAqpArp MP: 2, 4 6 CCqrCApqApr *1.6 (Sum) CApqAqp *1.4 : CApqAqp *1.4 : p/q, q/p CApqAqp : CAqpApq (2) 7 CCqrCAqpApr SE 8 CCqrCCpqCpr *2.05 (Syll) p/Cqr, q/CAqpApr, r/CAqpArp 9 CCCAqpAprCAqpArpCCCqrCAqpAprCCqrCAqpArp SUB 10 CCCqrCAqpAprCCqrCAqpArp MP: 9, 5 11 CCqrCAqpArp MP: 10, 7 This should be called SUM. This is the first use of the rule SE. Note RE will not work PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.4 12/29/2017 15:50:08 *2.4 CApApqApq PROOF ABBREVIATION *2.06 p/ApApq, q/AAppq, r/Apq+(1) *2.31 q/p, r/q+(2) (1)+C(2)-(3) *2.38 p/q, q/App, r/p+C*1.2-(4) (3)+C(4)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/ApApq, q/AAppq, r/Apq (1) 2 CCApApqAAppqCCAAppqApqCApApqApq SUB 3 CApAqrAApqr *2.31 q/p, r/q (2) 4 CApApqAAppq SUB (3) 5 CCAAppqApqCApApqApq MP: 2, 4 6 CCqrCAqpArp *2.38 p/q, q/App, r/p 7 CCApppCAAppqApq SUB 8 CAppp *1.2 (Taut) (4) 9 CAAppqApq MP: 7, 8 10 CApApqApq MP: 5, 9 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.41 12/29/2017 15:50:08 *2.41 CAqApqApq PROOF ABBREVIATION *2.06 p/AqApq, q/ApAqq, r/Apq+(1) *1.5 p/q, q/p, r/q+(2) (1)+C(2)-(3) *1.6 q/Aqq, r/q+C*1.2 p/q-(4) (3)+C(4)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/AqApq, q/ApAqq, r/Apq (1) 2 CCAqApqApAqqCCApAqqApqCAqApqApq SUB 3 CApAqrAqApr *1.5 (Assoc) p/q, q/p, r/q (2) 4 CAqApqApAqq SUB (3) 5 CCApAqqApqCAqApqApq MP: 2, 4 6 CCqrCApqApr *1.6 (Sum) q/Aqq, r/q 7 CCAqqqCApAqqApq SUB 8 CAppp *1.2 (Taut) p/q 9 CAqqq SUB (4) 10 CApAqqApq MP: 7, 9 11 CAqApqApq MP: 5, 10 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.42 12/29/2017 15:50:08 *2.42 CANpCpqCpq PROOF ABBREVIATION *2.4 p/Np+*1.01;*1.01;Prop PROOF 1 CApApqApq *2.4 p/Np 2 CANpANpqANpq SUB Cpq=ANpq Df. *1.01 3 CANpCpqANpq REP Cpq=ANpq Df. *1.01 4 CANpCpqCpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.43 12/29/2017 15:50:08 *2.43 CCpCpqCpq PROOF ABBREVIATION *2.42+*1.01 q/Cpq;Prop PROOF 1 CANpCpqCpq *2.42 Cpq=ANpq Df. *1.01 q/Cpq CpCpq=ANpCpq Df. 2 CCpCpqCpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.45 12/29/2017 15:50:08 *2.45 CNApqNp PROOF ABBREVIATION *2.16 q/Apq+C*2.2-Prop PROOF 1 CCpqCNqNp *2.16 q/Apq 2 CCpApqCNApqNp SUB 3 CpApq *2.2 4 CNApqNp MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.46 12/29/2017 15:50:08 *2.46 CNApqNq PROOF ABBREVIATION *2.16 p/q, q/Apq+C*1.3-Prop PROOF 1 CCpqCNqNp *2.16 p/q, q/Apq 2 CCqApqCNApqNq SUB 3 CqApq *1.3 (Add) 4 CNApqNq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.47 12/29/2017 15:50:08 *2.47 CNApqANpq PROOF ABBREVIATION *2.45+(1) *2.2 p/Np+(2) *2.06 p/NApq, q/Np, r/ANpq+C(1)-C(2)-Prop PROOF (1) 1 CNApqNp *2.45 2 CpApq *2.2 p/Np (2) 3 CNpANpq SUB 4 CCpqCCqrCpr *2.06 (Syll) p/NApq, q/Np, r/ANpq 5 CCNApqNpCCNpANpqCNApqANpq SUB 6 CCNpANpqCNApqANpq MP: 5, 1 7 CNApqANpq MP: 6, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.48 12/29/2017 15:50:08 *2.48 CNApqApNq PROOF ABBREVIATION *2.46+(1) *1.3 q/Nq+(2) *2.06 p/NApq, q/Nq, r/ApNq+C(1)-C(2)-Prop PROOF (1) 1 CNApqNq *2.46 2 CqApq *1.3 (Add) q/Nq (2) 3 CNqApNq SUB 4 CCpqCCqrCpr *2.06 (Syll) p/NApq, q/Nq, r/ApNq 5 CCNApqNqCCNqApNqCNApqApNq SUB 6 CCNqApNqCNApqApNq MP: 5, 1 7 CNApqApNq MP: 6, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.49 12/29/2017 15:50:08 *2.49 CNApqANpNq PROOF ABBREVIATION *2.45+(1) *2.2 p/Np, q/Nq+(2) *2.06 p/NApq, q/Np, r/ANpNq+C(1)-C(2)-Prop PROOF (1) 1 CNApqNp *2.45 2 CpApq *2.2 p/Np, q/Nq (2) 3 CNpANpNq SUB 4 CCpqCCqrCpr *2.06 (Syll) p/NApq, q/Np, r/ANpNq 5 CCNApqNpCCNpANpNqCNApqANpNq SUB 6 CCNpANpNqCNApqANpNq MP: 5, 1 7 CNApqANpNq MP: 6, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.5 12/29/2017 15:50:08 *2.5 CNCpqCNpq PROOF ABBREVIATION *2.47 p/Np+*1.01;*1.01 p/Np;Prop PROOF 1 CNApqANpq *2.47 p/Np 2 CNANpqANNpq SUB Cpq=ANpq Df. *1.01 3 CNCpqANNpq REP Cpq=ANpq Df. *1.01 p/Np CNpq=ANNpq Df. 4 CNCpqCNpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.51 12/29/2017 15:50:08 *2.51 CNCpqCpNq PROOF ABBREVIATION *2.48 p/Np+*1.01;*1.01 q/Nq;Prop PROOF 1 CNApqApNq *2.48 p/Np 2 CNANpqANpNq SUB Cpq=ANpq Df. *1.01 3 CNCpqANpNq REP Cpq=ANpq Df. *1.01 q/Nq CpNq=ANpNq Df. 4 CNCpqCpNq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.52 12/29/2017 15:50:08 *2.52 CNCpqCNpNq PROOF ABBREVIATION *2.49 p/Np+*1.01;*1.01 p/Np, q/Nq;Prop PROOF 1 CNApqANpNq *2.49 p/Np 2 CNANpqANNpNq SUB Cpq=ANpq Df. *1.01 3 CNCpqANNpNq REP Cpq=ANpq Df. *1.01 p/Np, q/Nq CNpNq=ANNpNq Df. 4 CNCpqCNpNq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.521 12/29/2017 15:50:08 *2.521 CNCpqCqp PROOF ABBREVIATION *2.52+(1) *2.17 p/q, q/p+(2) *2.06 p/NCpq, q/CNpNq, r/Cqp+C*2.52-C*2.17 p/q, q/p-Prop PROOF (1) 1 CNCpqCNpNq *2.52 2 CCNqNpCpq *2.17 (Transp) p/q, q/p (2) 3 CCNpNqCqp SUB 4 CCpqCCqrCpr *2.06 (Syll) p/NCpq, q/CNpNq, r/Cqp 5 CCNCpqCNpNqCCCNpNqCqpCNCpqCqp SUB 6 CNCpqCNpNq *2.52 7 CCCNpNqCqpCNCpqCqp MP: 5, 6 8 CCNqNpCpq *2.17 (Transp) p/q, q/p 9 CCNpNqCqp SUB 10 CNCpqCqp MP: 7, 9 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.53 12/29/2017 15:50:08 *2.53 CApqCNpq PROOF ABBREVIATION *2.38 p/q, q/p, r/NNp+C*2.12;*1.01 p/Np;Prop PROOF 1 CCqrCAqpArp *2.38 p/q, q/p, r/NNp 2 CCpNNpCApqANNpq SUB 3 CpNNp *2.12 4 CApqANNpq MP: 2, 3 Cpq=ANpq Df. *1.01 p/Np CNpq=ANNpq Df. 5 CApqCNpq REP This shortens the *2.25 paradigm. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.54 12/29/2017 15:50:08 *2.54 CCNpqApq PROOF ABBREVIATION *2.38 p/q, q/NNp, r/p+C*2.14-*1.01 p/Np;Prop PROOF 1 CCqrCAqpArp *2.38 p/q, q/NNp, r/p 2 CCNNppCANNpqApq SUB 3 CNNpp *2.14 4 CANNpqApq MP: 2, 3 Cpq=ANpq Df. *1.01 p/Np CNpq=ANNpq Df. 5 CCNpqApq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.55 12/29/2017 15:50:08 *2.55 CNpCApqq PROOF ABBREVIATION *2.04 p/Apq, q/Np, r/q+C*2.53-Prop PROOF 1 CCpCqrCqCpr *2.04 (Comm) p/Apq, q/Np, r/q 2 CCApqCNpqCNpCApqq SUB 3 CApqCNpq *2.53 4 CNpCApqq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.56 12/29/2017 15:50:08 *2.56 CNqCApqp PROOF ABBREVIATION *2.55 p/q, q/p+SE(*1.4:*1.4 p/q, q/p);Prop PROOF 1 CNpCApqq *2.55 p/q, q/p 2 CNqCAqpp SUB CApqAqp *1.4 : CApqAqp *1.4 : p/q, q/p CApqAqp : CAqpApq 3 CNqCApqp SE I used SE instead of RE as in the book. This proof is the first in which the theorem for SE is listed. It differs from the previous demonstrations in that the element to be commuted is not at the beginning or at the end. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.6 12/29/2017 15:50:08 *2.6 CCNpqCCpqq PROOF ABBREVIATION *2.38 p/q, q/Np, r/q+(1) *2.05 p/ANpq, q/Aqq, r/q+C*1.2 p/q-(2) *2.06 p/CNpq, q/CANpqAqq, r/CANpqq+C(1)-C(2)-*1.01;Prop PROOF 1 CCqrCAqpArp *2.38 p/q, q/Np, r/q (1) 2 CCNpqCANpqAqq SUB 3 CCqrCCpqCpr *2.05 (Syll) p/ANpq, q/Aqq, r/q 4 CCAqqqCCANpqAqqCANpqq SUB 5 CAppp *1.2 (Taut) p/q 6 CAqqq SUB (2) 7 CCANpqAqqCANpqq MP: 4, 6 8 CCpqCCqrCpr *2.06 (Syll) p/CNpq, q/CANpqAqq, r/CANpqq 9 CCCNpqCANpqAqqCCCANpqAqqCANpqqCCNpqCANpqq SUB 10 CCCANpqAqqCANpqqCCNpqCANpqq MP: 9, 2 11 CCNpqCANpqq MP: 10, 7 Cpq=ANpq Df. *1.01 12 CCNpqCCpqq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.61 12/29/2017 15:50:08 *2.61 CCpqCCNpqq PROOF ABBREVIATION *2.04 p/CNpq, q/Cpq, r/q+C*2.6-Prop PROOF 1 CCpCqrCqCpr *2.04 (Comm) p/CNpq, q/Cpq, r/q 2 CCCNpqCCpqqCCpqCCNpqq SUB 3 CCNpqCCpqq *2.6 4 CCpqCCNpqq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.62 12/29/2017 15:50:08 *2.62 CApqCCpqq PROOF ABBREVIATION *2.06 p/Apq, q/CNpq, r/CCpqq+C*2.53-C*2.6-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/Apq, q/CNpq, r/CCpqq 2 CCApqCNpqCCCNpqCCpqqCApqCCpqq SUB 3 CApqCNpq *2.53 4 CCCNpqCCpqqCApqCCpqq MP: 2, 3 5 CCNpqCCpqq *2.6 6 CApqCCpqq MP: 4, 5 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.621 12/29/2017 15:50:08 *2.621 CCpqCApqq PROOF ABBREVIATION *2.04 p/Apq, q/Cpq, r/q+C*2.62-Prop PROOF 1 CCpCqrCqCpr *2.04 (Comm) p/Apq, q/Cpq, r/q 2 CCApqCCpqqCCpqCApqq SUB 3 CApqCCpqq *2.62 4 CCpqCApqq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.63 12/29/2017 15:50:08 *2.63 CApqCANpqq PROOF ABBREVIATION *2.62+*1.01;Prop PROOF 1 CApqCCpqq *2.62 Cpq=ANpq Df. *1.01 2 CApqCANpqq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.64 12/29/2017 15:50:08 *2.64 CApqCApNqp PROOF ABBREVIATION *2.05 p/Apq, q/Aqp, r/CANqpp+C*2.63 p/q, q/p+C*1.4-(#1) (#1);SE(*1.4 p/Nq, q/p:*1.4 q/Nq); Prop PROOF 1 CCqrCCpqCpr *2.05 (Syll) p/Apq, q/Aqp, r/CANqpp 2 CCAqpCANqppCCApqAqpCApqCANqpp SUB 3 CApqCANpqq *2.63 p/q, q/p 4 CAqpCANqpp SUB 5 CCApqAqpCApqCANqpp MP: 2, 4 6 CApqAqp *1.4 (Perm) (#1) 7 CApqCANqpp MP: 5, 6 CApqAqp *1.4 : CApqAqp *1.4 p/Nq, q/p : q/Nq CANqpApNq : CApNqANqp 8 CApqCApNqp SE I used (#1) instead of (1), but I remember why. It probably doesn’t make a difference. I used SE instead of RE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.65 12/29/2017 15:50:08 *2.65 CCpqCCpNqNp PROOF ABBREVIATION *2.64 p/Np+*1.01;*1.01 q/Nq;*2.65 PROOF 1 CApqCApNqp *2.64 p/Np 2 CANpqCANpNqNp SUB Cpq=ANpq Df. *1.01 3 CCpqCANpNqNp REP Cpq=ANpq Df. *1.01 q/Nq CpNq=ANpNq Df. 4 CCpqCCpNqNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.67 12/29/2017 15:50:08 *2.67 CCApqqCpq PROOF ABBREVIATION *2.06 p/CNpq, q/Apq, r/q+C*2.54-(1) *2.06 q/CNpq, r/q+C*2.24-(2) *2.06 p/CApqq, q/CCNpqq, r/Cpq+C(1)-C(2)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/CNpq, q/Apq, r/q 2 CCCNpqApqCCApqqCCNpqq SUB 3 CCNpqApq *2.54 (1) 4 CCApqqCCNpqq MP: 2, 3 5 CCpqCCqrCpr *2.06 (Syll) q/CNpq, r/q 6 CCpCNpqCCCNpqqCpq SUB 7 CpCNpq *2.24 (2) 8 CCCNpqqCpq MP: 6, 7 9 CCpqCCqrCpr *2.06 (Syll) p/CApqq, q/CCNpqq, r/Cpq 10 CCCApqqCCNpqqCCCCNpqqCpqCCApqqCpq SUB 11 CCCCNpqqCpqCCApqqCpq MP: 10, 4 12 CCApqqCpq MP: 11, 8 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.68 12/29/2017 15:50:08 *2.68 CCCpqqApq PROOF ABBREVIATION *2.67 p/Np+*1.01;(1) *2.06 p/CCpqq, q/CNpq, r/Apq-C(1)-C*2.54-Prop PROOF 1 CCApqqCpq *2.67 p/Np 2 CCANpqqCNpq SUB Cpq=ANpq Df. *1.01 (1) 3 CCCpqqCNpq REP 4 CCpqCCqrCpr *2.06 (Syll) p/CCpqq, q/CNpq, r/Apq 5 CCCCpqqCNpqCCCNpqApqCCCpqqApq SUB 6 CCCNpqApqCCCpqqApq MP: 5, 3 7 CCNpqApq *2.54 8 CCCpqqApq MP: 6, 7 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.69 12/29/2017 15:50:08 *2.69 CCCpqqCCqpp PROOF ABBREVIATION *2.06 p/CCpqq, q/Apq, r/Aqp+C*2.68-C*1.4-(1) *2.06 p/CCpqq, q/Aqp, r/CCqpp+C(1)-C*2.62 p/q, q/p-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/CCpqq, q/Apq, r/Aqp 2 CCCCpqqApqCCApqAqpCCCpqqAqp SUB 3 CCCpqqApq *2.68 4 CCApqAqpCCCpqqAqp MP: 2, 3 5 CApqAqp *1.4 (Perm) (1) 6 CCCpqqAqp MP: 4, 5 7 CCpqCCqrCpr *2.06 (Syll) p/CCpqq, q/Aqp, r/CCqpp 8 CCCCpqqAqpCCAqpCCqppCCCpqqCCqpp SUB 9 CCAqpCCqppCCCpqqCCqpp MP: 8, 6 10 CApqCCpqq *2.62 p/q, q/p 11 CAqpCCqpp SUB 12 CCCpqqCCqpp MP: 9, 11 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.73 12/29/2017 15:50:08 *2.73 CCpqCAApqrAqr PROOF ABBREVIATION *2.621+(1) *2.38 p/r, q/Apq, r/q+(2) *2.06 p/Cpq, q/CApqq, r/CAApqrAqr+C*2.621-C*2.38 p/r, q/Apq, r/q-Prop PROOF (1) 1 CCpqCApqq *2.621 2 CCqrCAqpArp *2.38 p/r, q/Apq, r/q (2) 3 CCApqqCAApqrAqr SUB 4 CCpqCCqrCpr *2.06 (Syll) p/Cpq, q/CApqq, r/CAApqrAqr 5 CCCpqCApqqCCCApqqCAApqrAqrCCpqCAApqrAqr SUB 6 CCpqCApqq *2.621 7 CCCApqqCAApqrAqrCCpqCAApqrAqr MP: 5, 6 8 CCqrCAqpArp *2.38 p/r, q/Apq, r/q 9 CCApqqCAApqrAqr SUB 10 CCpqCAApqrAqr MP: 7, 9 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.74 12/29/2017 15:50:08 *2.74 CCqpCAApqrApr PROOF ABBREVIATION *2.73 p/q, q/p+(1) *1.5+SE(*2.31:*2.32);SE(*2.31 p/q, q/p:*2.32 p/q, q/p);(2) *2.06 p/AApqr, q/AAqpr, r/Apr+C(2)-(3) *2.06 p/Cqp, q/CAAqprApr, r/CAApqrApr-C(1)-C(3)-Prop PROOF 1 CCpqCAApqrAqr *2.73 p/q, q/p (1) 2 CCqpCAAqprApr SUB 3 CApAqrAqApr *1.5 (Assoc) CApAqrAApqr *2.31 : CAApqrApAqr *2.32 4 CAApqrAqApr SE CApAqrAApqr *2.31 : CAApqrApAqr *2.32 p/q, q/p : p/q, q/p CAqAprAAqpr : CAAqprAqApr (2) 5 CAApqrAAqpr SE 6 CCpqCCqrCpr *2.06 (Syll) p/AApqr, q/AAqpr, r/Apr 7 CCAApqrAAqprCCAAqprAprCAApqrApr SUB (3) 8 CCAAqprAprCAApqrApr MP: 7, 5 9 CCpqCCqrCpr *2.06 (Syll) p/Cqp, q/CAAqprApr, r/CAApqrApr 10 CCCqpCAAqprAprCCCAAqprAprCAApqrAprCCqpCAApqrApr SUB 11 CCCAAqprAprCAApqrAprCCqpCAApqrApr MP: 10, 2 12 CCqpCAApqrApr MP: 11, 8 Used SE instead of RE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.75 12/29/2017 15:50:08 *2.75 CApqCApCqrApr PROOF ABBREVIATION *2.74 q/Nq+SE(*2.32 q/Nq:*2.31 q/Nq);(1) *2.53 p/q, q/p+(2) *2.05 p/Aqp, q/CNqp, r/CApANqrApr+C(1)-C(2)-(#1) (#1);*1.01 p/q, q/r;SE(*1.4:*1.4 p/q, q/p);Prop PROOF 1 CCqpCAApqrApr *2.74 q/Nq 2 CCNqpCAApNqrApr SUB CAApqrApAqr *2.32 : CApAqrAApqr *2.31 q/Nq : q/Nq CAApNqrApANqr : CApANqrAApNqr (1) 3 CCNqpCApANqrApr SE 4 CApqCNpq *2.53 p/q, q/p (2) 5 CAqpCNqp SUB 6 CCqrCCpqCpr *2.05 (Syll) p/Aqp, q/CNqp, r/CApANqrApr 7 CCCNqpCApANqrAprCCAqpCNqpCAqpCApANqrApr SUB 8 CCAqpCNqpCAqpCApANqrApr MP: 7, 3 (#1) 9 CAqpCApANqrApr MP: 8, 5 Cpq=ANpq Df. *1.01 p/q, q/r Cqr=ANqr Df. 10 CAqpCApCqrApr REP CApqAqp *1.4 : CApqAqp *1.4 : p/q, q/p CApqAqp : CAqpApq 11 CApqCApCqrApr SE Used SE instead of RE The *2.31 called for the use of SE. Note that the use Is in the middle of a line. To properly use SE, one must have the implication going both ways. The demonstration should have called for *2.32 also. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.76 12/29/2017 15:50:08 *2.76 CApCqrCApqApr PROOF ABBREVIATION *2.04 p/Apq, q/ApCqr, r/Apr+C*2.75-Prop PROOF 1 CCpCqrCqCpr *2.04 (Comm) p/Apq, q/ApCqr, r/Apr 2 CCApqCApCqrAprCApCqrCApqApr SUB 3 CApqCApCqrApr *2.75 4 CApCqrCApqApr MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.77 12/29/2017 15:50:08 *2.77 CCpCqrCCpqCpr PROOF ABBREVIATION *2.76 p/Np+*1.01 q/Cqr;*1.01;*1.01 q/r;Prop PROOF 1 CApCqrCApqApr *2.76 p/Np 2 CANpCqrCANpqANpr SUB Cpq=ANpq Df. *1.01 q/Cqr CpCqr=ANpCqr Df. 3 CCpCqrCANpqANpr REP Cpq=ANpq Df. *1.01 4 CCpCqrCCpqANpr REP Cpq=ANpq Df. *1.01 q/r Cpr=ANpr Df. 5 CCpCqrCCpqCpr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.8 12/29/2017 15:50:08 *2.8 CAqrCANrsAqs PROOF ABBREVIATION *2.06 p/Aqr, q/CNrq, r/CANrsAqs+(1) *2.05 p/Aqr, q/Arq, r/CNrq+C*2.53 p/r-C*1.4 p/q, q/r-(2) (1)+C(2)-(3) *2.38 p/s, q/Nr, r/q+(4) (3)+C(4)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/Aqr, q/CNrq, r/CANrsAqs (1) 2 CCAqrCNrqCCCNrqCANrsAqsCAqrCANrsAqs SUB 3 CCqrCCpqCpr *2.05 (Syll) p/Aqr, q/Arq, r/CNrq 4 CCArqCNrqCCAqrArqCAqrCNrq SUB 5 CApqCNpq *2.53 p/r 6 CArqCNrq SUB 7 CCAqrArqCAqrCNrq MP: 4, 6 8 CApqAqp *1.4 (Perm) p/q, q/r 9 CAqrArq SUB (2) 10 CAqrCNrq MP: 7, 9 (3) 11 CCCNrqCANrsAqsCAqrCANrsAqs MP: 2, 10 12 CCqrCAqpArp *2.38 p/s, q/Nr, r/q (4) 13 CCNrqCANrsAqs SUB 14 CAqrCANrsAqs MP: 11, 13 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.81 12/29/2017 15:50:08 *2.81 CCqCrsCApqCAprAps PROOF ABBREVIATION *1.6 r/Crs+(1) *2.05 p/Apq, q/ApCrs, r/CAprAps+C*2.76 q/r, r/s-(2) *2.06 p/CqCrs, q/CApqApCrs, r/CApqCAprAps+C(1)-C(2)-Prop PROOF 1 CCqrCApqApr *1.6 (Sum) r/Crs (1) 2 CCqCrsCApqApCrs SUB 3 CCqrCCpqCpr *2.05 (Syll) p/Apq, q/ApCrs, r/CAprAps 4 CCApCrsCAprApsCCApqApCrsCApqCAprAps SUB 5 CApCqrCApqApr *2.76 q/r, r/s 6 CApCrsCAprAps SUB (2) 7 CCApqApCrsCApqCAprAps MP: 4, 6 8 CCpqCCqrCpr *2.06 (Syll) p/CqCrs, q/CApqApCrs, r/CApqCAprAps 9 CCCqCrsCApqApCrsCCCApqApCrsCApqCAprApsCCqCrsCApqCAprAps SUB 10 CCCApqApCrsCApqCAprApsCCqCrsCApqCAprAps MP: 9, 2 11 CCqCrsCApqCAprAps MP: 10, 7 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.82 12/29/2017 15:50:08 *2.82 CApAqrCApANrsApAqs PROOF ABBREVIATION *2.81 q/Aqr, r/ANrs, s/Aqs+C*2.8-Prop PROOF 1 CCqCrsCApqCAprAps *2.81 q/Aqr, r/ANrs, s/Aqs 2 CCAqrCANrsAqsCApAqrCApANrsApAqs SUB 3 CAqrCANrsAqs *2.8 4 CApAqrCApANrsApAqs MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.83 12/29/2017 15:50:08 *2.83 CCpCqrCCpCrsCpCqs PROOF ABBREVIATION *2.82 p/Np, q/Nq+*1.01 q/ANqr;*1.01 p/q, q/r;*1.01 q/ANrs;(#1) (#1);*1.01 p/r, q/s;*1.01 q/ANqs;*1.01 p/q, q/s;Prop PROOF 1 CApAqrCApANrsApAqs *2.82 p/Np, q/Nq 2 CANpANqrCANpANrsANpANqs SUB Cpq=ANpq Df. *1.01 q/ANqr CpANqr=ANpANqr Df. 3 CCpANqrCANpANrsANpANqs REP Cpq=ANpq Df. *1.01 p/q, q/r Cqr=ANqr Df. 4 CCpCqrCANpANrsANpANqs REP Cpq=ANpq Df. *1.01 q/ANrs CpANrs=ANpANrs Df. (#1) 5 CCpCqrCCpANrsANpANqs REP Cpq=ANpq Df. *1.01 p/r, q/s Crs=ANrs Df. 6 CCpCqrCCpCrsANpANqs REP Cpq=ANpq Df. *1.01 q/ANqs CpANqs=ANpANqs Df. 7 CCpCqrCCpCrsCpANqs REP Cpq=ANpq Df. *1.01 p/q, q/s Cqs=ANqs Df. 8 CCpCqrCCpCrsCpCqs REP This proof is split into two parts because of the length of the proof abbreviation. The split does not occur in PM. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.85.0 12/29/2017 15:50:08 *2.85.0 CCCApqAprCApqrCCApqAprCqr PROOF ABBREVIATION *2.85.0+Prop PROOF 1 CCCApqAprCApqrCCApqAprCqr *2.85.0 This is the troublesome line in *2.85, i.e., the one composed from (1) and *2.83 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.85 12/29/2017 15:50:08 *2.85 CCApqAprApCqr PROOF ABBREVIATION *2.06 p/q, q/Apq+C*1.3-(1) *2.06 p/Np, q/CAprr, r/CCApqAprCApqr+(2.1) *2.55 q/r+(2.2) (2.1)+C(2.2)-(2.3) *2.05 p/Apq, q/Apr+(2.4) (2.3)+C(2.4)-(2.5) *2.06 p/Np, q/CCApqAprCApqr, r/CCApqAprCqr+(2.6) (2.6)+C(2.5)-(2.7) *2.85.0+(2.8) (2.7)+C(2.8)-(2) *2.06 p/CApqApr, q/CNpCqr, r/ApCqr+(3.1) *2.04 p/Np, q/CApqApr, r/Cqr+C(2)-(3.2) (3.1)+C(3.2)-(3.3) *2.54 q/Cqr+(3.4) (3.3)+C(3.4)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/q, q/Apq 2 CCqApqCCApqrCqr SUB 3 CqApq *1.3 (Add) (1) 4 CCApqrCqr MP: 2, 3 5 CCpqCCqrCpr *2.06 (Syll) p/Np, q/CAprr, r/CCApqAprCApqr (2.1) 6 CCNpCAprrCCCAprrCCApqAprCApqrCNpCCApqAprCApqr SUB 7 CNpCApqq *2.55 q/r (2.2) 8 CNpCAprr SUB (2.3) 9 CCCAprrCCApqAprCApqrCNpCCApqAprCApqr MP: 6, 8 10 CCqrCCpqCpr *2.05 (Syll) p/Apq, q/Apr (2.4) 11 CCAprrCCApqAprCApqr SUB (2.5) 12 CNpCCApqAprCApqr MP: 9, 11 13 CCpqCCqrCpr *2.06 (Syll) p/Np, q/CCApqAprCApqr, r/CCApqAprCqr (2.6) 14 CCNpCCApqAprCApqrCCCCApqAprCApqrCCApqAprCqrCNpCCApqAprCqr SUB (2.7) 15 CCCCApqAprCApqrCCApqAprCqrCNpCCApqAprCqr MP: 14, 12 (2.8) 16 CCCApqAprCApqrCCApqAprCqr *2.85.0 (2) 17 CNpCCApqAprCqr MP: 15, 16 18 CCpqCCqrCpr *2.06 (Syll) p/CApqApr, q/CNpCqr, r/ApCqr (3.1) 19 CCCApqAprCNpCqrCCCNpCqrApCqrCCApqAprApCqr SUB 20 CCpCqrCqCpr *2.04 (Comm) p/Np, q/CApqApr, r/Cqr 21 CCNpCCApqAprCqrCCApqAprCNpCqr SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.85(CONT.) (3.2) 22 CCApqAprCNpCqr MP: 21, 17 (3.3) 23 CCCNpCqrApCqrCCApqAprApCqr MP: 19, 22 24 CCNpqApq *2.54 q/Cqr (3.4) 25 CCNpCqrApCqr SUB 26 CCApqAprApCqr MP: 23, 25 Note the use of *2.85.0 There are subparts to each of the above. In particular the subpart of part 2 which is denoted by (1).*2.83 is of particular interest. DJO takes it to mean that *2.83, or some substitution instance, is of the form CPQ where P is equiform with (1). The consequent should be equiform with the result needed at this point in the proof. Following the paradigm of the remark following in *2.31 this is Ccd, or in the instant case CCCApqAprCApqrCCApqAprCqr. The demonstration of this theorem is in error because the desired result cannot be achieved in the indicated manner. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *2.86 12/29/2017 15:50:08 *2.86 CCCpqCprCpCqr PROOF ABBREVIATION *2.85 p/Np+*1.01;*1.01 q/r;*1.01 q/Cqr;*2.86 PROOF 1 CCApqAprApCqr *2.85 p/Np 2 CCANpqANprANpCqr SUB Cpq=ANpq Df. *1.01 3 CCCpqANprANpCqr REP Cpq=ANpq Df. *1.01 q/r Cpr=ANpr Df. 4 CCCpqCprANpCqr REP Cpq=ANpq Df. *1.01 q/Cqr CpCqr=ANpCqr Df. 5 CCCpqCprCpCqr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.01 12/29/2017 15:50:08 *3.01 Kpq=NANpNq Df. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.02 12/29/2017 15:50:08 *3.02 REDUNDANT Pp. This definition is redundant in the notation used here. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.03 12/29/2017 15:50:08 *3.03 KUpVp (Conjunction Rule) PROOF ABBREVIATION ASSUMP Up+(#1) ASSUMP Vp+(#2) *2.11 p/ANUpNVp+(1) *2.32 p/NUp, q/NVp, r/NANUpNVp+C(1);*1.01 p/Vp, q/NANUpNVp;(#3) (#3);*1.01 p/Up, q/CVpNANUpNVp;(2) (2)+*3.01 p/Up, q/Vp;(3) (3)+C(#1)-C(#2)-Prop PROOF (#1) 1 Up ASSUMP (#2) 2 Vp ASSUMP 3 ApNp *2.11 p/ANUpNVp (1) 4 AANUpNVpNANUpNVp SUB 5 CAApqrApAqr *2.32 p/NUp, q/NVp, r/NANUpNVp 6 CAANUpNVpNANUpNVpANUpANVpNANUpNVp SUB 7 ANUpANVpNANUpNVp MP: 6, 4 Cpq=ANpq Df. *1.01 p/Vp, q/NANUpNVp CVpNANUpNVp=ANVpNANUpNVp Df. (#3) 8 ANUpCVpNANUpNVp REP Cpq=ANpq Df. *1.01 p/Up, q/CVpNANUpNVp CUpCVpNANUpNVp=ANUpCVpNANUpNVp Df. (2) 9 CUpCVpNANUpNVp REP Kpq=NANpNq Df. *3.01 p/Up, q/Vp KUpVp=NANUpNVp Df. (3) 10 CUpCVpKUpVp REP 11 CVpKUpVp MP: 10, 1 12 KUpVp MP: 11, 2 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.1 12/29/2017 15:50:08 *3.1 CKpqNANpNq PROOF ABBREVIATION *2.08 p/Kpq+*3.01 II;Prop PROOF 1 Cpp *2.08 (Id) p/Kpq 2 CKpqKpq SUB Kpq=NANpNq Df. *3.01 3 CKpqNANpNq REP II PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.11 12/29/2017 15:50:08 *3.11 CNANpNqKpq PROOF ABBREVIATION *2.08 p/Kpq+*3.01;Prop PROOF 1 Cpp *2.08 (Id) p/Kpq 2 CKpqKpq SUB Kpq=NANpNq Df. *3.01 3 CNANpNqKpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.12 12/29/2017 15:50:08 *3.12 AANpNqKpq PROOF ABBREVIATION *2.11 p/ANpNq+*3.01;Prop PROOF 1 ApNp *2.11 p/ANpNq 2 AANpNqNANpNq SUB Kpq=NANpNq Df. *3.01 3 AANpNqKpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.13 12/29/2017 15:50:08 *3.13 CNKpqANpNq PROOF ABBREVIATION *2.15 p/ANpNq, q/Kpq+C*3.11-Prop PROOF 1 CCNpqCNqp *2.15 p/ANpNq, q/Kpq 2 CCNANpNqKpqCNKpqANpNq SUB 3 CNANpNqKpq *3.11 4 CNKpqANpNq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.14 12/29/2017 15:50:08 *3.14 CANpNqNKpq PROOF ABBREVIATION *2.03 p/Kpq, q/ANpNq+C*3.1-Prop PROOF 1 CCpNqCqNp *2.03 (Transp) p/Kpq, q/ANpNq 2 CCKpqNANpNqCANpNqNKpq SUB 3 CKpqNANpNq *3.1 4 CANpNqNKpq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.2 12/29/2017 15:50:08 *3.2 CpCqKpq PROOF ABBREVIATION *3.12+SE(*2.31 p/Np, q/Nq, r/Kpq:*2.32 p/Np, q/Nq, r/Kpq);(#1) (#1);*1.01 q/ANqKpq;*1.01 p/q, q/Kpq;Prop PROOF 1 AANpNqKpq *3.12 CApAqrAApqr *2.31 : CAApqrApAqr *2.32 p/Np, q/Nq, r/Kpq : p/Np, q/Nq, r/Kpq CANpANqKpqAANpNqKpq : CAANpNqKpqANpANqKpq (#1) 2 ANpANqKpq SE Cpq=ANpq Df. *1.01 q/ANqKpq CpANqKpq=ANpANqKpq Df. 3 CpANqKpq REP Cpq=ANpq Df. *1.01 p/q, q/Kpq CqKpq=ANqKpq Df. 4 CpCqKpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.21 12/29/2017 15:50:08 *3.21 CqCpKpq PROOF ABBREVIATION *2.04 r/Kpq+C*3.2-Prop PROOF 1 CCpCqrCqCpr *2.04 (Comm) r/Kpq 2 CCpCqKpqCqCpKpq SUB 3 CpCqKpq *3.2 4 CqCpKpq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.22 12/29/2017 15:50:08 *3.22 CKpqKqp PROOF ABBREVIATION *2.06 p/NKqp, q/ANqNp, r/ANpNq+(1.1) *3.13 p/q, q/p+(1.2) (1.1)+C(1.2)-(1.3) *1.4 p/Nq, q/Np+(1.4) (1.3)+C(1.4)-(1.5) *2.06 p/NKqp, q/ANpNq, r/NKpq+(1.6) (1.6)+C(1.5)-(1.7) *3.14+(1.8) (1.7)+C(1.8)-(1) *2.17 p/Kpq, q/Kqp+C(1)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/NKqp, q/ANqNp, r/ANpNq (1.1) 2 CCNKqpANqNpCCANqNpANpNqCNKqpANpNq SUB 3 CNKpqANpNq *3.13 p/q, q/p (1.2) 4 CNKqpANqNp SUB (1.3) 5 CCANqNpANpNqCNKqpANpNq MP: 2, 4 6 CApqAqp *1.4 (Perm) p/Nq, q/Np (1.4) 7 CANqNpANpNq SUB (1.5) 8 CNKqpANpNq MP: 5, 7 9 CCpqCCqrCpr *2.06 (Syll) p/NKqp, q/ANpNq, r/NKpq (1.6) 10 CCNKqpANpNqCCANpNqNKpqCNKqpNKpq SUB (1.7) 11 CCANpNqNKpqCNKqpNKpq MP: 10, 8 (1.8) 12 CANpNqNKpq *3.14 (1) 13 CNKqpNKpq MP: 11, 12 14 CCNqNpCpq *2.17 (Transp) p/Kpq, q/Kqp 15 CCNKqpNKpqCKpqKqp SUB 16 CKpqKqp MP: 15, 13 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.22.1 12/29/2017 15:50:08 *3.22.1 CCKpqKrqCKpqKqr PROOF ABBREVIATION *3.22.1+Prop PROOF 1 CCKpqKrqCKpqKqr *3.22.1 This is here to make *3.47 work. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.22.2 12/29/2017 15:50:08 *3.22.2 CCKqrKsrCKqrKrs PROOF ABBREVIATION *3.22.2+Prop PROOF 1 CCKqrKsrCKqrKrs *3.22.2 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.24 12/29/2017 15:50:08 *3.24 NKpNp PROOF ABBREVIATION *3.14 q/Np+C*2.11 p/Np-Prop PROOF 1 CANpNqNKpq *3.14 q/Np 2 CANpNNpNKpNp SUB 3 ApNp *2.11 p/Np 4 ANpNNp SUB 5 NKpNp MP: 2, 4 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.26 12/29/2017 15:50:08 *3.26 CKpqp (Simp) PROOF ABBREVIATION *2.02 p/q, q/p+(1) (1)+*1.01 q/Cqp;*1.01 p/q, q/p;(2.1) *2.31 p/Np, q/Nq, r/p-C(2.1)-(2.2) *2.53 p/ANpNq, q/p+C(2.2)-(2) (2)+*3.01;Prop PROOF 1 CqCpq *2.02 (Simp) p/q, q/p (1) 2 CpCqp SUB Cpq=ANpq Df. *1.01 q/Cqp CpCqp=ANpCqp Df. 3 ANpCqp REP Cpq=ANpq Df. *1.01 p/q, q/p Cqp=ANqp Df. (2.1) 4 ANpANqp REP 5 CApAqrAApqr *2.31 p/Np, q/Nq, r/p 6 CANpANqpAANpNqp SUB (2.2) 7 AANpNqp MP: 6, 4 8 CApqCNpq *2.53 p/ANpNq, q/p 9 CAANpNqpCNANpNqp SUB (2) 10 CNANpNqp MP: 9, 7 Kpq=NANpNq Df. *3.01 11 CKpqp REP First time that an antecedent in a demonstration has not been given explicitly. In this case it depends upon definitions applied to (1). I call the antecedent (2.1). This is the first example of an extended use of MODUS PONENS. This demonstration follows the paradigm of *2.25. It is not like that of the note of *2.31, since the proposition to be proved is not “Cad”. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.26.1 12/29/2017 15:50:08 *3.26.1 CCCKpqpCCpKpqEpKpqCCpKpqEpKpq PROOF ABBREVIATION *3.26.1+Prop PROOF 1 CCCKpqpCCpKpqEpKpqCCpKpqEpKpq *3.26.1 This is here to make *4.71 work. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.27 12/29/2017 15:50:08 *3.27 CKpqq (Simp) PROOF ABBREVIATION *2.06 p/Kpq, q/Kqp, r/q+(1) *3.22+(2) (1)+C(2)-(3) *3.26 p/q, q/p+(4) (3)+C(4)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/Kpq, q/Kqp, r/q (1) 2 CCKpqKqpCCKqpqCKpqq SUB (2) 3 CKpqKqp *3.22 (3) 4 CCKqpqCKpqq MP: 2, 3 5 CKpqp *3.26 (Simp) p/q, q/p (4) 6 CKqpq SUB 7 CKpqq MP: 4, 6 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.27.1 12/29/2017 15:50:08 *3.27.1 CKCrNqEpAqrCAqrp PROOF ABBREVIATION *3.27.1+Prop PROOF 1 CKCrNqEpAqrCAqrp *3.27.1 This is here for *5.75 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.3 12/29/2017 15:50:08 *3.3 CCKpqrCpCqr (Exp) PROOF ABBREVIATION *2.06 p/CKpqr, q/CNANpNqr, r/CNrANpNq+(1) *2.08 p/CNANpNqr+*3.01;(2) (1)+C(2)-(3) *2.15 p/ANpNq, q/r+(4) (3)+C(4)-(5) *2.06 p/CKpqr, q/CNrANpNq, r/CNrCpNq+(6) (6)+C(5)-(7) *2.08 p/CNrCpNq+*1.01 q/Nq;(8) (7)+C(8)-(9) *2.06 p/CKpqr, q/CNrCpNq, r/CpCNrNq+(10) (10)+C(9)-(11) *2.04 p/Nr, q/p, r/Nq+(12) (11)+C(12)-(13) *2.06 p/CKpqr, q/CpCNrNq, r/CpCqr+(14) (14)+C(13)-(15) *2.05 q/CNrNq, r/Cqr+C*2.17 p/q, q/r-(16) (15)+C(16)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/CKpqr, q/CNANpNqr, r/CNrANpNq (1) 2 CCCKpqrCNANpNqrCCCNANpNqrCNrANpNqCCKpqrCNrANpNq SUB 3 Cpp *2.08 (Id) p/CNANpNqr 4 CCNANpNqrCNANpNqr SUB Kpq=NANpNq Df. *3.01 (2) 5 CCKpqrCNANpNqr REP (3) 6 CCCNANpNqrCNrANpNqCCKpqrCNrANpNq MP: 2, 5 7 CCNpqCNqp *2.15 p/ANpNq, q/r (4) 8 CCNANpNqrCNrANpNq SUB (5) 9 CCKpqrCNrANpNq MP: 6, 8 10 CCpqCCqrCpr *2.06 (Syll) p/CKpqr, q/CNrANpNq, r/CNrCpNq (6) 11 CCCKpqrCNrANpNqCCCNrANpNqCNrCpNqCCKpqrCNrCpNq SUB (7) 12 CCCNrANpNqCNrCpNqCCKpqrCNrCpNq MP: 11, 9 13 Cpp *2.08 (Id) p/CNrCpNq 14 CCNrCpNqCNrCpNq SUB Cpq=ANpq Df. *1.01 q/Nq CpNq=ANpNq Df. (8) 15 CCNrANpNqCNrCpNq REP (9) 16 CCKpqrCNrCpNq MP: 12, 15 17 CCpqCCqrCpr *2.06 (Syll) p/CKpqr, q/CNrCpNq, r/CpCNrNq (10) 18 CCCKpqrCNrCpNqCCCNrCpNqCpCNrNqCCKpqrCpCNrNq SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.3(CONT.) (11) 19 CCCNrCpNqCpCNrNqCCKpqrCpCNrNq MP: 18, 16 20 CCpCqrCqCpr *2.04 (Comm) p/Nr, q/p, r/Nq (12) 21 CCNrCpNqCpCNrNq SUB (13) 22 CCKpqrCpCNrNq MP: 19, 21 23 CCpqCCqrCpr *2.06 (Syll) p/CKpqr, q/CpCNrNq, r/CpCqr (14) 24 CCCKpqrCpCNrNqCCCpCNrNqCpCqrCCKpqrCpCqr SUB (15) 25 CCCpCNrNqCpCqrCCKpqrCpCqr MP: 24, 22 26 CCqrCCpqCpr *2.05 (Syll) q/CNrNq, r/Cqr 27 CCCNrNqCqrCCpCNrNqCpCqr SUB 28 CCNqNpCpq *2.17 (Transp) p/q, q/r 29 CCNrNqCqr SUB (16) 30 CCpCNrNqCpCqr MP: 27, 29 31 CCKpqrCpCqr MP: 25, 30 This is an extended example of the paradigm of *2.31 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.31 12/29/2017 15:50:08 *3.31 CCpCqrCKpqr (Imp) PROOF ABBREVIATION *2.06 p/CpCqr, q/ANpANqr, r/AANpNqr+(1) *2.08 p/ANpANqr+*1.01 p/q, q/r;*1.01 q/Cqr;(2) (1)+C(2)-(3) *2.31 p/Np, q/Nq+(4) (3)+C(4)-(5) *2.06 p/CpCqr, q/AANpNqr, r/CNANpNqr+(6) (6)+C(5)-(7) *2.53 p/ANpNq, q/r+(8) (7)+C(8)-(9) *2.06 p/CpCqr, q/CNANpNqr, r/CKpqr+(10) (10)+C(9)-(11) *2.08 p/CKpqr+*3.01;(12) (11)+C(12)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/CpCqr, q/ANpANqr, r/AANpNqr (1) 2 CCCpCqrANpANqrCCANpANqrAANpNqrCCpCqrAANpNqr SUB 3 Cpp *2.08 (Id) p/ANpANqr 4 CANpANqrANpANqr SUB Cpq=ANpq Df. *1.01 p/q, q/r Cqr=ANqr Df. 5 CANpCqrANpANqr REP Cpq=ANpq Df. *1.01 q/Cqr CpCqr=ANpCqr Df. (2) 6 CCpCqrANpANqr REP (3) 7 CCANpANqrAANpNqrCCpCqrAANpNqr MP: 2, 6 8 CApAqrAApqr *2.31 p/Np, q/Nq (4) 9 CANpANqrAANpNqr SUB (5) 10 CCpCqrAANpNqr MP: 7, 9 11 CCpqCCqrCpr *2.06 (Syll) p/CpCqr, q/AANpNqr, r/CNANpNqr (6) 12 CCCpCqrAANpNqrCCAANpNqrCNANpNqrCCpCqrCNANpNqr SUB (7) 13 CCAANpNqrCNANpNqrCCpCqrCNANpNqr MP: 12, 10 14 CApqCNpq *2.53 p/ANpNq, q/r (8) 15 CAANpNqrCNANpNqr SUB (9) 16 CCpCqrCNANpNqr MP: 13, 15 17 CCpqCCqrCpr *2.06 (Syll) p/CpCqr, q/CNANpNqr, r/CKpqr (10) 18 CCCpCqrCNANpNqrCCCNANpNqrCKpqrCCpCqrCKpqr SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.31(CONT.) (11) 19 CCCNANpNqrCKpqrCCpCqrCKpqr MP: 18, 16 20 Cpp *2.08 (Id) p/CKpqr 21 CCKpqrCKpqr SUB Kpq=NANpNq Df. *3.01 (12) 22 CCNANpNqrCKpqr REP 23 CCpCqrCKpqr MP: 19, 22 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.33 12/29/2017 15:50:08 *3.33 CKCpqCqrCpr (Syll) PROOF ABBREVIATION *3.31 p/Cpq, q/Cqr, r/Cpr+C*2.06-Prop PROOF 1 CCpCqrCKpqr *3.31 (Imp) p/Cpq, q/Cqr, r/Cpr 2 CCCpqCCqrCprCKCpqCqrCpr SUB 3 CCpqCCqrCpr *2.06 (Syll) 4 CKCpqCqrCpr MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.34 12/29/2017 15:50:08 *3.34 CKCqrCpqCpr (Syll) PROOF ABBREVIATION *3.31 p/Cqr, q/Cpq, r/Cpr+C*2.05-Prop PROOF 1 CCpCqrCKpqr *3.31 (Imp) p/Cqr, q/Cpq, r/Cpr 2 CCCqrCCpqCprCKCqrCpqCpr SUB 3 CCqrCCpqCpr *2.05 (Syll) 4 CKCqrCpqCpr MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.35 12/29/2017 15:50:08 *3.35 CKpCpqq (Ass) PROOF ABBREVIATION *3.31 q/Cpq, r/q+C*2.27-Prop PROOF 1 CCpCqrCKpqr *3.31 (Imp) q/Cpq, r/q 2 CCpCCpqqCKpCpqq SUB 3 CpCCpqq *2.27 4 CKpCpqq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.37 12/29/2017 15:50:08 *3.37 CCKpqrCKpNrNq (Transp) PROOF ABBREVIATION *2.05 q/Cqr, r/CNrNq+C*2.16 p/q, q/r-(1) *3.3+(2) *3.31 q/Nr, r/Nq+(3) *2.06 p/CKpqr, q/CpCqr, r/CpCNrNq-C(2)-C(1)-(4.1) *2.06 p/CKpqr, q/CpCNrNq, r/CKpNrNq-C(4.1)-C(3)-Prop PROOF 1 CCqrCCpqCpr *2.05 (Syll) q/Cqr, r/CNrNq 2 CCCqrCNrNqCCpCqrCpCNrNq SUB 3 CCpqCNqNp *2.16 p/q, q/r 4 CCqrCNrNq SUB (1) 5 CCpCqrCpCNrNq MP: 2, 4 (2) 6 CCKpqrCpCqr *3.3 (Exp) 7 CCpCqrCKpqr *3.31 (Imp) q/Nr, r/Nq (3) 8 CCpCNrNqCKpNrNq SUB 9 CCpqCCqrCpr *2.06 (Syll) p/CKpqr, q/CpCqr, r/CpCNrNq 10 CCCKpqrCpCqrCCCpCqrCpCNrNqCCKpqrCpCNrNq SUB 11 CCCpCqrCpCNrNqCCKpqrCpCNrNq MP: 10, 6 (4.1) 12 CCKpqrCpCNrNq MP: 11, 5 13 CCpqCCqrCpr *2.06 (Syll) p/CKpqr, q/CpCNrNq, r/CKpNrNq 14 CCCKpqrCpCNrNqCCCpCNrNqCKpNrNqCCKpqrCKpNrNq SUB 15 CCCpCNrNqCKpNrNqCCKpqrCKpNrNq MP: 14, 12 16 CCKpqrCKpNrNq MP: 15, 8 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.4 12/29/2017 15:50:08 *3.4 CKpqCpq PROOF ABBREVIATION *2.16 p/NCpq, q/CpNq+C*2.51-*1.01 q/Nq;*3.01;SE(*2.14 p/Cpq:*2.12 p/Cpq);Prop PROOF 1 CCpqCNqNp *2.16 p/NCpq, q/CpNq 2 CCNCpqCpNqCNCpNqNNCpq SUB 3 CNCpqCpNq *2.51 4 CNCpNqNNCpq MP: 2, 3 Cpq=ANpq Df. *1.01 q/Nq CpNq=ANpNq Df. 5 CNANpNqNNCpq REP Kpq=NANpNq Df. *3.01 6 CKpqNNCpq REP CNNpp *2.14 : CpNNp *2.12 p/Cpq : p/Cpq CNNCpqCpq : CCpqNNCpq 7 CKpqCpq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.41 12/29/2017 15:50:08 *3.41 CCprCKpqr PROOF ABBREVIATION *2.06 p/Kpq, q/p+C*3.26-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/Kpq, q/p 2 CCKpqpCCprCKpqr SUB 3 CKpqp *3.26 (Simp) 4 CCprCKpqr MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.42 12/29/2017 15:50:08 *3.42 CCqrCKpqr PROOF ABBREVIATION *2.06 p/Kpq+C*3.27-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/Kpq 2 CCKpqqCCqrCKpqr SUB 3 CKpqq *3.27 (Simp) 4 CCqrCKpqr MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.43 12/29/2017 15:50:08 *3.43 CKCpqCprCpKqr (Comp) PROOF ABBREVIATION *3.2 p/q, q/r+(1) *2.06 p/Cpq, q/CpCrKqr, r/CCprCpKqr+(2.1) *2.05 r/CrKqr+C(1)-(2.2) (2.1)+C(2.2)-(2.3) *2.77 q/r, r/Kqr+(2.4) (2.3)+C(2.4)-(2) *3.31 p/Cpq, q/Cpr, r/CpKqr+C(2)-Prop PROOF 1 CpCqKpq *3.2 p/q, q/r (1) 2 CqCrKqr SUB 3 CCpqCCqrCpr *2.06 (Syll) p/Cpq, q/CpCrKqr, r/CCprCpKqr (2.1) 4 CCCpqCpCrKqrCCCpCrKqrCCprCpKqrCCpqCCprCpKqr SUB 5 CCqrCCpqCpr *2.05 (Syll) r/CrKqr 6 CCqCrKqrCCpqCpCrKqr SUB (2.2) 7 CCpqCpCrKqr MP: 6, 2 (2.3) 8 CCCpCrKqrCCprCpKqrCCpqCCprCpKqr MP: 4, 7 9 CCpCqrCCpqCpr *2.77 q/r, r/Kqr (2.4) 10 CCpCrKqrCCprCpKqr SUB (2) 11 CCpqCCprCpKqr MP: 8, 10 12 CCpCqrCKpqr *3.31 (Imp) p/Cpq, q/Cpr, r/CpKqr 13 CCCpqCCprCpKqrCKCpqCprCpKqr SUB 14 CKCpqCprCpKqr MP: 13, 11 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.44 12/29/2017 15:50:08 *3.44 CKCqpCrpCAqrp PROOF ABBREVIATION *2.06 p/KCNqrCrp, q/CNqp, r/CCqpp+(1.1) *3.33 p/Nq, q/r, r/p+(1.2) (1.1)+C(1.2)-(1.3) *2.6 p/q, q/p+(1.4) (1.3)+C(1.4)-(1) *2.06 p/CNqr, q/CCrpCCqpp, r/CKCqpCrpp+(2.1) *3.3 p/CNqr, q/Crp, r/CCqpp+C(1)-(2.2) (2.1)+C(2.2)-(2.3) *3.31 p/Cqp, q/Crp, r/p+(2.41) *2.04 p/Crp, q/Cqp, r/p+(2.42) SYLL (2.41), (2.42)+(2.4) (2.3)+C(2.4)-(2) *2.04 p/CNqr, q/KCqpCrp, r/p+C(2)-(3.1) *2.06 q/CNqr, r/p, p/Aqr+C*2.53 p/q, q/r-(3.2) SYLL (3.1), (3.2)+Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/KCNqrCrp, q/CNqp, r/CCqpp (1.1) 2 CCKCNqrCrpCNqpCCCNqpCCqppCKCNqrCrpCCqpp SUB 3 CKCpqCqrCpr *3.33 (Syll) p/Nq, q/r, r/p (1.2) 4 CKCNqrCrpCNqp SUB (1.3) 5 CCCNqpCCqppCKCNqrCrpCCqpp MP: 2, 4 6 CCNpqCCpqq *2.6 p/q, q/p (1.4) 7 CCNqpCCqpp SUB (1) 8 CKCNqrCrpCCqpp MP: 5, 7 9 CCpqCCqrCpr *2.06 (Syll) p/CNqr, q/CCrpCCqpp, r/CKCqpCrpp (2.1) 10 CCCNqrCCrpCCqppCCCCrpCCqppCKCqpCrppCCNqrCKCqpCrpp SUB 11 CCKpqrCpCqr *3.3 (Exp) p/CNqr, q/Crp, r/CCqpp 12 CCKCNqrCrpCCqppCCNqrCCrpCCqpp SUB (2.2) 13 CCNqrCCrpCCqpp MP: 12, 8 (2.3) 14 CCCCrpCCqppCKCqpCrppCCNqrCKCqpCrpp MP: 10, 13 15 CCpCqrCKpqr *3.31 (Imp) p/Cqp, q/Crp, r/p (2.41) 16 CCCqpCCrppCKCqpCrpp SUB 17 CCpCqrCqCpr *2.04 (Comm) p/Crp, q/Cqp, r/p (2.42) 18 CCCrpCCqppCCqpCCrpp SUB (2.4) 19 CCCrpCCqppCKCqpCrpp SYLL: 16, 18 (2) 20 CCNqrCKCqpCrpp MP: 14, 19 21 CCpCqrCqCpr *2.04 (Comm) p/CNqr, q/KCqpCrp, r/p 22 CCCNqrCKCqpCrppCKCqpCrpCCNqrp SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.44(CONT.) (3.1) 23 CKCqpCrpCCNqrp MP: 22, 20 24 CCpqCCqrCpr *2.06 (Syll) q/CNqr, r/p, p/Aqr 25 CCAqrCNqrCCCNqrpCAqrp SUB 26 CApqCNpq *2.53 p/q, q/r 27 CAqrCNqr SUB (3.2) 28 CCCNqrpCAqrp MP: 25, 27 29 CKCqpCrpCAqrp SYLL: 23, 28 In the last part of the proof CCKCqpCrpCCNqrpCKCqpCrpCAqrp should be constructed from *2.53 and Syll. The proposition is then obtained by applying Modus Ponens to this and (3.1). PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.45 12/29/2017 15:50:08 *3.45 CCpqCKprKqr (Fact) PROOF ABBREVIATION *2.06 p/Cpq, q/CCqNrCpNr, r/CNCpNrNCqNr+(1) *2.06 r/Nr+(2) (1)+C(2)-(3) *2.16 p/CqNr, q/CpNr+(4) (3)+C(4)-(5) *2.06 p/Cpq, q/CNCpNrNCqNr, r/CKprKqr+(6) (6)+C(5)-(7) *2.08 p/CNCpNrNCqNr+*1.01 q/Nr II;*1.01 p/q, q/Nr II;(#1) (#1);*3.01 q/r;*3.01 p/q, q/r;(8) (7)+C(8)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/Cpq, q/CCqNrCpNr, r/CNCpNrNCqNr (1) 2 CCCpqCCqNrCpNrCCCCqNrCpNrCNCpNrNCqNrCCpqCNCpNrNCqNr SUB 3 CCpqCCqrCpr *2.06 (Syll) r/Nr (2) 4 CCpqCCqNrCpNr SUB (3) 5 CCCCqNrCpNrCNCpNrNCqNrCCpqCNCpNrNCqNr MP: 2, 4 6 CCpqCNqNp *2.16 p/CqNr, q/CpNr (4) 7 CCCqNrCpNrCNCpNrNCqNr SUB (5) 8 CCpqCNCpNrNCqNr MP: 5, 7 9 CCpqCCqrCpr *2.06 (Syll) p/Cpq, q/CNCpNrNCqNr, r/CKprKqr (6) 10 CCCpqCNCpNrNCqNrCCCNCpNrNCqNrCKprKqrCCpqCKprKqr SUB (7) 11 CCCNCpNrNCqNrCKprKqrCCpqCKprKqr MP: 10, 8 12 Cpp *2.08 (Id) p/CNCpNrNCqNr 13 CCNCpNrNCqNrCNCpNrNCqNr SUB Cpq=ANpq Df. *1.01 q/Nr CpNr=ANpNr Df. 14 CCNCpNrNCqNrCNANpNrNCqNr REP II Cpq=ANpq Df. *1.01 p/q, q/Nr CqNr=ANqNr Df. (#1) 15 CCNCpNrNCqNrCNANpNrNANqNr REP II Kpq=NANpNq Df. *3.01 q/r Kpr=NANpNr Df. 16 CCNCpNrNCqNrCKprNANqNr REP Kpq=NANpNq Df. *3.01 p/q, q/r Kqr=NANqNr Df. (8) 17 CCNCpNrNCqNrCKprKqr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.45(CONT.) 18 CCpqCKprKqr MP: 11, 17 This demonstration is a mixed paradigm. The first and second lines follow *2.31, the second and third lines follow *2.25. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.47 12/29/2017 15:50:08 *3.47 CKCprCqsCKpqKrs PROOF ABBREVIATION *2.06 p/KCprCqs, q/Cpr, r/CKpqKrq+(1.1) *3.26 p/Cpr, q/Cqs+(1.2) (1.1)+C(1.2)-(1.3) *3.45 q/r, r/q+(1.4) (1.3)+C(1.4)-(1.5) *2.06 p/KCprCqs, q/CKpqKrq, r/CKpqKqr+(1.6) (1.6)+C(1.5)-(1.7) *3.22.1+(1.8) (1.7)+C(1.8)-(1) *2.06 p/KCprCqs, q/Cqs, r/CKqrKsr+(2.1) *3.27 p/Cpr, q/Cqs+(2.2) (2.1)+C(2.2)-(2.3) *3.45 p/q, q/s+(2.4) (2.3)+C(2.4)-(2.5) *2.06 p/KCprCqs, q/CKqrKsr, r/CKqrKrs+(2.6) (2.6)+C(2.5)-(2.7) *3.22.2+(2.8) (2.7)+C(2.8)-(2) *2.83 p/KCprCqs, q/Kpq, r/Kqr, s/Krs+C(1)-C(2)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/KCprCqs, q/Cpr, r/CKpqKrq (1.1) 2 CCKCprCqsCprCCCprCKpqKrqCKCprCqsCKpqKrq SUB 3 CKpqp *3.26 (Simp) p/Cpr, q/Cqs (1.2) 4 CKCprCqsCpr SUB (1.3) 5 CCCprCKpqKrqCKCprCqsCKpqKrq MP: 2, 4 6 CCpqCKprKqr *3.45 (Fact) q/r, r/q (1.4) 7 CCprCKpqKrq SUB (1.5) 8 CKCprCqsCKpqKrq MP: 5, 7 9 CCpqCCqrCpr *2.06 (Syll) p/KCprCqs, q/CKpqKrq, r/CKpqKqr (1.6) 10 CCKCprCqsCKpqKrqCCCKpqKrqCKpqKqrCKCprCqsCKpqKqr SUB (1.7) 11 CCCKpqKrqCKpqKqrCKCprCqsCKpqKqr MP: 10, 8 (1.8) 12 CCKpqKrqCKpqKqr *3.22.1 (1) 13 CKCprCqsCKpqKqr MP: 11, 12 14 CCpqCCqrCpr *2.06 (Syll) p/KCprCqs, q/Cqs, r/CKqrKsr (2.1) 15 CCKCprCqsCqsCCCqsCKqrKsrCKCprCqsCKqrKsr SUB 16 CKpqq *3.27 (Simp) p/Cpr, q/Cqs (2.2) 17 CKCprCqsCqs SUB (2.3) 18 CCCqsCKqrKsrCKCprCqsCKqrKsr MP: 15, 17 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.47(CONT.) 19 CCpqCKprKqr *3.45 (Fact) p/q, q/s (2.4) 20 CCqsCKqrKsr SUB (2.5) 21 CKCprCqsCKqrKsr MP: 18, 20 22 CCpqCCqrCpr *2.06 (Syll) p/KCprCqs, q/CKqrKsr, r/CKqrKrs (2.6) 23 CCKCprCqsCKqrKsrCCCKqrKsrCKqrKrsCKCprCqsCKqrKrs SUB (2.7) 24 CCCKqrKsrCKqrKrsCKCprCqsCKqrKrs MP: 23, 21 (2.8) 25 CCKqrKsrCKqrKrs *3.22.2 (2) 26 CKCprCqsCKqrKrs MP: 24, 25 27 CCpCqrCCpCrsCpCqs *2.83 p/KCprCqs, q/Kpq, r/Kqr, s/Krs 28 CCKCprCqsCKpqKqrCCKCprCqsCKqrKrsCKCprCqsCKpqKrs SUB 29 CCKCprCqsCKqrKrsCKCprCqsCKpqKrs MP: 28, 13 30 CKCprCqsCKpqKrs MP: 29, 26 This demonstration is in error. The demonstration will not work with both +*3.03 and *2.83 in the last step. The proof presented here used *2.83 and +ignores *3.03. Note the use of *3.22.1 and *3.22.2 in this proof. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.48 12/29/2017 15:50:08 *3.48 CKCprCqsCApqArs PROOF ABBREVIATION *2.06 p/KCprCqs, q/Cpr, r/CApqArq+(1.1) *3.26 p/Cpr, q/Cqs+(1.2) (1.1)+C(1.2)-(1.3) *2.38 p/q, q/p+(1.4) (1.3)+C(1.4)-(1.5) *2.06 p/KCprCqs, q/CApqArq, r/CApqAqr+(1.6) (1.6)+C(1.5)-(1.7) *1.4.1+(1.8) (1.7)+C(1.8)-(1) *2.06 p/KCprCqs, q/Cqs, r/CAqrAsr+(2.1) *3.27 p/Cpr, q/Cqs+(2.2) (2.1)+C(2.2)+(2.3) *2.38 p/r, r/s+(2.4) (2.3)+C(2.4)-(2.5) *2.06 p/KCprCqs, q/CAqrAsr, r/CAqrArs+(2.6) (2.6)+C(2.5)-(2.7) *1.4.2+(2.8) (2.6)+C(2.8)-(2) *2.83 p/KCprCqs, q/Apq, r/Aqr, s/Ars+C(1)-C(2)-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/KCprCqs, q/Cpr, r/CApqArq (1.1) 2 CCKCprCqsCprCCCprCApqArqCKCprCqsCApqArq SUB 3 CKpqp *3.26 (Simp) p/Cpr, q/Cqs (1.2) 4 CKCprCqsCpr SUB (1.3) 5 CCCprCApqArqCKCprCqsCApqArq MP: 2, 4 6 CCqrCAqpArp *2.38 p/q, q/p (1.4) 7 CCprCApqArq SUB (1.5) 8 CKCprCqsCApqArq MP: 5, 7 9 CCpqCCqrCpr *2.06 (Syll) p/KCprCqs, q/CApqArq, r/CApqAqr (1.6) 10 CCKCprCqsCApqArqCCCApqArqCApqAqrCKCprCqsCApqAqr SUB (1.7) 11 CCCApqArqCApqAqrCKCprCqsCApqAqr MP: 10, 8 (1.8) 12 CCApqArqCApqAqr *1.4.1 (1) 13 CKCprCqsCApqAqr MP: 11, 12 14 CCpqCCqrCpr *2.06 (Syll) p/KCprCqs, q/Cqs, r/CAqrAsr (2.1) 15 CCKCprCqsCqsCCCqsCAqrAsrCKCprCqsCAqrAsr SUB 16 CKpqq *3.27 (Simp) p/Cpr, q/Cqs (2.2) 17 CKCprCqsCqs SUB (2.3) 18 CCCqsCAqrAsrCKCprCqsCAqrAsr MP: 15, 17 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *3.48(CONT.) 19 CCqrCAqpArp *2.38 p/r, r/s (2.4) 20 CCqsCAqrAsr SUB (2.5) 21 CKCprCqsCAqrAsr MP: 18, 20 22 CCpqCCqrCpr *2.06 (Syll) p/KCprCqs, q/CAqrAsr, r/CAqrArs (2.6) 23 CCKCprCqsCAqrAsrCCCAqrAsrCAqrArsCKCprCqsCAqrArs SUB (2.7) 24 CCCAqrAsrCAqrArsCKCprCqsCAqrArs MP: 23, 21 (2.8) 25 CCAqrAsrCAqrArs *1.4.2 (2) 26 CKCprCqsCAqrArs MP: 24, 25 27 CCpCqrCCpCrsCpCqs *2.83 p/KCprCqs, q/Apq, r/Aqr, s/Ars 28 CCKCprCqsCApqAqrCCKCprCqsCAqrArsCKCprCqsCApqArs SUB 29 CCKCprCqsCAqrArsCKCprCqsCApqArs MP: 28, 13 30 CKCprCqsCApqArs MP: 29, 26 Note the use of *1.4.1 and *1.4.2. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.01 12/29/2017 15:50:08 *4.01 Epq=KCpqCqp Df. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.02 12/29/2017 15:50:08 *4.02 EEpqr=KEpqEqr Df. This definition resolves an ambiguity in *4.87. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.1 12/29/2017 15:50:08 *4.1 ECpqCNqNp PROOF ABBREVIATION *2.16+(1) *2.17+(2) *3.03 (1), (2)+*4.01 p/Cpq, q/CNqNp;Prop PROOF (1) 1 CCpqCNqNp *2.16 (2) 2 CCNqNpCpq *2.17 (Transp) 3 KCCpqCNqNpCCNqNpCpq *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 p/Cpq, q/CNqNp ECpqCNqNp=KCCpqCNqNpCCNqNpCpq Df. 4 ECpqCNqNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.11 12/29/2017 15:50:08 *4.11 EEpqENpNq (Transp) PROOF ABBREVIATION *2.16+(1) *2.16 p/q, q/p+(2) *3.03 (1), (2)+(3) *3.47 p/Cpq, q/Cqp, r/CNqNp, s/CNpNq+C(3)-*4.01;(#1) (#1);SE(*3.22 p/CNqNp, q/CNpNq:*3.22 p/CNpNq, q/CNqNp);*4.01 p/Np, q/Nq;(4) *2.17+(5) *2.17 p/q, q/p+(6) *3.03 (5), (6)+(7) *3.47 p/CNqNp, q/CNpNq, r/Cpq, s/Cqp+C(7)-*4.01;(#2) (#2);SE(*3.22 p/CNqNp, q/CNpNq:*3.22 p/CNpNq, q/CNqNp);*4.01 p/Np, q/Nq;(8) *3.03 (4), (8)+*4.01 p/Epq, q/ENpNq;Prop PROOF (1) 1 CCpqCNqNp *2.16 2 CCpqCNqNp *2.16 p/q, q/p (2) 3 CCqpCNpNq SUB (3) 4 KCCpqCNqNpCCqpCNpNq *3.03: 2, 3 5 CKCprCqsCKpqKrs *3.47 p/Cpq, q/Cqp, r/CNqNp, s/CNpNq 6 CKCCpqCNqNpCCqpCNpNqCKCpqCqpKCNqNpCNpNq SUB 7 CKCpqCqpKCNqNpCNpNq MP: 6, 4 Epq=KCpqCqp Df. *4.01 (#1) 8 CEpqKCNqNpCNpNq REP CKpqKqp *3.22 : CKpqKqp *3.22 p/CNqNp, q/CNpNq : p/CNpNq, q/CNqNp CKCNqNpCNpNqKCNpNqCNqNp : CKCNpNqCNqNpKCNqNpCNpNq 9 CEpqKCNpNqCNqNp SE Epq=KCpqCqp Df. *4.01 p/Np, q/Nq ENpNq=KCNpNqCNqNp Df. (4) 10 CEpqENpNq REP (5) 11 CCNqNpCpq *2.17 (Transp) 12 CCNqNpCpq *2.17 (Transp) p/q, q/p (6) 13 CCNpNqCqp SUB (7) 14 KCCNqNpCpqCCNpNqCqp *3.03: 12, 13 15 CKCprCqsCKpqKrs *3.47 p/CNqNp, q/CNpNq, r/Cpq, s/Cqp 16 CKCCNqNpCpqCCNpNqCqpCKCNqNpCNpNqKCpqCqp SUB 17 CKCNqNpCNpNqKCpqCqp MP: 16, 14 Epq=KCpqCqp Df. *4.01 (#2) 18 CKCNqNpCNpNqEpq REP CKpqKqp *3.22 : CKpqKqp *3.22 p/CNqNp, q/CNpNq : p/CNpNq, q/CNqNp CKCNqNpCNpNqKCNpNqCNqNp : CKCNpNqCNqNpKCNqNpCNpNq 19 CKCNpNqCNqNpEpq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.11(CONT.) Epq=KCpqCqp Df. *4.01 p/Np, q/Nq ENpNq=KCNpNqCNqNp Df. (8) 20 CENpNqEpq REP 21 KCEpqENpNqCENpNqEpq *3.03: 10, 20 Epq=KCpqCqp Df. *4.01 p/Epq, q/ENpNq EEpqENpNq=KCEpqENpNqCENpNqEpq Df. 22 EEpqENpNq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.12 12/29/2017 15:50:08 *4.12 EEpNqEqNp PROOF ABBREVIATION *2.03+(1) *2.15 p/q, q/p+(2) *3.03 (1), (2)+(3) *3.47 p/CpNq, r/CqNp, q/CNqp, s/CNpq+C(3)-(#1) (#1)+*4.01 q/Nq;*4.01 p/q, q/Np;(4) *2.03 p/q, q/p+(5) *2.15+(6) *3.03 (5),(6)+(7) *3.47 p/CqNp, q/CNpq, r/CpNq, s/CNqp+C(7)-(#2) (#2);*4.01 p/q, q/Np;*4.01 q/Nq;(8) *3.03 (4), (8)+*4.01 p/EpNq, q/EqNp;Prop PROOF (1) 1 CCpNqCqNp *2.03 (Transp) 2 CCNpqCNqp *2.15 p/q, q/p (2) 3 CCNqpCNpq SUB (3) 4 KCCpNqCqNpCCNqpCNpq *3.03: 1, 3 5 CKCprCqsCKpqKrs *3.47 p/CpNq, r/CqNp, q/CNqp, s/CNpq 6 CKCCpNqCqNpCCNqpCNpqCKCpNqCNqpKCqNpCNpq SUB (#1) 7 CKCpNqCNqpKCqNpCNpq MP: 6, 4 Epq=KCpqCqp Df. *4.01 q/Nq EpNq=KCpNqCNqp Df. 8 CEpNqKCqNpCNpq REP Epq=KCpqCqp Df. *4.01 p/q, q/Np EqNp=KCqNpCNpq Df. (4) 9 CEpNqEqNp REP 10 CCpNqCqNp *2.03 (Transp) p/q, q/p (5) 11 CCqNpCpNq SUB (6) 12 CCNpqCNqp *2.15 (7) 13 KCCqNpCpNqCCNpqCNqp *3.03: 11, 12 14 CKCprCqsCKpqKrs *3.47 p/CqNp, q/CNpq, r/CpNq, s/CNqp 15 CKCCqNpCpNqCCNpqCNqpCKCqNpCNpqKCpNqCNqp SUB (#2) 16 CKCqNpCNpqKCpNqCNqp MP: 15, 13 Epq=KCpqCqp Df. *4.01 p/q, q/Np EqNp=KCqNpCNpq Df. 17 CEqNpKCpNqCNqp REP Epq=KCpqCqp Df. *4.01 q/Nq EpNq=KCpNqCNqp Df. (8) 18 CEqNpEpNq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.12(CONT.) 19 KCEpNqEqNpCEqNpEpNq *3.03: 9, 18 Epq=KCpqCqp Df. *4.01 p/EpNq, q/EqNp EEpNqEqNp=KCEpNqEqNpCEqNpEpNq Df. 20 EEpNqEqNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.12.1 12/29/2017 15:50:08 *4.12.1 ECKqrNpCpNKqr PROOF ABBREVIATION *4.12.1+Prop PROOF 1 ECKqrNpCpNKqr *4.12.1 This is here to make *4.32 work. This seems to be evidence that BR thought he could move from . . . Epq. . . to . . . Cpq. . . when E is not the major connective. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.13 12/29/2017 15:50:08 *4.13 EpNNp PROOF ABBREVIATION *2.12+(1) *2.14+(2) *3.03 (1), (2)+*4.01 q/NNp;Prop PROOF (1) 1 CpNNp *2.12 (2) 2 CNNpp *2.14 3 KCpNNpCNNpp *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 q/NNp EpNNp=KCpNNpCNNpp Df. 4 EpNNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.14 12/29/2017 15:50:08 *4.14 ECKpqrCKpNrNq PROOF ABBREVIATION *3.37+(1) *3.37 q/Nr, r/Nq+SE(*4.13 p/q);SE(*4.13 p/r);(2) *3.03 (1), (2)+*4.01 p/CKpqr, q/CKpNrNq;Prop PROOF (1) 1 CCKpqrCKpNrNq *3.37 (Transp) 2 CCKpqrCKpNrNq *3.37 (Transp) q/Nr, r/Nq 3 CCKpNrNqCKpNNqNNr SUB EpNNp *4.13 p/q EqNNq 4 CCKpNrNqCKpqNNr SE EpNNp *4.13 p/r ErNNr (2) 5 CCKpNrNqCKpqr SE 6 KCCKpqrCKpNrNqCCKpNrNqCKpqr *3.03: 2, 5 Epq=KCpqCqp Df. *4.01 p/CKpqr, q/CKpNrNq ECKpqrCKpNrNq=KCCKpqrCKpNrNqCCKpNrNqCKpqr Df. 7 ECKpqrCKpNrNq REP First use of SE with an equivalence. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.15 12/29/2017 15:50:08 *4.15 ECKpqNrCKqrNp PROOF ABBREVIATION *4.14 p/q, q/p, r/Nr+SE(*4.13 p/r);SE(*3.22:*3.22 p/q, q/p);Prop PROOF 1 ECKpqrCKpNrNq *4.14 p/q, q/p, r/Nr 2 ECKqpNrCKqNNrNp SUB EpNNp *4.13 p/r ErNNr 3 ECKqpNrCKqrNp SE CKpqKqp *3.22 : CKpqKqp *3.22 : p/q, q/p CKpqKqp : CKqpKpq 4 ECKpqNrCKqrNp SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.2 12/29/2017 15:50:08 *4.2 Epp PROOF ABBREVIATION *3.2 p/Cpp, q/Cpp+C*2.08-C*2.08;*4.01 q/p;Prop PROOF 1 CpCqKpq *3.2 p/Cpp, q/Cpp 2 CCppCCppKCppCpp SUB 3 Cpp *2.08 (Id) 4 CCppKCppCpp MP: 2, 3 5 Cpp *2.08 (Id) 6 KCppCpp MP: 4, 5 Epq=KCpqCqp Df. *4.01 q/p Epp=KCppCpp Df. 7 Epp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.21 12/29/2017 15:50:08 *4.21 EEpqEqp PROOF ABBREVIATION *3.22 p/Cpq, q/Cqp+(1) *3.22 p/Cqp, q/Cpq+(2) *3.03 (1), (2)+*4.01;*4.01;(#1) (#1);*4.01 p/q, q/p;*4.01 p/q, q/p;(#2) (#2);*4.01 p/Epq, q/Eqp;Prop PROOF 1 CKpqKqp *3.22 p/Cpq, q/Cqp (1) 2 CKCpqCqpKCqpCpq SUB 3 CKpqKqp *3.22 p/Cqp, q/Cpq (2) 4 CKCqpCpqKCpqCqp SUB 5 KCKCpqCqpKCqpCpqCKCqpCpqKCpqCqp *3.03: 2, 4 Epq=KCpqCqp Df. *4.01 6 KCEpqKCqpCpqCKCqpCpqKCpqCqp REP Epq=KCpqCqp Df. *4.01 (#1) 7 KCEpqKCqpCpqCKCqpCpqEpq REP Epq=KCpqCqp Df. *4.01 p/q, q/p Eqp=KCqpCpq Df. 8 KCEpqEqpCKCqpCpqEpq REP Epq=KCpqCqp Df. *4.01 p/q, q/p Eqp=KCqpCpq Df. (#2) 9 KCEpqEqpCEqpEpq REP Epq=KCpqCqp Df. *4.01 p/Epq, q/Eqp EEpqEqp=KCEpqEqpCEqpEpq Df. 10 EEpqEqp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.22 12/29/2017 15:50:08 *4.22 CKEpqEqrEpr PROOF ABBREVIATION *2.06 p/KEpqEqr, q/Epq, r/Cpq+(1.1) *3.26 p/Epq, q/Eqr+(1.2) (1.1)+C(1.2)-(1.3) *3.26 p/Cpq, q/Cqp+*4.01;(1.4) (1.3)+C(1.4)-(1) *2.06 p/KEpqEqr, q/Eqr, r/Cqr+(2.1) *3.27 p/Epq, q/Eqr+(2.2) (2.1)+C(2.2)-(2.3) *3.26 p/Cqr, q/Crq+*4.01 p/q, q/r+(2.4) (2.3)+C(2.4)-(2) *2.83 p/KEpqEqr, q/p, r/q, s/r+C(1)-C(2)-(3) *2.06 p/KEpqEqr, q/Eqr, r/Crq+(4.1) *3.27 p/Epq, q/Eqr+(4.2) (4.1)+C(4.2)-(4.3) *3.27 p/Cqr, q/Crq+*4.01 p/q, q/r;(4.4) (4.3)+C(4.4)-(4) *2.06 p/KEpqEqr, q/Epq, r/Cqp+(5.1) *3.26 p/Epq, q/Eqr+(5.2) (5.1)+C(5.2)-(5.3) *3.27 p/Cpq, q/Cqp+*4.01;(5.4) (5.3)+C(5.4)-(5) *2.83 p/KEpqEqr, q/r, r/q, s/p+C(4)-C(5)-(6) *3.03 (3),(6)+(#1) *3.43 p/KEpqEqr, q/Cpr, r/Crp+C(#1);*4.01 q/r;Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/KEpqEqr, q/Epq, r/Cpq (1.1) 2 CCKEpqEqrEpqCCEpqCpqCKEpqEqrCpq SUB 3 CKpqp *3.26 (Simp) p/Epq, q/Eqr (1.2) 4 CKEpqEqrEpq SUB (1.3) 5 CCEpqCpqCKEpqEqrCpq MP: 2, 4 6 CKpqp *3.26 (Simp) p/Cpq, q/Cqp 7 CKCpqCqpCpq SUB Epq=KCpqCqp Df. *4.01 (1.4) 8 CEpqCpq REP (1) 9 CKEpqEqrCpq MP: 5, 8 10 CCpqCCqrCpr *2.06 (Syll) p/KEpqEqr, q/Eqr, r/Cqr (2.1) 11 CCKEpqEqrEqrCCEqrCqrCKEpqEqrCqr SUB 12 CKpqq *3.27 (Simp) p/Epq, q/Eqr (2.2) 13 CKEpqEqrEqr SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.22(CONT.) (2.3) 14 CCEqrCqrCKEpqEqrCqr MP: 11, 13 15 CKpqp *3.26 (Simp) p/Cqr, q/Crq 16 CKCqrCrqCqr SUB Epq=KCpqCqp Df. *4.01 p/q, q/r Eqr=KCqrCrq Df. (2.4) 17 CEqrCqr REP (2) 18 CKEpqEqrCqr MP: 14, 17 19 CCpCqrCCpCrsCpCqs *2.83 p/KEpqEqr, q/p, r/q, s/r 20 CCKEpqEqrCpqCCKEpqEqrCqrCKEpqEqrCpr SUB 21 CCKEpqEqrCqrCKEpqEqrCpr MP: 20, 9 (3) 22 CKEpqEqrCpr MP: 21, 18 23 CCpqCCqrCpr *2.06 (Syll) p/KEpqEqr, q/Eqr, r/Crq (4.1) 24 CCKEpqEqrEqrCCEqrCrqCKEpqEqrCrq SUB 25 CKpqq *3.27 (Simp) p/Epq, q/Eqr (4.2) 26 CKEpqEqrEqr SUB (4.3) 27 CCEqrCrqCKEpqEqrCrq MP: 24, 26 28 CKpqq *3.27 (Simp) p/Cqr, q/Crq 29 CKCqrCrqCrq SUB Epq=KCpqCqp Df. *4.01 p/q, q/r Eqr=KCqrCrq Df. (4.4) 30 CEqrCrq REP (4) 31 CKEpqEqrCrq MP: 27, 30 32 CCpqCCqrCpr *2.06 (Syll) p/KEpqEqr, q/Epq, r/Cqp (5.1) 33 CCKEpqEqrEpqCCEpqCqpCKEpqEqrCqp SUB 34 CKpqp *3.26 (Simp) p/Epq, q/Eqr (5.2) 35 CKEpqEqrEpq SUB (5.3) 36 CCEpqCqpCKEpqEqrCqp MP: 33, 35 37 CKpqq *3.27 (Simp) p/Cpq, q/Cqp 38 CKCpqCqpCqp SUB Epq=KCpqCqp Df. *4.01 (5.4) 39 CEpqCqp REP (5) 40 CKEpqEqrCqp MP: 36, 39 41 CCpCqrCCpCrsCpCqs *2.83 p/KEpqEqr, q/r, r/q, s/p 42 CCKEpqEqrCrqCCKEpqEqrCqpCKEpqEqrCrp SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.22(CONT.) 43 CCKEpqEqrCqpCKEpqEqrCrp MP: 42, 31 (6) 44 CKEpqEqrCrp MP: 43, 40 (#1) 45 KCKEpqEqrCprCKEpqEqrCrp *3.03: 22, 44 46 CKCpqCprCpKqr *3.43 (Comp) p/KEpqEqr, q/Cpr, r/Crp 47 CKCKEpqEqrCprCKEpqEqrCrpCKEpqEqrKCprCrp SUB 48 CKEpqEqrKCprCrp MP: 47, 45 Epq=KCpqCqp Df. *4.01 q/r Epr=KCprCrp Df. 49 CKEpqEqrEpr REP (#1) indicates the conjunction of (3) and (4). PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.24 12/29/2017 15:50:08 *4.24 EpKpp PROOF ABBREVIATION *3.26 q/p+(1) *2.43 q/Kpp+C*3.2 q/p+(2) *3.2 p/CpKpp, q/CKppp+C(2)-C(1);*4.01 q/Kpp;Prop PROOF 1 CKpqp *3.26 (Simp) q/p (1) 2 CKppp SUB 3 CCpCpqCpq *2.43 q/Kpp 4 CCpCpKppCpKpp SUB 5 CpCqKpq *3.2 q/p 6 CpCpKpp SUB (2) 7 CpKpp MP: 4, 6 8 CpCqKpq *3.2 p/CpKpp, q/CKppp 9 CCpKppCCKpppKCpKppCKppp SUB 10 CCKpppKCpKppCKppp MP: 9, 7 11 KCpKppCKppp MP: 10, 2 Epq=KCpqCqp Df. *4.01 q/Kpp EpKpp=KCpKppCKppp Df. 12 EpKpp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.25 12/29/2017 15:50:08 *4.25 EpApp PROOF ABBREVIATION *1.3 q/p+(1) *1.2+(2) *3.03 (1), (2)+*4.01 q/App;Prop PROOF 1 CqApq *1.3 (Add) q/p (1) 2 CpApp SUB (2) 3 CAppp *1.2 (Taut) 4 KCpAppCAppp *3.03: 2, 3 Epq=KCpqCqp Df. *4.01 q/App EpApp=KCpAppCAppp Df. 5 EpApp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.3 12/29/2017 15:50:08 *4.3 EKpqKqp PROOF ABBREVIATION *3.22+(1) (1) p/q, q/p+(2) *3.03 (1), (2)+*4.01 p/Kpq, q/Kqp;Prop PROOF (1) 1 CKpqKqp *3.22 p/q, q/p (2) 2 CKqpKpq SUB 3 KCKpqKqpCKqpKpq *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 p/Kpq, q/Kqp EKpqKqp=KCKpqKqpCKqpKpq Df. 4 EKpqKqp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.31 12/29/2017 15:50:08 *4.31 EApqAqp PROOF ABBREVIATION *1.4+(1) (1) p/q, q/p+(2) *3.03 (1), (2)+*4.01 p/Apq, q/Aqp;Prop PROOF (1) 1 CApqAqp *1.4 (Perm) p/q, q/p (2) 2 CAqpApq SUB 3 KCApqAqpCAqpApq *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 p/Apq, q/Aqp EApqAqp=KCApqAqpCAqpApq Df. 4 EApqAqp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.32 12/29/2017 15:50:08 *4.32 EKKpqrKpKqr PROOF ABBREVIATION *4.22 p/CKpqNr, q/CKqrNp, r/CpNKqr+(1.1) *4.15+(1.2) *4.12.1+(1.3) *3.03 (1.2), (1.3)+(1.4) (1.1)+C(1.4)-(1) *4.11 p/CKpqNr, q/CpNKqr+C(1)-(#1) (#1);*1.01 p/Kpq, q/Nr;*3.01 p/Kpq, q/r;(#2) (#2);*1.01 q/NKqr;*3.01 q/Kqr;Prop PROOF 1 CKEpqEqrEpr *4.22 p/CKpqNr, q/CKqrNp, r/CpNKqr (1.1) 2 CKECKpqNrCKqrNpECKqrNpCpNKqrECKpqNrCpNKqr SUB (1.2) 3 ECKpqNrCKqrNp *4.15 (1.3) 4 ECKqrNpCpNKqr *4.12.1 (1.4) 5 KECKpqNrCKqrNpECKqrNpCpNKqr *3.03: 3, 4 (1) 6 ECKpqNrCpNKqr MP: 2, 5 7 EEpqENpNq *4.11 (Transp) p/CKpqNr, q/CpNKqr 8 EECKpqNrCpNKqrENCKpqNrNCpNKqr SUB (#1) 9 ENCKpqNrNCpNKqr MP: 8, 6 Cpq=ANpq Df. *1.01 p/Kpq, q/Nr CKpqNr=ANKpqNr Df. 10 ENANKpqNrNCpNKqr REP Kpq=NANpNq Df. *3.01 p/Kpq, q/r KKpqr=NANKpqNr Df. (#2) 11 EKKpqrNCpNKqr REP Cpq=ANpq Df. *1.01 q/NKqr CpNKqr=ANpNKqr Df. 12 EKKpqrNANpNKqr REP Kpq=NANpNq Df. *3.01 q/Kqr KpKqr=NANpNKqr Df. 13 EKKpqrKpKqr REP Note the use of *4.12.1 here. First instance of “E” as a major corrective in an implication. The note at the end of the demonstration in PM expands to: *4.22 p/a, q/b, r/c+(1) THM+(2) THM+(3) *3.03 (2), (3)+(4) (1)+C(4)-(5) *4.22 p/a, q/c, r/d+(6) THM+(7) *3.03 (5), (7)+(8) (6)+C(8)-Prop PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.33 12/29/2017 15:50:08 *4.33 EAApqrApAqr PROOF ABBREVIATION *2.32+(1) *2.31+(2) *3.03 (1), (2);*4.01 p/AApqr, q/ApAqr;Prop PROOF (1) 1 CAApqrApAqr *2.32 (2) 2 CApAqrAApqr *2.31 3 KCAApqrApAqrCApAqrAApqr *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 p/AApqr, q/ApAqr EAApqrApAqr=KCAApqrApAqrCApAqrAApqr Df. 4 EAApqrApAqr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.36 12/29/2017 15:50:08 *4.36 CEpqEKprKqr PROOF ABBREVIATION *3.45+(1) (1) p/q, q/p+(2) *3.03 (1), (2)+(3) *3.47 p/Cpq, q/Cqp, r/CKprKqr, s/CKqrKpr+C(3)-(#1) (#1);*4.01;*4.01 p/Kpr, q/Kqr;Prop PROOF (1) 1 CCpqCKprKqr *3.45 (Fact) p/q, q/p (2) 2 CCqpCKqrKpr SUB (3) 3 KCCpqCKprKqrCCqpCKqrKpr *3.03: 1, 2 4 CKCprCqsCKpqKrs *3.47 p/Cpq, q/Cqp, r/CKprKqr, s/CKqrKpr 5 CKCCpqCKprKqrCCqpCKqrKprCKCpqCqpKCKprKqrCKqrKpr SUB (#1) 6 CKCpqCqpKCKprKqrCKqrKpr MP: 5, 3 Epq=KCpqCqp Df. *4.01 7 CEpqKCKprKqrCKqrKpr REP Epq=KCpqCqp Df. *4.01 p/Kpr, q/Kqr EKprKqr=KCKprKqrCKqrKpr Df. 8 CEpqEKprKqr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.37 12/29/2017 15:50:08 *4.37 CEpqEAprAqr PROOF ABBREVIATION *2.38 p/r, q/p, r/q+(1) *2.38 p/r, r/p+(2) *3.03 (1), (2)+(3) *3.47 p/Cpq, q/Cqp, r/CAprAqr, s/CAqrApr+C(3)-(#1) (#1)+*4.01;*4.01 p/Apr, q/Aqr;Prop PROOF 1 CCqrCAqpArp *2.38 p/r, q/p, r/q (1) 2 CCpqCAprAqr SUB 3 CCqrCAqpArp *2.38 p/r, r/p (2) 4 CCqpCAqrApr SUB (3) 5 KCCpqCAprAqrCCqpCAqrApr *3.03: 2, 4 6 CKCprCqsCKpqKrs *3.47 p/Cpq, q/Cqp, r/CAprAqr, s/CAqrApr 7 CKCCpqCAprAqrCCqpCAqrAprCKCpqCqpKCAprAqrCAqrApr SUB (#1) 8 CKCpqCqpKCAprAqrCAqrApr MP: 7, 5 Epq=KCpqCqp Df. *4.01 9 CEpqKCAprAqrCAqrApr REP Epq=KCpqCqp Df. *4.01 p/Apr, q/Aqr EAprAqr=KCAprAqrCAqrApr Df. 10 CEpqEAprAqr REP Here we take SUM to mean *2.38. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.38 12/29/2017 15:50:08 *4.38 CKEprEqsEKpqKrs PROOF ABBREVIATION *3.47+(1) (1) p/s, q/r, r/q, s/p+(2) *3.03 (1), (2)+(3) *3.47 p/KCprCqs, r/CKpqKrs, q/KCsqCrp, s/CKsrKqp+C(3)-(#1) (#1)+SE(*3.22 p/q, q/p:*3.22);SE(*3.22 p/s, q/r:*3.22 p/r, q/s);(#2) (#2)+*4.01 p/Kpq, q/Krs;SE(*4.32 p/Cpr, q/Cqs, r/KCsqCrp);(#3) (#3)+SE(*4.32 p/Cqs, q/Csq, r/Crp);(#4) (#4)+*4.01 p/q, q/s;SE(*3.22 p/Eqs, q/Crp:*3.22 p/Crp, q/Eqs);(#5) (#5)+SE(*4.32 p/Cpr, r/Eqs, q/Crp);*4.01 q/r;Prop PROOF (1) 1 CKCprCqsCKpqKrs *3.47 p/s, q/r, r/q, s/p (2) 2 CKCsqCrpCKsrKqp SUB (3) 3 KCKCprCqsCKpqKrsCKCsqCrpCKsrKqp *3.03: 1, 2 4 CKCprCqsCKpqKrs *3.47 p/KCprCqs, r/CKpqKrs, q/KCsqCrp, s/CKsrKqp 5 CKCKCprCqsCKpqKrsCKCsqCrpCKsrKqpCKKCprCqsKCsqCrpKCKpqKrsCKsrKqp SUB (#1) 6 CKKCprCqsKCsqCrpKCKpqKrsCKsrKqp MP: 5, 3 CKpqKqp *3.22 : CKpqKqp *3.22 p/q, q/p : CKqpKpq : CKpqKqp 7 CKKCprCqsKCsqCrpKCKpqKrsCKsrKpq SE CKpqKqp *3.22 : CKpqKqp *3.22 p/s, q/r : p/r, q/s CKsrKrs : CKrsKsr (#2) 8 CKKCprCqsKCsqCrpKCKpqKrsCKrsKpq SE Epq=KCpqCqp Df. *4.01 p/Kpq, q/Krs EKpqKrs=KCKpqKrsCKrsKpq Df. 9 CKKCprCqsKCsqCrpEKpqKrs REP EKKpqrKpKqr *4.32 p/Cpr, q/Cqs, r/KCsqCrp EKKCprCqsKCsqCrpKCprKCqsKCsqCrp (#3) 10 CKCprKCqsKCsqCrpEKpqKrs SE EKKpqrKpKqr *4.32 p/Cqs, q/Csq, r/Crp EKKCqsCsqCrpKCqsKCsqCrp (#4) 11 CKCprKKCqsCsqCrpEKpqKrs SE Epq=KCpqCqp Df. *4.01 p/q, q/s Eqs=KCqsCsq Df. 12 CKCprKEqsCrpEKpqKrs REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.38(CONT.) CKpqKqp *3.22 : CKpqKqp *3.22 p/Eqs, q/Crp : p/Crp, q/Eqs CKEqsCrpKCrpEqs : CKCrpEqsKEqsCrp (#5) 13 CKCprKCrpEqsEKpqKrs SE EKKpqrKpKqr *4.32 p/Cpr, r/Eqs, q/Crp EKKCprCrpEqsKCprKCrpEqs 14 CKKCprCrpEqsEKpqKrs SE Epq=KCpqCqp Df. *4.01 q/r Epr=KCprCrp Df. 15 CKEprEqsEKpqKrs REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.39 12/29/2017 15:50:08 *4.39 CKEprEqsEApqArs PROOF ABBREVIATION *4.39+Prop PROOF 1 CKEprEqsEApqArs *4.39 Don’t have a good proof yet of this proposition. In later proofs, such as *5.22, showed typos in the theorem. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.4 12/29/2017 15:50:08 *4.4 EKpAqrAKpqKpr PROOF ABBREVIATION *2.06 q/KCqKpqCrKpr, r/CAqrAKpqKpr+(1.1) *3.2+(#1) (#1) q/r, r/q+(#2) *3.03 (#1), (#2)-(#3) *3.43 q/CqKpq, r/CrKpr+C(#3)-(1.2) (1.1)+C(1.2)-(1.3) *3.48 p/q, q/r, r/Kpq, s/Kpr+(1.4) (1.3)+C(1.4)-(1) *3.31 q/Aqr, r/AKpqKpr+C(1)-(2) *3.26+(#5) (#5) q/r+(#6) *3.03 (#5), (#6)+(#7) *3.44 q/Kpq, r/Kpr+C(#7)-(3) *3.27+(#8) (#8) q/r+(#9) *3.03 (#8), (#9)+(#10) *3.48 p/Kpq, q/Kpr, r/q, s/r+C(#10)-(4) *3.03 (3), (4)+(#11) *3.43 p/AKpqKpr, q/p, r/Aqr+C(#11)-(5) *3.03 (2), (5)+*4.01 p/KpAqr, q/AKpqKpr-Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) q/KCqKpqCrKpr, r/CAqrAKpqKpr (1.1) 2 CCpKCqKpqCrKprCCKCqKpqCrKprCAqrAKpqKprCpCAqrAKpqKpr SUB (#1) 3 CpCqKpq *3.2 q/r, r/q (#2) 4 CpCrKpr SUB (#3) 5 KCpCqKpqCpCrKpr *3.03: 3, 4 6 CKCpqCprCpKqr *3.43 (Comp) q/CqKpq, r/CrKpr 7 CKCpCqKpqCpCrKprCpKCqKpqCrKpr SUB (1.2) 8 CpKCqKpqCrKpr MP: 7, 5 (1.3) 9 CCKCqKpqCrKprCAqrAKpqKprCpCAqrAKpqKpr MP: 2, 8 10 CKCprCqsCApqArs *3.48 p/q, q/r, r/Kpq, s/Kpr (1.4) 11 CKCqKpqCrKprCAqrAKpqKpr SUB (1) 12 CpCAqrAKpqKpr MP: 9, 11 13 CCpCqrCKpqr *3.31 (Imp) q/Aqr, r/AKpqKpr 14 CCpCAqrAKpqKprCKpAqrAKpqKpr SUB (2) 15 CKpAqrAKpqKpr MP: 14, 12 (#5) 16 CKpqp *3.26 (Simp) q/r (#6) 17 CKprp SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.4(CONT.) (#7) 18 KCKpqpCKprp *3.03: 16, 17 19 CKCqpCrpCAqrp *3.44 q/Kpq, r/Kpr 20 CKCKpqpCKprpCAKpqKprp SUB (3) 21 CAKpqKprp MP: 20, 18 (#8) 22 CKpqq *3.27 (Simp) q/r (#9) 23 CKprr SUB (#10) 24 KCKpqqCKprr *3.03: 22, 23 25 CKCprCqsCApqArs *3.48 p/Kpq, q/Kpr, r/q, s/r 26 CKCKpqqCKprrCAKpqKprAqr SUB (4) 27 CAKpqKprAqr MP: 26, 24 (#11) 28 KCAKpqKprpCAKpqKprAqr *3.03: 21, 27 29 CKCpqCprCpKqr *3.43 (Comp) p/AKpqKpr, q/p, r/Aqr 30 CKCAKpqKprpCAKpqKprAqrCAKpqKprKpAqr SUB (5) 31 CAKpqKprKpAqr MP: 30, 28 32 KCKpAqrAKpqKprCAKpqKprKpAqr *3.03: 15, 31 Epq=KCpqCqp Df. *4.01 p/KpAqr, q/AKpqKpr EKpAqrAKpqKpr=KCKpAqrAKpqKprCAKpqKprKpAqr Df. 33 EKpAqrAKpqKpr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.41 12/29/2017 15:50:08 *4.41 EApKqrKApqApr PROOF ABBREVIATION *1.6 q/Kqr, r/q+C*3.26 p/q, q/r-(1) *1.6 q/Kqr+C*3.27 p/q, q/r+(2) *3.03 (1), (2)+(#1) *3.43 p/ApKqr, q/Apq, r/Apr+C(#1)-(3) *2.06 p/KApqApr, q/KCNpqCNpr, r/CNpKqr+(4.1) *2.53+(#2) (#2) q/r+(#3) *3.03 (#2), (#3)+(#4) *3.47 p/Apq, q/Apr, r/CNpq, s/CNpr+C(#4)-(4.2) (4.1)+C(4.2)-(4.3) *3.43 p/Np+(4.4) (4.3)+C(4.4)-(4.5) *2.06 p/KApqApr, q/CNpKqr, r/ApKqr+(4.6) (4.6)+C(4.5)-(4.7) *2.54 q/Kqr+(4.8) (4.7)+C(4.8)-(4) *3.03 (3), (4)+*4.01 p/ApKqr, q/KApqApr;Prop PROOF 1 CCqrCApqApr *1.6 (Sum) q/Kqr, r/q 2 CCKqrqCApKqrApq SUB 3 CKpqp *3.26 (Simp) p/q, q/r 4 CKqrq SUB (1) 5 CApKqrApq MP: 2, 4 6 CCqrCApqApr *1.6 (Sum) q/Kqr 7 CCKqrrCApKqrApr SUB 8 CKpqq *3.27 (Simp) p/q, q/r 9 CKqrr SUB (2) 10 CApKqrApr MP: 7, 9 (#1) 11 KCApKqrApqCApKqrApr *3.03: 5, 10 12 CKCpqCprCpKqr *3.43 (Comp) p/ApKqr, q/Apq, r/Apr 13 CKCApKqrApqCApKqrAprCApKqrKApqApr SUB (3) 14 CApKqrKApqApr MP: 13, 11 15 CCpqCCqrCpr *2.06 (Syll) p/KApqApr, q/KCNpqCNpr, r/CNpKqr (4.1) 16 CCKApqAprKCNpqCNprCCKCNpqCNprCNpKqrCKApqAprCNpKqr SUB (#2) 17 CApqCNpq *2.53 q/r (#3) 18 CAprCNpr SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.41(CONT.) (#4) 19 KCApqCNpqCAprCNpr *3.03: 17, 18 20 CKCprCqsCKpqKrs *3.47 p/Apq, q/Apr, r/CNpq, s/CNpr 21 CKCApqCNpqCAprCNprCKApqAprKCNpqCNpr SUB (4.2) 22 CKApqAprKCNpqCNpr MP: 21, 19 (4.3) 23 CCKCNpqCNprCNpKqrCKApqAprCNpKqr MP: 16, 22 24 CKCpqCprCpKqr *3.43 (Comp) p/Np (4.4) 25 CKCNpqCNprCNpKqr SUB (4.5) 26 CKApqAprCNpKqr MP: 23, 25 27 CCpqCCqrCpr *2.06 (Syll) p/KApqApr, q/CNpKqr, r/ApKqr (4.6) 28 CCKApqAprCNpKqrCCCNpKqrApKqrCKApqAprApKqr SUB (4.7) 29 CCCNpKqrApKqrCKApqAprApKqr MP: 28, 26 30 CCNpqApq *2.54 q/Kqr (4.8) 31 CCNpKqrApKqr SUB (4) 32 CKApqAprApKqr MP: 29, 31 33 KCApKqrKApqAprCKApqAprApKqr *3.03: 14, 32 Epq=KCpqCqp Df. *4.01 p/ApKqr, q/KApqApr EApKqrKApqApr=KCApKqrKApqAprCKApqAprApKqr Df. 34 EApKqrKApqApr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.42 12/29/2017 15:50:08 *4.42 EpAKpqKpNq PROOF ABBREVIATION *3.21 q/AqNq+C*2.11 p/q-(1) *3.26 q/AqNq+(2) *4.22 q/KpAqNq, r/AKpqKpNq+(3.1) *3.03 (1), (2)+*4.01 q/KpAqNq;(3.2) *4.4 r/Nq+(3.3) *3.03 (3.2), (3.3)+(3.4) (3.1)+C(3.4)-Prop PROOF 1 CqCpKpq *3.21 q/AqNq 2 CAqNqCpKpAqNq SUB 3 ApNp *2.11 p/q 4 AqNq SUB (1) 5 CpKpAqNq MP: 2, 4 6 CKpqp *3.26 (Simp) q/AqNq (2) 7 CKpAqNqp SUB 8 CKEpqEqrEpr *4.22 q/KpAqNq, r/AKpqKpNq (3.1) 9 CKEpKpAqNqEKpAqNqAKpqKpNqEpAKpqKpNq SUB 10 KCpKpAqNqCKpAqNqp *3.03: 5, 7 Epq=KCpqCqp Df. *4.01 q/KpAqNq EpKpAqNq=KCpKpAqNqCKpAqNqp Df. (3.2) 11 EpKpAqNq REP 12 EKpAqrAKpqKpr *4.4 r/Nq (3.3) 13 EKpAqNqAKpqKpNq SUB (3.4) 14 KEpKpAqNqEKpAqNqAKpqKpNq *3.03: 11, 13 15 EpAKpqKpNq MP: 9, 14 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.43.0 12/29/2017 15:50:08 *4.43.0 CCKCNpqCNpNqpCKApqApNqp PROOF ABBREVIATION *4.43.0+Prop PROOF 1 CCKCNpqCNpNqpCKApqApNqp *4.43.0 This is here to make *4.43 work PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.43 12/29/2017 15:50:08 *4.43 EpKApqApNq PROOF ABBREVIATION *2.2+(#1) (#1) q/Nq+(#2) *3.03 (#1), (#2)+(#3) *3.43 q/Apq, r/ApNq+C(#3)-(1) *2.65 p/Np+SE(*2.14:*2.12);(#4) *3.31 p/CNpq, q/CNpNq, r/p+C(#4)-(#5) *4.43.0+C(#5)-(2) *3.03 (1), (2)+*4.01 q/KApqApNq;Prop PROOF (#1) 1 CpApq *2.2 q/Nq (#2) 2 CpApNq SUB (#3) 3 KCpApqCpApNq *3.03: 1, 2 4 CKCpqCprCpKqr *3.43 (Comp) q/Apq, r/ApNq 5 CKCpApqCpApNqCpKApqApNq SUB (1) 6 CpKApqApNq MP: 5, 3 7 CCpqCCpNqNp *2.65 p/Np 8 CCNpqCCNpNqNNp SUB CNNpp *2.14 : CpNNp *2.12 (#4) 9 CCNpqCCNpNqp SE 10 CCpCqrCKpqr *3.31 (Imp) p/CNpq, q/CNpNq, r/p 11 CCCNpqCCNpNqpCKCNpqCNpNqp SUB (#5) 12 CKCNpqCNpNqp MP: 11, 9 13 CCKCNpqCNpNqpCKApqApNqp *4.43.0 (2) 14 CKApqApNqp MP: 13, 12 15 KCpKApqApNqCKApqApNqp *3.03: 6, 14 Epq=KCpqCqp Df. *4.01 q/KApqApNq EpKApqApNq=KCpKApqApNqCKApqApNqp Df. 16 EpKApqApNq REP Note the use of *4.43.0 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.44 12/29/2017 15:50:08 *4.44 EpApKpq PROOF ABBREVIATION *2.2 q/Kpq+(1) *2.08+(#1) *3.26+(#2) *3.03 (#1), (#2)+(#3) *3.44 q/p, r/Kpq+C(#3)-(2) *3.03 (1), (2)+*4.01 q/ApKpq;Prop PROOF 1 CpApq *2.2 q/Kpq (1) 2 CpApKpq SUB (#1) 3 Cpp *2.08 (Id) (#2) 4 CKpqp *3.26 (Simp) (#3) 5 KCppCKpqp *3.03: 3, 4 6 CKCqpCrpCAqrp *3.44 q/p, r/Kpq 7 CKCppCKpqpCApKpqp SUB (2) 8 CApKpqp MP: 7, 5 9 KCpApKpqCApKpqp *3.03: 2, 8 Epq=KCpqCqp Df. *4.01 q/ApKpq EpApKpq=KCpApKpqCApKpqp Df. 10 EpApKpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.45 12/29/2017 15:50:08 *4.45 EpKpApq PROOF ABBREVIATION *3.26 q/Apq+(1) *2.2 q/Kpq+SE(*4.41 q/p, r/q);SE(*4.25);(2) *3.03 (2), (1)+*4.01 q/KpApq;Prop PROOF 1 CKpqp *3.26 (Simp) q/Apq (1) 2 CKpApqp SUB 3 CpApq *2.2 q/Kpq 4 CpApKpq SUB EApKqrKApqApr *4.41 q/p, r/q EApKpqKAppApq 5 CpKAppApq SE EpApp *4.25 (2) 6 CpKpApq SE 7 KCpKpApqCKpApqp *3.03: 6, 2 Epq=KCpqCqp Df. *4.01 q/KpApq EpKpApq=KCpKpApqCKpApqp Df. 8 EpKpApq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.5 12/29/2017 15:50:08 *4.5 EKpqNANpNq PROOF ABBREVIATION *4.2 p/Kpq+*3.01 II;Prop PROOF 1 Epp *4.2 p/Kpq 2 EKpqKpq SUB Kpq=NANpNq Df. *3.01 3 EKpqNANpNq REP II PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.51 12/29/2017 15:50:08 *4.51 ENKpqANpNq PROOF ABBREVIATION *4.5+SE(*4.12 p/Kpq, q/ANpNq);SE(*4.21 p/ANpNq, q/NKpq);Prop PROOF 1 EKpqNANpNq *4.5 EEpNqEqNp *4.12 p/Kpq, q/ANpNq EEKpqNANpNqEANpNqNKpq 2 EANpNqNKpq SE EEpqEqp *4.21 p/ANpNq, q/NKpq EEANpNqNKpqENKpqANpNq 3 ENKpqANpNq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.52 12/29/2017 15:50:08 *4.52 EKpNqNANpq PROOF ABBREVIATION *4.5 q/Nq+SE(*4.13 p/q);Prop PROOF 1 EKpqNANpNq *4.5 q/Nq 2 EKpNqNANpNNq SUB EpNNp *4.13 p/q EqNNq 3 EKpNqNANpq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.53 12/29/2017 15:50:08 *4.53 ENKpNqANpq PROOF ABBREVIATION *4.52+SE(*4.12 p/KpNq, q/ANpq);SE(*4.21 p/ANpq, q/NKpNq);Prop PROOF 1 EKpNqNANpq *4.52 EEpNqEqNp *4.12 p/KpNq, q/ANpq EEKpNqNANpqEANpqNKpNq 2 EANpqNKpNq SE EEpqEqp *4.21 p/ANpq, q/NKpNq EEANpqNKpNqENKpNqANpq 3 ENKpNqANpq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.54 12/29/2017 15:50:08 *4.54 EKNpqNApNq PROOF ABBREVIATION *4.5 p/Np+SE(*4.13);Prop PROOF 1 EKpqNANpNq *4.5 p/Np 2 EKNpqNANNpNq SUB EpNNp *4.13 3 EKNpqNApNq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.55 12/29/2017 15:50:08 *4.55 ENKNpqApNq PROOF ABBREVIATION *4.54+SE(*4.12 p/KNpq, q/ApNq);SE(*4.21 p/ApNq, q/NKNpq);Prop PROOF 1 EKNpqNApNq *4.54 EEpNqEqNp *4.12 p/KNpq, q/ApNq EEKNpqNApNqEApNqNKNpq 2 EApNqNKNpq SE EEpqEqp *4.21 p/ApNq, q/NKNpq EEApNqNKNpqENKNpqApNq 3 ENKNpqApNq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.56 12/29/2017 15:50:08 *4.56 EKNpNqNApq PROOF ABBREVIATION *4.54 q/Nq+SE(*4.13 p/q);Prop PROOF 1 EKNpqNApNq *4.54 q/Nq 2 EKNpNqNApNNq SUB EpNNp *4.13 p/q EqNNq 3 EKNpNqNApq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.57 12/29/2017 15:50:08 *4.57 ENKNpNqApq PROOF ABBREVIATION *4.56+SE(*4.12 p/KNpNq, q/Apq);SE(*4.21 p/Apq, q/NKNpNq);Prop PROOF 1 EKNpNqNApq *4.56 EEpNqEqNp *4.12 p/KNpNq, q/Apq EEKNpNqNApqEApqNKNpNq 2 EApqNKNpNq SE EEpqEqp *4.21 p/Apq, q/NKNpNq EEApqNKNpNqENKNpNqApq 3 ENKNpNqApq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.6 12/29/2017 15:50:08 *4.6 ECpqANpq PROOF ABBREVIATION *4.2 p/Cpq+*1.01 II;Prop PROOF 1 Epp *4.2 p/Cpq 2 ECpqCpq SUB Cpq=ANpq Df. *1.01 3 ECpqANpq REP II PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.61 12/29/2017 15:50:08 *4.61 ENCpqKpNq PROOF ABBREVIATION *4.6+SE(*4.11 p/Cpq, q/ANpq);SE(*4.52);Prop PROOF 1 ECpqANpq *4.6 EEpqENpNq *4.11 p/Cpq, q/ANpq EECpqANpqENCpqNANpq 2 ENCpqNANpq SE EKpNqNANpq *4.52 3 ENCpqKpNq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.62 12/29/2017 15:50:08 *4.62 ECpNqANpNq PROOF ABBREVIATION *4.6 q/Nq+Prop PROOF 1 ECpqANpq *4.6 q/Nq 2 ECpNqANpNq SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.63 12/29/2017 15:50:08 *4.63 ENCpNqKpq PROOF ABBREVIATION *4.62+SE(*4.11 p/CpNq, q/ANpNq);SE(*4.5);Prop PROOF 1 ECpNqANpNq *4.62 EEpqENpNq *4.11 p/CpNq, q/ANpNq EECpNqANpNqENCpNqNANpNq 2 ENCpNqNANpNq SE EKpqNANpNq *4.5 3 ENCpNqKpq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.64 12/29/2017 15:50:08 *4.64 ECNpqApq PROOF ABBREVIATION *2.54+(1) *2.53+(2) *3.03 (1), (2)+*4.01 p/CNpq, q/Apq;Prop PROOF (1) 1 CCNpqApq *2.54 (2) 2 CApqCNpq *2.53 3 KCCNpqApqCApqCNpq *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 p/CNpq, q/Apq ECNpqApq=KCCNpqApqCApqCNpq Df. 4 ECNpqApq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.65 12/29/2017 15:50:08 *4.65 ENCNpqKNpNq PROOF ABBREVIATION *4.64+SE(*4.11 p/CNpq, q/Apq);SE(*4.56);Prop PROOF 1 ECNpqApq *4.64 EEpqENpNq *4.11 p/CNpq, q/Apq EECNpqApqENCNpqNApq 2 ENCNpqNApq SE EKNpNqNApq *4.56 3 ENCNpqKNpNq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.66 12/29/2017 15:50:08 *4.66 ECNpNqApNq PROOF ABBREVIATION *4.64 q/Nq+Prop PROOF 1 ECNpqApq *4.64 q/Nq 2 ECNpNqApNq SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.68 12/29/2017 15:50:08 *4.68 ECNpNqApNq PROOF ABBREVIATION *4.64 q/Nq+Prop PROOF 1 ECNpqApq *4.64 q/Nq 2 ECNpNqApNq SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.67 12/29/2017 15:50:08 *4.67 ENCNpNqKNpq PROOF ABBREVIATION *4.66+SE(*4.11 p/CNpNq, q/ApNq);SE(*4.54);Prop PROOF 1 ECNpNqApNq *4.66 EEpqENpNq *4.11 p/CNpNq, q/ApNq EECNpNqApNqENCNpNqNApNq 2 ENCNpNqNApNq SE EKNpqNApNq *4.54 3 ENCNpNqKNpq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.7 12/29/2017 15:50:08 *4.7 ECpqCpKpq PROOF ABBREVIATION *2.05 q/Kpq, r/q+C*3.27-(1) *3.3 p/Cpp, q/Cpq, r/CpKpq+C*3.43 q/p, r/q-C*2.08-(2) *3.03 (2), (1)+*4.01 p/Cpq, q/CpKpq;Prop PROOF 1 CCqrCCpqCpr *2.05 (Syll) q/Kpq, r/q 2 CCKpqqCCpKpqCpq SUB 3 CKpqq *3.27 (Simp) (1) 4 CCpKpqCpq MP: 2, 3 5 CCKpqrCpCqr *3.3 (Exp) p/Cpp, q/Cpq, r/CpKpq 6 CCKCppCpqCpKpqCCppCCpqCpKpq SUB 7 CKCpqCprCpKqr *3.43 (Comp) q/p, r/q 8 CKCppCpqCpKpq SUB 9 CCppCCpqCpKpq MP: 6, 8 10 Cpp *2.08 (Id) (2) 11 CCpqCpKpq MP: 9, 10 12 KCCpqCpKpqCCpKpqCpq *3.03: 11, 4 Epq=KCpqCqp Df. *4.01 p/Cpq, q/CpKpq ECpqCpKpq=KCCpqCpKpqCCpKpqCpq Df. 13 ECpqCpKpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.71 12/29/2017 15:50:08 *4.71 ECpqEpKpq PROOF ABBREVIATION *3.21 p/CpKpq, q/CKpqp+*4.01 q/Kpq;(#1) *3.26.1+C(#1)-(1) *3.26 p/CpKpq, q/CKpqp+*4.01 q/Kpq;(2) *3.03 (1), (2)+*4.01 p/CpKpq, q/EpKpq;(3) *4.7+(4) *3.03 (4), (3)+(#2) *4.22 p/Cpq, q/CpKpq, r/EpKpq+C(#2)-Prop PROOF 1 CqCpKpq *3.21 p/CpKpq, q/CKpqp 2 CCKpqpCCpKpqKCpKpqCKpqp SUB Epq=KCpqCqp Df. *4.01 q/Kpq EpKpq=KCpKpqCKpqp Df. (#1) 3 CCKpqpCCpKpqEpKpq REP 4 CCCKpqpCCpKpqEpKpqCCpKpqEpKpq *3.26.1 (1) 5 CCpKpqEpKpq MP: 4, 3 6 CKpqp *3.26 (Simp) p/CpKpq, q/CKpqp 7 CKCpKpqCKpqpCpKpq SUB Epq=KCpqCqp Df. *4.01 q/Kpq EpKpq=KCpKpqCKpqp Df. (2) 8 CEpKpqCpKpq REP 9 KCCpKpqEpKpqCEpKpqCpKpq *3.03: 5, 8 Epq=KCpqCqp Df. *4.01 p/CpKpq, q/EpKpq ECpKpqEpKpq=KCCpKpqEpKpqCEpKpqCpKpq Df. (3) 10 ECpKpqEpKpq REP (4) 11 ECpqCpKpq *4.7 (#2) 12 KECpqCpKpqECpKpqEpKpq *3.03: 11, 10 13 CKEpqEqrEpr *4.22 p/Cpq, q/CpKpq, r/EpKpq 14 CKECpqCpKpqECpKpqEpKpqECpqEpKpq SUB 15 ECpqEpKpq MP: 14, 12 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.72 12/29/2017 15:50:08 *4.72 ECpqEqApq PROOF ABBREVIATION *4.22 p/Cpq, q/CNqNp, r/ENqKNqNp+(1) *4.1+(2) *4.71 p/Nq, q/Np+(3) *3.03 (2), (3)+(4) (1)+C(4)-(5) *4.22 p/Cpq, q/ENqKNqNp, r/EqNKNqNp+(6) *4.12 p/KNqNp+SE(*4.21 p/KNqNp, q/Nq)+(7) *3.03 (5), (7)+(8) (6)+C(8)-(9) *4.22 p/Cpq, q/EqNKNqNp, r/EqAqp+(10) *4.21 p/q, q/NKNqNp+SE(*4.57 p/q, q/p)+(11) *3.03 (9), (11)+(12) (10)+C(12)-(13) *4.22 p/Cpq, q/EqAqp, r/EqApq+(14) *4.21 p/q, q/Aqp+SE(*4.31);(15) *3.03 (13), (15)+(16) (14)+C(16)-Prop PROOF 1 CKEpqEqrEpr *4.22 p/Cpq, q/CNqNp, r/ENqKNqNp (1) 2 CKECpqCNqNpECNqNpENqKNqNpECpqENqKNqNp SUB (2) 3 ECpqCNqNp *4.1 4 ECpqEpKpq *4.71 p/Nq, q/Np (3) 5 ECNqNpENqKNqNp SUB (4) 6 KECpqCNqNpECNqNpENqKNqNp *3.03: 3, 5 (5) 7 ECpqENqKNqNp MP: 2, 6 8 CKEpqEqrEpr *4.22 p/Cpq, q/ENqKNqNp, r/EqNKNqNp (6) 9 CKECpqENqKNqNpEENqKNqNpEqNKNqNpECpqEqNKNqNp SUB 10 EEpNqEqNp *4.12 p/KNqNp 11 EEKNqNpNqEqNKNqNp SUB EEpqEqp *4.21 p/KNqNp, q/Nq EEKNqNpNqENqKNqNp (7) 12 EENqKNqNpEqNKNqNp SE (8) 13 KECpqENqKNqNpEENqKNqNpEqNKNqNp *3.03: 7, 12 (9) 14 ECpqEqNKNqNp MP: 9, 13 15 CKEpqEqrEpr *4.22 p/Cpq, q/EqNKNqNp, r/EqAqp (10) 16 CKECpqEqNKNqNpEEqNKNqNpEqAqpECpqEqAqp SUB 17 EEpqEqp *4.21 p/q, q/NKNqNp 18 EEqNKNqNpENKNqNpq SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.72(CONT.) ENKNpNqApq *4.57 p/q, q/p ENKNqNpAqp (11) 19 EEqAqpENKNqNpq SE (12) 20 KECpqEqNKNqNpEEqAqpENKNqNpq *3.03: 14, 19 ************************************************************ MODUS PONENS ERROR ST. NUM IS 296 IMP_NUM IS 1 LINE[IMP_NUM] IS CKEpqEqrEpr ANT_NUM IS 20 LINE[ANT_NUM] IS KECpqEqNKNqNpEEqAqpENKNqNpq The original notes said there is a problem with this proof. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.73 12/29/2017 15:50:08 *4.73 CqEpKpq PROOF ABBREVIATION *2.02+(1) *4.71+DE;(2) *2.06 p/q, q/Cpq, r/EpKpq+C(1)-C(2)-Prop PROOF (1) 1 CqCpq *2.02 (Simp) 2 ECpqEpKpq *4.71 (2) 3 CCpqEpKpq DE 4 CCpqCCqrCpr *2.06 (Syll) p/q, q/Cpq, r/EpKpq 5 CCqCpqCCCpqEpKpqCqEpKpq SUB 6 CCCpqEpKpqCqEpKpq MP: 5, 1 7 CqEpKpq MP: 6, 3 This uses “DE”. I don’t recall having used this before. This proof might not work. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.74 12/29/2017 15:50:08 *4.74 CNpEqApq PROOF ABBREVIATION *2.21+(1) *4.72+DE;(2) *2.06 p/Np, q/Cpq, r/EqApq+C(1)-C(2)-Prop PROOF (1) 1 CNpCpq *2.21 2 ECpqEqApq *4.72 (2) 3 CCpqEqApq DE 4 CCpqCCqrCpr *2.06 (Syll) p/Np, q/Cpq, r/EqApq 5 CCNpCpqCCCpqEqApqCNpEqApq SUB 6 CCCpqEqApqCNpEqApq MP: 5, 1 7 CNpEqApq MP: 6, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.76 12/29/2017 15:50:08 *4.76 EKCpqCprCpKqr PROOF ABBREVIATION *4.41 p/Np+*1.01 q/Kqr;*1.01;*1.01 q/r;(#1) (#1)+SE(*4.21 p/CpKqr, q/KCpqCpr);Prop PROOF 1 EApKqrKApqApr *4.41 p/Np 2 EANpKqrKANpqANpr SUB Cpq=ANpq Df. *1.01 q/Kqr CpKqr=ANpKqr Df. 3 ECpKqrKANpqANpr REP Cpq=ANpq Df. *1.01 4 ECpKqrKCpqANpr REP Cpq=ANpq Df. *1.01 q/r Cpr=ANpr Df. (#1) 5 ECpKqrKCpqCpr REP EEpqEqp *4.21 p/CpKqr, q/KCpqCpr EECpKqrKCpqCprEKCpqCprCpKqr 6 EKCpqCprCpKqr SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.77.0 12/29/2017 15:50:08 *4.77.0 CCAqrpKCqpCrp PROOF ABBREVIATION *4.77.0+Prop PROOF 1 CCAqrpKCqpCrp *4.77.0 This is used in *4.77. The problem here is to get CCAqrpKCqpCrp from *1.3 and *2.2. This proof is the same as *5.77 in TI. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.77 12/29/2017 15:50:08 *4.77 EKCqpCrpCAqrp PROOF ABBREVIATION *3.44+(1) *4.77.0+(2) *3.03 (1), (2)+*4.01 p/KCqpCrp, q/CAqrp;Prop PROOF (1) 1 CKCqpCrpCAqrp *3.44 (2) 2 CCAqrpKCqpCrp *4.77.0 3 KCKCqpCrpCAqrpCCAqrpKCqpCrp *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 p/KCqpCrp, q/CAqrp EKCqpCrpCAqrp=KCKCqpCrpCAqrpCCAqrpKCqpCrp Df. 4 EKCqpCrpCAqrp REP Note the use of *4.77.0. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.77.1 12/29/2017 15:50:08 *4.77.1 CCAqrpCrp PROOF ABBREVIATION *4.77.1+Prop PROOF 1 CCAqrpCrp *4.77.1 This is here for *5.75 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.78.0 12/29/2017 15:50:08 *4.78.0 EANpAAqNprANpAANpqr PROOF ABBREVIATION *4.78.0+Prop PROOF 1 EANpAAqNprANpAANpqr *4.78.0 This is to come from *4.31 and *4.37 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.78.01 12/29/2017 15:50:08 *4.78.01 EAANpNpAqrANpAqr PROOF ABBREVIATION *4.78.01+Prop PROOF 1 EAANpNpAqrANpAqr *4.78.01 This is to come from *4.25 and *4.37 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.78 12/29/2017 15:50:08 *4.78 EACpqCprCpAqr PROOF ABBREVIATION *4.22 p/ACpqCpr, q/AANpqANpr, r/ANpAAqNpr+(1) *4.2 p/AANpqANpr+*1.01;*1.01 q/r+(2) *4.33 p/Np, r/ANpr+SE(*4.33 p/q, q/Np)+(3) *3.03 (2), (3)+(4) (1)+C(4)-(5) *4.22 p/ACpqCpr, q/ANpAAqNpr, r/ANpAANpqr+(6) *4.78.0+(7) *3.03 (5), (7)+(8) (6)+C(8)-(9) *4.22 p/ACpqCpr, q/ANpAANpqr, r/AANpNpAqr-(10) *4.33 p/Np, q/ANpq+SE(*4.21 p/AANpANpqr, q/ANpAANpqr);(#1) (#1);SE(*4.33 p/Np, q/Np, r/q);SE(*4.33 p/ANpNp);(11) *3.03 (9), (11)+(12) (10)+C(12)-(13) *4.22 p/ACpqCpr, q/AANpNpAqr, r/ANpAqr-(14) *4.78.01-(15) *3.03 (13), (15)+(16) (14)+C(16)-(17) *4.22 p/ACpqCpr, q/ANpAqr, r/CpAqr-(18) *4.2 p/CpAqr+*1.01 q/Aqr;(19) *3.03 (17), (19)-(20) (18)+C(20)-Prop PROOF 1 CKEpqEqrEpr *4.22 p/ACpqCpr, q/AANpqANpr, r/ANpAAqNpr (1) 2 CKEACpqCprAANpqANprEAANpqANprANpAAqNprEACpqCprANpAAqNpr SUB 3 Epp *4.2 p/AANpqANpr 4 EAANpqANprAANpqANpr SUB Cpq=ANpq Df. *1.01 5 EACpqANprAANpqANpr REP Cpq=ANpq Df. *1.01 q/r Cpr=ANpr Df. (2) 6 EACpqCprAANpqANpr REP 7 EAApqrApAqr *4.33 p/Np, r/ANpr 8 EAANpqANprANpAqANpr SUB EAApqrApAqr *4.33 p/q, q/Np EAAqNprAqANpr (3) 9 EAANpqANprANpAAqNpr SE (4) 10 KEACpqCprAANpqANprEAANpqANprANpAAqNpr *3.03: 6, 9 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.78(CONT.) (5) 11 EACpqCprANpAAqNpr MP: 2, 10 12 CKEpqEqrEpr *4.22 p/ACpqCpr, q/ANpAAqNpr, r/ANpAANpqr (6) 13 CKEACpqCprANpAAqNprEANpAAqNprANpAANpqrEACpqCprANpAANpqr SUB (7) 14 EANpAAqNprANpAANpqr *4.78.0 (8) 15 KEACpqCprANpAAqNprEANpAAqNprANpAANpqr *3.03: 11, 14 (9) 16 EACpqCprANpAANpqr MP: 13, 15 17 CKEpqEqrEpr *4.22 p/ACpqCpr, q/ANpAANpqr, r/AANpNpAqr (10) 18 CKEACpqCprANpAANpqrEANpAANpqrAANpNpAqrEACpqCprAANpNpAqr SUB 19 EAApqrApAqr *4.33 p/Np, q/ANpq 20 EAANpANpqrANpAANpqr SUB EEpqEqp *4.21 p/AANpANpqr, q/ANpAANpqr EEAANpANpqrANpAANpqrEANpAANpqrAANpANpqr (#1) 21 EANpAANpqrAANpANpqr SE EAApqrApAqr *4.33 p/Np, q/Np, r/q EAANpNpqANpANpq 22 EANpAANpqrAAANpNpqr SE EAApqrApAqr *4.33 p/ANpNp EAAANpNpqrAANpNpAqr (11) 23 EANpAANpqrAANpNpAqr SE (12) 24 KEACpqCprANpAANpqrEANpAANpqrAANpNpAqr *3.03: 16, 23 (13) 25 EACpqCprAANpNpAqr MP: 18, 24 26 CKEpqEqrEpr *4.22 p/ACpqCpr, q/AANpNpAqr, r/ANpAqr (14) 27 CKEACpqCprAANpNpAqrEAANpNpAqrANpAqrEACpqCprANpAqr SUB (15) 28 EAANpNpAqrANpAqr *4.78.01 (16) 29 KEACpqCprAANpNpAqrEAANpNpAqrANpAqr *3.03: 25, 28 (17) 30 EACpqCprANpAqr MP: 27, 29 31 CKEpqEqrEpr *4.22 p/ACpqCpr, q/ANpAqr, r/CpAqr (18) 32 CKEACpqCprANpAqrEANpAqrCpAqrEACpqCprCpAqr SUB 33 Epp *4.2 p/CpAqr 34 ECpAqrCpAqr SUB Cpq=ANpq Df. *1.01 q/Aqr CpAqr=ANpAqr Df. (19) 35 EANpAqrCpAqr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.78(CONT.) (20) 36 KEACpqCprANpAqrEANpAqrCpAqr *3.03: 30, 35 37 EACpqCprCpAqr MP: 32, 36 Note the use of *4.78.0. Note the use of *4.78.01. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.79 12/29/2017 15:50:08 *4.79 EACqpCrpCKqrp PROOF ABBREVIATION *4.79+Prop PROOF 1 EACqpCrpCKqrp *4.79 Need to work on this proof. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.8 12/29/2017 15:50:08 *4.8 ECpNpNp PROOF ABBREVIATION *2.01+(1) *2.02 q/Np+(2) *3.03 (1), (2)+*4.01 p/CpNp, q/Np;Prop PROOF (1) 1 CCpNpNp *2.01 (Abs) 2 CqCpq *2.02 (Simp) q/Np (2) 3 CNpCpNp SUB 4 KCCpNpNpCNpCpNp *3.03: 1, 3 Epq=KCpqCqp Df. *4.01 p/CpNp, q/Np ECpNpNp=KCCpNpNpCNpCpNp Df. 5 ECpNpNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.81 12/29/2017 15:50:08 *4.81 ECNppp PROOF ABBREVIATION *2.18+(1) *2.02 q/p, p/Np+(2) *3.03 (1), (2)+*4.01 p/CNpp, q/p;Prop PROOF (1) 1 CCNppp *2.18 2 CqCpq *2.02 (Simp) q/p, p/Np (2) 3 CpCNpp SUB 4 KCCNpppCpCNpp *3.03: 1, 3 Epq=KCpqCqp Df. *4.01 p/CNpp, q/p ECNppp=KCCNpppCpCNpp Df. 5 ECNppp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.82 12/29/2017 15:50:08 *4.82 EKCpqCpNqNp PROOF ABBREVIATION *3.31 p/Cpq, q/CpNq, r/Np+C*2.65-(1) *2.21+(2) *2.21 q/Nq+(3) *3.03 (2), (3)+(4) *3.43 p/Np, q/Cpq, r/CpNq+C(4)-(5) *3.03 (1), (5)+*4.01 p/KCpqCpNq, q/Np;Prop PROOF 1 CCpCqrCKpqr *3.31 (Imp) p/Cpq, q/CpNq, r/Np 2 CCCpqCCpNqNpCKCpqCpNqNp SUB 3 CCpqCCpNqNp *2.65 (1) 4 CKCpqCpNqNp MP: 2, 3 (2) 5 CNpCpq *2.21 6 CNpCpq *2.21 q/Nq (3) 7 CNpCpNq SUB (4) 8 KCNpCpqCNpCpNq *3.03: 6, 7 9 CKCpqCprCpKqr *3.43 (Comp) p/Np, q/Cpq, r/CpNq 10 CKCNpCpqCNpCpNqCNpKCpqCpNq SUB (5) 11 CNpKCpqCpNq MP: 10, 8 12 KCKCpqCpNqNpCNpKCpqCpNq *3.03: 4, 11 Epq=KCpqCqp Df. *4.01 p/KCpqCpNq, q/Np EKCpqCpNqNp=KCKCpqCpNqNpCNpKCpqCpNq Df. 13 EKCpqCpNqNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.83 12/29/2017 15:50:08 *4.83 EKCpqCNpqq PROOF ABBREVIATION *3.31 p/Cpq, q/CNpq, r/q+C*2.61-(1) *2.02+(2) *2.02 p/Np+(3) *3.03 (2), (3)+(4) *3.43 p/q, q/Cpq, r/CNpq+C(4)-(5) *3.03 (1), (5)+*4.01 p/KCpqCNpq;Prop PROOF 1 CCpCqrCKpqr *3.31 (Imp) p/Cpq, q/CNpq, r/q 2 CCCpqCCNpqqCKCpqCNpqq SUB 3 CCpqCCNpqq *2.61 (1) 4 CKCpqCNpqq MP: 2, 3 (2) 5 CqCpq *2.02 (Simp) 6 CqCpq *2.02 (Simp) p/Np (3) 7 CqCNpq SUB (4) 8 KCqCpqCqCNpq *3.03: 6, 7 9 CKCpqCprCpKqr *3.43 (Comp) p/q, q/Cpq, r/CNpq 10 CKCqCpqCqCNpqCqKCpqCNpq SUB (5) 11 CqKCpqCNpq MP: 10, 8 12 KCKCpqCNpqqCqKCpqCNpq *3.03: 4, 11 Epq=KCpqCqp Df. *4.01 p/KCpqCNpq EKCpqCNpqq=KCKCpqCNpqqCqKCpqCNpq Df. 13 EKCpqCNpqq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.84 12/29/2017 15:50:08 *4.84 CEpqECprCqr PROOF ABBREVIATION *2.06+(1) (1) p/q, q/p+(2) *3.03 (2), (1)+(3) *3.47 p/Cqp, q/Cpq, r/CCprCqr, s/CCqrCpr+C(3)-(4) (4)+*4.01 p/q, q/p;*4.01 p/Cpr, q/Cqr;SE(*4.21 p/q, q/p);Prop PROOF (1) 1 CCpqCCqrCpr *2.06 (Syll) p/q, q/p (2) 2 CCqpCCprCqr SUB (3) 3 KCCqpCCprCqrCCpqCCqrCpr *3.03: 2, 1 4 CKCprCqsCKpqKrs *3.47 p/Cqp, q/Cpq, r/CCprCqr, s/CCqrCpr 5 CKCCqpCCprCqrCCpqCCqrCprCKCqpCpqKCCprCqrCCqrCpr SUB (4) 6 CKCqpCpqKCCprCqrCCqrCpr MP: 5, 3 Epq=KCpqCqp Df. *4.01 p/q, q/p Eqp=KCqpCpq Df. 7 CEqpKCCprCqrCCqrCpr REP Epq=KCpqCqp Df. *4.01 p/Cpr, q/Cqr ECprCqr=KCCprCqrCCqrCpr Df. 8 CEqpECprCqr REP EEpqEqp *4.21 p/q, q/p EEqpEpq 9 CEpqECprCqr SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.85 12/29/2017 15:50:08 *4.85 CEpqECrpCrq PROOF ABBREVIATION *2.05 p/r, q/p, r/q+(1) *2.05 p/r, r/p+(2) *3.03 (1), (2)+(3) *3.47 p/Cpq, q/Cqp, r/CCrpCrq, s/CCrqCrp+C(3)-(4) (4)+*4.01;*4.01 p/Crp, q/Crq;Prop PROOF 1 CCqrCCpqCpr *2.05 (Syll) p/r, q/p, r/q (1) 2 CCpqCCrpCrq SUB 3 CCqrCCpqCpr *2.05 (Syll) p/r, r/p (2) 4 CCqpCCrqCrp SUB (3) 5 KCCpqCCrpCrqCCqpCCrqCrp *3.03: 2, 4 6 CKCprCqsCKpqKrs *3.47 p/Cpq, q/Cqp, r/CCrpCrq, s/CCrqCrp 7 CKCCpqCCrpCrqCCqpCCrqCrpCKCpqCqpKCCrpCrqCCrqCrp SUB (4) 8 CKCpqCqpKCCrpCrqCCrqCrp MP: 7, 5 Epq=KCpqCqp Df. *4.01 9 CEpqKCCrpCrqCCrqCrp REP Epq=KCpqCqp Df. *4.01 p/Crp, q/Crq ECrpCrq=KCCrpCrqCCrqCrp Df. 10 CEpqECrpCrq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.86 12/29/2017 15:50:08 *4.86 CEpqEEprEqr PROOF ABBREVIATION *4.84+(1) *4.85+(2) *3.03 (1), (2)+(3) *3.47 p/Epq, q/Epq, r/ECprCqr, s/ECrpCrq+C(3)-(#1) (#1)+SE(*4.24 p/Epq);(4) *4.38 p/Cpr, q/Crp, r/Cqr, s/Crq+(5) *2.06 p/Epq, q/KECprCqrECrpCrq, r/EKCprCrpKCqrCrq+C(4)-C(5)-(6) (6)+*4.01 q/r;*4.01 p/q, q/r;Prop PROOF (1) 1 CEpqECprCqr *4.84 (2) 2 CEpqECrpCrq *4.85 (3) 3 KCEpqECprCqrCEpqECrpCrq *3.03: 1, 2 4 CKCprCqsCKpqKrs *3.47 p/Epq, q/Epq, r/ECprCqr, s/ECrpCrq 5 CKCEpqECprCqrCEpqECrpCrqCKEpqEpqKECprCqrECrpCrq SUB (#1) 6 CKEpqEpqKECprCqrECrpCrq MP: 5, 3 EpKpp *4.24 p/Epq EEpqKEpqEpq (4) 7 CEpqKECprCqrECrpCrq SE 8 CKEprEqsEKpqKrs *4.38 p/Cpr, q/Crp, r/Cqr, s/Crq (5) 9 CKECprCqrECrpCrqEKCprCrpKCqrCrq SUB 10 CCpqCCqrCpr *2.06 (Syll) p/Epq, q/KECprCqrECrpCrq, r/EKCprCrpKCqrCrq 11 CCEpqKECprCqrECrpCrqCCKECprCqrECrpCrqEKCprCrpKCqrCrqCEpqEKCprCrpKCqrCrq SUB 12 CCKECprCqrECrpCrqEKCprCrpKCqrCrqCEpqEKCprCrpKCqrCrq MP: 11, 7 (6) 13 CEpqEKCprCrpKCqrCrq MP: 12, 9 Epq=KCpqCqp Df. *4.01 q/r Epr=KCprCrp Df. 14 CEpqEEprKCqrCrq REP Epq=KCpqCqp Df. *4.01 p/q, q/r Eqr=KCqrCrq Df. 15 CEpqEEprEqr REP This proof seems natural, but does not use *4.21 or *4.22. I don’t know a way to get this prop. With them. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.87 12/29/2017 15:50:08 *4.87 EEECKpqrCpCqrCqCprCKqpr PROOF ABBREVIATION *3.3+(1) *3.31+(2) *3.03 (1), (2)+*4.01 p/CKpqr, q/CpCqr;(3) *2.04+(4) *2.04 p/q, q/p+(5) *3.03 (4), (5)+*4.01 p/CpCqr, q/CqCpr+(6) *2.06 p/CqCpr, q/CpCqr, r/CKpqr+C*2.04 p/q, q/p-C*3.31-(7) *2.06 p/CKpqr, q/CpCqr, r/CqCpr+C*3.3-C*2.04-(8) *3.03 (7), (8)+*4.01 p/CqCpr, q/CKpqr+SE(*4.3)+(9) *3.03 (3), (6)+*4.02 p/CKpqr, q/CpCqr, r/CqCpr;(10) *3.03 (10), (9)+*4.02 p/ECKpqrCpCqr, q/CqCpr, r/CKqpr;Prop PROOF (1) 1 CCKpqrCpCqr *3.3 (Exp) (2) 2 CCpCqrCKpqr *3.31 (Imp) 3 KCCKpqrCpCqrCCpCqrCKpqr *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 p/CKpqr, q/CpCqr ECKpqrCpCqr=KCCKpqrCpCqrCCpCqrCKpqr Df. (3) 4 ECKpqrCpCqr REP (4) 5 CCpCqrCqCpr *2.04 (Comm) 6 CCpCqrCqCpr *2.04 (Comm) p/q, q/p (5) 7 CCqCprCpCqr SUB 8 KCCpCqrCqCprCCqCprCpCqr *3.03: 6, 7 Epq=KCpqCqp Df. *4.01 p/CpCqr, q/CqCpr ECpCqrCqCpr=KCCpCqrCqCprCCqCprCpCqr Df. (6) 9 ECpCqrCqCpr REP 10 CCpqCCqrCpr *2.06 (Syll) p/CqCpr, q/CpCqr, r/CKpqr 11 CCCqCprCpCqrCCCpCqrCKpqrCCqCprCKpqr SUB 12 CCpCqrCqCpr *2.04 (Comm) p/q, q/p 13 CCqCprCpCqr SUB 14 CCCpCqrCKpqrCCqCprCKpqr MP: 11, 13 15 CCpCqrCKpqr *3.31 (Imp) (7) 16 CCqCprCKpqr MP: 14, 15 17 CCpqCCqrCpr *2.06 (Syll) p/CKpqr, q/CpCqr, r/CqCpr 18 CCCKpqrCpCqrCCCpCqrCqCprCCKpqrCqCpr SUB 19 CCKpqrCpCqr *3.3 (Exp) 20 CCCpCqrCqCprCCKpqrCqCpr MP: 18, 19 21 CCpCqrCqCpr *2.04 (Comm) (8) 22 CCKpqrCqCpr MP: 20, 21 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *4.87(CONT.) 23 KCCqCprCKpqrCCKpqrCqCpr *3.03: 16, 22 Epq=KCpqCqp Df. *4.01 p/CqCpr, q/CKpqr ECqCprCKpqr=KCCqCprCKpqrCCKpqrCqCpr Df. 24 ECqCprCKpqr REP EKpqKqp *4.3 (9) 25 ECqCprCKqpr SE 26 KECKpqrCpCqrECpCqrCqCpr *3.03: 4, 9 EEpqr=KEpqEqr Df. *4.02 p/CKpqr, q/CpCqr, r/CqCpr EECKpqrCpCqrCqCpr=KECKpqrCpCqrECpCqrCqCpr Df. (10) 27 EECKpqrCpCqrCqCpr REP 28 KEECKpqrCpCqrCqCprECqCprCKqpr *3.03: 27, 25 EEpqr=KEpqEqr Df. *4.02 p/ECKpqrCpCqr, q/CqCpr, r/CKqpr EEECKpqrCpCqrCqCprCKqpr=KEECKpqrCpCqrCqCprECqCprCKqpr Df. 29 EEECKpqrCpCqrCqCprCKqpr REP This requires a resolution of the ambiguity of *4.87 in the Russell-Peano notation. Examine *5.47. It also requires a statement of the meaning of the left side of Def. *4.03. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.1 12/29/2017 15:50:08 *5.1 CKpqEpq PROOF ABBREVIATION *3.4+(1) (1) p/q, q/p+(2) *3.22+(3) SYLL (2), (3)+(4) *3.03 (1), (4)+(5) *3.43 p/Kpq, q/Cpq, r/Cqp+C(5);*4.01;Prop PROOF (1) 1 CKpqCpq *3.4 p/q, q/p (2) 2 CKqpCqp SUB (3) 3 CKpqKqp *3.22 (4) 4 CKpqCqp SYLL: 2, 3 (5) 5 KCKpqCpqCKpqCqp *3.03: 1, 4 6 CKCpqCprCpKqr *3.43 (Comp) p/Kpq, q/Cpq, r/Cqp 7 CKCKpqCpqCKpqCqpCKpqKCpqCqp SUB 8 CKpqKCpqCqp MP: 7, 5 Epq=KCpqCqp Df. *4.01 9 CKpqEpq REP This proof comes from a fellow student named Bob Flagg PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.1 12/29/2017 15:50:08 *5.1 CKpqEpq PROOF ABBREVIATION *3.4+(1) *2.06 p/Kpq, q/Kqp, r/Cqp+C*3.22-C*3.4 p/q, q/p;(2) *3.03 (1), (2)+(3) *3.43 p/Kpq, q/Cpq, r/Cqp+C(3);*4.01;Prop *5.1 CKpqEpq PROOF (1) 1 CKpqCpq *3.4 2 CCpqCCqrCpr *2.06 (Syll) p/Kpq, q/Kqp, r/Cqp 3 CCKpqKqpCCKqpCqpCKpqCqp SUB 4 CKpqKqp *3.22 5 CCKqpCqpCKpqCqp MP: 3, 4 6 CKpqCpq *3.4 p/q, q/p 7 CKqpCqp SUB (2) 8 CKpqCqp MP: 5, 7 (3) 9 KCKpqCpqCKpqCqp *3.03: 6, 8 10 CKCpqCprCpKqr *3.43 (Comp) p/Kpq, q/Cpq, r/Cqp 11 CKCKpqCpqCKpqCqpCKpqKCpqCqp SUB 12 CKpqKCpqCqp MP: 11, 9 Epq=KCpqCqp Df. *4.01 13 CKpqEpq REP ************************************************************ The last line of the proof and the thesis which was read in do not agree! The program takes the thesis which was read in to be correct; ************************************************************ This proof comes notes of Dan O’Leary, but it had not been entered. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.11 12/29/2017 15:50:08 *5.11 ACpqCNpq PROOF ABBREVIATION *2.54 p/Cpq, q/CNpq+C*2.5-Prop PROOF 1 CCNpqApq *2.54 p/Cpq, q/CNpq 2 CCNCpqCNpqACpqCNpq SUB 3 CNCpqCNpq *2.5 4 ACpqCNpq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.12 12/29/2017 15:50:08 *5.12 ACpqCpNq PROOF ABBREVIATION *2.54 p/Cpq, q/CpNq+C*2.51-Prop PROOF 1 CCNpqApq *2.54 p/Cpq, q/CpNq 2 CCNCpqCpNqACpqCpNq SUB 3 CNCpqCpNq *2.51 4 ACpqCpNq MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.13 12/29/2017 15:50:08 *5.13 ACpqCqp PROOF ABBREVIATION *2.521+*1.01 p/NCpq, q/Cqp;SE(*4.13 p/Cpq);Prop PROOF 1 CNCpqCqp *2.521 Cpq=ANpq Df. *1.01 p/NCpq, q/Cqp CNCpqCqp=ANNCpqCqp Df. 2 ANNCpqCqp REP EpNNp *4.13 p/Cpq ECpqNNCpq 3 ACpqCqp SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.14 12/29/2017 15:50:08 *5.14 ACpqCqr PROOF ABBREVIATION *2.16 p/q, q/Cpq+C*2.02-(1) *2.21 p/q, q/r+(2) SYLL (1), (2)+(3) *2.54 p/Cpq, q/Cqr+C(3)-Prop PROOF 1 CCpqCNqNp *2.16 p/q, q/Cpq 2 CCqCpqCNCpqNq SUB 3 CqCpq *2.02 (Simp) (1) 4 CNCpqNq MP: 2, 3 5 CNpCpq *2.21 p/q, q/r (2) 6 CNqCqr SUB (3) 7 CNCpqCqr SYLL: 4, 6 8 CCNpqApq *2.54 p/Cpq, q/Cqr 9 CCNCpqCqrACpqCqr SUB 10 ACpqCqr MP: 9, 7 This proof comes from a fellow student named Bob Flagg PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.14 12/29/2017 15:50:08 *5.14 ACpqCqr PROOF ABBREVIATION *2.16 p/q, q/Cpq+C*2.02-(1) *2.21 p/q, q/r+(2) *2.06 p/NCpq, q/Nq, r/Cpq+C(1)-C(2)-(#1) (#1);*1.01 p/NCpq, q/Cqr; SE(*4.13 p/Cpq);Prop PROOF 1 CCpqCNqNp *2.16 p/q, q/Cpq 2 CCqCpqCNCpqNq SUB 3 CqCpq *2.02 (Simp) (1) 4 CNCpqNq MP: 2, 3 5 CNpCpq *2.21 p/q, q/r (2) 6 CNqCqr SUB 7 CCpqCCqrCpr *2.06 (Syll) p/NCpq, q/Nq, r/Cpq 8 CCNCpqNqCCNqCpqCNCpqCpq SUB 9 CCNqCpqCNCpqCpq MP: 8, 4 ************************************************************ MODUS PONENS ERROR ST. NUM IS 296 IMP_NUM IS 1 LINE[IMP_NUM] IS CCpqCNqNp ANT_NUM IS 6 LINE[ANT_NUM] IS CNqCqr This proof comes notes of Dan O’Leary, but it had not been entered. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.15 12/29/2017 15:50:08 *5.15 AEpqEpNq PROOF ABBREVIATION *2.06 p/NCpq, q/KpNq, r/EpNq+(1.1) *4.61+DE;(1.2) (1.1)+C(1.2)-(1.3) *5.1 q/Nq+(1.4) (1.3)+C(1.4)-(1.5) *2.54 p/Cpq, q/EpNq+C(1.5)-(1) (1)+SE(*4.31 p/Cpq, q/EpNq);(#1) *2.06 p/NCqp, q/KqNp, r/EqNp+(2.1) *4.61 p/q, q/p+DE;(2.2) (2.1)+C(2.2)-(2.3) *5.1 p/q, q/Np+(2.4) (2.3)+C(2.4)-(2.5) *2.06 p/NCqp, q/EqNp, r/EpNq+(2.6) (2.6)+C(2.5)-(2.7) *4.12 p/q, q/p+DE;(2.8) (2.7)+C(2.8)-(2.9) *2.54 p/Cqp, q/EpNq+C(2.9)-(2) (2)+SE(*4.31 p/Cqp, q/EpNq);(#2) *3.03 (#1), (#2)+(#3) *4.41 p/EpNq, q/Cpq, r/Cqp+C(#3);*4.01;SE(4.31 p/EpNq, q/Epq);Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/NCpq, q/KpNq, r/EpNq (1.1) 2 CCNCpqKpNqCCKpNqEpNqCNCpqEpNq SUB 3 ENCpqKpNq *4.61 (1.2) 4 CNCpqKpNq DE (1.3) 5 CCKpNqEpNqCNCpqEpNq MP: 2, 4 6 CKpqEpq *5.1 q/Nq (1.4) 7 CKpNqEpNq SUB (1.5) 8 CNCpqEpNq MP: 5, 7 9 CCNpqApq *2.54 p/Cpq, q/EpNq 10 CCNCpqEpNqACpqEpNq SUB (1) 11 ACpqEpNq MP: 10, 8 EApqAqp *4.31 p/Cpq, q/EpNq EACpqEpNqAEpNqCpq (#1) 12 AEpNqCpq SE 13 CCpqCCqrCpr *2.06 (Syll) p/NCqp, q/KqNp, r/EqNp (2.1) 14 CCNCqpKqNpCCKqNpEqNpCNCqpEqNp SUB 15 ENCpqKpNq *4.61 p/q, q/p 16 ENCqpKqNp SUB PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.15(CONT.) (2.2) 17 CNCqpKqNp DE (2.3) 18 CCKqNpEqNpCNCqpEqNp MP: 14, 17 19 CKpqEpq *5.1 p/q, q/Np (2.4) 20 CKqNpEqNp SUB (2.5) 21 CNCqpEqNp MP: 18, 20 22 CCpqCCqrCpr *2.06 (Syll) p/NCqp, q/EqNp, r/EpNq (2.6) 23 CCNCqpEqNpCCEqNpEpNqCNCqpEpNq SUB (2.7) 24 CCEqNpEpNqCNCqpEpNq MP: 23, 21 25 EEpNqEqNp *4.12 p/q, q/p 26 EEqNpEpNq SUB (2.8) 27 CEqNpEpNq DE (2.9) 28 CNCqpEpNq MP: 24, 27 29 CCNpqApq *2.54 p/Cqp, q/EpNq 30 CCNCqpEpNqACqpEpNq SUB (2) 31 ACqpEpNq MP: 30, 28 EApqAqp *4.31 p/Cqp, q/EpNq EACqpEpNqAEpNqCqp (#2) 32 AEpNqCqp SE (#3) 33 KAEpNqCpqAEpNqCqp *3.03: 12, 32 34 EApKqrKApqApr *4.41 p/EpNq, q/Cpq, r/Cqp 35 EAEpNqKCpqCqpKAEpNqCpqAEpNqCqp SUB 36 AEpNqKCpqCqp MP: 35, 33 Epq=KCpqCqp Df. *4.01 37 AEpNqEpq REP 4.31 ************************************************************ SE (EQUIV.) ERROR PART IS SE(4.31 p/EpNq, q/Epq) S1 IS 4.31 p/EpNq, q/Epq S2 IS AEpNqCqp THM IS ST. NUM IS 414 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.16 12/29/2017 15:50:08 *5.16 NKEpqEpNq PROOF ABBREVIATION *2.06 p/KEpqCpNq, q/KCpqCpNq, r/Np+(1.1) *3.26 p/KCpqCpNq, q/Cqp+SE(*4.32 p/Cpq, q/CpNq, r/Cqp);(#1) (#1)+SE(*4.3 p/CpNq, q/Cqp);SE(*4.32 p/Cpq, q/Cqp, r/CpNq);*4.01;(1.2) (1.1)+C(1.2)-(1.3) *4.82;DE+(1.4) (1.3)+C(1.4)-(1) *2.06 p/KEpqCpNq, q/KCqpCpNq, r/CqNq+(2.1) *3.27 p/Cpq, q/KCqpCpNq+SE(*4.32 p/Cpq, q/Cqp, r/CpNq);*4.01;(2.2) (2.1)+C(2.2)-(2.3) *3.33 p/q, q/p, r/Nq+(2.4) (2.3)+C(2.4)-(2.5) *2.06 p/KEpqCpNq, q/CqNq, r/Nq+(2.6) (2.6)+C(2.5)-(2.7) *2.01 p/q+(2.8) (2.7)+C(2.8)-(2) *2.06 p/KEpqCpNq, q/KNpNq, r/NCNqp+(3.1) *3.03 (1), (2)+(3.21) *3.43 p/KEpqCpNq, q/Np, r/Nq+C(3.21)-(3.2) (3.1)+C(3.2)-(3.3) *4.65 p/q, q/p+SE(*4.21 p/NCNqp, q/KNqNp);SE(*4.3 p/Np, q/Nq);DE;(3.4) (3.3)+C(3.4)-(3) *2.06 p/Epq, q/CCpNqNCNqp, r/ANCpNqNCNqp+(4.1) *3.3 p/Epq, q/CpNq, r/NCNqp+C(3)-(4.2) (4.1)+C(4.2)-(4.3) *2.08 p/ANCpNqNCNqp+*1.01 p/CpNq, q/NCNqp;(4.4) (4.3)+C(4.4)-(4.5) *2.06 p/Epq, q/ANCpNqNCNqp, r/NEpNq+(4.6) (4.6)+C(4.5)-(4.7) *4.51 p/CpNq, q/CNqp+*4.01 q/Nq;DER;(4.8) (4.7)+C(4.8)-(4) (4)+*1.01 p/Epq, q/NEpNq;SE(*4.13 p/ANEpqNEpNq);*3.01 p/Epq, q/EpNq;Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/KEpqCpNq, q/KCpqCpNq, r/Np (1.1) 2 CCKEpqCpNqKCpqCpNqCCKCpqCpNqNpCKEpqCpNqNp SUB 3 CKpqp *3.26 (Simp) p/KCpqCpNq, q/Cqp 4 CKKCpqCpNqCqpKCpqCpNq SUB EKKpqrKpKqr *4.32 p/Cpq, q/CpNq, r/Cqp EKKCpqCpNqCqpKCpqKCpNqCqp (#1) 5 CKCpqKCpNqCqpKCpqCpNq SE EKpqKqp *4.3 p/CpNq, q/Cqp EKCpNqCqpKCqpCpNq 6 CKCpqKCqpCpNqKCpqCpNq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.16(CONT.) EKKpqrKpKqr *4.32 p/Cpq, q/Cqp, r/CpNq EKKCpqCqpCpNqKCpqKCqpCpNq 7 CKKCpqCqpCpNqKCpqCpNq SE Epq=KCpqCqp Df. *4.01 (1.2) 8 CKEpqCpNqKCpqCpNq REP (1.3) 9 CCKCpqCpNqNpCKEpqCpNqNp MP: 2, 8 10 EKCpqCpNqNp *4.82 (1.4) 11 CKCpqCpNqNp DE (1) 12 CKEpqCpNqNp MP: 9, 11 13 CCpqCCqrCpr *2.06 (Syll) p/KEpqCpNq, q/KCqpCpNq, r/CqNq (2.1) 14 CCKEpqCpNqKCqpCpNqCCKCqpCpNqCqNqCKEpqCpNqCqNq SUB 15 CKpqq *3.27 (Simp) p/Cpq, q/KCqpCpNq 16 CKCpqKCqpCpNqKCqpCpNq SUB EKKpqrKpKqr *4.32 p/Cpq, q/Cqp, r/CpNq EKKCpqCqpCpNqKCpqKCqpCpNq 17 CKKCpqCqpCpNqKCqpCpNq SE Epq=KCpqCqp Df. *4.01 (2.2) 18 CKEpqCpNqKCqpCpNq REP (2.3) 19 CCKCqpCpNqCqNqCKEpqCpNqCqNq MP: 14, 18 20 CKCpqCqrCpr *3.33 (Syll) p/q, q/p, r/Nq (2.4) 21 CKCqpCpNqCqNq SUB (2.5) 22 CKEpqCpNqCqNq MP: 19, 21 23 CCpqCCqrCpr *2.06 (Syll) p/KEpqCpNq, q/CqNq, r/Nq (2.6) 24 CCKEpqCpNqCqNqCCCqNqNqCKEpqCpNqNq SUB (2.7) 25 CCCqNqNqCKEpqCpNqNq MP: 24, 22 26 CCpNpNp *2.01 (Abs) p/q (2.8) 27 CCqNqNq SUB (2) 28 CKEpqCpNqNq MP: 25, 27 29 CCpqCCqrCpr *2.06 (Syll) p/KEpqCpNq, q/KNpNq, r/NCNqp (3.1) 30 CCKEpqCpNqKNpNqCCKNpNqNCNqpCKEpqCpNqNCNqp SUB (3.21) 31 KCKEpqCpNqNpCKEpqCpNqNq *3.03: 12, 28 32 CKCpqCprCpKqr *3.43 (Comp) p/KEpqCpNq, q/Np, r/Nq 33 CKCKEpqCpNqNpCKEpqCpNqNqCKEpqCpNqKNpNq SUB (3.2) 34 CKEpqCpNqKNpNq MP: 33, 31 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.16(CONT.) (3.3) 35 CCKNpNqNCNqpCKEpqCpNqNCNqp MP: 30, 34 36 ENCNpqKNpNq *4.65 p/q, q/p 37 ENCNqpKNqNp SUB EEpqEqp *4.21 p/NCNqp, q/KNqNp EENCNqpKNqNpEKNqNpNCNqp 38 EKNqNpNCNqp SE EKpqKqp *4.3 p/Np, q/Nq EKNpNqKNqNp 39 EKNpNqNCNqp SE (3.4) 40 CKNpNqNCNqp DE (3) 41 CKEpqCpNqNCNqp MP: 35, 40 42 CCpqCCqrCpr *2.06 (Syll) p/Epq, q/CCpNqNCNqp, r/ANCpNqNCNqp (4.1) 43 CCEpqCCpNqNCNqpCCCCpNqNCNqpANCpNqNCNqpCEpqANCpNqNCNqp SUB 44 CCKpqrCpCqr *3.3 (Exp) p/Epq, q/CpNq, r/NCNqp 45 CCKEpqCpNqNCNqpCEpqCCpNqNCNqp SUB (4.2) 46 CEpqCCpNqNCNqp MP: 45, 41 (4.3) 47 CCCCpNqNCNqpANCpNqNCNqpCEpqANCpNqNCNqp MP: 43, 46 48 Cpp *2.08 (Id) p/ANCpNqNCNqp 49 CANCpNqNCNqpANCpNqNCNqp SUB Cpq=ANpq Df. *1.01 p/CpNq, q/NCNqp CCpNqNCNqp=ANCpNqNCNqp Df. (4.4) 50 CCCpNqNCNqpANCpNqNCNqp REP (4.5) 51 CEpqANCpNqNCNqp MP: 47, 50 52 CCpqCCqrCpr *2.06 (Syll) p/Epq, q/ANCpNqNCNqp, r/NEpNq (4.6) 53 CCEpqANCpNqNCNqpCCANCpNqNCNqpNEpNqCEpqNEpNq SUB (4.7) 54 CCANCpNqNCNqpNEpNqCEpqNEpNq MP: 53, 51 55 ENKpqANpNq *4.51 p/CpNq, q/CNqp 56 ENKCpNqCNqpANCpNqNCNqp SUB Epq=KCpqCqp Df. *4.01 q/Nq EpNq=KCpNqCNqp Df. 57 ENEpNqANCpNqNCNqp REP (4.8) 58 CANCpNqNCNqpNEpNq DER (4) 59 CEpqNEpNq MP: 54, 58 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.16(CONT.) Cpq=ANpq Df. *1.01 p/Epq, q/NEpNq CEpqNEpNq=ANEpqNEpNq Df. 60 ANEpqNEpNq REP EpNNp *4.13 p/ANEpqNEpNq EANEpqNEpNqNNANEpqNEpNq 61 NNANEpqNEpNq SE Kpq=NANpNq Df. *3.01 p/Epq, q/EpNq KEpqEpNq=NANEpqNEpNq Df. 62 NKEpqEpNq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.17 12/29/2017 15:50:08 *5.17 EKApqNKpqEpNq PROOF ABBREVIATION *4.21 p/CNqp, q/Aqp+C*4.64 p/q, q/p;SE(*4.31);(1) *4.11 p/NCpNq, q/Kpq+C*4.63;SE(*4.13 p/CpNq);SE(*4.21 p/NKpq, q/CpNq);(2) *3.03 (1), (2)+(3) *4.38 p/Apq, q/NKpq, r/CNqp, s/CpNq+C(3);(#1) (#1);*4.01 p/Nq, q/p;SE(*4.21 p/Nq, q/p);Prop PROOF 1 EEpqEqp *4.21 p/CNqp, q/Aqp 2 EECNqpAqpEAqpCNqp SUB 3 ECNpqApq *4.64 p/q, q/p 4 ECNqpAqp SUB 5 EAqpCNqp MP: 2, 4 EApqAqp *4.31 (1) 6 EApqCNqp SE 7 EEpqENpNq *4.11 (Transp) p/NCpNq, q/Kpq 8 EENCpNqKpqENNCpNqNKpq SUB 9 ENCpNqKpq *4.63 10 ENNCpNqNKpq MP: 8, 9 EpNNp *4.13 p/CpNq ECpNqNNCpNq 11 ECpNqNKpq SE EEpqEqp *4.21 p/NKpq, q/CpNq EENKpqCpNqECpNqNKpq (2) 12 ENKpqCpNq SE (3) 13 KEApqCNqpENKpqCpNq *3.03: 6, 12 14 CKEprEqsEKpqKrs *4.38 p/Apq, q/NKpq, r/CNqp, s/CpNq 15 CKEApqCNqpENKpqCpNqEKApqNKpqKCNqpCpNq SUB (#1) 16 EKApqNKpqKCNqpCpNq MP: 15, 13 Epq=KCpqCqp Df. *4.01 p/Nq, q/p ENqp=KCNqpCpNq Df. 17 EKApqNKpqENqp REP EEpqEqp *4.21 p/Nq, q/p EENqpEpNq 18 EKApqNKpqEpNq SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.17(CONT.) PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.18 12/29/2017 15:50:08 *5.18 EEpqNEpNq PROOF ABBREVIATION *5.15+(1) *5.16+(2) *3.03 (1), (2)+(3) *5.17 p/Epq, q/EpNq+C(3)-Prop PROOF (1) 1 AEpqEpNq *5.15 (2) 2 NKEpqEpNq *5.16 (3) 3 KAEpqEpNqNKEpqEpNq *3.03: 1, 2 4 EKApqNKpqEpNq *5.17 p/Epq, q/EpNq 5 EKAEpqEpNqNKEpqEpNqEEpqNEpNq SUB 6 EEpqNEpNq MP: 5, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.19 12/29/2017 15:50:08 *5.19 NEpNp PROOF ABBREVIATION *5.18 q/p+C*4.2-Prop PROOF 1 EEpqNEpNq *5.18 q/p 2 EEppNEpNp SUB 3 Epp *4.2 4 NEpNp MP: 2, 3 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.21 12/29/2017 15:50:08 *5.21 CKNpNqEpq PROOF ABBREVIATION *5.1 p/Np, q/Nq+(1) *4.11+DER;(2) SYLL (1), (2)+Prop PROOF 1 CKpqEpq *5.1 p/Np, q/Nq (1) 2 CKNpNqENpNq SUB 3 EEpqENpNq *4.11 (Transp) (2) 4 CENpNqEpq DER 5 CKNpNqEpq SYLL: 2, 4 This is a version of the proof using SYLL PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.21 12/29/2017 15:50:08 *5.21 CKNpNqEpq PROOF ABBREVIATION *5.1 p/Np, q/Nq+(1) *4.11+DER;(2) *2.06 p/KNpNq, q/ENpNq, r/Epq+C(1)-C(2)-Prop PROOF 1 CKpqEpq *5.1 p/Np, q/Nq (1) 2 CKNpNqENpNq SUB 3 EEpqENpNq *4.11 (Transp) (2) 4 CENpNqEpq DER 5 CCpqCCqrCpr *2.06 (Syll) p/KNpNq, q/ENpNq, r/Epq 6 CCKNpNqENpNqCCENpNqEpqCKNpNqEpq SUB 7 CCENpNqEpqCKNpNqEpq MP: 6, 2 8 CKNpNqEpq MP: 7, 4 This is a version of the proof using MP I don’t remember why I made two versions PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.22 12/29/2017 15:50:08 *5.22 ENEpqAKpNqKqNp PROOF ABBREVIATION *4.61+(1) *4.61 p/q, q/p+(2) *3.03 (1), (2)+(3) *4.39 p/NCpq, q/NCqp, r/KpNq, s/KqNp+C(3)-(#1) (#1)+SE(*4.51 p/Cpq, q/Cqp);*4.01;Prop PROOF (1) 1 ENCpqKpNq *4.61 2 ENCpqKpNq *4.61 p/q, q/p (2) 3 ENCqpKqNp SUB (3) 4 KENCpqKpNqENCqpKqNp *3.03: 2, 3 5 CKEprEqsEApqArs *4.39 p/NCpq, q/NCqp, r/KpNq, s/KqNp 6 CKENCpqKpNqENCqpKqNpEANCpqNCqpAKpNqKqNp SUB (#1) 7 EANCpqNCqpAKpNqKqNp MP: 6, 4 ENKpqANpNq *4.51 p/Cpq, q/Cqp ENKCpqCqpANCpqNCqp 8 ENKCpqCqpAKpNqKqNp SE Epq=KCpqCqp Df. *4.01 9 ENEpqAKpNqKqNp REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.23 12/29/2017 15:50:08 *5.23 EEpqAKpqKNpNq PROOF ABBREVIATION *5.18+(1) *5.22 q/Nq+(2) SYLL (1), (2)+(3);SE(*4.13 p/q);SE(*4.3 p/Np, q/Nq);Prop PROOF (1) 1 EEpqNEpNq *5.18 2 ENEpqAKpNqKqNp *5.22 q/Nq (2) 3 ENEpNqAKpNNqKNqNp SUB 4 CEpqAKpNNqKNqNp SYLL: 1, 3 EpNNp *4.13 p/q EqNNq 5 CEpqAKpqKNqNp SE EKpqKqp *4.3 p/Np, q/Nq EKNpNqKNqNp 6 CEpqAKpqKNpNq SE ************************************************************ The last line of the proof and the thesis which was read in do not agree! The program takes the thesis which was read in to be correct; ************************************************************ The notes of Dan O’Leary have some suggestions to make this proof work. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.24 12/29/2017 15:50:08 *5.24 ENAKpqKNpNqAKpNqKqNp PROOF ABBREVIATION *5.22+SE(*5.23);Prop PROOF 1 ENEpqAKpNqKqNp *5.22 EEpqAKpqKNpNq *5.23 2 ENAKpqKNpNqAKpNqKqNp SE PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.25 12/29/2017 15:50:08 *5.25 EApqCCpqq PROOF ABBREVIATION *2.62+(1) *2.68+(2) *3.03 (1), (2)+(3);*4.01 p/Apq, q/CCpqq;Prop PROOF (1) 1 CApqCCpqq *2.62 (2) 2 CCCpqqApq *2.68 3 KCApqCCpqqCCCpqqApq *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 p/Apq, q/CCpqq EApqCCpqq=KCApqCCpqqCCCpqqApq Df. 4 EApqCCpqq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.3 12/29/2017 15:50:08 *5.3 ECKpqrCKpqKpr PROOF ABBREVIATION *5.3+Prop PROOF 1 ECKpqrCKpqKpr *5.3 Need to work out the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.31 12/29/2017 15:50:08 *5.31 CKrCpqCpKqr PROOF ABBREVIATION *2.06 p/KrCpq, q/r, r/Cpr+(1.1) *3.26 p/r, q/Cpq+(1.2) (1.1)+C(1.2)+(1.3) *2.02 q/r+(1.4) (1.3)+C(1.4)-(1) *3.27 p/r, q/Cpq+(2) *3.03 (2), (1)+(3) *3.43 p/KrCpq, q/Cpq, r/Cpr+C(3)-(4) *3.43+(5) SYLL (4), (5)+Prop PROOF 1 CCpqCCqrCpr *2.06 (Syll) p/KrCpq, q/r, r/Cpr (1.1) 2 CCKrCpqrCCrCprCKrCpqCpr SUB 3 CKpqp *3.26 (Simp) p/r, q/Cpq (1.2) 4 CKrCpqr SUB (1.3) 5 CCrCprCKrCpqCpr MP: 2, 4 6 CqCpq *2.02 (Simp) q/r (1.4) 7 CrCpr SUB (1) 8 CKrCpqCpr MP: 5, 7 9 CKpqq *3.27 (Simp) p/r, q/Cpq (2) 10 CKrCpqCpq SUB (3) 11 KCKrCpqCpqCKrCpqCpr *3.03: 10, 8 12 CKCpqCprCpKqr *3.43 (Comp) p/KrCpq, q/Cpq, r/Cpr 13 CKCKrCpqCpqCKrCpqCprCKrCpqKCpqCpr SUB (4) 14 CKrCpqKCpqCpr MP: 13, 11 (5) 15 CKCpqCprCpKqr *3.43 (Comp) 16 CKrCpqCpKqr SYLL: 14, 15 The notes make some suggestions for changes. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.32 12/29/2017 15:50:08 *5.32 ECpEqrEKpqKpr PROOF ABBREVIATION *5.32+Prop PROOF 1 ECpEqrEKpqKpr *5.32 Need to work out the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.33 12/29/2017 15:50:08 *5.33 EKpCqrKpCKpqr PROOF ABBREVIATION *4.73 q/p, p/q+SE(*4.3 p/q, q/p)+(1) *4.84 p/q, q/Kpq+(2) SYLL (1), (2)+(3);SE(*5.32 q/Cqr, r/CKpqr);Prop PROOF 1 CqEpKpq *4.73 q/p, p/q 2 CpEqKqp SUB EKpqKqp *4.3 p/q, q/p EKqpKpq (1) 3 CpEqKpq SE 4 CEpqECprCqr *4.84 p/q, q/Kpq (2) 5 CEqKpqECqrCKpqr SUB 6 CpECqrCKpqr SYLL: 3, 5 ECpEqrEKpqKpr *5.32 q/Cqr, r/CKpqr ECpECqrCKpqrEKpCqrKpCKpqr 7 EKpCqrKpCKpqr SE The notes suggest using MP instead of SYLL as the inference rule PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.35 12/29/2017 15:50:08 *5.35 CKCpqCprCpEqr PROOF ABBREVIATION *2.05 q/Kqr, r/Eqr+C*5.1 p/q, q/r+(1) *3.43+(2) SYLL (1), (2)+Prop PROOF 1 CCqrCCpqCpr *2.05 (Syll) q/Kqr, r/Eqr 2 CCKqrEqrCCpKqrCpEqr SUB 3 CKpqEpq *5.1 p/q, q/r 4 CKqrEqr SUB (1) 5 CCpKqrCpEqr MP: 2, 4 (2) 6 CKCpqCprCpKqr *3.43 (Comp) 7 CKCpqCprCpEqr SYLL: 5, 6 The notes question the use of *2.05 PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.36 12/29/2017 15:50:08 *5.36 EkpEpqKqEpq PROOF ABBREVIATION *5.36+Prop PROOF 1 EkpEpqKqEpq *5.36 Need to work out the demonstration. This is the first use of Ass. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.4 12/29/2017 15:50:08 *5.4 ECpCpqCpq PROOF ABBREVIATION *2.43+(1) *2.02 q/Cpq+(2) *3.03 (1), (2)+(3);*4.01 p/CpCpq, q/Cpq;Prop PROOF (1) 1 CCpCpqCpq *2.43 2 CqCpq *2.02 (Simp) q/Cpq (2) 3 CCpqCpCpq SUB 4 KCCpCpqCpqCCpqCpCpq *3.03: 1, 3 Epq=KCpqCqp Df. *4.01 p/CpCpq, q/Cpq ECpCpqCpq=KCCpCpqCpqCCpqCpCpq Df. 5 ECpCpqCpq REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.41 12/29/2017 15:50:08 *5.41 ECCpqCprCpCqr PROOF ABBREVIATION *2.86+(1) *2.77+(2) *3.03 (1), (2)+(3);*4.01 p/CCpqCpr, q/CpCqr;Prop PROOF (1) 1 CCCpqCprCpCqr *2.86 (2) 2 CCpCqrCCpqCpr *2.77 3 KCCCpqCprCpCqrCCpCqrCCpqCpr *3.03: 1, 2 Epq=KCpqCqp Df. *4.01 p/CCpqCpr, q/CpCqr ECCpqCprCpCqr=KCCCpqCprCpCqrCCpCqrCCpqCpr Df. 4 ECCpqCprCpCqr REP PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.42 12/29/2017 15:50:08 *5.42 ECpCqrCpCqKpr PROOF ABBREVIATION *5.42+Prop PROOF 1 ECpCqrCpCqKpr *5.42 Need to work out the demonstration. The notes say, “Need to look at *4.87” PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.44 12/29/2017 15:50:08 *5.44 CCpqECprCpKqr PROOF ABBREVIATION *5.44+Prop PROOF 1 CCpqECprCpKqr *5.44 Need to work out the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.5 12/29/2017 15:50:08 *5.5 CpECpqq PROOF ABBREVIATION *5.5+Prop PROOF 1 CpECpqq *5.5 Need to work out the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.01 12/29/2017 15:50:08 *5.01 CpEqEpq PROOF ABBREVIATION *5.501+Prop PROOF 1 *5.501 ************************************************************ The last line of the proof and the thesis which was read in do not agree! The program takes the thesis which was read in to be correct; ************************************************************ Need to work out the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.53 12/29/2017 15:50:08 *5.53 ECAApqrsKKCpsCqsCrs PROOF ABBREVIATION *4.77 p/s, q/Apq+SE(*4.77 p/s, q/p, r/q);(1) (#1);SE(*4.21 p/KKCpsCqsCrs, q/CAApqrs);Prop PROOF 1 EKCqpCrpCAqrp *4.77 p/s, q/Apq 2 EKCApqsCrsCAApqrs SUB EKCqpCrpCAqrp *4.77 p/s, q/p, r/q EKCpsCqsCApqs (1) 3 EKKCpsCqsCrsCAApqrs SE EEpqEqp *4.21 p/KKCpsCqsCrs, q/CAApqrs EEKKCpsCqsCrsCAApqrsECAApqrsKKCpsCqsCrs 4 ECAApqrsKKCpsCqsCrs SE The notes say, “This nice proof comes from Debra Brown” PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.54 12/29/2017 15:50:08 *5.54 EKpqApEKpqq PROOF ABBREVIATION *5.54+Prop PROOF 1 EKpqApEKpqq *5.54 Need to work out the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.55 12/29/2017 15:50:08 *5.55 EApqApEApqq PROOF ABBREVIATION *5.55+Prop PROOF 1 EApqApEApqq *5.55 Need to work out the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.6 12/29/2017 15:50:08 *5.6 ECKpNqrCpAqr PROOF ABBREVIATION *5.6+Prop PROOF 1 ECKpNqrCpAqr *5.6 Need to work out the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.6.1 12/29/2017 15:50:08 *5.6.1 CKCrNqEpAqrCKpNqr PROOF ABBREVIATION *5.6.1+Prop PROOF 1 CKCrNqEpAqrCKpNqr *5.6.1 This is here for *5.75. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.61 12/29/2017 15:50:08 *5.61 EKApqNqKpNq PROOF ABBREVIATION *4.74 p/q, q/p+SE(*5.32 p/Nq, q/p, r/Aqp);(#1) (#1)+SE(*4.3 p/Nq, q/p);SE(*4.3 p/Nq, q/Aqp);SE(*4.31);(#2) (#2)+SE(*4.21 p/KpNq, q/KApqNq);Prop PROOF 1 CNpEqApq *4.74 p/q, q/p 2 CNqEpAqp SUB ECpEqrEKpqKpr *5.32 p/Nq, q/p, r/Aqp ECNqEpAqpEKNqpKNqAqp (#1) 3 EKNqpKNqAqp SE EKpqKqp *4.3 p/Nq, q/p EKNqpKpNq 4 EKpNqKNqAqp SE EKpqKqp *4.3 p/Nq, q/Aqp EKNqAqpKAqpNq 5 EKpNqKAqpNq SE EApqAqp *4.31 (#2) 6 EKpNqKApqNq SE EEpqEqp *4.21 p/KpNq, q/KApqNq EEKpNqKApqNqEKApqNqKpNq 7 EKApqNqKpNq SE The notes say that this proof comes from Debra Brown. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.62 12/29/2017 15:50:08 *5.62 EAKpqNqApNq PROOF ABBREVIATION *4.7 p/q, q/p+*1.01 p/q, q/p;*1.01 p/q, q/Kqp;(#1) (#1);SE(*4.31 p/Nq, q/p);SE(*4.31 p/Nq, q/Kqp);(#2) (#2);SE(*4.3);SE(*4.21 p/ApNq, q/AKpqNq);Prop PROOF 1 ECpqCpKpq *4.7 p/q, q/p 2 ECqpCqKqp SUB Cpq=ANpq Df. *1.01 p/q, q/p Cqp=ANqp Df. 3 EANqpCqKqp REP Cpq=ANpq Df. *1.01 p/q, q/Kqp CqKqp=ANqKqp Df. (#1) 4 EANqpANqKqp REP EApqAqp *4.31 p/Nq, q/p EANqpApNq 5 EApNqANqKqp SE EApqAqp *4.31 p/Nq, q/Kqp EANqKqpAKqpNq (#2) 6 EApNqAKqpNq SE EKpqKqp *4.3 7 EApNqAKpqNq SE EEpqEqp *4.21 p/ApNq, q/AKpqNq EEApNqAKpqNqEAKpqNqApNq 8 EAKpqNqApNq SE The notes say that this proof comes from Debra Brown PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.63 12/29/2017 15:50:08 *5.63 EApqApKNpq PROOF ABBREVIATION *5.62 p/q, q/Np+SE(*4.13);SE(*4.13);(#1) (#1);SE(*4.31 p/KqNp, q/p);SE(*4.31);(#2) (#2);SE(*4.3 p/q, q/Np);SE(*4.21 p/ApKNpq, q/Apq);Prop PROOF 1 EAKpqNqApNq *5.62 p/q, q/Np 2 EAKqNpNNpAqNNp SUB EpNNp *4.13 3 EAKqNppAqNNp SE EpNNp *4.13 (#1) 4 EAKqNppAqp SE EApqAqp *4.31 p/KqNp, q/p EAKqNppApKqNp 5 EApKqNpAqp SE EApqAqp *4.31 (#2) 6 EApKqNpApq SE EKpqKqp *4.3 p/q, q/Np EKqNpKNpq 7 EApKNpqApq SE EEpqEqp *4.21 p/ApKNpq, q/Apq EEApKNpqApqEApqApKNpq 8 EApqApKNpq SE The notes say that this proof comes from Debra Brown PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.7 12/29/2017 15:50:08 *5.7 EEAprAqrArEpq PROOF ABBREVIATION *5.7 +Prop PROOF 1 *5.7 ************************************************************ The last line of the proof and the thesis which was read in do not agree! The program takes the thesis which was read in to be correct; ************************************************************ Need to work out the demonstration. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.71 12/29/2017 15:50:08 *5.71 CqNrEApKqrKpr PROOF ABBREVIATION *4.4+SE(*4.3 q/Aqr);(1.1) (1.1) p/r, q/p, r/q+SE(*4.3 p/r, q/p);SE(*4.3 p/r);(1) *2.06 p/CqNr, q/NKqr, r/EAKprKqr+(2.1) *4.62 p/q, q/r+(2.21) *4.51 p/q, q/r+(2.22) SYLL (2.21), (2.22)+(2.2) (2.1)+C(2.2)-(2.3) *4.7 p/Kqr, q/Kpr+SE(*4.21 p/Kpr, q/AKqrKpr);(#1) (#1)+SE(*4.31 p/Kpr, q/Kqr);(2.4) (2.3)+C(2.4)-(2);SE((1));Prop PROOF 1 EKpAqrAKpqKpr *4.4 EKpqKqp *4.3 q/Aqr EKpAqrKAqrp (1.1) 2 EKAqrpAKpqKpr SE p/r, q/p, r/q 3 EKApqrAKrpKrq SUB EKpqKqp *4.3 p/r, q/p EKrpKpr 4 EKApqrAKprKrq SE EKpqKqp *4.3 p/r EKrqKqr (1) 5 EKApqrAKprKqr SE 6 CCpqCCqrCpr *2.06 (Syll) p/CqNr, q/NKqr, r/EAKprKqr (2.1) 7 CCCqNrNKqrCCNKqrEAKprKqrCCqNrEAKprKqr SUB 8 ECpNqANpNq *4.62 p/q, q/r (2.21) 9 ECqNrANqNr SUB 10 ENKpqANpNq *4.51 p/q, q/r (2.22) 11 ENKqrANqNr SUB ************************************************************ SYLL ERROR THM1 IS CqNr#ANqNr THM2 IS NKqr#ANqNr ST. NUM IS 369 ANT1 IS CqNr CONS1 IS ANqNr ANT2 IS NKqr CONS2 IS ANqNr The notes say that this proof is defective in that the move from (1) and (2) seems OK. This is the first use of SE with a line inside the same proof Need to fix SYLL in the program so that CPQ, CRQ gives CPR. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.74 12/29/2017 15:50:08 *5.74 ECpEqrECpqCpr PROOF ABBREVIATION *5.41+(1.1) (1.1) q/r, r/q+(1.2) *3.03 (1.1), (1.2)+(1) *4.22 p/ECpqCpr, q/KCpCqrCpCrq, r/CpEqr+(2.1) *4.38 p/CCpqCpr, q/CCprCpq, r/CpCqr, s/CpCrq+C(1)-(#1);*4.01 p/Cpq, q/Cpr;(2.2) *4.76 q/Cqr, r/Crq;*4.01 p/q, q/r;(2.3) *3.03 (2.2), (2.3)+(2.4) (2.1)+C(2.4)-(#2);SE(*4.21 p/ECpqCpr, q/CpEqr);Prop PROOF (1.1) 1 ECCpqCprCpCqr *5.41 q/r, r/q (1.2) 2 ECCprCpqCpCrq SUB (1) 3 KECCpqCprCpCqrECCprCpqCpCrq *3.03: 1, 2 4 CKEpqEqrEpr *4.22 p/ECpqCpr, q/KCpCqrCpCrq, r/CpEqr (2.1) 5 CKEECpqCprKCpCqrCpCrqEKCpCqrCpCrqCpEqrEECpqCprCpEqr SUB 6 CKEprEqsEKpqKrs *4.38 p/CCpqCpr, q/CCprCpq, r/CpCqr, s/CpCrq 7 CKECCpqCprCpCqrECCprCpqCpCrqEKCCpqCprCCprCpqKCpCqrCpCrq SUB 8 EKCCpqCprCCprCpqKCpCqrCpCrq MP: 7, 3 Epq=KCpqCqp Df. *4.01 p/Cpq, q/Cpr ECpqCpr=KCCpqCprCCprCpq Df. (2.2) 9 EECpqCprKCpCqrCpCrq REP 10 EKCpqCprCpKqr *4.76 q/Cqr, r/Crq 11 EKCpCqrCpCrqCpKCqrCrq SUB Epq=KCpqCqp Df. *4.01 p/q, q/r Eqr=KCqrCrq Df. (2.3) 12 EKCpCqrCpCrqCpEqr REP (2.4) 13 KEECpqCprKCpCqrCpCrqEKCpCqrCpCrqCpEqr *3.03: 9, 12 14 EECpqCprCpEqr MP: 5, 13 EEpqEqp *4.21 p/ECpqCpr, q/CpEqr EEECpqCprCpEqrECpEqrECpqCpr 15 ECpEqrECpqCpr SE The proof line ending in (2.2) wrapped during data entry. I don’t know if +that will cause a problem. The notes say that his follows the paradigm of *4.32. PRINCIPIA MATHEMATICA Pt. 1 Sec. A *5.75 12/29/2017 15:50:08 *5.75 CKCrNqEpAqrEKpNqr PROOF ABBREVIATION *5.6.1+(1) *2.06 p/KCrNqEpAqr, q/CAqrp, r/Crp+(2.1) *3.27.1+(2.2) (2.1)+C(2.2)-(2.3) *4.77.2+(2.4) (2.3)+C(2.4)-(2) *3.26 p/CrNq, q/EpAqr+(3) *2.06 p/KCrNqEpAqr, q/KCrpCrNq, r/CrKpNq+(4.1) *3.03 (2), (3)+(4.21) *3.43 p/KCrNqEpAqr, q/Crp, r/CrNq+C(4.21)-(4.2) (4.1)+C(4.2)-(4.3) *3.43 p/r, q/p, r/Nq+(4.4) (4.3)+C(4.4)-(4) *3.03 (1), (2)+(5.1) *3.43 p/KCrNqEpAqr, q/CKpNqr, r/CrKpNq+C(5.1)-(5.2) (5.2)+*4.01 p/KpNq, q/r;Prop PROOF (1) 1 CKCrNqEpAqrCKpNqr *5.6.1 2 CCpqCCqrCpr *2.06 (Syll) p/KCrNqEpAqr, q/CAqrp, r/Crp (2.1) 3 CCKCrNqEpAqrCAqrpCCCAqrpCrpCKCrNqEpAqrCrp SUB (2.2) 4 CKCrNqEpAqrCAqrp *3.27.1 (2.3) 5 CCCAqrpCrpCKCrNqEpAqrCrp MP: 3, 4 (2.4) 6 *4.77.2 (2) 7 CCAqrpCrpCKCrNqEpAqrCrp MP: 5, 6 8 CKpqp *3.26 (Simp) p/CrNq, q/EpAqr (3) 9 CKCrNqEpAqrCrNq SUB 10 CCpqCCqrCpr *2.06 (Syll) p/KCrNqEpAqr, q/KCrpCrNq, r/CrKpNq (4.1) 11 CCKCrNqEpAqrKCrpCrNqCCKCrpCrNqCrKpNqCKCrNqEpAqrCrKpNq SUB (4.21) 12 KCCAqrpCrpCKCrNqEpAqrCrpCKCrNqEpAqrCrNq *3.03: 7, 9 13 CKCpqCprCpKqr *3.43 (Comp) p/KCrNqEpAqr, q/Crp, r/CrNq 14 CKCKCrNqEpAqrCrpCKCrNqEpAqrCrNqCKCrNqEpAqrKCrpCrNq SUB ************************************************************ MODUS PONENS ERROR ST. NUM IS 296 IMP_NUM IS 1 LINE[IMP_NUM] IS CKCrNqEpAqrCKpNqr ANT_NUM IS 12 LINE[ANT_NUM] IS KCCAqrpCrpCKCrNqEpAqrCrpCKCrNqEpAqrCrNq The line ending is (2.4) has a note suggesting that *4.77.2 should be *4.77.1 This is the first use of Hp to indicate the hypothesis of the theorem to prove. Hp does not show up in this proof. Notice the need for additional theorems *5.6.1, *3.27.1, and *4.77.1 SUMMARY OF THEOREMS AND DEFINITIONS 12/29/2017 15:50:08 *1.01 Cpq=ANpq *1.2 CAppp (Taut) *1.3 CqApq (Add) *1.4 CApqAqp (Perm) *1.4.1 CCApqArqCApqAqr *1.4.2 CCAqrAsrCAqrArs *1.5 CApAqrAqApr (Assoc) *1.6 CCqrCApqApr (Sum) *2.01 CCpNpNp (Abs) *2.02 CqCpq (Simp) *2.03 CCpNqCqNp (Transp) *2.04 CCpCqrCqCpr (Comm) *2.05 CCqrCCpqCpr (Syll) *2.06 CCpqCCqrCpr (Syll) *2.07 CpApp *2.08 Cpp (Id) *2.1 ANpp *2.11 ApNp *2.12 CpNNp *2.13 ApNNNp *2.14 CNNpp *2.15 CCNpqCNqp *2.16 CCpqCNqNp *2.17 CCNqNpCpq (Transp) *2.18 CCNppp *2.2 CpApq *2.21 CNpCpq *2.24 CpCNpq *2.25 ApCApqq *2.26 ANpCCpqq *2.27 CpCCpqq *2.3 CApAqrApArq *2.31 CApAqrAApqr *2.32 CAApqrApAqr *2.36 CCqrCApqArp *2.37 CCqrCAqpApr *2.38 CCqrCAqpArp *2.4 CApApqApq *2.41 CAqApqApq *2.42 CANpCpqCpq *2.43 CCpCpqCpq *2.45 CNApqNp *2.46 CNApqNq *2.47 CNApqANpq *2.48 CNApqApNq *2.49 CNApqANpNq *2.5 CNCpqCNpq *2.51 CNCpqCpNq *2.52 CNCpqCNpNq *2.521 CNCpqCqp SUMMARY OF THEOREMS AND DEFINITIONS (CONT.) *2.53 CApqCNpq *2.54 CCNpqApq *2.55 CNpCApqq *2.56 CNqCApqp *2.6 CCNpqCCpqq *2.61 CCpqCCNpqq *2.62 CApqCCpqq *2.621 CCpqCApqq *2.63 CApqCANpqq *2.64 CApqCApNqp *2.65 CCpqCCpNqNp *2.67 CCApqqCpq *2.68 CCCpqqApq *2.69 CCCpqqCCqpp *2.73 CCpqCAApqrAqr *2.74 CCqpCAApqrApr *2.75 CApqCApCqrApr *2.76 CApCqrCApqApr *2.77 CCpCqrCCpqCpr *2.8 CAqrCANrsAqs *2.81 CCqCrsCApqCAprAps *2.82 CApAqrCApANrsApAqs *2.83 CCpCqrCCpCrsCpCqs *2.85.0 CCCApqAprCApqrCCApqAprCqr *2.85 CCApqAprApCqr *2.86 CCCpqCprCpCqr *3.01 Kpq=NANpNq *3.03 KUpVp (Conjunction Rule) *3.1 CKpqNANpNq *3.11 CNANpNqKpq *3.12 AANpNqKpq *3.13 CNKpqANpNq *3.14 CANpNqNKpq *3.2 CpCqKpq *3.21 CqCpKpq *3.22 CKpqKqp *3.22.1 CCKpqKrqCKpqKqr *3.22.2 CCKqrKsrCKqrKrs *3.24 NKpNp *3.26 CKpqp (Simp) *3.26.1 CCCKpqpCCpKpqEpKpqCCpKpqEpKpq *3.27 CKpqq (Simp) *3.27.1 CKCrNqEpAqrCAqrp *3.3 CCKpqrCpCqr (Exp) *3.31 CCpCqrCKpqr (Imp) *3.33 CKCpqCqrCpr (Syll) *3.34 CKCqrCpqCpr (Syll) *3.35 CKpCpqq (Ass) *3.37 CCKpqrCKpNrNq (Transp) *3.4 CKpqCpq SUMMARY OF THEOREMS AND DEFINITIONS (CONT.) *3.41 CCprCKpqr *3.42 CCqrCKpqr *3.43 CKCpqCprCpKqr (Comp) *3.44 CKCqpCrpCAqrp *3.45 CCpqCKprKqr (Fact) *3.47 CKCprCqsCKpqKrs *3.48 CKCprCqsCApqArs *4.01 Epq=KCpqCqp *4.02 EEpqr=KEpqEqr *4.1 ECpqCNqNp *4.11 EEpqENpNq (Transp) *4.12 EEpNqEqNp *4.12.1 ECKqrNpCpNKqr *4.13 EpNNp *4.14 ECKpqrCKpNrNq *4.15 ECKpqNrCKqrNp *4.2 Epp *4.21 EEpqEqp *4.22 CKEpqEqrEpr *4.24 EpKpp *4.25 EpApp *4.3 EKpqKqp *4.31 EApqAqp *4.32 EKKpqrKpKqr *4.33 EAApqrApAqr *4.36 CEpqEKprKqr *4.37 CEpqEAprAqr *4.38 CKEprEqsEKpqKrs *4.39 CKEprEqsEApqArs *4.4 EKpAqrAKpqKpr *4.41 EApKqrKApqApr *4.42 EpAKpqKpNq *4.43.0 CCKCNpqCNpNqpCKApqApNqp *4.43 EpKApqApNq *4.44 EpApKpq *4.45 EpKpApq *4.5 EKpqNANpNq *4.51 ENKpqANpNq *4.52 EKpNqNANpq *4.53 ENKpNqANpq *4.54 EKNpqNApNq *4.55 ENKNpqApNq *4.56 EKNpNqNApq *4.57 ENKNpNqApq *4.6 ECpqANpq *4.61 ENCpqKpNq *4.62 ECpNqANpNq *4.63 ENCpNqKpq *4.64 ECNpqApq *4.65 ENCNpqKNpNq SUMMARY OF THEOREMS AND DEFINITIONS (CONT.) *4.66 ECNpNqApNq *4.68 ECNpNqApNq *4.67 ENCNpNqKNpq *4.7 ECpqCpKpq *4.71 ECpqEpKpq *4.72 ECpqEqApq *4.73 CqEpKpq *4.74 CNpEqApq *4.76 EKCpqCprCpKqr *4.77.0 CCAqrpKCqpCrp *4.77 EKCqpCrpCAqrp *4.77.1 CCAqrpCrp *4.78.0 EANpAAqNprANpAANpqr *4.78.01EAANpNpAqrANpAqr *4.78 EACpqCprCpAqr *4.79 EACqpCrpCKqrp *4.8 ECpNpNp *4.81 ECNppp *4.82 EKCpqCpNqNp *4.83 EKCpqCNpqq *4.84 CEpqECprCqr *4.85 CEpqECrpCrq *4.86 CEpqEEprEqr *4.87 EEECKpqrCpCqrCqCprCKqpr *5.1 CKpqEpq *5.11 ACpqCNpq *5.12 ACpqCpNq *5.13 ACpqCqp *5.14 ACpqCqr *5.15 AEpqEpNq *5.16 NKEpqEpNq *5.17 EKApqNKpqEpNq *5.18 EEpqNEpNq *5.19 NEpNp *5.21 CKNpNqEpq *5.22 ENEpqAKpNqKqNp *5.23 EEpqAKpqKNpNq *5.24 ENAKpqKNpNqAKpNqKqNp *5.25 EApqCCpqq *5.3 ECKpqrCKpqKpr *5.31 CKrCpqCpKqr *5.32 ECpEqrEKpqKpr *5.33 EKpCqrKpCKpqr *5.35 CKCpqCprCpEqr *5.36 EkpEpqKqEpq *5.4 ECpCpqCpq *5.41 ECCpqCprCpCqr *5.42 ECpCqrCpCqKpr *5.44 CCpqECprCpKqr *5.5 CpECpqq SUMMARY OF THEOREMS AND DEFINITIONS (CONT.) *5.01 CpEqEpq *5.53 ECAApqrsKKCpsCqsCrs *5.54 EKpqApEKpqq *5.55 EApqApEApqq *5.6 ECKpNqrCpAqr *5.6.1 CKCrNqEpAqrCKpNqr *5.61 EKApqNqKpNq *5.62 EAKpqNqApNq *5.63 EApqApKNpq *5.7 EEAprAqrArEpq *5.71 CqNrEApKqrKpr *5.74 ECpEqrECpqCpr *5.75 CKCrNqEpAqrEKpNqr SNOBOL4 statistics summary- 1.714 ms. Compilation time 81.534 ms. Execution time 161393 Statements executed, 45143 failed 27415 Arithmetic operations performed 84025 Pattern matches performed 3 Regenerations of dynamic storage 11.900 ms. Execution time in GC 1486 Reads performed 6638 Writes performed 505.188 ns. Average per statement executed 1979.460 Thousand statements per second