Are there axioms in a natural deduction system?

Question

In the Hilbert system, a proof may include some axioms. In a natural deduction system, it seems no axiom is involved, at least from the examples I read in logic books. So, I wonder how axioms such as those for ZFC play a role in a natural deduction system. Thanks.

Answer 1

Hilbert system and natural deduction can be seen as two "dual" approaches to writing formal proofs. Roughly, when it comes to deriving formulas that are valid in a specific logical system (classical logic, intuitionistic logic, and so on), the Hilbert system has many logical axioms and minimizes the number of inference rules (in the propositional case, the only inference rule is modus ponens), while natural deduction only uses inference rules and has no axioms.

In natural deduction, a logical derivation can be represented as a tree-like structure whose leaves $A_1, \dots, A_n$ (except the discharged ones, but let us abstract from that for the moment) are the assumptions or hypotheses, and whose root $B$ is the conclusion or thesis. It means that "from $A_1, \dots, A_n$ one can derive $B$", often noted $A_1, \dots, A_n \vdash B$. If you look at your derivation top-down, you start from the hypotheses $A_1, \dots, A_n$ and you conclude $B$ by only repeatedly using the inference rules of natural deduction (which are syntactical manipulations of the logic symbols$-$connectives and quantifiers$-$occurring in a formula), without using any axioms. The special case $n = 0$ means that $B$ is a logically valid formula (also known as a tautology in propositional classical logic), which is derived without any assumptions (as well as without any axioms): indeed, in the derivation proving $B$, the leaves are not "active" anymore, since all of them are been discharged by inference rules such as $\to_\text{intro}$ occurring in the derivation. By the way, note that proving $A_1, \dots, A_n \vdash B$ is equivalent to prove $\vdash (A_1 \land \dots \land A_n) \to B$.

What happens when you want to use a formal system to write proofs in a specific mathematical theory (for instance, set theory as axiomatized in ZFC) and not in a purely logical framework? The point is that to formalize a mathematical theory, you have to manipulate non-logical symbols (such as $\in$ in ZFC), and you need to "teach" your formal system$-$which is purely syntactical$-$how to manipulate them. The most natural and common way to do that in a formal system such as Hilbert calculus or natural deduction is to add non-logical axioms that are specific to that mathematical theory (for instance, the axioms of ZFC). By "non-logical" I mean that the axioms of the mathematical theory are not logically valid formulas (otherwise there would be no need to add them) and they talk about basic properties that hold only in that mathematical theory.

In natural deduction, adding axioms means that you add $0$-ary inference rules, that is, inference rules with no premises and whose conclusion is one of the non-logical axioms. This way, a natural deduction derivation within a mathematical theory $\mathcal{T}$ (such as ZFC), where $\mathcal{T}$ is the set of axioms formally defining the mathematical theory, is a tree-like structure whose leaves $A_1, \dots, A_n, A_{n+1}, \dots, A_m$ are either assumptions $A_1, \dots, A_n$ or axioms $A_{n+1}, \dots, A_m \in \mathcal{T}$, and whose root $B$ is the conclusion. It means that "from $A_1, \dots, A_n$ one can derive $B$, through the axioms $A_{n+1}, \dots, A_m \in \mathcal{T}$", often noted $A_1, \dots, A_n \vdash_\mathcal{T} B$. Of course, the case $m = n$ means that your derivation never used any axioms in $\mathcal{T}$, and so $B$ is a logical consequence of the assumptions $A_1, \dots, A_n$, independently of the theory $\mathcal{T}$. There is an important technical difference between the assumptions $A_1, \dots A_n$ and the axioms $A_{n+1}, \dots, A_m$: the former can be discharged by logical inference rules such as $\to_\text{intro}$, the latter cannot.

There is an alternative view to deal with formal proofs of a mathematical theory $\mathcal{T}$ in natural deduction. You do not distinguish between axioms in $\mathcal{T}$ and assumptions, all the leaves of the derivation are considered as assumptions (which can be discharged by logical inference rules such as $\to_\text{intro}$). Technically, the tree-like structure of a natural deduction derivation is the same as in the previous viewpoint, what changes is the way you look at it. In particular, with this viewpoint, you lose the distinction between the hypotheses that are used to logically derive the thesis, and the non-logical axioms of the mathematical theory. Thanks to this lack of distinction, it still holds that proving $A_1, \dots, A_n, A_{n+1}, \dots, A_m \vdash B$ is equivalent to prove $\vdash (A_1 \land \dots \land A_n \land A_{n+1} \land \dots \land A_m) \to B$.

---

In my opinion, using natural deduction or other formal proof systems to prove theorems in a mathematical theory such as ZFC can be of interest in only two cases:

• as a theoretical inquiry as a matter of principle;

• to understand how proof assistants (such as Coq, HOL/Isabelle, Agda, and Lean) work to get verified proofs.

For practical purposes, using natural deduction or any other formal systems to prove theorems in any mathematical theory such as ZFC is a tedious operation that yields very long and almost incomprehensible proofs (even when the theorem to prove is a basic property) where is hard to grasp the mathematical ideas behind a stream of a myriad of syntactical manipulations. As an example, consider the (almost unintelligible!) natural deduction derivation below that proves the basic fact

$$\forall \forall a \forall b \forall c \, \big( \in a \cap (b \cup c) \to x \in (a \cap b) \cup (a \cap c) \big)$$

in ZFC, starting from the following "axioms" (see also a comment at the end of this section):

• $\text{ax}_1$: $\ \forall x \forall y \forall z \, (x \in y \cap z \to (x \in y \land x \in z) )$,

• $\text{ax}_2$: $\ \forall x \forall y \forall z \, ((x \in y \land x \in z) \to x \in y \cap z )$,

• $\text{ax}_3$: $\ \forall x \forall y \forall z \, (x \in y \cup z \to (x \in y \lor x \in z) )$.

So, a natural deduction derivation proving $\vdash_{\text{ax}_1, \text{ax}_2, \text{ax}_3} \forall \forall a \forall b \forall c \, \big( \in a \cap (b \cup c) \to x \in (a \cap b) \cup (a \cap c) \big)$ is the following

$$\small \dfrac { {\displaystyle [x \in a \cap (b \cup c)]^\circ \atop {\displaystyle{{\vdots \pi} \atop x \in b \lor x \in c}}} \quad \displaystyle{{ [x \in a \cap (b \cup c)]^\circ, [x \in b]^*} \atop \displaystyle{\vdots \pi_1 \atop x \in (a \cap b) \cup (a \cap c)}} \quad \displaystyle{{ [x \in a \cap (b \cup c)]^\circ, [x \in c]^*} \atop \displaystyle{\vdots \pi_2 \atop x \in (a \cap b) \cup (a \cap c)}} } {\dfrac {x \in (a \cap b) \cup (a \cap c)} {\dfrac{x \in a \cap (b \cup c) \to x \in (a \cap b) \cup (a \cap c) }{\forall x \forall a \forall b \forall c \big(x \in a \cap (b \cup c) \to x \in (a \cap b) \cup (a \cap c) \big)}\forall_i \times 4} \!\to_i^\circ } \!\lor_e^* $$

where the derivation $\pi$ proving $ \ x \in a \cap (b \cup c) \vdash_{\text{ax}_1, \, \text{ax}_3} x \in b \lor x \in c$ is the following $$\small \dfrac { \dfrac {\dfrac{}{\text{ax}_3}} {x \in b \cup c \to (x \!\in\! b \lor x \!\in\! c)} \!{\scriptstyle \forall_e \times 3} \quad \dfrac { \dfrac {\dfrac{}{\text{ax}_1}} {x \in a \cap (b \cup c) \to (x \!\in\! a \land x \in b \cup c)} {\scriptstyle\forall_e \times 3} \quad { \atop \displaystyle{x \in a \cap (b \cup c)}} } {\dfrac{x \in a \land x \in b \cup c}{x \in b \cup c}\land_{e_2}} \!\!\to_e } {x \in b \lor x \in c} \!\!\to_e $$

and the derivation $\pi_1$ proving $ \ x \in a \cap (b \cup c), \, x \in b \vdash_{\text{ax}_1, \, \text{ax}_2} x \in (a \cap b) \cup (a \cap c)$ is the following (with $B = (x \!\in\!a \land x \!\in\! b) \to \in a \cap b$) $$ \dfrac { \dfrac {\dfrac{}{\text{ax}_2}} {B} {\scriptstyle\forall_e \times 3} \quad \dfrac { \dfrac { \dfrac {\dfrac{}{\text{ax}_1}} {x \in a \cap (b \cup c) \to (x \!\in\! a \land x \in b \cup c)} {\scriptstyle\forall_e \times 3} \quad { \atop \displaystyle{x \in a \cap (b \cup c)}} } {\dfrac {x \in a \land x \in b \cup c} {x \in a} \land_{e_1} } \!\to_e { \atop {\atop \displaystyle{\atop \displaystyle{x \in b}}}} } {x \in a \land x \in b} \land_i } {\dfrac{x \in a \cap b}{x \in (a \cap b) \cup (a \cap c)}\lor_{i_1}} \!\to_e $$

and the derivation $\pi_2$ proving $ \ x \in a \cap (b \cup c),\, x \in c \vdash_{\text{ax}_1, \, \text{ax}_2} x \in (a \cap b) \cup (a \cap c)$ is the following (with $C = (x \!\in\!a \land x \!\in\! c) \to \in a \cap c$) $$ \dfrac { \dfrac {\dfrac{}{\text{ax}_2}} {C} {\scriptstyle\forall_e \times 3} \quad \dfrac { \dfrac { \dfrac {\dfrac{}{\text{ax}_1}} {x \in a \cap (b \cup c) \to (x \!\in\! a \land x \in b \cup c)} {\scriptstyle\forall_e \times 3} \quad { \atop \displaystyle{x \in a \cap (b \cup c)}} } {\dfrac {x \in a \land x \in b \cup c} {x \in a} \land_{e_1} } \!\to_e { \atop {\atop \displaystyle{\atop \displaystyle{x \in c}}}} } {x \in a \land x \in c} \land_i } {\dfrac{x \in a \cap c}{x \in (a \cap b) \cup (a \cap c)}\lor_{i_2}} \!\to_e $$

Note that in the usual presentation of ZFC (see for instance here), the formulas I called $\text{ax}_1$, $\text{ax}_2$ and $\text{ax}_3$ are not axioms but immediate consequences of more basic axioms. Therefore, the derivations above are actually bigger (and impossible to represent in one page), because they hide the derivations of $\text{ax}_1$, $\text{ax}_2$ and $\text{ax}_3$ from the real axioms of ZFC.

---

For further and more sophisticated details about axioms in formal proof systems (with a slightly different point of view), see here and here.