This article contains a list of sample Hilbert-style deductive systems for propositional logic.
Contents
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 syntactically complete, otherwise said that no new axiom not already consequence of the existing axioms can be added without making the logic inconsistent. 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
We assume this rule is included in all systems below unless stated otherwise.
Frege's axiom system:
Hilbert's axiom system:
Łukasiewicz's axiom systems:
Łukasiewicz and Tarski's axiom system:
Meredith's axiom system:
Mendelson's axiom system:
Russell's axiom system:
Sobociński's axiom systems:
Implication and falsum
Instead of negation, classical logic can also be formulated using the functionally complete set
Tarski–Bernays–Wajsberg axiom system:
Church's axiom system:
Meredith's axiom systems:
Negation and disjunction
Instead of implication, classical logic can also be formulated using the functionally complete set
Russell–Bernays axiom system:
Meredith's axiom systems:
Dually, classical propositional logic can be defined using only conjunction and negation.
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:
Nicod's axiom system:
Łukasiewicz's axiom systems:
Wajsberg's axiom system:
Argonne axiom systems:
Computer analysis by Argonne has revealed > 60 additional single axiom systems that can be used to formulate NAND propositional calculus.
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:
Łukasiewicz and Tarski's axiom systems:
Łukasiewicz's axiom system:
Intuitionistic and intermediate logics
Intuitionistic logic is a subsystem of classical logic. It is commonly formulated with
Alternatively, intuitionistic logic may be axiomatized using
Intermediate logics are in between intuitionistic logic and classical logic. Here are a few intermediate logics:
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:
Meredith's axiom systems:
Hilbert's axiom systems:
Positive propositional calculus
Positive propositional calculus is the fragment of intuitionistic logic using only the (non functionally complete) connectives
Optionally, we may also include the connective
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
or the pair of axioms
Intuitionistic logic in language with negation can be axiomatized over the positive calculus by the pair of axioms
or the pair of axioms
Classical logic in the language
or the pair of axioms
Fitch calculus takes any of the axiom systems for positive propositional calculus and adds the axioms
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
Iséki's axiom system:
Iséki–Arai axiom system:
Arai's axiom systems;
Łukasiewicz's axiom systems:
Meredith's axiom systems:
Kalman's axiom system:
Winker's axiom systems:
XCB axiom system: