First-order logic and inference rules

A classical natural-deduction presentation permits the following rules. Assumptions may be used while they remain open, and a discharged assumption is removed from the hypotheses of the resulting conclusion.

• From $P,Q$, infer $P\land Q$; from a conjunction, infer either component.
• From $P$, infer $P\lor Q$, and similarly from $Q$. From $P\lor Q$ and deductions of $R$ from each alternative, infer $R$.
• A deduction of $Q$ under an additional assumption $P$ gives $P\Rightarrow Q$ after discharging $P$. From $P$ and $P\Rightarrow Q$, infer $Q$ (modus ponens).
• A deduction of contradiction under $P$ gives $\neg P$. From $P,\neg P$, infer contradiction; from contradiction infer any formula. Classical logic also permits eliminating double negation.
• From $\forall x\,P(x)$, infer $P(t)$ for an admissible term $t$. To infer $\forall x\,P(x)$, prove the instance for an arbitrary object not occurring freely in undischarged assumptions.
• From $P(t)$, infer $\exists x\,P(x)$. To use an existential statement, introduce a fresh witness, deduce a conclusion independent of that witness, and discharge the witness assumption.
• Equality is reflexive, and equal terms may be substituted for one another in formulas.

These are foundational rules, not theorems requiring a prior mathematical structure. Particular theories add nonlogical axioms, such as those governing sets.

The statement $\forall x\,\exists y\,P(x,y)$ allows the chosen $y$ to depend on $x$. The statement $\exists y\,\forall x\,P(x,y)$ requires one choice valid for every $x$. They need not be equivalent.

• Jonathan Pila, Set Theory, Sections 2–9 and 15.
• John Stalker, Natural deduction for first-order logic.