Saturday, July 5, 2014

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