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