A Hilbert-style proof system consists of:

1. Axiom schemas: Infinite families of logical axioms, such as:

   • $\phi \to (\psi \to \phi)$
   • $(\phi \to (\psi \to \chi)) \to ((\phi \to \psi) \to (\phi \to \chi))$
   • $(\neg \phi \to \neg \psi) \to (\psi \to \phi)$
   • $\forall x \, \phi \to \phi[x/t]$ (if $t$ is substitutable for $x$)
   • $\forall x \, (\phi \to \psi) \to (\phi \to \forall x \, \psi)$ (if $x$ not free in $\phi$)

2. Inference rule (typically just one):

   • Modus Ponens: From $\phi$ and $\phi \to \psi$, infer $\psi$

A proof of $\psi$ from $\Gamma$ is a sequence of formulas $\phi_1, \ldots, \phi_n = \psi$ where each $\phi_i$ is either an axiom, a member of $\Gamma$, or follows from earlier formulas by modus ponens.

Natural deduction uses inference rules without axioms, designed to mirror natural mathematical reasoning:

Introduction and elimination rules for each connective:

• $\land$-introduction: From $\phi$ and $\psi$, infer $\phi \land \psi$
• $\land$-elimination: From $\phi \land \psi$, infer $\phi$ (or $\psi$)
• $\to$-introduction: If $\psi$ can be derived assuming $\phi$, then derive $\phi \to \psi$
• $\to$-elimination (modus ponens): From $\phi$ and $\phi \to \psi$, infer $\psi$
• $\forall$-introduction: From $\phi$, infer $\forall x \, \phi$ (if $x$ not free in any assumption)
• $\forall$-elimination: From $\forall x \, \phi$, infer $\phi[x/t]$
• $\exists$-introduction: From $\phi[x/t]$, infer $\exists x \, \phi$
• $\exists$-elimination: From $\exists x \, \phi$ and a derivation of $\psi$ from $\phi$ (with fresh $x$), infer $\psi$

Natural deduction proofs are trees rather than sequences, with assumptions discharged by introduction rules.

The sequent calculus (Gentzen's LK) uses sequents of the form $\Gamma \Rightarrow \Delta$, where $\Gamma$ and $\Delta$ are finite sets of formulas. The intuitive meaning is "if all formulas in $\Gamma$ are true, then at least one formula in $\Delta$ is true."

Inference rules manipulate sequents, with separate left rules (introducing formulas on the left) and right rules (introducing formulas on the right) for each connective. For example: