List of Hilbert systems

This article contains a list of sample Hilbert-style deductive systems for propositional logics. 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. The formulations here use implication and negation 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: 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: First: Second: Third: Fourth: Łukasiewicz and Tarski's axiom system: Meredith's axiom system: Mendelson's axiom system: Russell's axiom system: Sobociński's axiom systems: First: Second: Instead of negation, classical logic can also be formulated using the functionally complete set of connectives. Tarski–Bernays–Wajsberg axiom system: Church's axiom system: Meredith's axiom systems: First: Second: Instead of implication, classical logic can also be formulated using the functionally complete set of connectives. These formulations use the following rule of inference; Russell–Bernays axiom system: Meredith's axiom systems: First: Second: Third: Dually, classical propositional logic can be defined using only conjunction and negation. Because Sheffer's stroke (also known as NAND operator) is functionally complete, it can be used to create an entire formulation of propositional calculus.