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 <http://www.gnu.org/licenses/>.



END_OF_TITLE
PRINCIPIA MATHEMATICA   Pt. 1 Sec. A
DEF
*1.01 Cpq=ANpq
INF
*1.1 Anything implied by a true elementary proposition is true. #
INF
*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. #
+
+
+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.
+
AX
*1.2 CAppp Taut
AX
*1.3 CqApq Add
AX
*1.4 CApqAqp Perm
*1.4.1+Prop
*1.4.1 CCApqArqCApqAqr
+
+This is here to make *3.48 work.
*1.4.2+Prop
*1.4.2 CCAqrAsrCAqrArs
+
+This is here to make *3.48 work.
AX
*1.5 CApAqrAqApr Assoc
AX
*1.6 CCqrCApqApr Sum
INF
*1.7 If p is an elementary proposition, then Np is an elementary 
proposition. #
INF
*1.71 If p and q are elementary propositions, Apq is an elementary 
proposition. #
INF
*1.72 If Up and Vp are elementary propositional functions which
take elementary propositions as arguments, AUpVp is an elementary 
propositional function. #
2&*1.2 p/Np+(1)
(1)+*1.01 q/Np;*2.01
*2.01 CCpNpNp Abs
2&*1.3 p/Np+(1)
(1)+*1.01;*2.02
*2.02 CqCpq Simp
2&*1.4 p/Np, q/Nq+(1)
(1)+*1.01 q/Nq;*1.01 p/q, q/Np;*2.03
*2.03 CCpNqCqNp Transp
2&*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
*2.04 CCpCqrCqCpr Comm
2&*1.6 p/Np+(1)
(1)+*1.01;*1.01 q/r;*2.05
*2.05 CCqrCCpqCpr Syll
3&*2.04 p/Cqr, q/Cpq, r/Cpr+(1)
*2.05+(2)
(1)+C(2)-*2.06
*2.06 CCpqCCqrCpr Syll
*1.3 q/p+*2.07
*2.07 CpApp
+
+ This introduces a typographical convention which is
+ explained in PM following the demonstration.
+
5&*2.05 q/App, r/p+(1)
*1.2+(2)
(1)+C(2)-(3)
*2.07+(4)
(3)+C(4)-*2.08
*2.08 Cpp Id
*2.08+*1.01 q/p;*2.1
*2.1 ANpp
2&*1.4 p/Np, q/p+(1)
(1)+C*2.1-*2.11
*2.11 ApNp
2&*2.11 p/Np+(1)
(1)+*1.01 q/NNp;*2.12
*2.12 CpNNp
4&*1.6 q/Np, r/NNNp+(1)
*2.12 p/Np+(2)
(1)+C(2)-(3)
(3)+C*2.11-*2.13
*2.13 ApNNNp
3&*1.4 q/NNNp+(1)
(1)+C*2.13-(2)
(2)+*1.01 p/NNp, q/p;*2.14
*2.14 CNNpp
12&*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
*2.15 CCNpqCNqp
+
+ The note on the proof of *2.15 introduces
+ a new demonstration paradigm.
+
3&*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
*2.16 CCpqCNqNp
+
+ This is the first use of Syll as a typographical convention.
+ Syll in square brackets is applied to (1) and (2).
+
3&*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
*2.17 CCNqNpCpq Transp
5&*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
*2.18 CCNppp
3&*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
*2.2 CpApq
*2.2 p/Np+*1.01;Prop
*2.21 CNpCpq
*2.04 p/Np, q/p, r/q+C*2.21-Prop
*2.24 CpCNpq
*1.5 p/NApq, q/p, r/q+C*2.1 p/Apq-*1.01 p/Apq;Prop
*2.25 ApCApqq
+
+ This introduces a proof paradigm.
+
*2.25 p/Np+*1.01;Prop
*2.26 ANpCCpqq
*2.26+*1.01 q/CCpqq;Prop
*2.27 CpCCpqq
*1.6 q/Aqr, r/Arq+C*1.4 p/q, q/r-Prop
*2.3 CApAqrApArq
9&*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
*2.31 CApAqrAApqr
+
+
+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.
+
+
9&*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
*2.32 CAApqrApAqr
+
+
+There are two minor typographical errors in the demonstration. The
+first and second line should each end with a dot.
+
+
INF
*2.33 REDUNDANT #
+
+This definition is redundant in the notation system used here. 
+
+
3&*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
*2.36 CCqrCApqArp
+
+
+This should also be called SUM.
+
+
3&*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
*2.37 CCqrCAqpApr
+
+
+This should also be called SUM.
+
+
3&*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
*2.38 CCqrCAqpArp
+
+
+This should be called SUM.
+
+
+This is the first use of the rule SE.
+
+Note RE will not work
+
+
5&*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
*2.4 CApApqApq
5&*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
*2.41 CAqApqApq
*2.4 p/Np+*1.01;*1.01;Prop
*2.42 CANpCpqCpq
*2.42+*1.01 q/Cpq;Prop
*2.43 CCpCpqCpq
*2.16 q/Apq+C*2.2-Prop
*2.45 CNApqNp
*2.16 p/q, q/Apq+C*1.3-Prop
*2.46 CNApqNq
3&*2.45+(1)
*2.2 p/Np+(2)
*2.06 p/NApq, q/Np, r/ANpq+C(1)-C(2)-Prop
*2.47 CNApqANpq
3&*2.46+(1)
*1.3 q/Nq+(2)
*2.06 p/NApq, q/Nq, r/ApNq+C(1)-C(2)-Prop
*2.48 CNApqApNq
3&*2.45+(1)
*2.2 p/Np, q/Nq+(2)
*2.06 p/NApq, q/Np, r/ANpNq+C(1)-C(2)-Prop
*2.49 CNApqANpNq
*2.47 p/Np+*1.01;*1.01 p/Np;Prop
*2.5 CNCpqCNpq
*2.48 p/Np+*1.01;*1.01 q/Nq;Prop
*2.51 CNCpqCpNq
*2.49 p/Np+*1.01;*1.01 p/Np, q/Nq;Prop
*2.52 CNCpqCNpNq
3&*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
*2.521 CNCpqCqp
*2.38 p/q, q/p, r/NNp+C*2.12;*1.01 p/Np;Prop
*2.53 CApqCNpq
+
+This shortens the *2.25 paradigm.
+
*2.38 p/q, q/NNp, r/p+C*2.14-*1.01 p/Np;Prop
*2.54 CCNpqApq
*2.04 p/Apq, q/Np, r/q+C*2.53-Prop
*2.55 CNpCApqq
*2.55 p/q, q/p+SE(*1.4:*1.4 p/q, q/p);Prop
*2.56 CNqCApqp
+
+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.
+
3&*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
*2.6 CCNpqCCpqq
*2.04 p/CNpq, q/Cpq, r/q+C*2.6-Prop
*2.61 CCpqCCNpqq
*2.06 p/Apq, q/CNpq, r/CCpqq+C*2.53-C*2.6-Prop
*2.62 CApqCCpqq
*2.04 p/Apq, q/Cpq, r/q+C*2.62-Prop
*2.621 CCpqCApqq
*2.62+*1.01;Prop
*2.63 CApqCANpqq
2&*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
*2.64 CApqCApNqp
+
+I used (#1) instead of (1), but I remember why.
+It probably doesn’t make a difference.
+
+I used SE instead of RE
+
*2.64 p/Np+*1.01;*1.01 q/Nq;*2.65
*2.65 CCpqCCpNqNp
3&*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
*2.67 CCApqqCpq
2&*2.67 p/Np+*1.01;(1)
*2.06 p/CCpqq, q/CNpq, r/Apq-C(1)-C*2.54-Prop
*2.68 CCCpqqApq
2&*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
*2.69 CCCpqqCCqpp
3&*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
*2.73 CCpqCAApqrAqr
4&*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
*2.74 CCqpCAApqrApr
+
+Used SE instead of RE
+
4&*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
*2.75 CApqCApCqrApr
+
+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.
+
*2.04 p/Apq, q/ApCqr, r/Apr+C*2.75-Prop
*2.76 CApCqrCApqApr
*2.76 p/Np+*1.01 q/Cqr;*1.01;*1.01 q/r;Prop
*2.77 CCpCqrCCpqCpr
5&*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
*2.8 CAqrCANrsAqs
3&*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
*2.81 CCqCrsCApqCAprAps
*2.81 q/Aqr, r/ANrs, s/Aqs+C*2.8-Prop
*2.82 CApAqrCApANrsApAqs
2&*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
*2.83 CCpCqrCCpCrsCpCqs
+
+This proof is split into two parts because of the length of the
+proof abbreviation. The split does not occur in PM.
+
*2.85.0+Prop
*2.85.0 CCCApqAprCApqrCCApqAprCqr
+
+This is the troublesome line in *2.85, i.e., the one composed from
+(1) and *2.83
+
15&*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
*2.85 CCApqAprApCqr
+
+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.
+
*2.85 p/Np+*1.01;*1.01 q/r;*1.01 q/Cqr;*2.86
*2.86 CCCpqCprCpCqr
DEF
*3.01 Kpq=NANpNq
INF
*3.02 REDUNDANT #
+
+This definition is redundant in the notation used here.
+
7&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
*3.03 KUpVp Conjunction Rule
*2.08 p/Kpq+*3.01 II;Prop
*3.1 CKpqNANpNq
*2.08 p/Kpq+*3.01;Prop
*3.11 CNANpNqKpq
*2.11 p/ANpNq+*3.01;Prop
*3.12 AANpNqKpq
*2.15 p/ANpNq, q/Kpq+C*3.11-Prop
*3.13 CNKpqANpNq
*2.03 p/Kpq, q/ANpNq+C*3.1-Prop
*3.14 CANpNqNKpq
2&*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
*3.2 CpCqKpq
*2.04 r/Kpq+C*3.2-Prop
*3.21 CqCpKpq
10&*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
*3.22 CKpqKqp
*3.22.1+Prop
*3.22.1 CCKpqKrqCKpqKqr
+
+This is here to make *3.47 work.
+
*3.22.2+Prop
*3.22.2 CCKqrKsrCKqrKrs
*3.14 q/Np+C*2.11 p/Np-Prop
*3.24 NKpNp
5&*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
*3.26 CKpqp Simp
+
+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”.
*3.26.1+Prop
*3.26.1 CCCKpqpCCpKpqEpKpqCCpKpqEpKpq
+
+This is here to make *4.71 work.
+
5&*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
*3.27 CKpqq Simp
*3.27.1+Prop
*3.27.1 CKCrNqEpAqrCAqrp
+
+This is here for *5.75
+
17&*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
*3.3 CCKpqrCpCqr Exp
+
+This is an extended example of the paradigm of *2.31
+
13&*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
*3.31 CCpCqrCKpqr Imp
*3.31 p/Cpq, q/Cqr, r/Cpr+C*2.06-Prop
*3.33 CKCpqCqrCpr Syll
*3.31 p/Cqr, q/Cpq, r/Cpr+C*2.05-Prop
*3.34 CKCqrCpqCpr Syll
*3.31 q/Cpq, r/q+C*2.27-Prop
*3.35 CKpCpqq Ass
5&*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
*3.37 CCKpqrCKpNrNq Transp
*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
*3.4 CKpqCpq
*2.06 p/Kpq, q/p+C*3.26-Prop
*3.41 CCprCKpqr
*2.06 p/Kpq+C*3.27-Prop
*3.42 CCqrCKpqr
7&*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
*3.43 CKCpqCprCpKqr Comp
15&*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
*3.44 CKCqpCrpCAqrp
+
+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).
+
10&*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
*3.45 CCpqCKprKqr Fact
+
+This demonstration is a mixed paradigm. The first and second
+lines follow *2.31, the second and third lines follow *2.25.
+
19&*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
*3.47 CKCprCqsCKpqKrs
+
+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.
+
19&*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
*3.48 CKCprCqsCApqArs
+
+Note the use of *1.4.1 and *1.4.2.
+
DEF
*4.01 Epq=KCpqCqp
DEF
*4.02 EEpqr=KEpqEqr
+
+This definition resolves an ambiguity in *4.87.
+
3&*2.16+(1)
*2.17+(2)
*3.03 (1), (2)+*4.01 p/Cpq, q/CNqNp;Prop
*4.1 ECpqCNqNp
11&*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
*4.11 EEpqENpNq Transp
11&*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
*4.12 EEpNqEqNp
*4.12.1+Prop
*4.12.1 ECKqrNpCpNKqr
+
+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.
+
3&*2.12+(1)
*2.14+(2)
*3.03 (1), (2)+*4.01 q/NNp;Prop
*4.13 EpNNp
3&*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
*4.14 ECKpqrCKpNrNq
+
+First use of SE with an equivalence.
+
*4.14 p/q, q/p, r/Nr+SE(*4.13 p/r);SE(*3.22:*3.22 p/q, q/p);Prop
*4.15 ECKpqNrCKqrNp
*3.2 p/Cpp, q/Cpp+C*2.08-C*2.08;*4.01 q/p;Prop
*4.2 Epp
5&*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
*4.21 EEpqEqp
24&*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
*4.22 CKEpqEqrEpr
+
+(#1) indicates the conjunction of (3) and (4).
+
3&*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
*4.24 EpKpp
3&*1.3 q/p+(1)
*1.2+(2)
*3.03 (1), (2)+*4.01 q/App;Prop
*4.25 EpApp
3&*3.22+(1)
(1) p/q, q/p+(2)
*3.03 (1), (2)+*4.01 p/Kpq, q/Kqp;Prop
*4.3 EKpqKqp
3&*1.4+(1)
(1) p/q, q/p+(2)
*3.03 (1), (2)+*4.01 p/Apq, q/Aqp;Prop
*4.31 EApqAqp
8&*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
*4.32 EKKpqrKpKqr
+
+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
3&*2.32+(1)
*2.31+(2)
*3.03 (1), (2);*4.01 p/AApqr, q/ApAqr;Prop
*4.33 EAApqrApAqr
5&*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
*4.36 CEpqEKprKqr
5&*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
*4.37 CEpqEAprAqr
+
+Here we take SUM to mean *2.38.
+
9&*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
*4.38 CKEprEqsEKpqKrs
+
*4.39+Prop
*4.39 CKEprEqsEApqArs
+
+Don’t have a good proof yet of this proposition.
+
+In later proofs, such as *5.22, showed typos in the theorem.
+
20&*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
*4.4 EKpAqrAKpqKpr
17&*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
*4.41 EApKqrKApqApr
7&*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
*4.42 EpAKpqKpNq
*4.43.0+Prop
*4.43.0 CCKCNpqCNpNqpCKApqApNqp
+
+This is here to make *4.43 work
+
8&*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
*4.43 EpKApqApNq
+
+Note the use of *4.43.0
+
6&*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
*4.44 EpApKpq
3&*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
*4.45 EpKpApq
*4.2 p/Kpq+*3.01 II;Prop
*4.5 EKpqNANpNq
*4.5+SE(*4.12 p/Kpq, q/ANpNq);SE(*4.21 p/ANpNq, q/NKpq);Prop
*4.51 ENKpqANpNq
*4.5 q/Nq+SE(*4.13 p/q);Prop
*4.52 EKpNqNANpq
*4.52+SE(*4.12 p/KpNq, q/ANpq);SE(*4.21 p/ANpq, q/NKpNq);Prop
*4.53 ENKpNqANpq
*4.5 p/Np+SE(*4.13);Prop
*4.54 EKNpqNApNq
+
*4.54+SE(*4.12 p/KNpq, q/ApNq);SE(*4.21 p/ApNq, q/NKNpq);Prop
*4.55 ENKNpqApNq
+
*4.54 q/Nq+SE(*4.13 p/q);Prop
*4.56 EKNpNqNApq
+
*4.56+SE(*4.12 p/KNpNq, q/Apq);SE(*4.21 p/Apq, q/NKNpNq);Prop
*4.57 ENKNpNqApq
*4.2 p/Cpq+*1.01 II;Prop
*4.6 ECpqANpq
*4.6+SE(*4.11 p/Cpq, q/ANpq);SE(*4.52);Prop
*4.61 ENCpqKpNq
*4.6 q/Nq+Prop
*4.62 ECpNqANpNq
*4.62+SE(*4.11 p/CpNq, q/ANpNq);SE(*4.5);Prop
*4.63 ENCpNqKpq
+
3&*2.54+(1)
*2.53+(2)
*3.03 (1), (2)+*4.01 p/CNpq, q/Apq;Prop
*4.64 ECNpqApq
+
*4.64+SE(*4.11 p/CNpq, q/Apq);SE(*4.56);Prop
*4.65 ENCNpqKNpNq
+
*4.64 q/Nq+Prop
*4.66 ECNpNqApNq
+
*4.64 q/Nq+Prop
*4.68 ECNpNqApNq
+
*4.66+SE(*4.11 p/CNpNq, q/ApNq);SE(*4.54);Prop
*4.67 ENCNpNqKNpq
+
3&*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
*4.7 ECpqCpKpq
7&*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
*4.71 ECpqEpKpq
17&*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
*4.72 ECpqEqApq
+
+The original notes said there is a problem with this proof.
+
3&*2.02+(1)
*4.71+DE;(2)
*2.06 p/q, q/Cpq, r/EpKpq+C(1)-C(2)-Prop
*4.73 CqEpKpq
+
+This uses “DE”. I don’t recall having used this before.
+This proof might not work.
+
3&*2.21+(1)
*4.72+DE;(2)
*2.06 p/Np, q/Cpq, r/EqApq+C(1)-C(2)-Prop
*4.74 CNpEqApq
+
2&*4.41 p/Np+*1.01 q/Kqr;*1.01;*1.01 q/r;(#1)
(#1)+SE(*4.21 p/CpKqr, q/KCpqCpr);Prop
*4.76 EKCpqCprCpKqr
+
*4.77.0+Prop
*4.77.0 CCAqrpKCqpCrp
+
+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.
+
3&*3.44+(1)
*4.77.0+(2)
*3.03 (1), (2)+*4.01 p/KCqpCrp, q/CAqrp;Prop
*4.77 EKCqpCrpCAqrp
+
+Note the use of *4.77.0.
+
*4.77.1+Prop
*4.77.1 CCAqrpCrp
+
+This is here for *5.75
+
*4.78.0+Prop
*4.78.0 EANpAAqNprANpAANpqr
+
+This is to come from *4.31 and *4.37
+
*4.78.01+Prop
*4.78.01 EAANpNpAqrANpAqr
+
+This is to come from *4.25 and *4.37
+
22&*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
*4.78 EACpqCprCpAqr
+
+Note the use of *4.78.0.
+
+Note the use of *4.78.01.
+
*4.79+Prop
*4.79 EACqpCrpCKqrp
+
+Need to work on this proof.
+
3&*2.01+(1)
*2.02 q/Np+(2)
*3.03 (1), (2)+*4.01 p/CpNp, q/Np;Prop
*4.8 ECpNpNp
3&*2.18+(1)
*2.02 q/p, p/Np+(2)
*3.03 (1), (2)+*4.01 p/CNpp, q/p;Prop
*4.81 ECNppp
6&*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
*4.82 EKCpqCpNqNp
6&*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
*4.83 EKCpqCNpqq
5&*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
*4.84 CEpqECprCqr
5&*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
*4.85 CEpqECrpCrq
8&*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
*4.86 CEpqEEprEqr
+
+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.
+
11&*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
*4.87 EEECKpqrCpCqrCqCprCKqpr
+
+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.
+
6&*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
*5.1 CKpqEpq
+
+This proof comes from a fellow student named Bob Flagg
+
5&*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
+
+This proof comes notes of Dan O’Leary, but it had not been entered.
+
*2.54 p/Cpq, q/CNpq+C*2.5-Prop
*5.11 ACpqCNpq
+
*2.54 p/Cpq, q/CpNq+C*2.51-Prop
*5.12 ACpqCpNq
+
*2.521+*1.01 p/NCpq, q/Cqp;SE(*4.13 p/Cpq);Prop
*5.13 ACpqCqp
+
4&*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
*5.14 ACpqCqr
+
+This proof comes from a fellow student named Bob Flagg
+
4&*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
*5.14 ACpqCqr
+
+This proof comes notes of Dan O’Leary, but it had not been entered.
+
20&*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
*5.15 AEpqEpNq
+
31&*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
*5.16 NKEpqEpNq
+
5&*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
*5.17 EKApqNKpqEpNq
+
4&*5.15+(1)
*5.16+(2)
*3.03 (1), (2)+(3)
*5.17 p/Epq, q/EpNq+C(3)-Prop
*5.18 EEpqNEpNq
+
*5.18 q/p+C*4.2-Prop
*5.19 NEpNp
+
3&*5.1 p/Np, q/Nq+(1)
*4.11+DER;(2)
SYLL (1), (2)+Prop
*5.21 CKNpNqEpq
+
+This is a version of the proof using SYLL
+
3&*5.1 p/Np, q/Nq+(1)
*4.11+DER;(2)
*2.06 p/KNpNq, q/ENpNq, r/Epq+C(1)-C(2)-Prop
*5.21 CKNpNqEpq
+
+This is a version of the proof using MP
+I don’t remember why I made two versions
+
5&*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
*5.22 ENEpqAKpNqKqNp
+
3&*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
*5.23 EEpqAKpqKNpNq
+
+The notes of Dan O’Leary have some suggestions to make this proof work.
+
*5.22+SE(*5.23);Prop
*5.24 ENAKpqKNpNqAKpNqKqNp
+
3&*2.62+(1)
*2.68+(2)
*3.03 (1), (2)+(3);*4.01 p/Apq, q/CCpqq;Prop
*5.25 EApqCCpqq
+
*5.3+Prop
*5.3 ECKpqrCKpqKpr
+
+Need to work out the demonstration.
+
10&*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
*5.31 CKrCpqCpKqr
+
+The notes make some suggestions for changes.
+
*5.32+Prop
*5.32 ECpEqrEKpqKpr
+
+Need to work out the demonstration.
+
3&*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
*5.33 EKpCqrKpCKpqr
+
+The notes suggest using MP instead of SYLL as the inference rule
+
3&*2.05 q/Kqr, r/Eqr+C*5.1 p/q, q/r+(1)
*3.43+(2)
SYLL (1), (2)+Prop
*5.35 CKCpqCprCpEqr
+
+The notes question the use of *2.05
+
*5.36+Prop
*5.36 EkpEpqKqEpq
+
+Need to work out the demonstration.
+
+This is the first use of Ass.
+
3&*2.43+(1)
*2.02 q/Cpq+(2)
*3.03 (1), (2)+(3);*4.01 p/CpCpq, q/Cpq;Prop
*5.4 ECpCpqCpq
+
3&*2.86+(1)
*2.77+(2)
*3.03 (1), (2)+(3);*4.01 p/CCpqCpr, q/CpCqr;Prop
*5.41 ECCpqCprCpCqr
+
*5.42+Prop
*5.42 ECpCqrCpCqKpr
+
+Need to work out the demonstration.
+
+The notes say, “Need to look at *4.87”
+
*5.44+Prop
*5.44 CCpqECprCpKqr
+
+Need to work out the demonstration.
+
*5.5+Prop
*5.5 CpECpqq
+
+Need to work out the demonstration.
+
*5.501+Prop
*5.01 CpEqEpq
+
+Need to work out the demonstration.
+
2&*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
*5.53 ECAApqrsKKCpsCqsCrs
+
+The notes say, “This nice proof comes from Debra Brown”
+
*5.54+Prop
*5.54 EKpqApEKpqq
+
+Need to work out the demonstration.
+
*5.55+Prop
*5.55 EApqApEApqq
+
+Need to work out the demonstration.
+
*5.6+Prop
*5.6 ECKpNqrCpAqr
+
+Need to work out the demonstration.
+
*5.6.1+Prop
*5.6.1 CKCrNqEpAqrCKpNqr
+
+This is here for *5.75.
+
3&*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
*5.61 EKApqNqKpNq
+
+The notes say that this proof comes from Debra Brown.
+
3&*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
*5.62 EAKpqNqApNq
+
+The notes say that this proof comes from Debra Brown
+
3&*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
*5.63 EApqApKNpq
+
+The notes say that this proof comes from Debra Brown
+
*5.7 +Prop
*5.7 EEAprAqrArEpq
+
+Need to work out the demonstration.
+
10&*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
*5.71 CqNrEApKqrKpr
+
+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.
+
8&*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
*5.74 ECpEqrECpqCpr
+
+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.
+
16&*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
*5.75 CKCrNqEpAqrEKpNqr
+
+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
+