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 semantically, 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, and in the exact complete choice of axioms over the chosenbasis of connectives.
Implication and negation
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:
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:
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:
Because Sheffer's stroke 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:
is a subsystem of classical logic. It is commonly formulated with as the set of basic connectives. It is not syntactically complete since it lacks excluded middle A∨¬A or Peirce's law →A which can be added without making the logic inconsistent. It has modus ponens as inference rule, and the following axioms: Alternatively, intuitionistic logic may be axiomatized using as the set of basic connectives, replacing the last axiom with Intermediate logics are in between intuitionistic logic and classical logic. Here are a few intermediate logics:
Jankov logic is an extension of intuitionistic logic, which can be axiomatized by the intuitionistic axiom system plus the axiom
Gödel–Dummett logic can be axiomatized over intuitionistic logic by adding the axiom
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:
First:
Second:
Third:
Hilbert's axiom systems:
First:
Second:
Third:
Positive propositional calculus
Positive propositional calculus is the fragment of intuitionistic logic using only the connectives. It can be axiomatized by any of the above-mentioned calculi for positive implicational calculus together with the axioms Optionally, we may also include the connective and the axioms 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, with no additional axiom schemas. Alternatively, it can also be axiomatized in the language by expanding the positive propositional calculus with the axiom 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 can be obtained from the positive propositional calculus by adding the axiom 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 equivalence connective, denoted here as. The rule of inference used in these systems is as follows: Iséki's axiom system: Iséki–Arai axiom system: Arai's axiom systems;
