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.

No comments:

Post a Comment