List of Hilbert systems

This article contains a list of sample Hilbert-style deductive systems for propositional logics.

Classical propositional calculus systems

Classical propositional calculus is the standard propositional logic. Its intended semantics is bivalent and its main property is that it is strongly complete, otherwise said that whenever a formula semantically follows from a set of premises, it also follows from that set syntactically. Many different equivalent complete axiom systems have been formulated. They differ in the choice of basic connectives used, which in all cases have to be functionally complete (i.e. able to express by composition all n-ary truth tables), and in the exact complete choice of axioms over the chosen basis of connectives.

Implication and negation

The formulations here use implication and negation ${\displaystyle \{\to ,\neg \}}$ as functionally complete set of basic connectives. Every logic system requires at least one non-nullary rule of inference. Classical propositional calculus typically uses the rule of modus ponens:

${\displaystyle {\frac {A,A\to B}{B}}.}$

We assume this rule is included in all systems below unless stated otherwise.

Frege's axiom system: ^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle (A\to B)\to (\neg B\to \neg A)}$

${\displaystyle \neg \neg A\to A}$

${\displaystyle A\to \neg \neg A}$

Hilbert's axiom system: ^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

${\displaystyle A\to (\neg A\to B)}$

${\displaystyle (A\to B)\to ((\neg A\to B)\to B)}$

Łukasiewicz's axiom systems: ^[1]

• First:

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle (\neg A\to A)\to A}$

  ${\displaystyle A\to (\neg A\to B)}$

• Second:

  ${\displaystyle ((A\to B)\to C)\to (\neg A\to C)}$

  ${\displaystyle ((A\to B)\to C)\to (B\to C)}$

  ${\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}$

• Third:

  ${\displaystyle A\to (B\to A)}$

  ${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (\neg A\to \neg B)\to (B\to A)}$

• Fourth:^{[ citation needed ]}

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle A\to (\neg A\to B)}$

  ${\displaystyle (\neg A\to B)\to ((B\to A)\to A)}$

Łukasiewicz and Tarski's axiom system: ^[2]

${\displaystyle [(A\to (B\to A))\to ([(\neg C\to (D\to \neg E))\to [(C\to (D\to F))\to ((E\to D)\to (E\to F))]]\to G)]\to (H\to G)}$

Meredith's axiom system:

${\displaystyle ((((A\to B)\to (\neg C\to \neg D))\to C)\to E)\to ((E\to A)\to (D\to A))}$

Mendelson's axiom system: ^[3]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (\neg A\to \neg B)\to ((\neg A\to B)\to A)}$

Russell's axiom system: ^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle \neg \neg A\to A}$

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

Sobociński's axiom systems: ^[1]

• First:

  ${\displaystyle \neg A\to (A\to B)}$

  ${\displaystyle A\to (B\to (C\to A))}$

  ${\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}$

• Second:

  ${\displaystyle (A\to B)\to (\neg B\to (A\to C))}$

  ${\displaystyle A\to (B\to (C\to A))}$

  ${\displaystyle (\neg A\to B)\to ((A\to B)\to B)}$

Implication and falsum

Instead of negation, classical logic can also be formulated using the functionally complete set ${\displaystyle \{\to ,\bot \}}$ of connectives.

Tarski–Bernays–Wajsberg axiom system:

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle A\to (B\to A)}$

${\displaystyle ((A\to B)\to A)\to A}$

${\displaystyle \bot \to A}$

Church's axiom system:

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle ((A\to \bot )\to \bot )\to A}$

Meredith's axiom systems:

• First: ^{[4] [5] [6]}

  ${\displaystyle ((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))}$

• Second: ^[4]

  ${\displaystyle ((A\to B)\to ((\bot \to C)\to D))\to ((D\to A)\to (E\to (F\to A)))}$

Negation and disjunction

Instead of implication, classical logic can also be formulated using the functionally complete set ${\displaystyle \{\neg ,\lor \}}$ of connectives. These formulations use the following rule of inference;

${\displaystyle {\frac {A,\neg A\lor B}{B}}.}$

Russell–Bernays axiom system:

${\displaystyle \neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))}$

${\displaystyle \neg (A\lor B)\lor (B\lor A)}$

${\displaystyle \neg A\lor (B\lor A)}$

${\displaystyle \neg (A\lor A)\lor A}$

Meredith's axiom systems: ^[7]

• First:

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg D\lor A)\lor (C\lor (E\lor A)))}$

• Second:

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg E\lor D)\lor (C\lor (A\lor D)))}$

• Third:

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg C\lor A)\lor (E\lor (D\lor A)))}$

Dually, classical propositional logic can be defined using only conjunction and negation.

Conjunction and negation

Rosser J. Barkley created a system based on conjunction and negation ${\displaystyle \{\wedge ,\neg \}}$, with the modus ponens as inference rule. In his book, ^[8] he used the implication to present his axiom schemes. "${\displaystyle C\rightarrow D}$" is an abbreviation for "${\displaystyle \neg (C\wedge \neg D)}$":

• ${\displaystyle A\rightarrow A\wedge A}$
• ${\displaystyle A\wedge B\rightarrow A}$
• ${\displaystyle \left(A\rightarrow B\right)\rightarrow \left(\neg \left(B\wedge C\right)\rightarrow \neg \left(C\wedge A\right)\right)}$

If we don't use the abbreviation, we get the axiom schemes in the following form:

• ${\displaystyle \neg (A\wedge \neg (A\wedge A))}$
• ${\displaystyle \neg ((A\wedge B)\wedge \neg A)}$
• ${\displaystyle \neg \left(\neg \left(A\wedge \neg B\right)\wedge \neg \neg \left(\neg \left(B\wedge C\right)\wedge \neg \neg \left(C\wedge A\right)\right)\right)}$

Also, modus ponens becomes:

• ${\displaystyle {\frac {A,\neg \left(A\wedge \neg B\right)}{B}}}$

Sheffer's stroke

Because Sheffer's stroke (also known as NAND operator) is functionally complete, it can be used to create an entire formulation of propositional calculus. NAND formulations use a rule of inference called Nicod's modus ponens:

${\displaystyle {\frac {A,A\mid (B\mid C)}{C}}.}$

Nicod's axiom system: ^[4]

${\displaystyle (A\mid (B\mid C))\mid [(E\mid (E\mid E))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

Łukasiewicz's axiom systems: ^[4]

• First:

  ${\displaystyle (A\mid (B\mid C))\mid [(D\mid (D\mid D))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

• Second:

  ${\displaystyle (A\mid (B\mid C))\mid [(A\mid (C\mid A))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

Wajsberg's axiom system: ^[4]

${\displaystyle (A\mid (B\mid C))\mid [((D\mid C)\mid [(A\mid D)\mid (A\mid D)])\mid (A\mid (A\mid B))]}$

Argonne axiom systems: ^[4]

• First:

${\displaystyle (A\mid (B\mid C))\mid [(A\mid (B\mid C))\mid ((D\mid C)\mid [(C\mid D)\mid (A\mid D)])]}$

• Second:

${\displaystyle (A\mid (B\mid C))\mid [([(B\mid D)\mid (A\mid D)]\mid (D\mid B))\mid ((C\mid B)\mid A)]}$ ^[9]

Computer analysis by Argonne has revealed over 60 additional single axiom systems that can be used to formulate NAND propositional calculus. ^[6]

Implicational propositional calculus

The implicational propositional calculus is the fragment of the classical propositional calculus which only admits the implication connective. It is not functionally complete (because it lacks the ability to express falsity and negation) but it is however syntactically complete. The implicational calculi below use modus ponens as an inference rule.

Bernays–Tarski axiom system: ^[10]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle ((A\to B)\to A)\to A}$

Łukasiewicz and Tarski's axiom systems:

• First: ^[10]

  ${\displaystyle [(A\to (B\to A))\to [([((C\to D)\to E)\to F]\to [(D\to F)\to (C\to F)])\to G]]\to G}$

• Second: ^[10]

  ${\displaystyle [(A\to B)\to ((C\to D)\to E)]\to ([F\to ((C\to D)\to E)]\to [(A\to F)\to (D\to E)])}$

• Third:

  ${\displaystyle ((A\to B)\to (C\to D))\to (E\to ((D\to A)\to (C\to A)))}$

• Fourth:

  ${\displaystyle ((A\to B)\to (C\to D))\to ((D\to A)\to (E\to (C\to A)))}$

Łukasiewicz's axiom system: ^{[11] [10]}

${\displaystyle ((A\to B)\to C)\to ((C\to A)\to (D\to A))}$

Intuitionistic and intermediate logics

Intuitionistic logic is a subsystem of classical logic. It is commonly formulated with ${\displaystyle \{\to ,\land ,\lor ,\bot \}}$ as the set of (functionally complete) basic connectives. It is not syntactically complete since it lacks excluded middle A∨¬A or Peirce's law ((A→B)→A)→A which can be added without making the logic inconsistent. It has modus ponens as inference rule, and the following axioms:

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (A\land B)\to A}$

${\displaystyle (A\land B)\to B}$

${\displaystyle A\to (B\to (A\land B))}$

${\displaystyle A\to (A\lor B)}$

${\displaystyle B\to (A\lor B)}$

${\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}$

${\displaystyle \bot \to A}$

Alternatively, intuitionistic logic may be axiomatized using ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$ as the set of basic connectives, replacing the last axiom with

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle \neg A\to (A\to B)}$

Intermediate logics are in between intuitionistic logic and classical logic. Here are a few intermediate logics:

• Jankov logic (KC) is an extension of intuitionistic logic, which can be axiomatized by the intuitionistic axiom system plus the axiom ^[12]

${\displaystyle \neg A\lor \neg \neg A.}$

• Gödel–Dummett logic (LC) can be axiomatized over intuitionistic logic by adding the axiom ^[12]

${\displaystyle (A\to B)\lor (B\to A).}$

Positive implicational calculus

The positive implicational calculus is the implicational fragment of intuitionistic logic. The calculi below use modus ponens as an inference rule.

Łukasiewicz's axiom system:

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

Meredith's axiom systems:

• First:

  ${\displaystyle E\to ((A\to B)\to (((D\to A)\to (B\to C))\to (A\to C)))}$

• Second:

  ${\displaystyle A\to (B\to A)}$

  ${\displaystyle (A\to B)\to ((A\to (B\to C))\to (A\to C))}$

• Third:

  ${\displaystyle ((A\to B)\to C)\to (D\to ((B\to (C\to E))\to (B\to E)))}$ ^[13]

Hilbert's axiom systems:

• First:

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

  ${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

  ${\displaystyle A\to (B\to A)}$

• Second:

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle A\to (B\to A)}$

• Third:

  ${\displaystyle A\to A}$

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

Positive propositional calculus

Positive propositional calculus is the fragment of intuitionistic logic using only the (non functionally complete) connectives ${\displaystyle \{\to ,\land ,\lor \}}$. It can be axiomatized by any of the above-mentioned calculi for positive implicational calculus together with the axioms

${\displaystyle (A\land B)\to A}$

${\displaystyle (A\land B)\to B}$

${\displaystyle A\to (B\to (A\land B))}$

${\displaystyle A\to (A\lor B)}$

${\displaystyle B\to (A\lor B)}$

${\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}$

Optionally, we may also include the connective ${\displaystyle \leftrightarrow }$ and the axioms

${\displaystyle (A\leftrightarrow B)\to (A\to B)}$

${\displaystyle (A\leftrightarrow B)\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to A)\to (A\leftrightarrow B))}$

Johansson's minimal logic can be axiomatized by any of the axiom systems for positive propositional calculus and expanding its language with the nullary connective ${\displaystyle \bot }$, with no additional axiom schemas. Alternatively, it can also be axiomatized in the language ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$ by expanding the positive propositional calculus with the axiom

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

or the pair of axioms

${\displaystyle (A\to B)\to (\neg B\to \neg A)}$

${\displaystyle A\to \neg \neg A}$

Intuitionistic logic in language with negation can be axiomatized over the positive calculus by the pair of axioms

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

${\displaystyle \neg A\to (A\to B)}$

or the pair of axioms ^[14]

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle \neg A\to (A\to B)}$

Classical logic in the language ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$ can be obtained from the positive propositional calculus by adding the axiom

${\displaystyle (\neg A\to \neg B)\to (B\to A)}$

or the pair of axioms

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

${\displaystyle \neg \neg A\to A}$

Fitch calculus takes any of the axiom systems for positive propositional calculus and adds the axioms ^[14]

${\displaystyle \neg A\to (A\to B)}$

${\displaystyle A\leftrightarrow \neg \neg A}$

${\displaystyle \neg (A\lor B)\leftrightarrow (\neg A\land \neg B)}$

${\displaystyle \neg (A\land B)\leftrightarrow (\neg A\lor \neg B)}$

Note that the first and third axioms are also valid in intuitionistic logic.

Equivalential calculus

Equivalential calculus is the subsystem of classical propositional calculus that only allows the (functionally incomplete) equivalence connective, denoted here as ${\displaystyle \equiv }$. The rule of inference used in these systems is as follows:

${\displaystyle {\frac {A,A\equiv B}{B}}.}$

Iséki's axiom system: ^[15]

${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

${\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}$

Iséki–Arai axiom system: ^[16]

${\displaystyle A\equiv A}$

${\displaystyle (A\equiv B)\equiv (B\equiv A)}$

${\displaystyle (A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))}$

Arai's axiom systems;

• First:

  ${\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}$

  ${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

• Second:

  ${\displaystyle (A\equiv B)\equiv (B\equiv A)}$

  ${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

Łukasiewicz's axiom systems: ^[17]

• First:

  ${\displaystyle (A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))}$

• Second:

  ${\displaystyle (A\equiv B)\equiv ((A\equiv C)\equiv (C\equiv B))}$

• Third:

  ${\displaystyle (A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C))}$

Meredith's axiom systems: ^[17]

• First:

  ${\displaystyle ((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))}$

• Second:

  ${\displaystyle A\equiv ((B\equiv (A\equiv C))\equiv (C\equiv B))}$

• Third:

  ${\displaystyle (A\equiv (B\equiv C))\equiv (C\equiv (A\equiv B))}$

• Fourth:

  ${\displaystyle (A\equiv B)\equiv (C\equiv ((B\equiv C)\equiv A))}$

• Fifth:

  ${\displaystyle (A\equiv B)\equiv (C\equiv ((C\equiv B)\equiv A))}$

• Sixth:

  ${\displaystyle ((A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)}$

• Seventh:

  ${\displaystyle ((A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)}$

Kalman's axiom system: ^[17]

${\displaystyle A\equiv ((B\equiv (C\equiv A))\equiv (C\equiv B))}$

Winker's axiom systems: ^[17]

• First:

  ${\displaystyle A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))}$

• Second:

  ${\displaystyle A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))}$

XCB axiom system: ^[17]

${\displaystyle A\equiv (((A\equiv B)\equiv (C\equiv B))\equiv C)}$

See also

• Paraconsistent logic § Included — a list of axiom schemas for a paraconsistent logic of the Hilbert style

References

1. Yasuyuki Imai, Kiyoshi Iséki, On axiom systems of propositional calculi, I, Proceedings of the Japan Academy. Volume 41, Number 6 (1965), 436–439.
2. Part XIII: Shôtarô Tanaka. On axiom systems of propositional calculi, XIII. Proc. Japan Acad., Volume 41, Number 10 (1965), 904–907.
3. Elliott Mendelson, Introduction to Mathematical Logic, Van Nostrand, New York, 1979, p. 31.
4. [Fitelson, 2001] "New Elegant Axiomatizations of Some Sentential Logics" by Branden Fitelson
5. (Computer analysis by Argonne has revealed this to be the shortest single axiom with least variables for propositional calculus).
6. "Some New Results in Logical Calculi Obtained Using Automated Reasoning", Zac Ernst, Ken Harris, & Branden Fitelson, http://www.mcs.anl.gov/research/projects/AR/award-2001/fitelson.pdf
7. C. Meredith, Single axioms for the systems (C, N), (C, 0) and (A, N) of the two-valued propositional calculus, Journal of Computing Systems, pp. 155–164, 1954.
8. Rosser J. Barkley, "Logic for Mathematicians", New York, McGraw-Hill, 1953.
9. , p. 9, A Spectrum of Applications of Automated Reasoning, Larry Wos; arXiv:cs/0205078v1
10. Investigations into the Sentential Calculus in Logic, Semantics, Metamathematics: Papers from 1923 to 1938 by Alfred Tarski, Corcoran, J., ed. Hackett. 1st edition edited and translated by J. H. Woodger, Oxford Uni. Press. (1956)
11. Łukasiewicz, J.. (1948). The Shortest Axiom of the Implicational Calculus of Propositions. Proceedings of the Royal Irish Academy. Section A: Mathematical and Physical Sciences, 52, 25–33. Retrieved from https://www.jstor.org/stable/20488489
12. A. Chagrov, M. Zakharyaschev, Modal logic, Oxford University Press, 1997.
13. C. Meredith, A single axiom of positive logic, Journal of Computing Systems, p. 169–170, 1954.
14. L. H. Hackstaff, Systems of Formal Logic, Springer, 1966.
15. Kiyoshi Iséki, On axiom systems of propositional calculi, XV, Proceedings of the Japan Academy. Volume 42, Number 3 (1966), 217–220.
16. Yoshinari Arai, On axiom systems of propositional calculi, XVII, Proceedings of the Japan Academy. Volume 42, Number 4 (1966), 351–354.
17. XCB, the Last of the Shortest Single Axioms for the Classical Equivalential Calculus, LARRY WOS, DOLPH ULRICH, BRANDEN FITELSON; arXiv:cs/0211015v1