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.

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?