Theorem 146 Error: Circular Reasoning in Defining Addition

I am indebted to Dr. Christoph Lamm for pointing out this error.

The rigorous definition of addition given in Section 2.10 (using primitive recursion) is based ultimately on Theorem 146 (Basic Principle of Recursive Definition). The proof of Theorem 146 assumes that the ordering relation \(<\) on \(\mathbf{N}\) has already been defined. But ordering on \(\mathbf{N}\) was defined earlier in Chapter 2 (Definition 61) using addition itself, resulting in circular reasoning.

Correction to the proof of Theorem 146

The proof of Theorem 146 needs to be corrected as follows so that the ordering relation \(<\) on \(\mathbf{N}\) is not used, and the set \(I_n\) is defined directly (without using the ordering relation) as described below.

Definition. Define a subset \(I\) of \(\mathbf{N}\) to be an initial set if for all \(k \in \mathbf{N}\), \(S(k) \in I\) implies \(k \in I\).

By routine induction arguments we get:

(For example, the second part of the first assertion is established by proving (by induction) that for all \(n\), if \(n \in I\) for any initial set \(I\), then \(1 \in I\).)

Now define \(I_n\) to be the unique initial set (as given by the last result above) containing \(n\) but not \(S(n)\). It follows that \(I_1 = \{1\}\), and \(I_{S(n)} = I_n \cup \{S(n)\}\) for all \(n\).

(Note that the ordering relation “\(m < n\)” can now be defined as “\(S(m) \in I_n\)”, but we avoid \(<\) altogether in the corrected proof of Theorem 146.)

With this definition of \(I_n\), the proof of Theorem 146 can correctly proceed exactly as before, but with the following changes throughout the proof:

For example, in the corrected proof we define a function \(u\) to be partially \(h\)-recursive with domain \(I_n\) if \( u \colon I_n \to Y\), \(u(1) = a\), and \(u(S(k)) = h(u(k))\) for every \(k\) such that \(S(k) \in I_n\).

A complete replacement proof for Theorem 146 can found in this PDF file.

Go back to the errata list for Set Theory.


Last updated: 2014 November 11, 17:30:00 EST