Implicational propositional calculus

From Wikipedia, the free encyclopedia

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 ...", "→", "\rightarrow \!", etc..

Contents

[edit] 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 PF
  • PQ is equivalent to (P→(QF))→F
  • PQ is equivalent to (PF)→Q
  • PQ is equivalent to ((PQ)→((QP)→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.

[edit] Axioms

Where in each case, P, Q, R may be replaced by any proposition which contains only "→" as a connective.

[edit] 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→((BA)→A))→((A→(BA))→(AA)) 1. axiom 2
  • A→((BA)→A) 2. axiom 1
  • (A→(BA))→(AA) 3. modus ponens 2,1
  • A→(BA) 4. axiom 1
  • AA 5. modus ponens 4,3 QED

And then proceed as explained in deduction theorem.

[edit] Substituting for falsity

If A and Z are propositions, then AZ 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, (AZ)→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.

[edit] 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 PkZ (when Pk is given the value falsity) or (PkZ)→Z (when Pk is given the value truth) one can deduce similar propositions for each subformula of S. This requires three lemmas given below.

[edit] Lemma for a true conclusion

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

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

[edit] Lemma for a false hypothesis

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

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

[edit] 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 PQ will be given the value falsity. So we need to show that (PQ)→Z can be proved from the assumptions about the valuation.

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

[edit] Completeness of the axioms, part 2

In the first part of the completeness proof, we showed that (SZ)→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 (PZ)→((SZ)→Z) and similarly we get ((PZ)→Z)→((SZ)→Z), both following from a reduced set of assumptions in which P does not occur.

    • (PZ)→((SZ)→Z) 1. hypothesis
      • ((PZ)→Z)→((SZ)→Z) 2. hypothesis
        • SZ 3. hypothesis
          • PZ 4. hypothesis
          • (SZ)→Z 5. modus ponens 4,1
          • Z 6. modus ponens 3,5
        • (PZ)→Z 7. deduction from 4 to 6
        • (SZ)→Z 8. modus ponens 7,2
        • Z 9. modus ponens 3,8
      • (SZ)→Z 10. deduction from 3 to 9
    • [((PZ)→Z)→((SZ)→Z)]→[(SZ)→Z] 11. deduction from 2 to 10
  • [(PZ)→((SZ)→Z)]→

([((PZ)→Z)→((SZ)→Z)]→[(SZ)→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 (SZ)→Z where S is a tautology and Z is any proposition. Now, we choose Z to be the same as S. Thus (SS)→S is a theorem whenever S is a tautology. But, SS 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.

[edit] 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)→((¬AB)→A) to derive (AB)→((¬AB)→B) which is then used to combine the lines of the truth table together.

[edit] See also

[edit] References

Languages