Implicational propositional calculus

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.


Wikimedia Foundation. 2010.

Игры ⚽ Поможем решить контрольную работу

Look at other dictionaries:

  • implicational propositional calculus — noun A minimalist version of propositional calculus which uses only the logical connectives ( implies ) and ( false ) …   Wiktionary

  • Propositional calculus — In mathematical logic, a propositional calculus or logic (also called sentential calculus or sentential logic) is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules… …   Wikipedia

  • Peirce's law — in logic is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic. In propositional calculus, Peirce s law says that (( P → Q )→ P )→ P . Written out, this… …   Wikipedia

  • Material conditional — The material conditional, also known as material implication, is a binary truth function, such that the compound sentence p→q (typically read if p then q or p implies q ) is logically equivalent to the negative compound: not (p and not q). A… …   Wikipedia

  • Peirce's law — noun The classically valid but intuitionistically non valid formula of propositional calculus, which can be used as an substitute for the law of excluded middle in implicational propositional calculus …   Wiktionary

  • List of mathematics articles (I) — NOTOC Ia IA automorphism ICER Icosagon Icosahedral 120 cell Icosahedral prism Icosahedral symmetry Icosahedron Icosian Calculus Icosian game Icosidodecadodecahedron Icosidodecahedron Icositetrachoric honeycomb Icositruncated dodecadodecahedron… …   Wikipedia

  • logic, history of — Introduction       the history of the discipline from its origins among the ancient Greeks to the present time. Origins of logic in the West Precursors of ancient logic       There was a medieval tradition according to which the Greek philosopher …   Universalium

  • formal logic — the branch of logic concerned exclusively with the principles of deductive reasoning and with the form rather than the content of propositions. [1855 60] * * * Introduction       the abstract study of propositions, statements, or assertively used …   Universalium

  • Necessary and sufficient condition — This article is about the formal terminology in logic. For causal meanings of the terms, see Causality. In logic, the words necessity and sufficiency refer to the implicational relationships between statements. The assertion that one statement is …   Wikipedia

  • Curry–Howard correspondence — A proof written as a functional program: the proof of commutativity of addition on natural numbers in the proof assistant Coq. nat ind stands for mathematical induction, eq ind for substitution of equals and f equal for taking the same function… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”