Axiomatic system (logic)

In logic, especially mathematical logic, an axiomatic system, sometimes called a "Hilbert-style" deductive system, is a type of system of formal deduction developed by Gottlob Frege, Jan Łukasiewicz, Russell and Whitehead, and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.

Most variants of axiomatic systems take a characteristic tack in the way they balance a trade-off between logical axioms and rules of inference. Axiomatic systems can be characterised by the choice of a large number of schemes of logical axioms and a small set of rules of inference. Systems of natural deduction take the opposite tack, including many deduction rules but very few or no axiom schemata. The most commonly studied axiomatic systems have either just one rule of inference – modus ponens, for propositional logics – or two – with generalisation, to handle predicate logics, as well – and several infinite axiom schemes. Axiomatic systems for alethic modal logics, sometimes called Hilbert-Lewis systems, additionally require the necessitation rule. Some systems use a finite list of concrete formulas as axioms instead of an infinite set of formulas via axiom schemes, in which case the uniform substitution rule is required.

A characteristic feature of the many variants of axiomatic systems is that the context is not changed in any of their rules of inference, while both natural deduction and sequent calculus contain some context-changing rules. Thus, if one is interested only in the derivability of tautologies, no hypothetical judgments, then one can formalize the axiomatic system in such a way that its rules of inference contain only judgments of a rather simple form. The same cannot be done with the other two deductions systems: as context is changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided – not even if we want to use them just for proving derivability of tautologies.

Propositional logic

In propositional logic, it is possible to perform proofs axiomatically, which means that certain tautologies are taken as self-evident and various others are deduced from them using modus ponens as an inference rule, and a rule of substitution. Alternatively, one uses axiom schemas instead of axioms, and no rule of substitution is used.

Frege's Begriffsschrift

Although axiomatic proof has been used since the famous Ancient Greek textbook, Euclid's Elements of Geometry, in propositional logic it dates back to Gottlob Frege's 1879 Begriffsschrift. Frege's system used only implication and negation as connectives, and it had six axioms, which were these ones:

• Proposition 1: $a\supset (b\supset a)$
• Proposition 2: $(c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))$
• Proposition 8: $(d\supset (b\supset a))\supset (b\supset (d\supset a))$
• Proposition 28: $(b\supset a)\supset (\neg a\supset \neg b)$
• Proposition 31: $\neg \neg a\supset a$
• Proposition 41: $a\supset \neg \neg a$

These were used by Frege together with modus ponens and a rule of substitution (which was used but never precisely stated) to yield a complete and consistent axiomatization of classical truth-functional propositional logic.

Łukasiewicz's P₂

Jan Łukasiewicz showed that, in Frege's system, "the third axiom is superfluous since it can be derived from the preceding two axioms, and that the last three axioms can be replaced by the single sentence $CCNpNqCpq$". Which, taken out of Łukasiewicz's Polish notation into modern notation, means $(\neg p\rightarrow \neg q)\rightarrow (p\rightarrow q)$. Hence, Łukasiewicz is credited with this system of three axioms:

• $p\to (q\to p)$
• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$
• $(\neg p\to \neg q)\to (q\to p)$

Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule. The exact same system was given (with an explicit substitution rule) by Alonzo Church, who referred to it as the system P_2, and helped popularize it.

Schematic form of P₂

A graphic representation of the deduction system

One may avoid using the rule of substitution by giving the axioms in schematic form, using them to generate an infinite set of axioms. Hence, using Greek letters to represent schemata (metalogical variables that may stand for any well-formed formulas), the axioms are given as:

• $\varphi \to (\psi \to \varphi )$
• $(\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))$
• $(\neg \varphi \to \neg \psi )\to (\psi \to \varphi )$

The schematic version of P₂ is attributed to John von Neumann, and is used in the Metamath "set.mm" formal proof database. It has also been attributed to Hilbert, and named ${\mathcal {H}}$ in this context.

Proof example in P₂

As an example, a proof of $A\to A$ in P₂ is given below. First, the axioms are given names:

(A1) $(p\to (q\to p))$

(A2) $((p\to (q\to r))\to ((p\to q)\to (p\to r)))$

(A3) $((\neg p\to \neg q)\to (q\to p))$

And the proof is as follows:

1. $A\to ((B\to A)\to A)$       (instance of (A1))
2. $(A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))$       (instance of (A2))
3. $(A\to (B\to A))\to (A\to A)$       (from (1) and (2) by modus ponens)
4. $A\to (B\to A)$       (instance of (A1))
5. $A\to A$       (from (4) and (3) by modus ponens)

Consistency and completeness of P₂

The crucial properties of this set of rules are that they are sound and complete. Informally this means that the rules are correct and that no other rules are required. These claims can be made more formal as follows. The proofs for the soundness and completeness of the propositional logic are not themselves proofs in propositional logic; these are theorems in ZFC used as a metatheory to prove properties of propositional logic.

We define a truth assignment as a function that maps propositional variables to true or false. Informally such a truth assignment can be understood as the description of a possible state of affairs (or possible world) where certain statements are true and others are not. The semantics of formulas can then be formalized by defining for which "state of affairs" they are considered to be true, which is what is done by the following definition.

We define when such a truth assignment A satisfies a certain well-formed formula with the following rules:

• A satisfies the propositional variable P if and only if A(P) = true
• A satisfies ¬φ if and only if A does not satisfy φ
• A satisfies (φ ∧ ψ) if and only if A satisfies both φ and ψ
• A satisfies (φ ∨ ψ) if and only if A satisfies at least one of either φ or ψ
• A satisfies (φ → ψ) if and only if it is not the case that A satisfies φ but not ψ
• A satisfies (φ ↔ ψ) if and only if A satisfies both φ and ψ or satisfies neither one of them

With this definition we can now formalize what it means for a formula φ to be implied by a certain set S of formulas. Informally this is true if in all worlds that are possible given the set of formulas S the formula φ also holds. This leads to the following formal definition: We say that a set S of well-formed formulas semantically entails (or implies) a certain well-formed formula φ if all truth assignments that satisfy all the formulas in S also satisfy φ.

Finally we define syntactical entailment such that φ is syntactically entailed by S if and only if we can derive it with the inference rules that were presented above in a finite number of steps. This allows us to formulate exactly what it means for the set of inference rules to be sound and complete:

Soundness: If the set of well-formed formulas S syntactically entails the well-formed formula φ then S semantically entails φ.

Completeness: If the set of well-formed formulas S semantically entails the well-formed formula φ then S syntactically entails φ.

For the above set of rules this is indeed the case.

Sketch of a soundness proof

(For most logical systems, this is the comparatively "simple" direction of proof)

Notational conventions: Let G be a variable ranging over sets of sentences. Let A, B and C range over sentences. For "G syntactically entails A" we write "G proves A". For "G semantically entails A" we write "G implies A".

We want to show: (A)(G) (if G proves A, then G implies A).

We note that "G proves A" has an inductive definition, and that gives us the immediate resources for demonstrating claims of the form "If G proves A, then ...". So our proof proceeds by induction.

1. Basis. Show: If A is a member of G, then G implies A.
2. Basis. Show: If A is an axiom, then G implies A.
3. Inductive step (induction on n, the length of the proof):
   1. Assume for arbitrary G and A that if G proves A in n or fewer steps, then G implies A.
   2. For each possible application of a rule of inference at step n + 1, leading to a new theorem B, show that G implies B.

Notice that Basis Step II can be omitted for natural deduction systems because they have no axioms. When used, Step II involves showing that each of the axioms is a (semantic) logical truth.

The Basis steps demonstrate that the simplest provable sentences from G are also implied by G, for any G. (The proof is simple, since the semantic fact that a set implies any of its members, is also trivial.) The Inductive step will systematically cover all the further sentences that might be provable—by considering each case where we might reach a logical conclusion using an inference rule—and shows that if a new sentence is provable, it is also logically implied. (For example, we might have a rule telling us that from "A" we can derive "A or B". In III.a We assume that if A is provable it is implied. We also know that if A is provable then "A or B" is provable. We have to show that then "A or B" too is implied. We do so by appeal to the semantic definition and the assumption we just made. A is provable from G, we assume. So it is also implied by G. So any semantic valuation making all of G true makes A true. But any valuation making A true makes "A or B" true, by the defined semantics for "or". So any valuation which makes all of G true makes "A or B" true. So "A or B" is implied.) Generally, the Inductive step will consist of a lengthy but simple case-by-case analysis of all the rules of inference, showing that each "preserves" semantic implication.

By the definition of provability, there are no sentences provable other than by being a member of G, an axiom, or following by a rule; so if all of those are semantically implied, the deduction calculus is sound.

Sketch of completeness proof

(This is usually the much harder direction of proof.)

We adopt the same notational conventions as above.

We want to show: If G implies A, then G proves A. We proceed by contraposition: We show instead that if G does not prove A then G does not imply A. If we show that there is a model where A does not hold despite G being true, then obviously G does not imply A. The idea is to build such a model out of our very assumption that G does not prove A.

1. G does not prove A. (Assumption)
2. If G does not prove A, then we can construct an (infinite) maximal set, G^∗, which is a superset of G and which also does not prove A.
   1. Place an ordering (with order type ω) on all the sentences in the language (e.g., shortest first, and equally long ones in extended alphabetical ordering), and number them (E₁, E₂, ...)
   2. Define a series G_n of sets (G₀, G₁, ...) inductively:
      1. $G_{0}=G$
      2. If $G_{k}\cup \{E_{k+1}\}$ proves A, then $G_{k+1}=G_{k}$
      3. If $G_{k}\cup \{E_{k+1}\}$ does not prove A, then $G_{k+1}=G_{k}\cup \{E_{k+1}\}$
   3. Define G^∗ as the union of all the G_n. (That is, G^∗ is the set of all the sentences that are in any G_n.)
   4. It can be easily shown that
      1. G^∗ contains (is a superset of) G (by (b.i));
      2. G^∗ does not prove A (because the proof would contain only finitely many sentences and when the last of them is introduced in some G_n, that G_n would prove A contrary to the definition of G_n); and
      3. G^∗ is a maximal set with respect to A: If any more sentences whatever were added to G^∗, it would prove A. (Because if it were possible to add any more sentences, they should have been added when they were encountered during the construction of the G_n, again by definition)
3. If G^∗ is a maximal set with respect to A, then it is truth-like. This means that it contains C if and only if it does not contain ¬C; If it contains C and contains "If C then B" then it also contains B; and so forth. In order to show this, one has to show the axiomatic system is strong enough for the following:
   • For any formulas C and D, if it proves both C and ¬C, then it proves D. From this it follows, that a maximal set with respect to A cannot prove both C and ¬C, as otherwise it would prove A.
   • For any formulas C and D, if it proves both C→D and ¬C→D, then it proves D. This is used, together with the deduction theorem, to show that for any formula, either it or its negation is in G^∗: Let B be a formula not in G^∗; then G^∗ with the addition of B proves A. Thus from the deduction theorem it follows that G^∗ proves B→A. But suppose ¬B were also not in G^∗, then by the same logic G^∗ also proves ¬B→A; but then G^∗ proves A, which we have already shown to be false.
   • For any formulas C and D, if it proves C and D, then it proves C→D.
   • For any formulas C and D, if it proves C and ¬D, then it proves ¬(C→D).
   • For any formulas C and D, if it proves ¬C, then it proves C→D.
   If additional logical operation (such as conjunction and/or disjunction) are part of the vocabulary as well, then there are additional requirement on the axiomatic system (e.g. that if it proves C and D, it would also prove their conjunction).
4. If G^∗ is truth-like there is a G^∗-Canonical valuation of the language: one that makes every sentence in G^∗ true and everything outside G^∗ false while still obeying the laws of semantic composition in the language. The requirement that it is truth-like is needed to guarantee that the laws of semantic composition in the language will be satisfied by this truth assignment.
5. A G^∗-canonical valuation will make our original set G all true, and make A false.
6. If there is a valuation on which G are true and A is false, then G does not (semantically) imply A.

Thus every system that has modus ponens as an inference rule, and proves the following theorems (including substitutions thereof) is complete:

• $p\to (\neg p\to q)$
• $(p\to q)\to ((\neg p\to q)\to q)$
• $p\to (q\to (p\to q))$
• $p\to (\neg q\to \neg (p\to q))$
• $\neg p\to (p\to q)$
• $p\to p$
• $p\to (q\to p)$
• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$

The first five are used for the satisfaction of the five conditions in stage III above, and the last three for proving the deduction theorem.

Example

As an example, it can be shown that as any other tautology, the three axioms of the classical propositional calculus system described earlier can be proven in any system that satisfies the above, namely that has modus ponens as an inference rule, and proves the above eight theorems (including substitutions thereof). Out of the eight theorems, the last two are two of the three axioms; the third axiom, $(\neg q\to \neg p)\to (p\to q)$, can be proven as well, as we now show.

For the proof we may use the hypothetical syllogism theorem (in the form relevant for this axiomatic system), since it only relies on the two axioms that are already in the above set of eight theorems. The proof then is as follows:

1. $q\to (p\to q)$       (instance of the 7th theorem)
2. $(q\to (p\to q))\to ((\neg q\to \neg p)\to (q\to (p\to q)))$       (instance of the 7th theorem)
3. $(\neg q\to \neg p)\to (q\to (p\to q))$       (from (1) and (2) by modus ponens)
4. $(\neg p\to (p\to q))\to ((\neg q\to \neg p)\to (\neg q\to (p\to q)))$       (instance of the hypothetical syllogism theorem)
5. $(\neg p\to (p\to q))$       (instance of the 5th theorem)
6. $(\neg q\to \neg p)\to (\neg q\to (p\to q))$       (from (5) and (4) by modus ponens)
7. $(q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))$       (instance of the 2nd theorem)
8. $((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))\to ((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))$       (instance of the 7th theorem)
9. $(\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))$       (from (7) and (8) by modus ponens)
10. $((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))\to$

    $(((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))))$       (instance of the 8th theorem)

11. $((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))$       (from (9) and (10) by modus ponens)
12. $(\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))$       (from (3) and (11) by modus ponens)
13. $((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))\to (((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q)))$       (instance of the 8th theorem)
14. $((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q))$       (from (12) and (13) by modus ponens)
15. $(\neg q\to \neg p)\to (p\to q)$       (from (6) and (14) by modus ponens)

Verifying completeness for the classical propositional calculus system

We now verify that the classical propositional calculus system described earlier can indeed prove the required eight theorems mentioned above. We use several lemmas proven here:

(DN1) $\neg \neg p\to p$ - Double negation (one direction)

(DN2) $p\to \neg \neg p$ - Double negation (another direction)

(HS1) $(q\to r)\to ((p\to q)\to (p\to r))$ - one form of Hypothetical syllogism

(HS2) $(p\to q)\to ((q\to r)\to (p\to r))$ - another form of Hypothetical syllogism

(TR1) $(p\to q)\to (\neg q\to \neg p)$ - Transposition

(TR2) $(\neg p\to q)\to (\neg q\to p)$ - another form of transposition.

(L1) $p\to ((p\to q)\to q)$

(L3) $(\neg p\to p)\to p$

We also use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.

• $p\to (\neg p\to q)$ - proof:
  1. $p\to (\neg q\to p)$       (instance of (A1))
  2. $(\neg q\to p)\to (\neg p\to \neg \neg q)$       (instance of (TR1))
  3. $p\to (\neg p\to \neg \neg q)$       (from (1) and (2) using the hypothetical syllogism metatheorem)
  4. $\neg \neg q\to q$       (instance of (DN1))
  5. $(\neg \neg q\to q)\to ((\neg p\to \neg \neg q)\to (\neg p\to q))$       (instance of (HS1))
  6. $(\neg p\to \neg \neg q)\to (\neg p\to q)$       (from (4) and (5) using modus ponens)
  7. $p\to (\neg p\to q)$       (from (3) and (6) using the hypothetical syllogism metatheorem)
• $(p\to q)\to ((\neg p\to q)\to q)$ - proof:
  1. $(p\to q)\to ((\neg q\to p)\to (\neg q\to q))$       (instance of (HS1))
  2. $(\neg q\to q)\to q$       (instance of (L3))
  3. $((\neg q\to q)\to q)\to (((\neg q\to p)\to (\neg q\to q))\to ((\neg q\to p)\to q))$       (instance of (HS1))
  4. $((\neg q\to p)\to (\neg q\to q))\to ((\neg q\to p)\to q)$       (from (2) and (3) by modus ponens)
  5. $(p\to q)\to ((\neg q\to p)\to q)$       (from (1) and (4) using the hypothetical syllogism metatheorem)
  6. $(\neg p\to q)\to (\neg q\to p)$       (instance of (TR2))
  7. $((\neg p\to q)\to (\neg q\to p))\to (((\neg q\to p)\to q)\to ((\neg p\to q)\to q))$       (instance of (HS2))
  8. $((\neg q\to p)\to q)\to ((\neg p\to q)\to q)$       (from (6) and (7) using modus ponens)
  9. $(p\to q)\to ((\neg p\to q)\to q)$       (from (5) and (8) using the hypothetical syllogism metatheorem)
• $p\to (q\to (p\to q))$ - proof:
  1. $q\to (p\to q)$       (instance of (A1))
  2. $(q\to (p\to q))\to (p\to (q\to (p\to q)))$       (instance of (A1))
  3. $p\to (q\to (p\to q))$       (from (1) and (2) using modus ponens)
• $p\to (\neg q\to \neg (p\to q))$ - proof:
  1. $p\to ((p\to q)\to q)$       (instance of (L1))
  2. $((p\to q)\to q)\to (\neg q\to \neg (p\to q))$       (instance of (TR1))
  3. $p\to (\neg q\to \neg (p\to q))$       (from (1) and (2) using the hypothetical syllogism metatheorem)
• $\neg p\to (p\to q)$ - proof:
  1. $\neg p\to (\neg q\to \neg p)$       (instance of (A1))
  2. $(\neg q\to \neg p)\to (p\to q)$       (instance of (A3))
  3. $\neg p\to (p\to q)$       (from (1) and (2) using the hypothetical syllogism metatheorem)
• $p\to p$ - proof given in the proof example above
• $p\to (q\to p)$ - axiom (A1)
• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$ - axiom (A2)

Another outline for a completeness proof

If a formula is a tautology, then there is a truth table for it which shows that each valuation yields the value true for the formula. Consider such a valuation. By mathematical induction on the length of the subformulas, show that the truth or falsity of the subformula follows from the truth or falsity (as appropriate for the valuation) of each propositional variable in the subformula. Then combine the lines of the truth table together two at a time by using "(P is true implies S) implies ((P is false implies S) implies S)". Keep repeating this until all dependencies on propositional variables have been eliminated. The result is that we have proved the given tautology. Since every tautology is provable, the logic is complete.

Different axiomatic proof system

It is possible to define another version of propositional calculus, which defines most of the syntax of the logical operators by means of axioms, and which uses only one inference rule.

Axioms

Let φ, χ, and ψ stand for well-formed formulas. (The well-formed formulas themselves would not contain any Greek letters, but only capital Roman letters, connective operators, and parentheses.) Then the axioms are as follows:

Axioms

Name	Axiom Schema	Description
THEN-1	$\phi \to (\chi \to \phi )$	Add hypothesis χ, implication introduction
THEN-2	$(\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))$	Distribute hypothesis $\phi$ over implication
AND-1	$\phi \land \chi \to \phi$	Eliminate conjunction
AND-2	$\phi \land \chi \to \chi$
AND-3	$\phi \to (\chi \to (\phi \land \chi ))$	Introduce conjunction
OR-1	$\phi \to \phi \lor \chi$	Introduce disjunction
OR-2	$\chi \to \phi \lor \chi$
OR-3	$(\phi \to \psi )\to ((\chi \to \psi )\to (\phi \lor \chi \to \psi ))$	Eliminate disjunction
NOT-1	$(\phi \to \chi )\to ((\phi \to \neg \chi )\to \neg \phi )$	Introduce negation
NOT-2	$\phi \to (\neg \phi \to \chi )$	Eliminate negation
NOT-3	$\phi \lor \neg \phi$	Excluded middle, classical logic
IFF-1	$(\phi \leftrightarrow \chi )\to (\phi \to \chi )$	Eliminate equivalence
IFF-2	$(\phi \leftrightarrow \chi )\to (\chi \to \phi )$
IFF-3	$(\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))$	Introduce equivalence

• Axiom THEN-2 may be considered to be a "distributive property of implication with respect to implication."
• Axioms AND-1 and AND-2 correspond to "conjunction elimination". The relation between AND-1 and AND-2 reflects the commutativity of the conjunction operator.
• Axiom AND-3 corresponds to "conjunction introduction."
• Axioms OR-1 and OR-2 correspond to "disjunction introduction." The relation between OR-1 and OR-2 reflects the commutativity of the disjunction operator.
• Axiom NOT-1 corresponds to "reductio ad absurdum."
• Axiom NOT-2 says that "anything can be deduced from a contradiction."
• Axiom NOT-3 is called "tertium non-datur" (Latin: "a third is not given") and reflects the semantic valuation of propositional formulas: a formula can have a truth-value of either true or false. There is no third truth-value, at least not in classical logic. Intuitionistic logicians do not accept the axiom NOT-3.

Inference rule

The inference rule is modus ponens:

${\frac {\phi ,\ \phi \to \chi }{\chi }}$.

Example of a proof in the different axiomatic system

The following is an example of a (syntactical) demonstration, involving only axioms THEN-1 and THEN-2:

Prove: $A\to A$ (Reflexivity of implication).

Proof:

1. $(A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))$

   Axiom THEN-2 with $\phi =A,\chi =B\to A,\psi =A$

2. $A\to ((B\to A)\to A)$

   Axiom THEN-1 with $\phi =A,\chi =B\to A$

3. $(A\to (B\to A))\to (A\to A)$

   From (1) and (2) by modus ponens.

4. $A\to (B\to A)$

   Axiom THEN-1 with $\phi =A,\chi =B$

5. $A\to A$

   From (3) and (4) by modus ponens.

Metalogic

Let a demonstration be represented by a sequence, with hypotheses to the left of the turnstile and the conclusion to the right of the turnstile. Then the deduction theorem can be stated as follows:

If the sequence

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi$

has been demonstrated, then it is also possible to demonstrate the sequence

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \to \psi$.

This deduction theorem (DT) is not itself formulated with propositional calculus: it is not a theorem of propositional calculus, but a theorem about propositional calculus. In this sense, it is a meta-theorem, comparable to theorems about the soundness or completeness of propositional calculus.

On the other hand, DT is so useful for simplifying the syntactical proof process that it can be considered and used as another inference rule, accompanying modus ponens. In this sense, DT corresponds to the natural conditional proof inference rule which is part of the first version of propositional calculus introduced in this article.

The converse of DT is also valid:

If the sequence

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \to \psi$

has been demonstrated, then it is also possible to demonstrate the sequence

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi$

in fact, the validity of the converse of DT is almost trivial compared to that of DT:

If

$\phi _{1},\ ...,\ \phi _{n}\vdash \chi \to \psi$

then

1: $\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi \to \psi$

2: $\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi$

and from (1) and (2) can be deduced

3: $\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \psi$

by means of modus ponens, Q.E.D.

The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. For example, by axiom AND-1 we have,

$\vdash \phi \wedge \chi \to \phi ,$

which can be transformed by means of the converse of the deduction theorem into

$\phi \wedge \chi \vdash \phi ,$

which tells us that the inference rule

${\frac {\phi \wedge \chi }{\phi }}$

is admissible. This inference rule is conjunction elimination, one of the inference rules used in natural deduction.

Conservative extensions

It is common to include in an axiomatic system for logic only axioms for implication and negation. Given these axioms, it is possible to form conservative extensions of the deduction theorem that permit the use of additional connectives. These extensions are called conservative because if a formula φ involving new connectives is rewritten as a logically equivalent formula θ involving only negation, implication, and universal quantification, then φ is derivable in the extended system if and only if θ is derivable in the original system. When fully extended, an axiomatic system will resemble more closely a system of natural deduction.

Existential quantification

• Introduction

$\forall x(\phi \to \exists y(\phi [x:=y]))$

• Elimination

$\forall x(\phi \to \psi )\to \exists x(\phi )\to \psi$ where $x$ is not a free variable of $\psi$.

Conjunction and disjunction

• Conjunction introduction and elimination

introduction: $\alpha \to (\beta \to \alpha \land \beta )$

elimination left: $\alpha \wedge \beta \to \alpha$

elimination right: $\alpha \wedge \beta \to \beta$

• Disjunction introduction and elimination

introduction left: $\alpha \to \alpha \vee \beta$

introduction right: $\beta \to \alpha \vee \beta$

elimination: $(\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )$

Metatheorems

Because axiomatic logical systems have very few deduction rules, it is common to prove metatheorems that show that additional deduction rules add no deductive power, in the sense that a deduction using the new deduction rules can be converted into a deduction using only the original deduction rules.

Some common metatheorems of this form are:

• The deduction theorem: $\Gamma ;\phi \vdash \psi$ if and only if $\Gamma \vdash \phi \to \psi$.
• $\Gamma \vdash \phi \leftrightarrow \psi$ if and only if $\Gamma \vdash \phi \to \psi$ and $\Gamma \vdash \psi \to \phi$.
• Contraposition: If $\Gamma ;\phi \vdash \psi$ then $\Gamma ;\lnot \psi \vdash \lnot \phi$.
• Generalization: If $\Gamma \vdash \phi$ and x does not occur free in any formula of $\Gamma$ then $\Gamma \vdash \forall x\phi$.

Some useful theorems and their proofs

Following are several theorems in propositional logic, along with their proofs (or links to these proofs in other articles). Note that since (P1) itself can be proved using the other axioms, in fact (P2), (P3) and (P4) suffice for proving all these theorems.

(HS1) $(q\to r)\to ((p\to q)\to (p\to r))$ - Hypothetical syllogism, see proof.

(L1) $p\to ((p\to q)\to q)$ - proof:

(1) $((p\to q)\to (p\to q))\to (((p\to q)\to p)\to ((p\to q)\to q))$       (instance of (P3))

(2) $(p\to q)\to (p\to q)$       (instance of (P1))

(3) $((p\to q)\to p)\to ((p\to q)\to q)$       (from (2) and (1) by modus ponens)

(4) $(((p\to q)\to p)\to ((p\to q)\to q))\to ((p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q)))$       (instance of (HS1))

(5) $(p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q))$       (from (3) and (4) by modus ponens)

(6) $p\to ((p\to q)\to p)$       (instance of (P2))

(7) $p\to ((p\to q)\to q)$       (from (6) and (5) by modus ponens)

The following two theorems are known together as Double negation:

(DN1)$\neg \neg p\to p$

(DN2) $p\to \neg \neg p$

See proofs.

(L2) $(p\to (q\to r))\to (q\to (p\to r))$ - for this proof we use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps:

(1) $(p\to (q\to r))\to ((p\to q)\to (p\to r))$       (instance of (P3))

(2) $((p\to q)\to (p\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))$       (instance of (HS1))

(3) $(p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))$       (from (1) and (2) using the hypothetical syllogism metatheorem)

(4) $((p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r))))\to (((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r))))$       (instance of (P3))

(5) $((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r)))$       (from (3) and (4) using modus ponens)

(6) $q\to (p\to q)$       (instance of (P2))

(7) $(q\to (p\to q))\to ((p\to (q\to r))\to (q\to (p\to q)))$       (instance of (P2))

(8) $(p\to (q\to r))\to (q\to (p\to q))$       (from (6) and (7) using modus ponens)

(9) $(p\to (q\to r))\to (q\to (p\to r))$       (from (8) and (5) using modus ponens)

(HS2) $(p\to q)\to ((q\to r)\to (p\to r))$ - an alternative form of the hypothetical syllogism. proof:

(1) $(q\to r)\to ((p\to q)\to (p\to r))$       (instance of (HS1))

(2) $((q\to r)\to ((p\to q)\to (p\to r)))\to ((p\to q)\to ((q\to r)\to (p\to r)))$       (instance of (L2))

(3) $(p\to q)\to ((q\to r)\to (p\to r))$ (from (1) and (2) by modus ponens)

(TR1) $(p\to q)\to (\neg q\to \neg p)$ - Transposition, see proof (the other direction of transposition is (P4)).

(TR2) $(\neg p\to q)\to (\neg q\to p)$ - another form of transposition; proof:

(1) $(\neg p\to q)\to (\neg q\to \neg \neg p)$       (instance of (TR1))

(2) $\neg \neg p\to p$       (instance of (DN1))

(3) $(\neg \neg p\to p)\to ((\neg q\to \neg \neg p)\to (\neg q\to p))$       (instance of (HS1))

(4) $(\neg q\to \neg \neg p)\to (\neg q\to p)$       (from (2) and (3) by modus ponens)

(5) $(\neg p\to q)\to (\neg q\to p)$       (from (1) and (4) using the hypothetical syllogism metatheorem)

(L3) $(\neg p\to p)\to p$ - proof:

(1) $\neg p\to (\neg \neg (q\to q)\to \neg p)$       (instance of (P2))

(2) $(\neg \neg (q\to q)\to \neg p)\to (p\to \neg (q\to q))$       (instance of (P4))

(3) $\neg p\to (p\to \neg (q\to q))$       (from (1) and (2) using the hypothetical syllogism metatheorem)

(4) $(\neg p\to (p\to \neg (q\to q)))\to ((\neg p\to p)\to (\neg p\to \neg (q\to q)))$       (instance of (P3))

(5) $(\neg p\to p)\to (\neg p\to \neg (q\to q))$       (from (3) and (4) using modes ponens)

(6) $(\neg p\to \neg (q\to q))\to ((q\to q)\to p)$       (instance of (P4))

(7) $(\neg p\to p)\to ((q\to q)\to p)$       (from (5) and (6) using the hypothetical syllogism metatheorem)

(8) $q\to q$       (instance of (P1))

(9) $(q\to q)\to (((q\to q)\to p)\to p)$       (instance of (L1))

(10) $((q\to q)\to p)\to p$       (from (8) and (9) using modes ponens)

(11) $(\neg p\to p)\to p$       (from (7) and (10) using the hypothetical syllogism metatheorem)

See also

• List of axiomatic systems in logic
• Natural deduction
• Curry–Howard correspondence
• Combinatory logic

References

• Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I. Vol. 1. Amsterdam: North Holland.
• Monk, J. Donald (1976). Mathematical Logic. Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. ISBN 978-0-387-90170-1.
• Ruzsa, Imre; Máté, András (1997). Bevezetés a modern logikába (in Hungarian). Budapest: Osiris Kiadó.
• Tarski, Alfred (1990). Bizonyítás és igazság (in Hungarian). Budapest: Gondolat. It is a Hungarian translation of Alfred Tarski's selected papers on semantic theory of truth.
• David Hilbert (1927) "The foundations of mathematics", translated by Stephan Bauer-Menglerberg and Dagfinn Føllesdal (pp. 464–479). in:
  • van Heijenoort, Jean (1967). From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (3rd printing 1976 ed.). Cambridge MA: Harvard University Press. ISBN 0-674-32449-8.
  • Hilbert's 1927, Based on an earlier 1925 "foundations" lecture (pp. 367–392), presents his 17 axioms -- axioms of implication #1-4, axioms about & and V #5-10, axioms of negation #11-12, his logical ε-axiom #13, axioms of equality #14-15, and axioms of number #16-17 -- along with the other necessary elements of his Formalist "proof theory" -- e.g. induction axioms, recursion axioms, etc; he also offers up a spirited defense against L.E.J. Brouwer's Intuitionism. Also see Hermann Weyl's (1927) comments and rebuttal (pp. 480–484), Paul Bernay's (1927) appendix to Hilbert's lecture (pp. 485–489) and Luitzen Egbertus Jan Brouwer's (1927) response (pp. 490–495)
• Kleene, Stephen Cole (1952). Introduction to Metamathematics (10th impression with 1971 corrections ed.). Amsterdam NY: North Holland Publishing Company. ISBN 0-7204-2103-9.
  • See in particular Chapter IV Formal System (pp. 69–85) wherein Kleene presents subchapters §16 Formal symbols, §17 Formation rules, §18 Free and bound variables (including substitution), §19 Transformation rules (e.g. modus ponens) -- and from these he presents 21 "postulates" -- 18 axioms and 3 "immediate-consequence" relations divided as follows: Postulates for the propostional calculus #1-8, Additional postulates for the predicate calculus #9-12, and Additional postulates for number theory #13-21.

External links

• Gaifman, Haim. "A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness" (PDF).
• Farmer, W. M. "Propositional logic" (PDF). It describes (among others) a part of the Hilbert-style deduction system (restricted to propositional calculus).