nLab natural numbers in SEAR

Natural numbers in SEAR

Natural numbers in SEAR


This page is a spin-off of the structural set theory described at SEAR. The aim is to define (individual) natural numbers in (a fragment of) SEAR without assuming the axiom of infinity. As a result, there should be a set with nn elements for all nn, but we will not have a set of all natural numbers unless we assume the axiom of infinity.

The aim is to use as few axioms/results as possible, in particular, not the result that the category of SEAR sets is a topos. What we define in the first instance is along the lines of natural numbers a la von Neumann.

Zero and one

Barring opinions whether zero should be a natural number, in SEAR we have sets \empty and 1\mathbf{1} with zero and one element respectively. These follow from axioms 0, 1 and 2 at SEAR.

Two and above

To define 2\mathbf{2} we consider P1P\mathbf{1}. In a classical setting, this would be a two-element set, but not so for intuitionistic SEAR. We know that 1\mathbf{1} has at least two subsets, namely \empty and 1\mathbf{1}, so we let 2\mathbf{2} be the subset of P1P\mathbf{1} consisting of the corresponding elements. Continuing to higher numbers, we know that n\mathbf{n} has nn elements, so nn one-element subsets. Together with another 'obvious' subset, this gives a set with n+1n+1 elements.

More formally, let ϕ 2:1P1\phi_2:\mathbf{1} \looparrowright P\mathbf{1} be the relation such that ϕ 2(*,empty)\phi_2(*,empty) and ϕ 2(*,1)\phi_2(*,\mathbf{1}). Then a tabulation |ϕ 2||\phi_2| has two elements. Let us fix one of these and call it 2\mathbf{2}.

Now assume we have defined a set n\mathbf{n} with nn elements, 1,,n1,\ldots,n, where n2n \geq 2. From axiom 3 we have a power set PnP\mathbf{n}. Let ϕ n+1:1Pn\phi_{n+1}:\mathbf{1} \looparrowright P\mathbf{n} be a relation such that ϕ n+1(*,u)\phi_{n+1}(*,u) whenever the subset {i|ϵ(i,u)}\{ i | \epsilon(i,u)\} of n\mathbf{n} has either exactly one element or is equal to all of n\mathbf{n}.

Mike Shulman: I think it’s fine, though AN might object. A more formal thing to say would be that ϕ n+1(*,u)\phi_{n+1}(*,u) whenever the subset {i|ϵ(i,u)}\{ i | \epsilon(i,u)\} of n\mathbf{n} has either exactly one element or is equal to all of n\mathbf{n}.

However, I don’t think your definition works when n=1n=1, since in that case, 1̲=1\underline{1} = \mathbf{1}! Perhaps instead of ϕ(*,n)\phi(*,\mathbf{n}) you want ϕ(*,)\phi(*,\emptyset)?

David Roberts: I’ve fixed the problem with 2\mathbf{2}, using Toby’s original suggestion, incorporated the more formal suggestion you made for ϕ n+1\phi_{n+1} and added a new definition below.

Then a tabulation of ϕ n+1\phi_{n+1} will have n+1n+1 elements and we fix one of these as n+1\mathbf{n+1}.

The construction on 1,2,\mathbf{1},\mathbf{2},\ldots only requires a fragment of SEAR, namely axioms 0,1,2 and 3, and even holds in the analogous fragment of bounded SEAR.

Alternative definition

To avoid having to treat 2\mathbf{2} as a special case, we can use another definition, again starting from 0,1\mathbf{0},\mathbf{1} as before.

Assume we have defined n\mathbf{n} for n1n \geq 1. Then let ψ n+1:1Pn\psi_{n+1}:\mathbf{1} \looparrowright P\mathbf{n} be the relation such that ψ n+1(*,u)\psi_{n+1}(*,u) whenever the subset {i|ϵ(i,u)}\{ i | \epsilon(i,u)\} of n\mathbf{n} has either exactly one element or no elements. A tabulation |ψ n+1||\psi_{n+1}| has n+1n+1 elements, and fixing one of these we denote it by n+1\mathbf{n+1}.

This definition holds in the same fragment of (bounded) SEAR as described above.

David Roberts: Does this remark (about collection/power sets) belong here or in the next section? Certainly, I haven’t gotten rid of power sets and I hope I haven’t included collection.

Mike Shulman: I think it belongs in the next section.

Toby: Sorry, I put my remarks in the wrong place! It was late …

Replacing the power set axiom by something else

As suggested by Toby, one could take as an axiom the existence of 2\mathbf{2}, together with axioms 0,1,2 and 5 (collection) of SEAR, instead of powersets (axiom 3). From Collection and 2\mathbf{2}, we get binary coproducts, so we could define n\mathbf{n} as 1(1(1))\mathbf{1}\coprod(\mathbf{1} \coprod ( \ldots\coprod \mathbf{1})\ldots) (nn times). (DR: this needs spelling out better, with tabulations, but that’s the general idea).

This definition also holds in the bounded fragment of SEAR.

With the axiom of infinity

based on this blog post and its predecessors

To construe elements nn \in \mathbb{N} as giving actual finite sets, we construct a “family” ϕ:F\phi\colon F \to \mathbb{N} where each fiber F nF_n is a set of cardinality nn. For example, consider the function

ϕ:×:(m,n)m+n+1 \phi\colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}\colon (m,n) \mapsto m + n + 1

Then, for each n0n \geq 0, the fiber ϕ 1(n)\phi^{-1}(n) is a set of cardinality nn.

If you use the Axiom of Collection, then it will do this for you automatically; you don't need to come up with an ad hoc representation of the family.


Mike Shulman: If you don’t want to use powersets, then I’m pretty sure you’ll need an axiom of coproducts. Unless I’m mistaken, the collection of subsingleton sets satisfies Axioms 0, 1, and 2.

David Roberts: Actually what I probably mean is not use the result that SetSet is a topos. I think you are correct on the subsingleton front, because it looks like we have no way of obtaining sets with more than one element without more axioms.

Toby: If you want to be cute, you can make the existence of 2\mathbf{2} an axiom and then get arbitrary binary coproducts using Collection. On the other hand, if you're happy using power sets, then don't bother proving that P1=2P\mathbf{1} = \mathbf{2} (which won't generalise to the intuitionistic case anyway); instead use Separation to carve out {xP1|x=x=1}\{ x \in P\mathbf{1} \;|\; x = \empty \;\vee\; x = \mathbf{1} \}. Then 3\mathbf{3} is a subset of P2P\mathbf{2}, etc; or make 3\mathbf{3} and 4\mathbf{4} both subsets of P2P\mathbf{2}, with the general rule going logarithmically.

Last revised on February 27, 2017 at 21:42:23. See the history of this page for a list of all contributions to it.