Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Smooth NNO and Gödelian incompleteness

Keith Elliott Peterson (Mar 12 2026 at 19:45):

I've been looking into the internal logic of smooth topoi (specifically well-adapted models for SDG) and came across a claim in Kostecki's Differential Geometry in Toposes (p. 15, footnote 9).
The text suggests that because the NNO in models with invertible infinitesimals (like \mathcal{Z} or \mathcal{B}) is of 'geometric' rather than 'arithmetic' origin, it may overcome the standard restrictions of Gödel's incompleteness theorems—partially due to the weakening of induction.
How formalized is this 'potential possibility' suggested by Lawvere and Reyes? Is there a known proof or a specific model where the internal NNO is demonstrably complete (or at least avoids the standard diagonal argument construction), or is this still primarily a foundational conjecture?

Screenshot_20260312_131920_Chrome.jpg

Kevin Carlson (Mar 12 2026 at 20:12):

Could you or anyone expand on how exactly induction is weakened? I guess the point is roughly that if there are invertible infinitesimals, then there must be some infinite natural numbers, as in hyperreal analysis, and the induction principle, if there is one, for these hypernatural numbers will be different than that for the plain naturals. But I don't know what such an induction principle would be; thinking about the little I know of hyperreal analysis, one usually seems to use the transfer principle to say that first-order statements behave the same with or without the invertible infinitesimals, but the second-order theory of the hyperreals , including the hypernaturals, seems scary and perhaps not much used. But presumably the geometry here makes this all make at least a bit more sense?

Jean-Baptiste Vienney (Mar 12 2026 at 20:12):

@Keith Elliott Peterson , to write in LaTeX, you can use two dollar symbols, then the LaTeX code, and then two other dollar symbols. Just to make your text better looking :slight_smile: (your question sounds really interesting)

Max New (Mar 12 2026 at 21:24):

I'm a bit confused. Surely Godel's incompleteness theorem applies to an NNO in any topos? The internal language of a topos is powerful enough to prove induction from the universal property of an NNO, so validate Peano's axioms.

I don't know the context but I think the text is saying that there is a different object that is not an NNO, and that is the "geometric" natural numbers, but not an NNO

Kevin Carlson (Mar 12 2026 at 22:51):

Yes, that's right, if there are invertible infinitesimals then it seems at least intuitively clear that the hypernaturals won't be an NNO, since, well, you just can't prove things for all hypernaturals by counting up from zero one at a time.

James Deikun (Mar 12 2026 at 23:33):

Yes, the screenshotted text is explicitly giving a formula to construct the object of "geometric natural numbers" (though I don't know what the formula means!) which it explicitly contrasts with the NNO.

James E Hanson (Mar 12 2026 at 23:46):

Is there a reference for Lawvere's suggested approach for 'overcoming' Gödel's incompleteness theorem, as alluded to in the footnote in the screenshot?

David Michael Roberts (Mar 12 2026 at 23:47):

Here's the document in question https://www.fuw.edu.pl/~kostecki/sdg.pdf

David Michael Roberts (Mar 12 2026 at 23:49):

Screenshot 2026-03-13 at 10.18.41 AM.png
Not massively helpful, but in case any of these ring bells for people

David Michael Roberts (Mar 12 2026 at 23:52):

Reyes' paper Synthetic reasoning and variable sets referenced further down doesn't seem to discuss it (I happen to have that book at hand)

James E Hanson (Mar 12 2026 at 23:59):

The thing is that the incompleteness theorem is extremely general. As long as the object in question is still a model of intuitionistic Robinson arithmetic (or even a weak subintuitionistic fragment thereof) , incompleteness will apply. In particular, induction isn't even really essential.

Ryan Wisnesky (Mar 13 2026 at 00:08):

Some of this might be a truism unrelated to decidability? 'the weakening of arithmetic means the restriction of the validity of induction' could simply mean 'the use of a non-initial model (of arithmetic) means the restriction of the use of initiality', which is true in general, for all theories regardless of decidability.

Kevin Carlson (Mar 13 2026 at 00:13):

James Deikun said:

(though I don't know what the formula means!)

I believe $Y$ is just Yoneda and $\ell$ might be the contravariant embedding of $C^\infty$-rings into $C^\infty$-schemes. In effect, the geometric natural numbers become the space whose smooth functions are the same as the smooth functions on $\mathbb{N}.$ But I don't understand why this isn't an NNO.

David Michael Roberts (Mar 13 2026 at 00:27):

I'm likewise nonplussed by the claim about Lawvere's claim

Matteo Capucci (he/him) (Mar 13 2026 at 08:22):

What an interesting paper... I don't understand how one would break induction though, and in any case Godel's incompleteness does not depend on it (I see James already mentioned it)

Matteo Capucci (he/him) (Mar 13 2026 at 08:27):

Though intuitively @Kevin Carlson's argument makes sense, so there should be topoi in which N has non-standard elements. I wonder if the NNO property only captures induction for standard elements then?

Morgan Rogers (he/him) (Mar 13 2026 at 12:12):

I would expect it to be possible that one or both of axioms 1 and 3 of Robinson arithmetic (following the Wikipedia page linked by Matteo) could fail for an alternative natural numbers in non-Boolean toposes.
However, decidability/incompleteness is already a bit less interesting in intuitionistic logic; a topos fails to be Boolean as soon as there is a subobject/proposition which fails to be complemented (failure of $\phi \vee \neg\phi$, where $\neg$ still makes sense as the Heyting pseudocomplement operation, so that $\neg\phi$ is the strongest proposition inconsistent with $\phi$ in the sense that $\phi \wedge \neg\phi \rightarrow \bot$), and any such proposition is automatically one for which no theory can prove the disjunction, let alone be able to prove one or the other.

Morgan Rogers (he/him) (Mar 13 2026 at 12:14):

I expect that the OP @Keith Elliott Peterson already understands what I mean given that the context is SDG which is incompatible with LEM, so I'm curious what kind of incompleteness statement you would expect to apply?

James Deikun (Mar 13 2026 at 13:47):

I expect a suitable intuitionistic version of this kind of incompleteness would be whenever you can prove a disjunction but you can't prove either disjunct.

James E Hanson (Mar 13 2026 at 16:14):

James Deikun said:

I expect a suitable intuitionistic version of this kind of incompleteness would be whenever you can prove a disjunction but you can't prove either disjunct.

But most 'standard' constructive theories actually do have the property that whenever they prove a disjunction they also prove one of the disjuncts.

James E Hanson (Mar 13 2026 at 16:16):

But the second incompleteness theorem and variants thereof are still pretty philosophically meaningful for intuitionistic theories. Heyting arithmetic has the disjunction property but can't prove that it has the disjunction property, for instance. (See Theorem 2 at the end of Friedman's paper here.)

James E Hanson (Mar 13 2026 at 16:17):

Changing what you decide to call 'the natural numbers' can't get around this.

Kevin Carlson (Mar 13 2026 at 16:19):

It would be quite frustrating if the improper citation style in Keith’s shared excerpt had sent us all down a mere wild goose chase.