This article contains a list of sample Hilbert-style deductive systems for propositional logics.
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.
Every logic system requires at least one non-nullary rule of inference.
These formulations use the following rule of inference; Russell–Bernays axiom system: Meredith's axiom systems:[8] Dually, classical propositional logic can be defined using only conjunction and negation.
Rosser J. Barkley created a system based on conjunction and negation
": If we don't use the abbreviation, we get the axiom schemes in the following form: Also, modus ponens becomes: 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:[5] Łukasiewicz's axiom systems:[5] Wajsberg's axiom system:[5] Argonne axiom systems:[5] Computer analysis by Argonne has revealed over 60 additional single axiom systems that can be used to formulate NAND propositional calculus.
The implicational calculi below use modus ponens as an inference rule.
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: Alternatively, intuitionistic logic may be axiomatized using
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