# 2.3: The Logical Axioms

- Page ID
- 9688

\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)

\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)

Let a first-order language \(\mathcal{L}\) be given. In this section we will gather together a collection \(\Lambda\) of logical axioms for \(\mathcal{L}\). This set of axioms, though infinite, will be decidable. Roughly this means that if we are given a formula \(\phi\) that is alleged to be an element of \(\Lambda\), we will be able to decide whether \(\phi \in \Lambda\) or \(\phi \notin \Lambda\). Furthermore, we could, in principle, design a computer program that would be able to decide membership in \(\Lambda\) in a finite amount of time.

After we have established the set of logical axioms \(\Lambda\) and we want to start doing mathematics, we will want to add additional axioms that are designed to allow us to deduce statements about whatever mathematical system we may have in mind. These will constitute the collection of nonlogical axioms, \(\Sigma\). For example, if we are working in number theory, using the language \(\mathcal{L}_{NT}\), along with the logical axioms \(\Lambda\) we will also want to use other axioms that concern the properties of addition and the ordering relation denoted by the symbol \(<\). These additional axioms are the formulas that we will place in \(\Sigma\). Then, from this expanded set of axioms \(\Lambda \cup \Sigma\) we will attempt to write deductions of formulas that make statements of number-theoretic interest. To reiterate: \(\Lambda\), the set of logical axioms, will be fixed, as will the collection of rules of inference. But the set of nonlogical axioms must be specified for each deduction. In the current section we set out the logical axioms only, dealing with the rules of inference in Section 2.4, and deferring our discussion of the nonlogical axioms until Section 2.8.

### Equality Axioms

We have taken the route of assuming that the equality symbol, \(=\), is a part of the language \(\mathcal{L}\). There are three groups of axioms that are designed for this symbol. The first just says that any object is equal to itself:

\[x = x \: \text{for each variable} \: x. \tag{E1}\]

For the second group of axioms, assume that \(x_1, x_2, \ldots, x_n\) are variables, \(y_1, y_2, \ldots, y_n\) are variables, and \(f\) is an \(n\)-ary function symbol.

\[\left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( f \left( x_1, x_2, \ldots, x_n \right) = f \left( y_1, y_2, \ldots, y_n \right) \right). \tag{E2}\]

The assumptions for the third group of axioms is the same as for the second group, except that \(R\) is assumed to be an \(n\)-ary relation symbol (\(R\) might be the equality symbol, which is seen as a binary relation symbol).

\[\left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( R \left( x_1, x_2, \ldots, x_n \right) \rightarrow R \rightarrow R \left( y_1, y_2, \ldots, y_n \right) \right). \tag{E3}\]

Axioms (E2) and (E3) are axioms that are designed to allow substitution of equals for equals. Nothing fancier than that.

### Quantifier Axioms

The quantifier axioms are designed to allow a very reasonable sort of entry in a deduction. Suppose that we know \(\forall x P \left( x \right)\). Then, if \(t\) is any term of the language, we should be able to state \(P \left( t \right)\). To avoid problems of the sort outlined at the beginning of Section 1.8, we will demand that the term \(t\) be substitutable for the variable \(x\).

\[\left( \forall x \phi \right) \rightarrow \phi_t^x, \: \text{if} \: t \: \text{is substitutable for} \: x \: \text{in} \: \phi. \tag{Q1}\]

\[\phi_t^x \rightarrow \left( \exists x \phi \right), \: \text{if} \: t \: \text{is substitutable for} \: x \: \text{in} \: \phi. \tag{Q2}\]

In many logic texts, axiom (Q1) would be called universal instantiation, while (Q2) would be known as existential generalization. We will avoid this impressive language and stick with the more mundane (Q1) and (Q2).

### Recap

Just to gather all of the logical axioms together in one place, let us state them once again. The set \(\Lambda\) of logical axioms is the collection of all formulas that fall into one of the following categories:

\[x = x \: \text{for each variable} \: x. \tag{E1}\]

\[\left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( f \left( x_1, x_2, \ldots, x_n \right) = f \left( y_1, y_2, \ldots, y_n \right) \right). \tag{E2}\]

\[\left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( R \left( x_1, x_2, \ldots, x_n \right) \rightarrow R \left( y_1, y_2, \ldots, y_n \right) \right). \tag{E3}\]

\[\left( \forall x \phi \right) \rightarrow \phi_t^x, \: \text{if} \: t \: \text{is substitutable for} \: x \: \text{in} \: \phi. \tag{Q1}\]

\[\phi_t^x \rightarrow \left( \exists x \phi \right), \: \text{if} \: t \: \text{is substitutable for} \: x \: \text{in} \: \phi. \tag{Q2}\]

Notice that \(\Lambda\) is decidable. We could write a compute program which, given a formula \(\phi\), can decide in a finite amount of time whether or not \(\phi\) is an element of \(\Lambda\).