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
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment