Implicational propositional calculus

In mathematical logic, the implicational propositional calculus is a version of classical (two-valued) propositional calculus which uses only one connective, called implication or conditional. In formulas, this binary operation is indicated by "implies", "if ..., then ...", "→", "$ightarrow\; !$", etc..

Virtual completeness as an operator

Implication alone is not complete as a logical operator because one cannot form all other two-valued truth functions from it. However, if one has a proposition which is known to be false and uses that as if it were a zero-ary connective for falsity, then one can define all other truth functions. So implication is virtually complete as an operator. If "P","Q", and "F" are propositions and "F" is known to be false, then:
*¬"P" is equivalent to "P"→"F"
*"P"∧"Q" is equivalent to ("P"→("Q"→"F"))→"F"
*"P"∨"Q" is equivalent to ("P"→"F")→"Q"
*"P"↔"Q" is equivalent to (("P"→"Q")→(("Q"→"P")→"F"))→"F"

More generally, since the above operators are known to be sufficient to express any truth function, it follows that any truth function can be expressed in terms of "→" and "F", if we have a proposition "F" which is known to be false.

It is worth noting that "F" is not definable from → and arbitrary sentence variables. Suppose there were such a (finite) formula, using only → and arbitrary sentence variables, equivalent to "F". Then, by the well-orderedness of formulae length, there would be a shortest such formula "S". "S" would certainly contain one instance of → (otherwise it would just be an arbitrary sentence variable and therefore not equivalent to "F") and hence would contain an instance of → whose scope was "S". In order for "S" to always be false, then, "S" would have to have a consequent that were always false, but such a consequent would be a constituent of "S" and therefore shorter in length. Hence the consequent would be a formula equivalent to "F" shorter than "S", but by assumption, "S" is the shortest such formula.

It follows as a corollary that {→} is not truth-functionally complete. It cannot, for example, be used to define the two-place truth function that always returns "false".

Axioms

*Axiom schema 1 is "P"→("Q"→"P").
*Axiom schema 2 is ("P"→("Q"→"R"))→(("P"→"Q")→("P"→"R")).
*Axiom schema 3 (Peirce's law) is (("P"→"Q")→"P")→"P".
*The one rule of inference (modus ponens) is: from "P" and "P"→"Q" infer "Q".Where in each case, "P", "Q", "R" may be replaced by any proposition which contains only "→" as a connective.

Deduction meta-theorem

The first task is to derive the deduction meta-theorem using axioms 1, 2, and modus ponens.
We begin by proving a theorem schema (where "A" and "B" may be replaced by any propositions which contain only "→" as a connective):
*("A"→(("B"→"A")→"A"))→(("A"→("B"→"A"))→("A"→"A")) 1. axiom 2
*"A"→(("B"→"A")→"A") 2. axiom 1
*("A"→("B"→"A"))→("A"→"A") 3. modus ponens 2,1
*"A"→("B"→"A") 4. axiom 1
*"A"→"A" 5. modus ponens 4,3 QED

And then proceed as explained in deduction theorem.

ubstituting for falsity

If "A" and "Z" are propositions, then "A"→"Z" is equivalent to (¬"A*")∨"Z", where "A*" is the result of replacing in "A" all, some, or none of the occurrences of "Z" by falsity. Similarly, ("A"→"Z")→"Z" is equivalent to "A*"∨"Z". So under some conditions, one can use them as substitutes for saying "A*" is false or "A*" is true respectively.

Completeness of the axioms, part 1

We will see that the axioms are complete in the sense that any tautology which contains only "→" as a connective can be deduced from them. Consider a tautology "S" which contains only "P1", "P2", ..., "Pn" as atomic propositions (propositional variables).

Choose a line in the truth table for "S". It shows the truth values of each subformula of "S" for a particular valuation (function from the propositional variables to {falsity, truth}). By mathematical induction on the length of the subformulas, we will show that from propositions of the form "Pk"→"Z" (when "Pk" is given the value falsity) or ("Pk"→"Z")→"Z" (when "Pk" is given the value truth) one can deduce similar propositions for each subformula of "S". This requires three lemmas given below.

Lemma for a true conclusion

Consider the subformula "P"→"Q" of "S". If "Q" is given the value truth by the valuation, then "P"→"Q" will be given the value truth also. So we need to show that (("P"→"Q")→"Z")→"Z" can be proved from the assumptions about the valuation.

**("Q"→"Z")→"Z" 1. hypothesis
***("P"→"Q")→"Z" 2. hypothesis
****"Q" 3. hypothesis
*****"P" 4. hypothesis
*****"Q" 5. reiteration of 3
****"P"→"Q" 6. deduction from 4 to 5
****"Z" 7. modus ponens 6,2
***"Q"→"Z" 8. deduction from 3 to 7
***"Z" 9. modus ponens 8,1
**(("P"→"Q")→"Z")→"Z" 10. deduction from 2 to 9
*(("Q"→"Z")→"Z")→((("P"→"Q")→"Z")→"Z") 11. deduction from 1 to 10 QED

Lemma for a false hypothesis

If "P" is given the value falsity by the valuation, then "P"→"Q" will be given the value truth. So we need to show that (("P"→"Q")→"Z")→"Z" can be proved from the assumptions about the valuation.

**"P"→"Z" 1. hypothesis
***("P"→"Q")→"Z" 2. hypothesis
****"Z"→"Q" 3. hypothesis
*****"P" 4. hypothesis
*****"Z" 5. modus ponens using steps 4 and 1
*****"Q" 6. modus ponens using steps 5 and 3
****"P"→"Q" 7. deduction from 4 to 6
****"Z" 8. modus ponens using steps 7 and 2
***("Z"→"Q")→"Z" 9. deduction from 3 to 8
***(("Z"→"Q")→"Z")→"Z" 10. Peirce's law
***"Z" 11. modus ponens using steps 9 and 10
**(("P"→"Q")→"Z")→"Z" 12. deduction from 2 to 11
*("P"→"Z")→(("P"→"Q")→"Z")→"Z") 13. deduction from 1 to 12 QED

Lemma for a true hypothesis and a false conclusion

If "P" is given the value truth and "Q" is given the value falsity by the valuation, then "P"→"Q" will be given the value falsity. So we need to show that ("P"→"Q")→"Z" can be proved from the assumptions about the valuation.

**("P"→"Z")→"Z" 1. hypothesis
***"Q"→"Z" 2. hypothesis
****"P"→"Q" 3. hypothesis
*****"P" 4. hypothesis
*****"Q" 5. modus ponens 4,3
*****"Z" 6. modus ponens 5,2
****"P"→"Z" 7. deduction from 4 to 6
****"Z" 8. modus ponens 7,1
***("P"→"Q")→"Z" 9. deduction from 3 to 8
**("Q"→"Z")→(("P"→"Q")→"Z") 10. deduction from 2 to 9
*(("P"→"Z")→"Z")→ [("Q"→"Z")→(("P"→"Q")→"Z")] 11. deduction from 1 to 10 QED

Completeness of the axioms, part 2

In the first part of the completeness proof, we showed that ("S"→"Z")→"Z" can be proved for each valuation of the tautology "S", given appropriate assumptions about the propositional variables. Now we will combine the valuations together and eliminate the assumptions about the propositional variables.

Consider one of the propositional variables which has not yet been eliminated from the assumptions, say it is "P". Then using the deduction meta-theorem, we get ("P"→"Z")→(("S"→"Z")→"Z") and similarly we get (("P"→"Z")→"Z")→(("S"→"Z")→"Z"), both following from a reduced set of assumptions in which "P" does not occur.

**("P"→"Z")→(("S"→"Z")→"Z") 1. hypothesis
***(("P"→"Z")→"Z")→(("S"→"Z")→"Z") 2. hypothesis
****"S"→"Z" 3. hypothesis
*****"P"→"Z" 4. hypothesis
*****("S"→"Z")→"Z" 5. modus ponens 4,1
*****"Z" 6. modus ponens 3,5
****("P"→"Z")→"Z" 7. deduction from 4 to 6
****("S"→"Z")→"Z" 8. modus ponens 7,2
****"Z" 9. modus ponens 3,8
***("S"→"Z")→"Z" 10. deduction from 3 to 9
** [(("P"→"Z")→"Z")→(("S"→"Z")→"Z")] → [("S"→"Z")→"Z"] 11. deduction from 2 to 10
* [("P"→"Z")→(("S"→"Z")→"Z")] →( [(("P"→"Z")→"Z")→(("S"→"Z")→"Z")] → [("S"→"Z")→"Z"] ) 12. deduction from 1 to 11 QED

So we can combine pairs of lines of the truth table together and repeat this process until all assumptions about the values of propositional variables have been eliminated. The result will be that we have proved ("S"→"Z")→"Z" where "S" is a tautology and "Z" is any proposition. Now, we choose "Z" to be the same as "S". Thus ("S"→"S")→"S" is a theorem whenever "S" is a tautology. But, "S"→"S" is an instance of the theorem schema we proved earlier. So by modus ponens, "S" is a theorem for any tautology "S". Thus our axioms are complete.

This proof is constructive. That is, given a tautology, one could actually follow the instructions and create a proof of it from our axioms. However, the length of such a proof would increase super-exponentially with the number of propositional variables in the tautology. So it is not a practical method for any but the very shortest tautologies. None the less, if you are stuck trying to develop a proof, it may help to start to generate one this way. You might discover short-cuts which would give you a proof of reasonable length.

Excluded middle in the completeness theorem

It is interesting to notice that the law of excluded middle (in the form of Peirce's law, our axiom 3) appears only once in our proof of completeness, to wit, in the proof of the lemma for a false hypothesis.

By contrast, the completeness proof for propositional logic in Mendelson (on which this one was loosely modelled) uses the law of excluded middle in many places, especially in the step where the lines of the truth table are combined together to eliminate dependence on the propositional variables. He uses his third axiom (¬"A"→¬"B")→((¬"A"→"B")→"A") to derive ("A"→"B")→((¬"A"→"B")→"B") which is then used to combine the lines of the truth table together.

ee also

*Propositional calculus
*Deduction theorem
*Peirce's law
*Tautology (logic)
*Truth table
*Valuation (logic)

References

* Mendelson, Elliot (1997) [http://worldcat.org/oclc/259359 "Introduction to Mathematical Logic", 4th ed.] London: Chapman & Hall.