Propositional calculus à la Hilbert

Classical propositional logic may be axiomatized as a proof system à la Hilbert with the following inference rules¹

tautology: $𝜙 ⊢ ⊤$
explosion: $⊥ ⊢ 𝜙$
$\lor$ -commutativity: $𝜙 \lor 𝜓 ⊣ ⊢ 𝜓 \lor 𝜙$
$\land$ -commutativity: $𝜙 \land 𝜓 ⊣ ⊢ 𝜓 \land 𝜙$
$\lor$ -associativity: $[𝜙 \lor 𝜓] \lor 𝛿 ⊣ ⊢ 𝜙 \lor [𝜓 \lor 𝜙]$
$\land$ -associativity: $[𝜙 \land 𝜓] \land 𝛿 ⊣ ⊢ 𝜙 \land [𝜓 \land 𝜙]$
De Morgan's laws:
- $\neg [𝜙 \lor 𝜓] ⊣ ⊢ \neg 𝜙 \land \neg 𝜓$
- $\neg 𝜙 \lor \neg 𝜓 ⊣ ⊢ \neg [𝜙 \land 𝜓]$
double negation: $\neg \neg 𝜙 ⊣ ⊢ 𝜙$
LEM: $⊤ ⊢ 𝜙 \lor \neg 𝜙$
non-contradiction: $𝜙 \land \neg 𝜙 ⊢ ⊥$
contraposition: $𝜙 \Rightarrow 𝜓 ⊣ ⊢ \neg 𝜓 \Rightarrow \neg 𝜙$
$\lor$ -absorption
- $𝜙 \lor (𝜙 \land 𝜓) ⊣ ⊢ 𝜙$
- $𝜙 \lor 𝜙 ⊣ ⊢ 𝜙$
- $⊤ ⊢ 𝜙 \lor ⊤$
- $𝜙 \lor ⊥ ⊣ ⊢ 𝜙$
$\land$ -absorption
- $𝜙 \land (𝜙 \lor 𝜓) ⊣ ⊢ 𝜙$
- $𝜙 \land 𝜙 ⊣ ⊢ 𝜙$
- $⊤ ⊢ 𝜙 \land ⊤$
- $𝜙 \land ⊥ ⊢ ⊥$

#state/tidy | #lang/en | #SemBr

Of course there are many choices as to which logical equivalences are considered “primary.” Those listed here are those students are allowed to use in CITS2211. ↩

Footnotes