I read the surreal number on nlab and it is written there:

It is a routine matter to rewrite the definitions in a more structural fashion, say within ETCS. In outline, a game is a rooted tree with no infinite branches and equipped with a labeling of each edge by a symbol $L$ or $R$.

and

In this set-up, the condition of no infinite branches plays the role of a foundation axiom, and inductive arguments tend to devolve upon the use of the principle of dependent choice.

But it is not the fact that any surreal number is a tree with finite depth, and many interesting results comes after depth $\omega$, therefore, it seems to me that the tree approach cannot formulate all the surreal numbers (unless we use something like a “transfinite tree”, whose definition in SEAR is not obvious to me as well.) but only all the surreals which is created on day $n\in\omega$. (Thanks for correcting me if I am already wrong here.)

I think there remains hope to capture “all of the surreals”, using the approach here

But again, as there is no universally approved notion of ordinals in structural set theory, we can only formulate ordinals with some base $A$, in the sense that an $A$ ordinal is an equivalence class of well-orders on $A$.I think this gives hope to formulate $A$-based surreals as functions from $A$-ordinals.

Is there any suggested approach to define the whole collection of surreals in structual set theory like SEAR or ETCS?

Another question is that: If we can capture surreals in SEAR perfectly, then we should be able to prove that each ordinal can be represented as a surreal. Since ordinals cannot be captured perfectly, “each ordinal can be represented as a surreal” will have an alternative statement as for surreals in SEAR. What would that statement be? Does it sound plausible to use “ordinals with some base” instead?

]]>It is well-known that we can do proof by induction in a topos using the natural number object, I am interested in proving the strong induction principle, and I am attempting to translate this proof here https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ( (I) $\to$ (SI) ) into an abstract version, so it works for the natural number object in a category satisfies ETCS (In particular, the topos satisfies well-foundedness, and every subobject has complement, therefore, this is a Boolean topos).

The $\le$ relation is given as the pullback of $o: 1\to N$, as the element $0$ of natural number, along the map truncated subtraction $-: N\times N \to N$, as in Sketch of an elephant by Johnstone (page 114, A2.5).

I think the statement of strong induction to prove is as the following.

For a subobject $p: P \to N$, if for an arbitary element $n: 1 \to N$ of the NNO, “all member $n_0: 1\to N$ such that $- \circ \langle n_0, n\rangle = o$ factorises through $P$” implies “$s \circ n: 1 \to N \to N$ factors through P”, then $P\cong N$.

I am not sure what to do with the $Q$ though, and I am not sure if constructing such a $Q$ need the comprehension axiom for ETCS, and hence have trouble translating the proof in the link to also work for NNO. I think if we translate the proof, then we should reduce the task of $P\cong N$ into the task of proving $Q \cong N$. I am now asking about how to construct such a $Q$, which corresponds to the predicate $Q$ in the link. Any help, please?

p.s. The problem that I am actually interested in is proving the well-foundedness of natural number object (explicitly, every non-empty set has a minimal element), but the “material set theoretic proof” using strong induction. Therefore I think I should get strong induction principle for NNO. It will also be great if we can directly prove the well-ordered principle for NNO. (Have searched online for well-orderedness and strong induction for NNO, but nothing helpful is found. Is there any material to read about them?)

]]>Hi,

I am trying to answer my own question here…

Is it possible to derive the axiom of induction from a model of the natural numbers?

…and came across this page on nLab:

This seems to have what I need, but the going is hard. I wonder if anyone can help.

I am stuck, for example, on what exactly $rec_p^n(...)$ is, and what a fibration is. The text says ’the above fibration’ but there is no fibration above so far as I can see, only what I’m guessing is a related display map. The page on fibrations is duanting and didn’t, at a quick glance, seem to give me the necessary relevant information.

All help appreciated!

Kind regards,

James

]]>[2] http://de.arxiv.org/abs/math/0103091 (10 pgs PDF)

Why is there so little interest in *finite* carries (extending residues to integers) since Gaus (1801) and Hensel (p-adics, 1913)?

They can profitably be used for elementary proofs of FLT and Goldbach (see [1] [2]). ]]>