I started looking at the following a few days after I read J. A. Kalman's paper on condensed detachment where he uses condensed detachment on non-tautologous formulas.
In some logical systems we can obtain a propositional variable as a theorem. For instance, if our axiom is CpCqr, then we have the following:
axiom 1 CpCqr.
D1.1 2 Cpq.
D2.2 3 p.
Since p could mean the constant false proposition "0" this means such a system can prove a false proposition. Most logical systems I've seen can only prove tautologies for some semantics. It turns out there exist logical systems which have non-tautologous formula, but also can't prove a propositional variable. Here's one:
axiom 1 CCCpqqp
D1.1 2 Cpp
It turns out that if our only inference rule is condensed detachment, and CCCpqqp is our only axiom, the entire system of theorems is {CCCpqqp, Cpp}. From Kalman's theorem that everything deducible from substitution and detachment is a substitution of a formula deducible by condensed detachment and conversely, it follows that you can't deduce a falsity just from substitution in this system.
That said, if you were to say join CCCpqqp to a system for classical logic like Lukasiewicz's preferred axiom set, then you could deduce a variable.
axiom 1 CCpqCCqrCpr
axiom 2 CpCNpq
axiom 3 CCNppp
axiom 4 CCCpqqp
D4.3 5 Np
D2.5 6 CNNpq
D6.5 7 p
Saturday, July 5, 2014
Monday, June 23, 2014
There's a correspondence between the use of derivable rules of inference and the notation used for condensed detachment. Let's say our axioms are
1 CCpqCCqrCpr
2 CpCNpq
3 CCNppp
and we have condensed detachment {Cab, a'} |-b' as our rule of inference. We can write a proof of Cpp as follows:
D1.2 4 CCCNpqrCpr
D4.3 5 Cpp
We could also write:
D1.2 4 CCNpqrCpr
DD1.2.3 5 Cpp
From axiom 1 and having condensed detachment as our rule of inference, we have
{Cab, Cb'c} |- Ca'c' as a rule of inference. In effect {Cab, Cb'c} |- Ca'c' with "x" as "Cab" and "y" as "Cb'c" produces the same formula as DD1.x.y. And in general it seems that if a derivable rule of inference comes as derivable just from one formula "f" by the rule generation schema "from |-Cab, we may infer a|-b" that the use of the derivable rule of inference on formulas a, ..., e corresponds to
D...Dfa...e where the number of "D's" equals the number of formulas in the sequence a, ..., e. For example, if we substituted r/CsCtCCCuvwx in CCpqCCqrCpr we would then have
9 CCpqCCqCsCtCCCuvwxCpCsCtCCCuvwx. For formulas i1,..., in, formula 9 has derivable rules of inference corresponding to:
DD9.i1.i2 {Cab, Cb'CcCdCCCefgh} |- Ca'Cc'Cd'CCCe'f'g'h'
DDD9.i1.i2.i3 {Cab, Cb'CcCdCCCefgh, a'} |- Cc'Cd'CCCe'f'g'h'
DDDD9.i1.i2.i3.i4 {Cab, Cb'CcCdCCCefgh, a', c'} |- Cd'CCCe'f'g'h'
DDDDD9.i1.i2.i3.i4.i5 {Cab, Cb'CcCdCCCefgh, a', c', d'} |- CCCe'f'g'h'
DDDDDD9.i1.i2.i3.i4.i5.i5 {Cab, Cb'CcCdCCCefgh, a', c', d', CCe'f'g'} |-h'
Consider the following proof of CCpCqrCCsqCpCsr.
axiom 1 CCpqCCqrCCpr
DD1.1.D1.1 2 CCpCqrCCsqCpCsr
We can thus, in effect, work through this proof in different ways. We could proceed as thus
axiom 1 CCpqCCqrCpr
D1.1 2 CCCCqrCprsCCpqs
D2.2 3 CCpCqrCCsqCpCsr
We could also though proceed by computing D1.1, and thus using the derivable rule of inference {Cab, Cb'c} |- Ca'c', computing DD1.1D1.1.
CCab C C b c C a c
| | | | ------
| | ---- ---- |
C C C Cqr Cpr s CCpqs
Thus, b/Cqr, c/Cpr, and s/Cac which turns into b/Cqr, c/Cpr, s/CaCpr. This proof is simpler than computing D2.2.
C CCC a b Ccb d CCcad
| | ---- |
---- --- | --------
CCC Cqr Cpr s CCpqs
Here the diagram suggests a/Cqr, b/Cpr, s/Ccb, d/CCpqs, which turns into a/Cqr, b/Cpr, s/CcCpr, d/CCpqCcCpr. The substitutions here end up more complex than when using the derivable rule of inference.
1 CCpqCCqrCpr
2 CpCNpq
3 CCNppp
and we have condensed detachment {Cab, a'} |-b' as our rule of inference. We can write a proof of Cpp as follows:
D1.2 4 CCCNpqrCpr
D4.3 5 Cpp
We could also write:
D1.2 4 CCNpqrCpr
DD1.2.3 5 Cpp
From axiom 1 and having condensed detachment as our rule of inference, we have
{Cab, Cb'c} |- Ca'c' as a rule of inference. In effect {Cab, Cb'c} |- Ca'c' with "x" as "Cab" and "y" as "Cb'c" produces the same formula as DD1.x.y. And in general it seems that if a derivable rule of inference comes as derivable just from one formula "f" by the rule generation schema "from |-Cab, we may infer a|-b" that the use of the derivable rule of inference on formulas a, ..., e corresponds to
D...Dfa...e where the number of "D's" equals the number of formulas in the sequence a, ..., e. For example, if we substituted r/CsCtCCCuvwx in CCpqCCqrCpr we would then have
9 CCpqCCqCsCtCCCuvwxCpCsCtCCCuvwx. For formulas i1,..., in, formula 9 has derivable rules of inference corresponding to:
DD9.i1.i2 {Cab, Cb'CcCdCCCefgh} |- Ca'Cc'Cd'CCCe'f'g'h'
DDD9.i1.i2.i3 {Cab, Cb'CcCdCCCefgh, a'} |- Cc'Cd'CCCe'f'g'h'
DDDD9.i1.i2.i3.i4 {Cab, Cb'CcCdCCCefgh, a', c'} |- Cd'CCCe'f'g'h'
DDDDD9.i1.i2.i3.i4.i5 {Cab, Cb'CcCdCCCefgh, a', c', d'} |- CCCe'f'g'h'
DDDDDD9.i1.i2.i3.i4.i5.i5 {Cab, Cb'CcCdCCCefgh, a', c', d', CCe'f'g'} |-h'
Consider the following proof of CCpCqrCCsqCpCsr.
axiom 1 CCpqCCqrCCpr
DD1.1.D1.1 2 CCpCqrCCsqCpCsr
We can thus, in effect, work through this proof in different ways. We could proceed as thus
axiom 1 CCpqCCqrCpr
D1.1 2 CCCCqrCprsCCpqs
D2.2 3 CCpCqrCCsqCpCsr
We could also though proceed by computing D1.1, and thus using the derivable rule of inference {Cab, Cb'c} |- Ca'c', computing DD1.1D1.1.
CCab C C b c C a c
| | | | ------
| | ---- ---- |
C C C Cqr Cpr s CCpqs
Thus, b/Cqr, c/Cpr, and s/Cac which turns into b/Cqr, c/Cpr, s/CaCpr. This proof is simpler than computing D2.2.
C CCC a b Ccb d CCcad
| | ---- |
---- --- | --------
CCC Cqr Cpr s CCpqs
Here the diagram suggests a/Cqr, b/Cpr, s/Ccb, d/CCpqs, which turns into a/Cqr, b/Cpr, s/CcCpr, d/CCpqCcCpr. The substitutions here end up more complex than when using the derivable rule of inference.
Friday, June 6, 2014
I wrote about a way to generate more bases for classical logic about a year ago, when you have either CCpqCCqrCpr or CpCqp upfront in the basis. Examples of such systems are {CCpqCCqrCpr, CCNppp, CpCNpq}-Lukasiewicz, {CCpqCCqrCpr, CCpCpqCpq, CpCqp, CCNpNqCqp}-Tarski, {CpCqp, CCpCqrCCpqCpr, CCNpqCCNpNqp}-I don't think think I've seen this before, but it's basically implied by a system of Mendelsohn since if any system has [C] CCpCqrCqCpr provable in a proper sub-basis without axioms a, ..., z, of the basis, then a can get replaced by D[C].a, b can get replaced by D[C].b, ... z can get replaced by D[C].z. For example, for the basis {CCpCqrCCpqCpr, CpCqp, CCNpNqCqp}, [C] can get proved in the sub-basis {CpCqp, CCpCqrCCpqCpr}. Thus, CCNpNqCqp can get replaced by CpCCNqNpq for the basis {CCpCqrCCpqCpr, CpCqp, CCNpNqCqp}.
The following 4-basis for C-N classical logic is independent:
1. CCCCpqCrqsCCrps
2. CCpqCCNppq
3. CCCNpqrCpr
4. Cpp
Or as a system with fewer symbols, the axioms of the following are independent.
1. CCpqCCqrCpr
2. CCpqCCNppq
3. CpCNpq
4. Cpp
Does there exist a shorter 4-basis with independent axioms for C-N classical logic?
I note also that the following four formulas are not independent
1. CCpqCCqrCpr
2. CCNppp
3. CCCNpqrCpr
4. Cpp
since D3.2 yields Cpp.
Does there exist a 3-basis or a 2-basis for classical logic where one of the axioms is Cpp?
The following 4-basis for C-N classical logic is independent:
1. CCCCpqCrqsCCrps
2. CCpqCCNppq
3. CCCNpqrCpr
4. Cpp
Or as a system with fewer symbols, the axioms of the following are independent.
1. CCpqCCqrCpr
2. CCpqCCNppq
3. CpCNpq
4. Cpp
Does there exist a shorter 4-basis with independent axioms for C-N classical logic?
I note also that the following four formulas are not independent
1. CCpqCCqrCpr
2. CCNppp
3. CCCNpqrCpr
4. Cpp
since D3.2 yields Cpp.
Does there exist a 3-basis or a 2-basis for classical logic where one of the axioms is Cpp?
Wednesday, May 28, 2014
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.
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.
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.
Subscribe to:
Posts (Atom)