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:
A , A → B B . {\displaystyle {\frac {A,A\to B}{B}}.}
We assume this rule is included in all systems below unless stated otherwise. Frege's axiom system:
A → ( B → A ) {\displaystyle A\to (B\to A)}
( A → ( B → C ) ) → ( ( A → B ) → ( A → C ) ) {\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
( A → ( B → C ) ) → ( B → ( A → C ) ) {\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
( A → B ) → ( ¬ B → ¬ A ) {\displaystyle (A\to B)\to (\neg B\to \neg A)}
¬ ¬ A → A {\displaystyle \neg \neg A\to A}
A → ¬ ¬ A {\displaystyle A\to \neg \neg A}
Hilbert's axiom system:
A → ( B → A ) {\displaystyle A\to (B\to A)}
( A → ( B → C ) ) → ( B → ( A → C ) ) {\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
( B → C ) → ( ( A → B ) → ( A → C ) ) {\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}
A → ( ¬ A → B ) {\displaystyle A\to (\neg A\to B)}
( A → B ) → ( ( ¬ A → B ) → B ) {\displaystyle (A\to B)\to ((\neg A\to B)\to B)}
Łukasiewicz's axiom systems:
First:
( A → B ) → ( ( B → C ) → ( A → C ) ) {\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
( ¬ A → A ) → A {\displaystyle (\neg A\to A)\to A}
A → ( ¬ A → B ) {\displaystyle A\to (\neg A\to B)}
Second:
( ( A → B ) → C ) → ( ¬ A → C ) {\displaystyle ((A\to B)\to C)\to (\neg A\to C)}
( ( A → B ) → C ) → ( B → C ) {\displaystyle ((A\to B)\to C)\to (B\to C)}
( ¬ A → C ) → ( ( B → C ) → ( ( A → B ) → C ) ) {\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}
Third:
A → ( B → A ) {\displaystyle A\to (B\to A)}
( A → ( B → C ) ) → ( ( A → B ) → ( A → C ) ) {\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
( ¬ A → ¬ B ) → ( B → A ) {\displaystyle (\neg A\to \neg B)\to (B\to A)}
Arai's axiom system:
( A → B ) → ( ( B → C ) → ( A → C ) ) {\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
A → ( ¬ A → B ) {\displaystyle A\to (\neg A\to B)}
… excerpt ends here. Continue reading the full article.
