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 elements for all , 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.
Barring opinions whether zero should be a natural number, in SEAR we have sets and with zero and one element respectively. These follow from axioms 0, 1 and 2 at SEAR.
To define we consider . In a classical setting, this would be a two-element set, but not so for intuitionistic SEAR. We know that has at least two subsets, namely and , so we let be the subset of consisting of the corresponding elements. Continuing to higher numbers, we know that has elements, so one-element subsets. Together with another 'obvious' subset, this gives a set with elements.
More formally, let be the relation such that and . Then a tabulation has two elements. Let us fix one of these and call it .
Now assume we have defined a set with elements, , where . From axiom 3 we have a power set . Let be a relation such that whenever the subset of has either exactly one element or is equal to all of .
Mike Shulman: I think it’s fine, though AN might object. A more formal thing to say would be that whenever the subset of has either exactly one element or is equal to all of .
However, I don’t think your definition works when , since in that case, ! Perhaps instead of you want ?
David Roberts: I’ve fixed the problem with , using Toby’s original suggestion, incorporated the more formal suggestion you made for and added a new definition below.
Then a tabulation of will have elements and we fix one of these as .
The construction on only requires a fragment of SEAR, namely axioms 0,1,2 and 3, and even holds in the analogous fragment of bounded SEAR.
To avoid having to treat as a special case, we can use another definition, again starting from as before.
Assume we have defined for . Then let be the relation such that whenever the subset of has either exactly one element or no elements. A tabulation has elements, and fixing one of these we denote it by .
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 …
As suggested by Toby, one could take as an axiom the existence of , together with axioms 0,1,2 and 5 (collection) of SEAR, instead of powersets (axiom 3). From Collection and , we get binary coproducts, so we could define as ( 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.
based on this blog post and its predecessors
To construe elements as giving actual finite sets, we construct a “family” where each fiber is a set of cardinality . For example, consider the function
Then, for each , the fiber is a set of cardinality .
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.
David Roberts: Actually what I probably mean is not use the result that 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 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 (which won't generalise to the intuitionistic case anyway); instead use Separation to carve out . Then is a subset of , etc; or make and both subsets of , with the general rule going logarithmically.