I ran Prover9 [1] with the following inputs:
1.
-P(i(x, y)) | -P(x) | P(y).
P(i(x,i(y,x))). %RVP
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). %SD
2.
-P(i(x, y)) | -P(x) | P(y).
-P(i(x, y)) | -P(i(y, z)) | P(i(x, z)).
P(i(x,i(y,x))). %RVP
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). %SD
-P(i(x, y)) | -P(i(y, z)) | P(i(x, z)) represents a derivable rule in the first system. I had the formula P(i(i(x, y), i(i(y, z), i(i(z, u), i(x, u))))) as the goal. The proof in the 1st system took 7.56 seconds, had 958 givens, generated 835656 formulas, and 23398 formulas kept. The proof in the 2nd system took 25.72 seconds, had 1450 givens, generated 3835597 formulas, and kept 26067 formulas. Both proofs took the same number of steps. The maximum clause weight of the second proof was lower than that of the first proof. As I understand things, this means that the longest formula of the second proof (excluding parentheses and predicate symbols) was shorter than that of the first proof. Here's the first proof:
% -------- Comments from original proof --------
% Proof 1 at 7.56 (+ 0.41) seconds.
% Length of proof is 21.
% Level of proof is 10.
% Maximum clause weight is 24.
% Given clauses 958.
1 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))) # label(non_clause) # label(goal). [goal].
2 -P(i(x,y)) | -P(x) | P(y). [assumption].
3 P(i(x,i(y,x))). [assumption].
4 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). [assumption].
5 -P(i(i(c1,c2),i(i(c2,c3),i(i(c3,c4),i(c1,c4))))). [deny(1)].
6 P(i(x,i(y,i(z,y)))). [hyper(2,a,3,a,b,3,a)].
7 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))). [hyper(2,a,4,a,b,4,a)].
8 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))). [hyper(2,a,3,a,b,4,a)].
11 P(i(x,i(y,i(z,i(u,z))))). [hyper(2,a,3,a,b,6,a)].
23 P(i(i(x,i(i(y,x),z)),i(x,z))). [hyper(2,a,7,a,b,6,a)].
39 P(i(i(x,i(i(y,i(z,y)),u)),i(x,u))). [hyper(2,a,7,a,b,11,a)].
43 P(i(i(i(x,i(y,z)),i(i(i(x,y),i(x,z)),u)),i(i(x,i(y,z)),u))). [hyper(2,a,7,a,b,8,a)].
126 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(2,a,23,a,b,8,a)].
419 P(i(i(i(x,y),z),i(y,z))). [hyper(2,a,39,a,b,126,a)].
441 P(i(x,i(i(i(y,z),u),i(z,u)))). [hyper(2,a,3,a,b,419,a)].
876 P(i(i(x,i(y,z)),i(y,i(x,z)))). [hyper(2,a,43,a,b,441,a)].
1406 P(i(i(x,y),i(i(y,z),i(x,z)))). [hyper(2,a,876,a,b,126,a)].
2202 P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). [hyper(2,a,1406,a,b,1406,a)].
2220 P(i(i(x,i(y,z)),i(x,i(i(z,u),i(y,u))))). [hyper(2,a,126,a,b,1406,a)].
23399 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))). [hyper(2,a,2202,a,b,2220,a)].
23400 $F. [resolve(23399,a,5,a)].
Here's the second proof:
% -------- Comments from original proof --------
% Proof 1 at 25.72 (+ 1.89) seconds.
% Length of proof is 21.
% Level of proof is 10.
% Maximum clause weight is 16.
% Given clauses 1450.
1 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))) # label(non_clause) # label(goal). [goal].
2 -P(i(x,y)) | -P(x) | P(y). [assumption].
3 -P(i(x,y)) | -P(i(y,z)) | P(i(x,z)). [assumption].
4 P(i(x,i(y,x))). [assumption].
5 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). [assumption].
6 -P(i(i(c1,c2),i(i(c2,c3),i(i(c3,c4),i(c1,c4))))). [deny(1)].
8 P(i(x,i(y,i(z,y)))). [hyper(2,a,4,a,b,4,a)].
10 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(3,a,4,a,b,5,a)].
14 P(i(i(x,y),i(x,x))). [hyper(2,a,5,a,b,4,a)].
31 P(i(x,x)). [hyper(2,a,14,a,b,8,a)].
33 P(i(i(i(x,y),x),i(i(x,y),y))). [hyper(2,a,5,a,b,31,a)].
146 P(i(x,i(i(x,y),y))). [hyper(3,a,4,a,b,33,a)].
166 P(i(i(i(x,i(y,x)),z),z)). [hyper(2,a,33,a,b,8,a)].
190 P(i(i(x,y),i(x,i(i(y,z),z)))). [hyper(2,a,10,a,b,146,a)].
344 P(i(i(i(x,y),z),i(y,z))). [hyper(3,a,10,a,b,166,a)].
601 P(i(i(x,i(y,z)),i(y,i(x,z)))). [hyper(3,a,5,a,b,344,a)].
3542 P(i(i(x,y),i(i(y,z),i(x,z)))). [hyper(3,a,190,a,b,601,a)].
5634 P(i(i(x,y),i(i(z,i(y,u)),i(z,i(x,u))))). [hyper(3,a,3542,a,b,10,a)].
5639 P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). [hyper(2,a,3542,a,b,3542,a)].
26068 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))). [hyper(3,a,5634,a,b,5639,a)].
26069 $F. [resolve(26068,a,6,a)].
The above may make it look like derived rules aren't of use. But I ran another trial looking for proofs of P(i(i(x, i(y, z)), i(y, i(x, z)))). For the first system I got the following proof:
% Proof 1 at 0.05 (+ 0.03) seconds.
% Length of proof is 17.
% Level of proof is 7.
% Maximum clause weight is 24.
% Given clauses 75.
1 P(i(i(x,i(y,z)),i(y,i(x,z)))) # label(non_clause) # label(goal). [goal].
2 -P(i(x,y)) | -P(x) | P(y). [assumption].
3 P(i(x,i(y,x))). [assumption].
4 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). [assumption].
5 -P(i(i(c1,i(c2,c3)),i(c2,i(c1,c3)))). [deny(1)].
6 P(i(x,i(y,i(z,y)))). [hyper(2,a,3,a,b,3,a)].
7 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))). [hyper(2,a,4,a,b,4,a)].
8 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))). [hyper(2,a,3,a,b,4,a)].
11 P(i(x,i(y,i(z,i(u,z))))). [hyper(2,a,3,a,b,6,a)].
23 P(i(i(x,i(i(y,x),z)),i(x,z))). [hyper(2,a,7,a,b,6,a)].
39 P(i(i(x,i(i(y,i(z,y)),u)),i(x,u))). [hyper(2,a,7,a,b,11,a)].
43 P(i(i(i(x,i(y,z)),i(i(i(x,y),i(x,z)),u)),i(i(x,i(y,z)),u))). [hyper(2,a,7,a,b,8,a)].
126 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(2,a,23,a,b,8,a)].
419 P(i(i(i(x,y),z),i(y,z))). [hyper(2,a,39,a,b,126,a)].
441 P(i(x,i(i(i(y,z),u),i(z,u)))). [hyper(2,a,3,a,b,419,a)].
876 P(i(i(x,i(y,z)),i(y,i(x,z)))). [hyper(2,a,43,a,b,441,a)].
877 $F. [resolve(876,a,5,a)].
For the second system I got the following proof:
% -------- Comments from original proof --------
% Proof 1 at 0.03 (+ 0.01) seconds.
% Length of proof is 15.
% Level of proof is 7.
% Maximum clause weight is 14.
% Given clauses 38.
1 P(i(i(x,i(y,z)),i(y,i(x,z)))) # label(non_clause) # label(goal). [goal].
2 -P(i(x,y)) | -P(x) | P(y). [assumption].
3 -P(i(x,y)) | -P(i(y,z)) | P(i(x,z)). [assumption].
4 P(i(x,i(y,x))). [assumption].
5 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). [assumption].
6 -P(i(i(c1,i(c2,c3)),i(c2,i(c1,c3)))). [deny(1)].
8 P(i(x,i(y,i(z,y)))). [hyper(2,a,4,a,b,4,a)].
10 P(i(i(x,y),i(i(z,x),i(z,y)))). [hyper(3,a,4,a,b,5,a)].
14 P(i(i(x,y),i(x,x))). [hyper(2,a,5,a,b,4,a)].
31 P(i(x,x)). [hyper(2,a,14,a,b,8,a)].
33 P(i(i(i(x,y),x),i(i(x,y),y))). [hyper(2,a,5,a,b,31,a)].
166 P(i(i(i(x,i(y,x)),z),z)). [hyper(2,a,33,a,b,8,a)].
344 P(i(i(i(x,y),z),i(y,z))). [hyper(3,a,10,a,b,166,a)].
601 P(i(i(x,i(y,z)),i(y,i(x,z)))). [hyper(3,a,5,a,b,344,a)].
602 $F. [resolve(601,a,6,a)].
Since the second proof here took some 602 formulas in comparison to 877 formulas of the first proof, the second proof has length of 15 in comparison to length 17 of the first proof, the clause weight is 14 in comparison to 24, the given clauses is 38 in comparison to 75, and it took slightly less time this suggest that *sometimes* using derived rules might make it easier for Prover9 to find a proof.
[1] W. McCune, "Prover9 and Mace4", http://www.cs.unm.edu/~mccune/Prover9, 2005-2010.
Wednesday, May 28, 2014
Monday, May 19, 2014
Professor Ulrich asks "Can a fully-automated proof of
the sufficiency of Meredith's 21-character single axiom,
CCCCCpqCNrNsrtCCtpCsp
/
((((p⊃q)⊃(~r⊃~s))⊃r)⊃t)⊃((t⊃p)⊃(s⊃p)), for classical logic in C and
N be found that equals (or shortens) Meredith's own derivation of Syl
= CCpqCCqrCpr / ((p⊃q)⊃((q⊃r)⊃(p⊃r)),
Scotus = CpCNpq / p⊃(~p⊃q), and Clavius
= CCNppp / (~p⊃p)⊃p
using just 41 condensed detachments?
UPDATE: Larry Wos has (with OTTER) now discovered a proof using only 38 applications of condensed detachment. See Automated reasoning and the discovery of missing and elegant proofs, L. Wos and G. Peiper, Rinton, Paramus, 2003, sections 3.1 through 3.3."
The question seems local to the derivation of {CCpqCCqrCpr, CpCNpq, CCNppp}. One might ask "Can a fully-automated proof of the sufficiency of Meredith's 21-character single axiom, CCCCCpqCNrNsrtCCtpCsp / ((((p⊃q)⊃(~r⊃~s))⊃r)⊃t)⊃((t⊃p)⊃(s⊃p)), for classical logic in C and N be found that requires less than 38 condensed detachments to get to the axioms for any distinct basis of C-N classical logic?"
It takes no more than 5 condensed detachments to get to CpCqp.
UPDATE: Larry Wos has (with OTTER) now discovered a proof using only 38 applications of condensed detachment. See Automated reasoning and the discovery of missing and elegant proofs, L. Wos and G. Peiper, Rinton, Paramus, 2003, sections 3.1 through 3.3."
The question seems local to the derivation of {CCpqCCqrCpr, CpCNpq, CCNppp}. One might ask "Can a fully-automated proof of the sufficiency of Meredith's 21-character single axiom, CCCCCpqCNrNsrtCCtpCsp / ((((p⊃q)⊃(~r⊃~s))⊃r)⊃t)⊃((t⊃p)⊃(s⊃p)), for classical logic in C and N be found that requires less than 38 condensed detachments to get to the axioms for any distinct basis of C-N classical logic?"
It takes no more than 5 condensed detachments to get to CpCqp.
Tuesday, May 13, 2014
Wednesday, May 7, 2014
Formula of the day: CCCpqrCsCCqCrtCqt
The last two formulas of the day were CpCqp and CCpCqrCCpqCpr. Together these form a set of axioms sufficient for the positive implicational calculus (equivalently they form a "basis" for the positive implicational calculus). C. A. Meredith figured out that CCCpqrCsCCqCrtCqt itself serves as a basis for the positive implicational calculus of propositions. To prove that{CpCqp-RVP, CCpCqrCCpqCpr-SD} yields CCCpqrCsCCqCrtCqt we can construct a demonstration as follows, with Ci standing for conditional introduction:
hypothesis 1 ! CCpqr
hypothesis 2 !@ s
hypothesis 3 !@# CqCrt
hypothesis 4 !@#$ q
RVP 5 !@#$ CqCpq
D5.4 6 !@#$ Cpq
D1.6 7 !@#$ r
D3.4 8 !@#$ Crt
D8.7 9 !@#$ t
Ci 4-9 10 !@# Cqt
Ci 3-10 11 !@ CCqCrtCqt
Ci 2-11 12 ! CsCCqCrtCqt
Ci 1-12 13 CCCpqrCsCCqCrtCqt.
We can expand all of this out and write a formal proof of {CCCpqrCsCCqCrtCqt} from the basis {CpCqp-RVP, CCpCqrCCpqCpr-SD} using any decent proof of the deduction metatheorem. Here the letters a, b, ..., n, o can get substituted by something else, but p, q, ..., y, z cannot. First we'll take out the "$" lines.
hypothesis 1 ! CCpqr
hypothesis 2 !@ s
hypothesis 3 !@# CqCrt
D[RVP].1 4 !@# CaCCpqr This is C4-1
D[SD].4 5 !@# CCaCpqCar
D5.RVP 6 !@# Cqr ... C4-7
D[RVP].3 7 !@# CaCqCrt ... C4-3
D[SD].7 8 !@# CCaqCaCrt
D8.[Caa] 9 !@# CqCrt ... C4-8
D[SD].9 10 !@# CCqrCqt
D10.6 11 !@# Cqt C4-9
.
.
.
Now for the "#" lines in the above demonstration. C3-3 and C3-9 match exactly. C3-10 we can obtain simply from SD just by substitution.
hypothesis 1 ! CCpqr
hypothesis 2 !@ s
theorem 3 !@ CCaCbCcdCaCCbcCbd (we'll use this when we used "SD" above)
D[RVP].1 4 !@ CaCCpqr
D[RVP].4 5 !@ CaCbCCpqr ... C3-4
D3.5 6 !@ CaCCbCpqCbr ... C3-5
theorem 7 !@ CaCbCcb
D[SD].6 8 !@ CCaCbCpqCaCbr
D8.7 9 !@ CaCqr ... C3-6
D3.RVP 10 !@ CCabCCcaCcb ... C3-8
D[SD].SD 11 !@ CCCaCbcCabCCaCbcCac
D11.9 12 !@ CCqCraCqa C3-11
Now the "@" lines.
hypothesis 1 ! CCpqr
theorem 2 ! CCaCbCcdCaCCbcCbd
theorem 3 ! CCaCbCcCdeCaCbCCcdCce (we'll use this where we used 3 above)
D[RVP].1 4 ! CaCCpqr C2-1
D[RVP].4 5 ! CaCbCCpqr C2-4
D[RVP].5 6 ! CaCbCcCCpqr ... C2-5
D3.6 7 ! CaCbCCcCpqCcr ... C2-6
theorem 8 ! CaCbCcCdc ... C2-7
D2.7 9 ! CaCCbCcCpqCbCcr ... C2-8
D[SD].9 10 ! CCaCbCcCpqCaCbCcr
D10.8 11 ! CaCbCqr ... C2-9
theorem 12 ! CaCbCcb
D3.12 13 ! CaCCbcCCdbCdc ... C2-10
D[SD].SD 14 ! CCCaCbcCabCCaCbcCac
D[RVP].14 15 ! CaCCCbCcdCbcCCbCcdCbd ... C2-11
D[SD].15 16 ! CCaCCbCcdCbcCaCCbCcdCbd
D16.11 17 ! CaCCqCrbCqr ... C2-12
And now we'll write the formal proof (allowing substitution for all lower case letters):
axiom 1 CpCqp C1-4
axiom 2 CCpCqrCCpqCpr
D1.2 3 CpCCqCrsCCqrCqs
D2.3 4 CCpCqCrsCpCCqrCqs ... SD above
D1.4 5 CpCCqCrCstCqCCrsCrt
D2.5 6 CCpCqCrCstCpCqCCrsCrt 2 above
D1.6 7 CpCCqCrCsCtuCqCrCCstCsu
D2.7 8 CCpCqCrCsCtuCpCqCrCCstCsu ... 3 above
D1.1 9 CpCqCrq
D2.9 10 CCpqCpCrq
D10.1 11 CpCqCrp ... C1-5
D10.11 12 CpCqCrCsp ... C1-6
D1.9 13 CpCqCrCsr ... C1-12
D1.13 14 CpCqCrCsCts ... C1-8
D8.12 15 CCpqCrCsCCtpCtq ... C1-7
D6.15 16 CCpqCrCCsCtpCsCtq ... C1-9
D4.16 17 CCpqCCrCsCtpCrCsCtq ... C1-10
D2.17 18 CCCpqCrCsCtpCCpqCrCsCtq
D18.14 19 CCCpqrCsCtCqr ... C1-11
D8.13 20 CpCqCCrsCCtrCts ... C1-13
D4.3 21 CpCCCqCrsCqrCCqCrsCqs ... C1-14
D1.21 22 CpCqCCCrCstCrsCCrCstCrt ... C1-15
D4.22 23 CpCCqCCrCstCrsCqCCrCstCrt ... C1-16
D2.23 24 CCpCqCCrCstCrsCpCqCCrCstCrt
D24.19 25 CCCpqrCsCCqCrtCqt
I'll point out that CCpqCCrpCrq is a theorem of this system as follows:
axiom 1 CpCqp
axiom 2 CCpCqrCCpqCpr
D1.2 3 CpCCqCrsCCqrCqs
D2.3 4 CCpCqCrsCpCCqrCqs
D4.1 5 CCpqCCrpCrq
But, even though it did appear in the set-ups to prove CCCpqrCsCCqCrtCqt, we never produced an actual proof of CCpqCCrpCrq, though we did produce a proof of CpCqCCrsCCtrCts in which CCpqCrpCrq can get said to qualify as contained within. I've used Prover9 to find a proof of {CpCqp, CCpCqrCCpqCpr} from {CCCpqrCsCCqCrtCqt}. Meredith also found that CtCCpqCCCspCqrCpr can also serve as a basis of the positive implicational calculus. Ted Ulrich has found some other single axioms for this system here.
Both axioms, "CtCCpqCCCspCqrCpr" and "CCCpqrCsCCqCrtCqt" have 17 symbols. A stronger system, the implicational calculus of propositions, has a single axiom with just 13 symbols.
Also, the conversion procedure I used implicitly here depends on *how* a particular meta-proof of the deduction meta-theorem works. If we have a different meta-proof of the deduction meta-theorem, we'll have a different conversion procedure. My May 10th answer here shows the same process via a distinct meta-proof of the meta-deduction theorem.
The last two formulas of the day were CpCqp and CCpCqrCCpqCpr. Together these form a set of axioms sufficient for the positive implicational calculus (equivalently they form a "basis" for the positive implicational calculus). C. A. Meredith figured out that CCCpqrCsCCqCrtCqt itself serves as a basis for the positive implicational calculus of propositions. To prove that{CpCqp-RVP, CCpCqrCCpqCpr-SD} yields CCCpqrCsCCqCrtCqt we can construct a demonstration as follows, with Ci standing for conditional introduction:
hypothesis 1 ! CCpqr
hypothesis 2 !@ s
hypothesis 3 !@# CqCrt
hypothesis 4 !@#$ q
RVP 5 !@#$ CqCpq
D5.4 6 !@#$ Cpq
D1.6 7 !@#$ r
D3.4 8 !@#$ Crt
D8.7 9 !@#$ t
Ci 4-9 10 !@# Cqt
Ci 3-10 11 !@ CCqCrtCqt
Ci 2-11 12 ! CsCCqCrtCqt
Ci 1-12 13 CCCpqrCsCCqCrtCqt.
We can expand all of this out and write a formal proof of {CCCpqrCsCCqCrtCqt} from the basis {CpCqp-RVP, CCpCqrCCpqCpr-SD} using any decent proof of the deduction metatheorem. Here the letters a, b, ..., n, o can get substituted by something else, but p, q, ..., y, z cannot. First we'll take out the "$" lines.
hypothesis 1 ! CCpqr
hypothesis 2 !@ s
hypothesis 3 !@# CqCrt
D[RVP].1 4 !@# CaCCpqr This is C4-1
D[SD].4 5 !@# CCaCpqCar
D5.RVP 6 !@# Cqr ... C4-7
D[RVP].3 7 !@# CaCqCrt ... C4-3
D[SD].7 8 !@# CCaqCaCrt
D8.[Caa] 9 !@# CqCrt ... C4-8
D[SD].9 10 !@# CCqrCqt
D10.6 11 !@# Cqt C4-9
.
.
.
Now for the "#" lines in the above demonstration. C3-3 and C3-9 match exactly. C3-10 we can obtain simply from SD just by substitution.
hypothesis 1 ! CCpqr
hypothesis 2 !@ s
theorem 3 !@ CCaCbCcdCaCCbcCbd (we'll use this when we used "SD" above)
D[RVP].1 4 !@ CaCCpqr
D[RVP].4 5 !@ CaCbCCpqr ... C3-4
D3.5 6 !@ CaCCbCpqCbr ... C3-5
theorem 7 !@ CaCbCcb
D[SD].6 8 !@ CCaCbCpqCaCbr
D8.7 9 !@ CaCqr ... C3-6
D3.RVP 10 !@ CCabCCcaCcb ... C3-8
D[SD].SD 11 !@ CCCaCbcCabCCaCbcCac
D11.9 12 !@ CCqCraCqa C3-11
Now the "@" lines.
hypothesis 1 ! CCpqr
theorem 2 ! CCaCbCcdCaCCbcCbd
theorem 3 ! CCaCbCcCdeCaCbCCcdCce (we'll use this where we used 3 above)
D[RVP].1 4 ! CaCCpqr C2-1
D[RVP].4 5 ! CaCbCCpqr C2-4
D[RVP].5 6 ! CaCbCcCCpqr ... C2-5
D3.6 7 ! CaCbCCcCpqCcr ... C2-6
theorem 8 ! CaCbCcCdc ... C2-7
D2.7 9 ! CaCCbCcCpqCbCcr ... C2-8
D[SD].9 10 ! CCaCbCcCpqCaCbCcr
D10.8 11 ! CaCbCqr ... C2-9
theorem 12 ! CaCbCcb
D3.12 13 ! CaCCbcCCdbCdc ... C2-10
D[SD].SD 14 ! CCCaCbcCabCCaCbcCac
D[RVP].14 15 ! CaCCCbCcdCbcCCbCcdCbd ... C2-11
D[SD].15 16 ! CCaCCbCcdCbcCaCCbCcdCbd
D16.11 17 ! CaCCqCrbCqr ... C2-12
And now we'll write the formal proof (allowing substitution for all lower case letters):
axiom 1 CpCqp C1-4
axiom 2 CCpCqrCCpqCpr
D1.2 3 CpCCqCrsCCqrCqs
D2.3 4 CCpCqCrsCpCCqrCqs ... SD above
D1.4 5 CpCCqCrCstCqCCrsCrt
D2.5 6 CCpCqCrCstCpCqCCrsCrt 2 above
D1.6 7 CpCCqCrCsCtuCqCrCCstCsu
D2.7 8 CCpCqCrCsCtuCpCqCrCCstCsu ... 3 above
D1.1 9 CpCqCrq
D2.9 10 CCpqCpCrq
D10.1 11 CpCqCrp ... C1-5
D10.11 12 CpCqCrCsp ... C1-6
D1.9 13 CpCqCrCsr ... C1-12
D1.13 14 CpCqCrCsCts ... C1-8
D8.12 15 CCpqCrCsCCtpCtq ... C1-7
D6.15 16 CCpqCrCCsCtpCsCtq ... C1-9
D4.16 17 CCpqCCrCsCtpCrCsCtq ... C1-10
D2.17 18 CCCpqCrCsCtpCCpqCrCsCtq
D18.14 19 CCCpqrCsCtCqr ... C1-11
D8.13 20 CpCqCCrsCCtrCts ... C1-13
D4.3 21 CpCCCqCrsCqrCCqCrsCqs ... C1-14
D1.21 22 CpCqCCCrCstCrsCCrCstCrt ... C1-15
D4.22 23 CpCCqCCrCstCrsCqCCrCstCrt ... C1-16
D2.23 24 CCpCqCCrCstCrsCpCqCCrCstCrt
D24.19 25 CCCpqrCsCCqCrtCqt
I'll point out that CCpqCCrpCrq is a theorem of this system as follows:
axiom 1 CpCqp
axiom 2 CCpCqrCCpqCpr
D1.2 3 CpCCqCrsCCqrCqs
D2.3 4 CCpCqCrsCpCCqrCqs
D4.1 5 CCpqCCrpCrq
But, even though it did appear in the set-ups to prove CCCpqrCsCCqCrtCqt, we never produced an actual proof of CCpqCCrpCrq, though we did produce a proof of CpCqCCrsCCtrCts in which CCpqCrpCrq can get said to qualify as contained within. I've used Prover9 to find a proof of {CpCqp, CCpCqrCCpqCpr} from {CCCpqrCsCCqCrtCqt}. Meredith also found that CtCCpqCCCspCqrCpr can also serve as a basis of the positive implicational calculus. Ted Ulrich has found some other single axioms for this system here.
Both axioms, "CtCCpqCCCspCqrCpr" and "CCCpqrCsCCqCrtCqt" have 17 symbols. A stronger system, the implicational calculus of propositions, has a single axiom with just 13 symbols.
Also, the conversion procedure I used implicitly here depends on *how* a particular meta-proof of the deduction meta-theorem works. If we have a different meta-proof of the deduction meta-theorem, we'll have a different conversion procedure. My May 10th answer here shows the same process via a distinct meta-proof of the meta-deduction theorem.
Tuesday, May 6, 2014
Logical Formula of the Day: self-distribution CCpCqrCCpqCpr.
Here's two links on condensed detachment. If we have two formulas Cab, and "a", condensed detachment produces the most general formula "b". For instance, if we have
1. CpCqp as "a" and
2. CCpCqrCCpqCpr as "Cab",
we could substitute "r" in CCpCqrCCpqCpr, and thus obtain CCpqCpp from a condensed detachment D2.1. We could also substitute "r" with "Cqp", and "p" with "Cqp" in CCpCqrCCpqCpr with Cqp obtaining CCCqpCqCqpCCCqppCCqpCqp, and then substitute "p" with "Cqp" in CpCqp obtaining CCqpCqCqp. Thus, from 1. and 2. we could detach CCCqpqCCqpCqp as a theorem. However, CCCqpqCCqpCqp is less general than CCpqCpp, since if we substitute "p" with "Cqp" in CCpqCpp, then we obtain CCCqpqCCqpCqp. So, condensed detachment Da.b obtains a form from which you can obtain every other theorem detachable from a substitution instance of "a" as the major premise and "b" as the minor premise.
Let's look a little at the system {CCpCqrCCpqCpr}
axiom 1 CCpCqrCCpqCpr
D1.1 2 CCCpCqrCpqCCpCqrCpr
D1.2 3 CCCCpCqrCpqCpCqrCCCpCqrCpqCpr
D1.3 4 CCCCCpCqrCpqCpCqrCCpCqrCpqCCCCpCqrCpqCpCqrCpr
Every theorem of this system obtained via condensed detachment has three variables. This follows, because the axiom has only three variables in the antecedent and the consequent. Thus, the second theorem has only three variables in the antecedent and the consequent.
If we have CCpCqrCCpqCpr and CpCqp as axioms or theorems, then we have a deduction metatheorem for the system which says "if we have an assumption "a" which leads to a formula "b" under the scope of some set of assumptions "g", then Cab holds under the scope of the assumptions "g" also". Or more concisely we can write:
Deduction Metatheorem: If {g, a} |- b, then {g}|-Cab.
Here's two links on condensed detachment. If we have two formulas Cab, and "a", condensed detachment produces the most general formula "b". For instance, if we have
1. CpCqp as "a" and
2. CCpCqrCCpqCpr as "Cab",
we could substitute "r" in CCpCqrCCpqCpr, and thus obtain CCpqCpp from a condensed detachment D2.1. We could also substitute "r" with "Cqp", and "p" with "Cqp" in CCpCqrCCpqCpr with Cqp obtaining CCCqpCqCqpCCCqppCCqpCqp, and then substitute "p" with "Cqp" in CpCqp obtaining CCqpCqCqp. Thus, from 1. and 2. we could detach CCCqpqCCqpCqp as a theorem. However, CCCqpqCCqpCqp is less general than CCpqCpp, since if we substitute "p" with "Cqp" in CCpqCpp, then we obtain CCCqpqCCqpCqp. So, condensed detachment Da.b obtains a form from which you can obtain every other theorem detachable from a substitution instance of "a" as the major premise and "b" as the minor premise.
Let's look a little at the system {CCpCqrCCpqCpr}
axiom 1 CCpCqrCCpqCpr
D1.1 2 CCCpCqrCpqCCpCqrCpr
D1.2 3 CCCCpCqrCpqCpCqrCCCpCqrCpqCpr
D1.3 4 CCCCCpCqrCpqCpCqrCCpCqrCpqCCCCpCqrCpqCpCqrCpr
Every theorem of this system obtained via condensed detachment has three variables. This follows, because the axiom has only three variables in the antecedent and the consequent. Thus, the second theorem has only three variables in the antecedent and the consequent.
If we have CCpCqrCCpqCpr and CpCqp as axioms or theorems, then we have a deduction metatheorem for the system which says "if we have an assumption "a" which leads to a formula "b" under the scope of some set of assumptions "g", then Cab holds under the scope of the assumptions "g" also". Or more concisely we can write:
Deduction Metatheorem: If {g, a} |- b, then {g}|-Cab.
Monday, May 5, 2014
Formula of the Day: Recursive Variable Prefixing CpCqp.
When proving that a logical system has a deduction metatheorem, CpCqp proves indispensable. In fact, CpCqp along with CCpCqrCCpqCpr or CCpqCCpCqrCpr suffices to prove a deduction metatheorem. Let's consider the system {CpCqp}. For this system:
Lemma: Every theorem obtainable by condensed detachment for the system {CpCqp} has the form C0C1...CnCpCqp.
Demonstration: The first theorem obtainable by condensed detachment is CpCqCrq. Now from {CpCqp, CpCqCrq} we can use either thesis as the minor premise, and either one as the major. If CpCqp is the major, then we will detach Cab where "a" is a variable and "b" consists of the minor premise. If CpCqCrq is the major premise, then we will obtain CpCqp. More generally, if we have CpCqp as the major premise and use any theorem "b" as the minor premise, we will obtain Cab upon a condensed detachment. If Cat, where "a" does not appear in "t" gets used as the major premise, then we will obtain "t" after a condensed detachment. Thus, any time we use condensed detachment in this system we'll either obtain CpCqp or some theorem which has CpCqp as its last 5 letters.
The above lemma can get argued also via mathematical induction.
Corollary: Every thesis (theorem or axiom) obtainable via condensed detachment for the system {CpCqp} can serve as a sole axiom for a system with the same theses as {CpCqp}.
Demonstration: Since every axiom has form C0C1...CnCpCqp by the above lemma, we can obtain CpCqp as a theorem of the system. Since CpCqp has C0C1...CnCpCqp as a theorem, it follows that the systems have the exact same theorems.
Consequently it follows that in addition to {CpCqp, CCpCqrCCpqCpr} sufficing to prove the deduction theorem *any* theorem obtainable from the system {CpCqp} solely by condensed detachment can take the place of CpCqp in {CpCqp, CCpCqrCCpqCpr} .
When proving that a logical system has a deduction metatheorem, CpCqp proves indispensable. In fact, CpCqp along with CCpCqrCCpqCpr or CCpqCCpCqrCpr suffices to prove a deduction metatheorem. Let's consider the system {CpCqp}. For this system:
Lemma: Every theorem obtainable by condensed detachment for the system {CpCqp} has the form C0C1...CnCpCqp.
Demonstration: The first theorem obtainable by condensed detachment is CpCqCrq. Now from {CpCqp, CpCqCrq} we can use either thesis as the minor premise, and either one as the major. If CpCqp is the major, then we will detach Cab where "a" is a variable and "b" consists of the minor premise. If CpCqCrq is the major premise, then we will obtain CpCqp. More generally, if we have CpCqp as the major premise and use any theorem "b" as the minor premise, we will obtain Cab upon a condensed detachment. If Cat, where "a" does not appear in "t" gets used as the major premise, then we will obtain "t" after a condensed detachment. Thus, any time we use condensed detachment in this system we'll either obtain CpCqp or some theorem which has CpCqp as its last 5 letters.
The above lemma can get argued also via mathematical induction.
Corollary: Every thesis (theorem or axiom) obtainable via condensed detachment for the system {CpCqp} can serve as a sole axiom for a system with the same theses as {CpCqp}.
Demonstration: Since every axiom has form C0C1...CnCpCqp by the above lemma, we can obtain CpCqp as a theorem of the system. Since CpCqp has C0C1...CnCpCqp as a theorem, it follows that the systems have the exact same theorems.
Consequently it follows that in addition to {CpCqp, CCpCqrCCpqCpr} sufficing to prove the deduction theorem *any* theorem obtainable from the system {CpCqp} solely by condensed detachment can take the place of CpCqp in {CpCqp, CCpCqrCCpqCpr} .
Sunday, May 4, 2014
Formula of the Day: C
δCpqδANpq.
"δ" in opposition to representing a propositional variable indicates a functorial variable of arity one. In other words, it stands for any of the unary functions presumed. Given the context of classical logic this means it stands for any of the functions belonging to {F, N, I, V} where F(0)=0, F(1)=0, N(0)=1, N(1)=0, I(0)=0, I(1)=1, V(0)=1, V(1). Thus we can check that CδCpqδANpq constitutes a tautology by checking that each member of {CFCpqFANpq, CNCpqNANpq, CICpqIANpq, CVCpqVANpq} is a tautology in 2-valued logic.
In notation for substitution for δ, an apostrophe " ' " means that we substitute the argument that follows delta for the apostrophe. For example, from 1 δp, 1 δ/C'q we substitute δ with C, then the argument that follows δ which is "p" in this case, and then "q" obtaining Cpq. If we write 2 CsδCpCqr, 2 δ/C'' that means we substitute δ with C, then the argument of δ CpCqr, then the argument of δ CpCqr obtaining CsCCpCqrCpCqr. If we write 3 CpCCpδqr, 3 δ/CC'r' then we write CC, the argument of δ q, r, and lastly the argument of δ "q" again in place of δq obtaining CpCCpCCqrqr. δ/' just means we substitute δ with the argument of δ.
δCpqδANpq can effectively take the place of a definition of the conditional "C" in a logical calculus. Let's consider CδCpqδANpq in the following system:
axiom 1 ApNp
axiom 2 CδCpqδANpq
2 δ/CCδCpqδ'CδANpqδCpq 3 CCCδCpqδCpqCδANpqδCpqCCδCpqδANpqCδANpqδCpq
2 δ/Cδ'δCpq 4 CCδCpqδCpqCδANpqδCpqD3.4 5 CCδCpqδANpqCδANpqδCpqD5.2 6 CδANpqδCpq6 δ/' 7 CANpqCpqD7.1 8 CpNNp
Thus, double negation introduction CpNNp follows from these two axioms.Saturday, May 3, 2014
Well-Formed Formula of the Day: ApNp
ApNp consists of a symbolic formulation of the law of the excluded middle "either a proposition is true or it is not true." If we wanted to use at as an axiom, we might want to have as a deduction rule {ANpq, p}->q, but even then we'd probably want to commute ApNp and use ANpp instead. Let's say we have ANpp as an axiom along with ANpANqp as an axiom. We might proceed as follows.
axiom 1 ANpp
axiom 2 ANpANqp
D2.2 3 ANpANqANrq
D2.1 4 ANpANqq
ApNp can get proved from the axiom set {CpCqp, CCpCqrCCpqCpr, CCNpqCCNpNqp, CpApq, CpAqp}. ApNp is unique among classical logic theorems which only have C, A, K, E, and N as connectives in them in that it has exactly 4 symbols.
ApNp consists of a symbolic formulation of the law of the excluded middle "either a proposition is true or it is not true." If we wanted to use at as an axiom, we might want to have as a deduction rule {ANpq, p}->q, but even then we'd probably want to commute ApNp and use ANpp instead. Let's say we have ANpp as an axiom along with ANpANqp as an axiom. We might proceed as follows.
axiom 1 ANpp
axiom 2 ANpANqp
D2.2 3 ANpANqANrq
D2.1 4 ANpANqq
ApNp can get proved from the axiom set {CpCqp, CCpCqrCCpqCpr, CCNpqCCNpNqp, CpApq, CpAqp}. ApNp is unique among classical logic theorems which only have C, A, K, E, and N as connectives in them in that it has exactly 4 symbols.
Friday, May 2, 2014
Formula of the Day: EEEpqrEpEqr
EEEpqrEpEqr comes as a way of saying that logical equivalence associates. Along with EEpqEqp can serve as one of the axioms of the equivalential calculus. Equivalential calculus allows us to deduce all tautologies which only have equivalence symbols and variables in them. The rule of inference for equivalential calculus comes as a modified form of detachment "from Eab, as well as "a", we may infer b" where "a" and "b" consist of meta-variables. Or more compactly
{Eab, a} -> b
We can condensed such an E-detachment along with uniform substitution just like we can condense C-detachment with uniform substitution. Taking EEEpqrEpEqr as an axiom, we can develop the system {EEEpqrEpEqr} as follows:
axiom 1 EEEpqrEpEqr
D1.1 2 EEpqErEpEqr
D1.2 3 EpEqErEpEqr
D2.1 4 EsEEEpqrEEpEqrs
D1.3 5 EpEqErEsEEpqErs
D1.4 6 EpEqEEErstEErEstEpq
D2.2 7 EpEEqrEEsEqErsp
D2.3 8 EsEpEEqErEpEqrs
The system with a single axiom which corresponds to each of these theorems has no last theorem under condensed detachment (unlike {Cpp} which has Cpp as its only theorem under condensed detachment). For {EEpqErEpEqr} each theorem will have some form Eab, which implies that there exists a substitution which enables a detachment from the antecedent of Epq of EEpqErEpEqr with EEpqErEpEqr as the major premise, and any theorem of the system {EEpqErEpEqr}. For the systems corresponding to theorems 3 through 8, each axiom serving as the major premise and any theorem serving as the minor premise enables a condensed detachment. Does *every* theorem EEEpqrEpEqr correspond to a system with a sole axiom which has no last theorem under condensed detachment?
EEEpqrEpEqr seems to come as a theorem that requires a fair amount of work to prove in the natural deduction systems I've encountered and in non-equivalential systems of logic which use definitions to get equivalences into the system.
EEEpqrEpEqr comes as a way of saying that logical equivalence associates. Along with EEpqEqp can serve as one of the axioms of the equivalential calculus. Equivalential calculus allows us to deduce all tautologies which only have equivalence symbols and variables in them. The rule of inference for equivalential calculus comes as a modified form of detachment "from Eab, as well as "a", we may infer b" where "a" and "b" consist of meta-variables. Or more compactly
{Eab, a} -> b
We can condensed such an E-detachment along with uniform substitution just like we can condense C-detachment with uniform substitution. Taking EEEpqrEpEqr as an axiom, we can develop the system {EEEpqrEpEqr} as follows:
axiom 1 EEEpqrEpEqr
D1.1 2 EEpqErEpEqr
D1.2 3 EpEqErEpEqr
D2.1 4 EsEEEpqrEEpEqrs
D1.3 5 EpEqErEsEEpqErs
D1.4 6 EpEqEEErstEErEstEpq
D2.2 7 EpEEqrEEsEqErsp
D2.3 8 EsEpEEqErEpEqrs
The system with a single axiom which corresponds to each of these theorems has no last theorem under condensed detachment (unlike {Cpp} which has Cpp as its only theorem under condensed detachment). For {EEpqErEpEqr} each theorem will have some form Eab, which implies that there exists a substitution which enables a detachment from the antecedent of Epq of EEpqErEpEqr with EEpqErEpEqr as the major premise, and any theorem of the system {EEpqErEpEqr}. For the systems corresponding to theorems 3 through 8, each axiom serving as the major premise and any theorem serving as the minor premise enables a condensed detachment. Does *every* theorem EEEpqrEpEqr correspond to a system with a sole axiom which has no last theorem under condensed detachment?
EEEpqrEpEqr seems to come as a theorem that requires a fair amount of work to prove in the natural deduction systems I've encountered and in non-equivalential systems of logic which use definitions to get equivalences into the system.
Thursday, May 1, 2014
Formula of the Day: The law of commutation CCpCqrCqCpr.
If we look at CCpCqrCqCpr it turns out that we can obtain the consequent implying the antecedent just from substitution. Let X p/a indicate that variable p gets substituted with a throughout formula X.
axiom 1 CCpCqrCqCpr
1 p/a 2 CCaCqrCqCar
2 q/p 3 CCaCprCpCar
3 a/q 4 CCqCprCpCqr
Or if we allow simultaneous substitution in a formula we can proceed as follows:
axiom 1 CCpCqrCqCpr
1 p/q, q/p 2 CCqCprCpCqr
The law of commutation, unlike the law of identity, can also serve as the sole axiom of a system under detachment, and from it as an axiom we can obtain well-formed formulas (or "formulas") which are not substitution instances of it (unlike Cpp as the sole axiom of a system).
axiom 1 CCpCqrCqCpr
D1.1 2 CpCCqCprCqr
D2.2 3 CCpCCqCCrCqsCrstCpt
D2.1 4 CCpCCCqCrsCrCqstCpt
D1.4 5 CpCCpCCCqCrsCrCqstt
D1.3 6 CpCCpCCqCCrCqsCrstt
D2.3 7 CCuCCCpCCqCCrCqsCrstCptvCuv
D2.7 8 CCwCCCuCCCpCCqCCrCqsCrstCptvCuvyCwy
D2.8 9 CCzCCCwCCCuCCCpCCqCCrCqsCrstCptvCuvyCwyaCza
The system {CCpCqrCqCpr} has no last most general theorem, as can get understood from theorem 2 CpCCqCprCqr. D2.x will always yield a theorem, since any variable can get substituted by any theorem, and CCqCprCqr where p is any theorem is a well-formed formula. Thus, D2.2 yields a theorem. D2.D2.2 yields a theorem. D2.D2.D2.2 yields a theorem and so on. Each theorem has more symbols than the last theorem also, since the antecedent "p" appears in the consequent of CpCCqCprCqr, and since every theorem has more symbols than Cp, the detached theorem having the form CCqCprCqr will have more letters than the theorem that served as the major premise. Theorems 5, and 6 also indicate that there exist subsystems of CCpCqrCqCpr which like the subsystem {CpCCqCprCqr} have no last most general theorem.
The law of commutation appeared in the first axiom system for propositional calculus ever proposed. Gottlob Frege's system was {CpCqp, CCpCqrCCpqCpr, CCpCqrCqCpr, CNNpp, CpNNp, CCpqCNqNp}. Jan Lukasiewicz figured out that the law of commutation could get derived from the first two axioms a few decades later. Here's a proof:
axiom 1 CpCqp
axiom 2 CCpCqrCCpqCpr
D1.2 3 CpCCqCrsCCqrCqs
D2.3 4 CCpCqCrsCpCCqrCqs
D1.4 5 CpCCqCrCstCqCCrsCrt
D2.5 6 CCpCqCrCstCpCqCCrsCrt
D6.1 7 CCpCqrCsCCpqCpr
D4.7 8 CCpCqrCCsCpqCsCpr
D2.8 9 CCCpCqrCsCpqCCpCqrCsCpr
D1.1 10 CpCqCrq
D9.10 11 CCpCqrCqCpr
The law of commutation also appears as an axiom or theorem in many other systems of logic. If one has it in a system S, and it does NOT need one of the axioms to get derived, then there may very well exist a way to figure out an alternative system A which has the same theorems as S. For instance, we'll start by pointing out that CCpCqrCqCpr comes as derivable from {CpCqp, CCpCqrCCpqCpr} above. Now since CCpqCNqNp and D [CCpCqrCCpqCpr].[CCpqCNqNp] exists it turns out that the theorems of Frege's system have another axiomization than {CpCqp, CCpCqrCCpqCpr, CNNpp, CpNNp, 5a-CCpqCNqNp}. Namely, that axiomization is {CpCqp, CCpCqrCCpqCpr, CNNpp, CpNNp, 5b-CNpCCqpNq}. To prove this we only need to write out that D[ CCpCqrCqCpr].5a yields 5b and D[CCpCqrCqCpr].5b yields 5a.
Also, let's suppose that we have CCpCqrCqCpr and Cpp as our axioms:
axiom 1 CCpCqrCqCpr
axiom 2 Cpp
D1.2 3 CpCCpqq
D3.2 4 CCCppqq
D1.4 5 CpCCCqqCprr
D1.5 6 CCCppCqrCqr
Notice that 6 is not the same formula as 4, but 6 is a more specialized (or less general) formula than 4 since we can obtain 6 from 4 by substitution only.
If we look at CCpCqrCqCpr it turns out that we can obtain the consequent implying the antecedent just from substitution. Let X p/a indicate that variable p gets substituted with a throughout formula X.
axiom 1 CCpCqrCqCpr
1 p/a 2 CCaCqrCqCar
2 q/p 3 CCaCprCpCar
3 a/q 4 CCqCprCpCqr
Or if we allow simultaneous substitution in a formula we can proceed as follows:
axiom 1 CCpCqrCqCpr
1 p/q, q/p 2 CCqCprCpCqr
The law of commutation, unlike the law of identity, can also serve as the sole axiom of a system under detachment, and from it as an axiom we can obtain well-formed formulas (or "formulas") which are not substitution instances of it (unlike Cpp as the sole axiom of a system).
axiom 1 CCpCqrCqCpr
D1.1 2 CpCCqCprCqr
D2.2 3 CCpCCqCCrCqsCrstCpt
D2.1 4 CCpCCCqCrsCrCqstCpt
D1.4 5 CpCCpCCCqCrsCrCqstt
D1.3 6 CpCCpCCqCCrCqsCrstt
D2.3 7 CCuCCCpCCqCCrCqsCrstCptvCuv
D2.7 8 CCwCCCuCCCpCCqCCrCqsCrstCptvCuvyCwy
D2.8 9 CCzCCCwCCCuCCCpCCqCCrCqsCrstCptvCuvyCwyaCza
The system {CCpCqrCqCpr} has no last most general theorem, as can get understood from theorem 2 CpCCqCprCqr. D2.x will always yield a theorem, since any variable can get substituted by any theorem, and CCqCprCqr where p is any theorem is a well-formed formula. Thus, D2.2 yields a theorem. D2.D2.2 yields a theorem. D2.D2.D2.2 yields a theorem and so on. Each theorem has more symbols than the last theorem also, since the antecedent "p" appears in the consequent of CpCCqCprCqr, and since every theorem has more symbols than Cp, the detached theorem having the form CCqCprCqr will have more letters than the theorem that served as the major premise. Theorems 5, and 6 also indicate that there exist subsystems of CCpCqrCqCpr which like the subsystem {CpCCqCprCqr} have no last most general theorem.
The law of commutation appeared in the first axiom system for propositional calculus ever proposed. Gottlob Frege's system was {CpCqp, CCpCqrCCpqCpr, CCpCqrCqCpr, CNNpp, CpNNp, CCpqCNqNp}. Jan Lukasiewicz figured out that the law of commutation could get derived from the first two axioms a few decades later. Here's a proof:
axiom 1 CpCqp
axiom 2 CCpCqrCCpqCpr
D1.2 3 CpCCqCrsCCqrCqs
D2.3 4 CCpCqCrsCpCCqrCqs
D1.4 5 CpCCqCrCstCqCCrsCrt
D2.5 6 CCpCqCrCstCpCqCCrsCrt
D6.1 7 CCpCqrCsCCpqCpr
D4.7 8 CCpCqrCCsCpqCsCpr
D2.8 9 CCCpCqrCsCpqCCpCqrCsCpr
D1.1 10 CpCqCrq
D9.10 11 CCpCqrCqCpr
The law of commutation also appears as an axiom or theorem in many other systems of logic. If one has it in a system S, and it does NOT need one of the axioms to get derived, then there may very well exist a way to figure out an alternative system A which has the same theorems as S. For instance, we'll start by pointing out that CCpCqrCqCpr comes as derivable from {CpCqp, CCpCqrCCpqCpr} above. Now since CCpqCNqNp and D [CCpCqrCCpqCpr].[CCpqCNqNp] exists it turns out that the theorems of Frege's system have another axiomization than {CpCqp, CCpCqrCCpqCpr, CNNpp, CpNNp, 5a-CCpqCNqNp}. Namely, that axiomization is {CpCqp, CCpCqrCCpqCpr, CNNpp, CpNNp, 5b-CNpCCqpNq}. To prove this we only need to write out that D[ CCpCqrCqCpr].5a yields 5b and D[CCpCqrCqCpr].5b yields 5a.
Also, let's suppose that we have CCpCqrCqCpr and Cpp as our axioms:
axiom 1 CCpCqrCqCpr
axiom 2 Cpp
D1.2 3 CpCCpqq
D3.2 4 CCCppqq
D1.4 5 CpCCCqqCprr
D1.5 6 CCCppCqrCqr
Notice that 6 is not the same formula as 4, but 6 is a more specialized (or less general) formula than 4 since we can obtain 6 from 4 by substitution only.
Subscribe to:
Posts (Atom)