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.
Monday, June 23, 2014
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?
Subscribe to:
Posts (Atom)