nLab Nelson arithmetic



Model theory




An extension of the first-order theory of Peano arithmetic as described in Edward Nelson’s paper, by introducing a set of “counting numbers” that we can’t use induction on.


Nelson arithmetic (NANA) is expressed in the language with a constant 00, unary predicate 𝒞\mathcal{C}, unary function symbol ss and binary functions ++,\cdot; it extends Peano arithmetic, which consists of the following axioms:

  1. x¬s(x)=0\forall_x \neg s(x) = 0;

  2. x,y(s(x)=s(y))(x=y)\forall_{x, y} (s(x) = s(y)) \Rightarrow (x = y);

  3. xx+0=x\forall_x x + 0 = x,

  4. x,yx+s(y)=s(x+y)\forall_{x, y} x + s(y) = s(x+y);

  5. xx0=0\forall_x x \cdot 0 = 0;

  6. x,yxs(y)=xy+x\forall_{x, y} x \cdot s(y) = x \cdot y + x;

  7. For any predicate φ\varphi in first-order logic in the language 00, ss, ++, \cdot (but not containing 𝒞\mathcal{C}), the axiom φ(0)( xφ(x)φ(Sx)) xφ(x)\varphi(0) \wedge (\forall_x \varphi(x) \Rightarrow \varphi(Sx)) \Rightarrow \forall_x \varphi(x);

with the two additional axioms regarding 𝒞\mathcal{C}:

  1. 𝒞(0)\mathcal{C}(0);

  2. x𝒞(x)𝒞(s(x))\forall_{x} \mathcal{C}(x) \Rightarrow \mathcal{C}(s(x));

We may choose to omit the axiom schema (7), in which case we refer to Nelson arithmetic without induction (NAIndNA-Ind). Without induction, it is not possible to prove that addition or multiplication are commutative or associative. Optionally, we could add the axiom xx=0 yx=s(y)\forall_x x = 0 \vee \exists_y x = s(y) from Robinson arithmetic so that the resulting theory extends Robinson arithmetic, however we don’t in this page.

Counting numbers

The predicate 𝒞\mathcal{C} is supposed to refer to “counting numbers”, in the familiar intuitive sense that the natural numbers are supposed to be for counting. Nelson states in his paper that

It follows (…) that 00, S0S0, SS0SS0, and so forth, are counting numbers. But we cannot prove that all numbers are counting numbers.

And indeed, there are many non-standard models of Nelson arithmetic where not every number in the model is a “counting number”/“natural number”. Unfortunately, nonstandard models of Peano arithmetic, which Nelson arithmetic extends, are hard to describe, and cannot have computable arithmetic operations.

Nonstandard models of NAIndNA-Ind are more common though. If one has any ordered ring R (meaning RR is partially ordered with ++ monotone, 010 \leq 1, and the elements 0\geq 0 are closed under multiplication), then the subset R 0={rRr0}R_{\geq 0} = \{r \in R \mid r \geq 0\} is a model of NAIndNA-Ind, where we may take the predicate C(a)C(a) to be a{0,1,1+1,1+1+1,}a \in \{0, 1, 1+1, 1+1+1, \cdots\} (the image of \mathbb{N} under the unique ring homomorphism R\mathbb{Z} \to R). For example, the non-negative rational numbers 0\mathbb{Q}_{\geq 0} and nonnegative real numbers 0\mathbb{R}_{\geq 0} both produce models in this way.

On the other extreme, one could define a model where 𝒞(a)\mathcal{C}(a) is true for all numbers aa in the model, and thus all number trivially are “counting numbers”, though in that case the “counting numbers” interpretation of the predicate doesn’t make much intuitive sense anymore.

Additionable, multiplicable, and exponentiable numbers

We define the unary predicate 𝒜\mathcal{A}, meaning “additionable number”, as 𝒜(x)\mathcal{A}(x) if for all counting numbers yy, y+xy + x is also a counting number. Similarly, we define the unary predicate \mathcal{M}, meaning “multiplicable number”, as (x)\mathcal{M}(x) if for all additionable numbers yy, yxy \cdot x is also an additionable number. Without induction, we don’t know that addition of “additionable numbers” or multiplication of “multiplicable numbers” is associative.

Let ()()(-)\uparrow(-) denote the exponentiation function; if we aren’t using induction, instead suppose that there is a binary function ()():N×NN(-)\uparrow(-):N \times N \to N called “exponentiation” such that

  • for all xNx \in N, x0=s(0)x \uparrow 0 = s(0)

  • for all x,yNx, y \in N, xs(y)=xxyx \uparrow s(y) = x \cdot x \uparrow y

Nelson states that

If we attempt to define “exponentiable number” in the same spirit, we are unable to prove that if x 1x_1 and x 2x_2 are exponentiable numbers then so is x 1x 2x_1 \uparrow x_2. There is a radical difference between addition and multiplication on the one hand and exponentiation, superexponentiation, and so forth, on the other hand. The obstacle is that exponentiation is not associative; for example, (22)3=43=64(2 \uparrow 2) \uparrow 3 = 4 \uparrow 3 = 64 whereas 2(23)=28=2562 \uparrow (2 \uparrow 3) = 2 \uparrow 8 = 256. For any specific numeral SSS… 0 we can indeed prove that it is an exponentiable number, but we cannot prove that the world of exponentiable numbers is closed under exponentiation.


The categorification of Nelson’s argument would proceed as follows: Suppose we have the subcategory CountSetFinSetCountSet \hookrightarrow FinSet of the category of finite sets whose cardinality is a counting number. (Here “finite” refers to the internal notion, not the external notion. Although our language only contains numbers, not sets, we can encode this category in PAPA using a skeleton of FinSetFinSet where objects are (internal) natural numbers and a morphism mnm \to n is encoded as a natural number less than n mn^m.)

Then we can form a further subcategory AddSetCountSetAddSet \hookrightarrow CountSet, consisting of the objects AA such that the coproduct A+CA + C exists in ContSetContSet for all CC in ContSetContSet. Although CountSetCountSet may not have had binary coproducts, AddSetAddSet has binary coproducts.

Next, we can form a further subcategory MultSetCountSetMultSet \hookrightarrow CountSet, consisting of the objects MM such that the product M×AM \times A exists in AddSetAddSet for all AA in AddSetAddSet. Although AddSetAddSet may not have had binary products, MultSetMultSet has binary products.

Now, we can form a further subcategory ExpSetMultSetExpSet \hookrightarrow MultSet, consisting of the objects EE such that the exponent M EM^E exists in MultSetMultSet for all MM in MultSetMultSet i.e. the exponentiable objects of MultSetMultSet. However, in constrast to the previous cases, we cannot prove that ExpSetExpSet has exponents (hence can’t prove that it’s cartesian closed, an elementary topos, a Π-pretopos, etc.).


The theory NANA, or a categorification thereof, provides an option to study mathematics using ultrafinitism, by viewing the counting numbers to be the correct notion of natural numbers and the other numbers to be an idealised abstraction. (If one wants to work without these “idealised abstractions”, induction would have to be substituted for weaker acceptable axioms.)

Categorifying the current axioms to the category of sets, the counting sets (represented by the sets SS in which 𝒞(S)\mathcal{C}(S) is inhabited) could not be proven to be symmetric monoidal with respect to either the disjoint union or the Cartesian product. Thus, Nelson’s CountSet? forms a framework of mathematics, which is sometimes called “ultrafinite mathematics”, that is significantly weaker than strongly predicative constructive finite mathematics. However, the subcategories of additionable finite sets AddSetAddSet and multiplicable finite sets MultSetMultSet can be proven to be symmetric monoidal.

Models of Nelson arithmetic

A model of Nelson arithmetic is a model of Peano arithmetic (N,0,S,+,)(N,0,S,+,\cdot), equipped with a subset CNC \subset N such that 0C0 \in C and aCa \in C implies S(a)CS(a) \in C.

A model of Nelson arithmetic without induction is a set NN with an element 0N0 \in N, a function s:NNs:N \to N, binary operations ()+():N×NN(-)+(-):N \times N \to N and ()():N×NN(-)\cdot(-):N \times N \to N, and a predicate 𝒞:NProp\mathcal{C}:N \to \mathrm{Prop}, such that the axioms 1-6, 8, 9 above are all satisfied. Explicitly, this means:

  • for all xNx \in N, ¬s(x)=0\neg s(x) = 0

  • for all x,yNx, y \in N, s(x)=s(y)s(x) = s(y) implies x=yx = y

  • for all xNx \in N, x+0=xx + 0 = x

  • for all x,yNx, y \in N, x+s(y)=s(x+y)x + s(y) = s(x+y)

  • for all xNx \in N, x0=0x \cdot 0 = 0

  • for all x,yNx, y \in N, xs(y)=xy+xx \cdot s(y) = x \cdot y + x

  • 𝒞(0)\mathcal{C}(0)

  • for all xNx \in N, 𝒞(x)\mathcal{C}(x) implies 𝒞(s(x))\mathcal{C}(s(x));

A homomorphism of models of Nelson arithmetic without induction NN and N N^{'} is a function f:NN f:N \to N^{'} such that

  • f(0 N)=0 N f(0_N) = 0_{N^{'}}

  • for all xNx \in N, 𝒞 N(x)\mathcal{C}_N(x) implies 𝒞 N (f(x))\mathcal{C}_{N^{'}}(f(x))

  • for all xNx \in N, f(s N(x))=s N (f(x))f(s_N(x)) = s_{N^{'}}(f(x))

  • for all x,yNx, y \in N, f(x+ Ny)=f(x)+ N f(y)f(x +_N y) = f(x) +_{N^{'}} f(y)

  • for all x,yNx, y \in N, f(x Ny)=f(x) N f(y)f(x \cdot_N y) = f(x) \cdot_{N^{'}} f(y)

Homomorphisms of models of Nelson arithmetic with induction are defined in the same way, but as with PAPA, the notion of elementary embeddings may be more useful.

The category of models of Nelson arithmetic without induction in a universe 𝒰\mathcal{U} is the category NelsonArithmetics 𝒰\mathrm{NelsonArithmetics}_\mathcal{U} whose objects Ob(NelsonArithmetics 𝒰)Ob(\mathrm{NelsonArithmetics}_\mathcal{U}) are the 𝒰\mathcal{U}-small models of Nelson arithmetic, and for any two objects AOb(NelsonArithmetics 𝒰)A \in Ob(\mathrm{NelsonArithmetics}_\mathcal{U}) and BOb(NelsonArithmetics 𝒰)B \in Ob(\mathrm{NelsonArithmetics}_\mathcal{U}) the morphisms Mor NelsonArithmetics 𝒰(A,B)Mor_{\mathrm{NelsonArithmetics}_\mathcal{U}}(A, B) are the homomorphisms of models of Nelson arithmetic as defined above.

This category is an accessible category. If 𝒰\mathcal{U} satisfies the axiom of finiteness (meaning it thinks every set is finite), then (because there are no finite models of NAIndNA-Ind) the category NelsonArithmetics 𝒰\mathrm{NelsonArithmetics}_\mathcal{U} is empty.

Example models

  • The set of natural numbers \mathbb{N} is the standard model of Nelson arithmetic, and is the initial model of Nelson arithmetic in the category of models of Nelson arithmetic.

  • If RR is any rig such that +1:RR{0}+1 : R \to R\setminus\{0\} is (total and) injective, then RR is a model of Nelson arithmetic without induction, where we may take S(r)=r+1S(r) = r + 1 and 𝒞\mathcal{C} to be any of: RR, the image of the function i:Ri : \mathbb{N} \to R defined by i(0)=0i(0) = 0, i(n+1)=i(n)+1i(n+1) = i(n)+1, or any other subset CC with 0C0 \in C and aCa+1Ca \in C \Rightarrow a + 1 \in C. Examples include:

  • The set of non-negative rational numbers 0\mathbb{Q}_{\geq 0} with s(q)q+1s(q) \coloneqq q + 1 and 𝒞(q)\mathcal{C}(q) for all q 0q \in \mathbb{Q}_{\geq 0} is a model of Nelson arithmetic without induction.

  • The set of non-negative real numbers 0\mathbb{R}_{\geq 0} with s(r)r+1s(r) \coloneqq r + 1 and 𝒞(r)\mathcal{C}(r) for all r 0r \in \mathbb{R}_{\geq 0} is a model of Nelson arithmetic without induction.

  • The subset P[x]P \subset \mathbb{Z}[x] of polynomials with leading coefficient nonnegative

  • Any free commutative \mathbb{N} -algebra on a generating set SS with s(r)r+1s(r) \coloneqq r + 1 and 𝒞(r)\mathcal{C}(r) for all r[S]r \in \mathbb{N}[S], is a model of Nelson arithmetic without induction.

  • The disjoint union set +𝟙\mathbb{N} + \mathbb{1} where *:𝟙*:\mathbb{1} is the unique element of the singleton cextends the model \mathbb{N} with:

  1. s(*)=*s(*) = *

  2. a.*+a=*=a+*\forall a \in \mathbb{N}. * + a = * = a + * and *+*=** + * = *

  3. a.*a=a\forall a \in \mathbb{N}. * \cdot a = a

  4. a\forall a \in \mathbb{N} + \mathbb{1}.a*=*. a \cdot * = *

  5. 𝒞(*)\mathcal{C}(*)

Is a model of Nelson arithmetic without induction. Note that multiplication is not commutative and that 0*=*0 \cdot * = *, so this is not an instance of the previous examples.

  • Given any nonstandard model NN of Peano arithmetic, and any subset CNC \subset N with 0C0 \in C and aCa+1Ca \in C \Rightarrow a+1 \in C, NN and CC together give a model of Nelson arithemtic.

Groupoidal categorification

The groupoidal categorification of Nelson arithmetic without induction is a groupoid 𝒢\mathcal{G} with

  • an object 0𝒢0 \in \mathcal{G},

  • a functor S:𝒢𝒢S:\mathcal{G} \to \mathcal{G},

  • a functor ()+():𝒢×𝒢𝒢(-)+(-):\mathcal{G} \times \mathcal{G} \to \mathcal{G}

  • a functor ()():𝒢×𝒢𝒢(-)\cdot(-):\mathcal{G} \times \mathcal{G} \to \mathcal{G}

  • for all A𝒢A \in \mathcal{G}, a function set (S(A)0)(S(A) \cong 0) \to \emptyset from the set of isomorphisms S(A)0S(A) \cong 0 to the empty set

  • for all A,B𝒢A, B \in \mathcal{G}, a function set (S(A)S(B))(AB)(S(A) \cong S(B)) \to (A \cong B) from the set of isomorphism S(A)S(B)S(A) \cong S(B) to the set of isomorphisms ABA \cong B

  • for all A𝒢A \in \mathcal{G}, a set of isomorphisms A+0AA + 0 \cong A

  • for all A,B𝒢A, B \in \mathcal{G}, a set of isomorphisms A+S(B)S(A+B)A + S(B) \cong S(A+B)

  • for all A𝒢A \in \mathcal{G}, a set of isomorphisms A0AA \cdot 0 \cong A

  • for all A,B𝒢A, B \in \mathcal{G}, a set of isomorphisms AS(B)AB+AA \cdot S(B) \cong A \cdot B + A

  • a Set-valued functor 𝒞:𝒢Set\mathcal{C}:\mathcal{G} \to \mathrm{Set}

  • an element p𝒞(0)p \in \mathcal{C}(0)

  • for all A𝒢A \in \mathcal{G}, a function f A:𝒞(A)𝒞(S(A))f_A:\mathcal{C}(A) \to \mathcal{C}(S(A))

See also


  • Edward Nelson, Warning Signs of a Possible Collapse of Contemporary Mathematics (pdf)

Last revised on May 17, 2022 at 15:12:37. See the history of this page for a list of all contributions to it.