Timeline for In constructive set theory, is it consistent for there to be a ring that models smooth infinitesimal analysis?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 11 at 14:50 | comment | added | Christopher King | @AndrejBauer hmm, I'd at least want something that's able to do a decent amount of set theory. I think HoTT (even without the univalence axiom) would work as well. I suppose the more interesting question is "what constructive principles/theories are compatible with SIA", but I was afraid that'd be a bit open ended. | |
| Jan 11 at 14:43 | comment | added | Christopher King | @MaxNew oh, I was in the mindset of constructing a full model of SIA while working in CZF. But if the model satisfies CZF, that works as a consistency proof too! | |
| Jan 11 at 9:45 | comment | added | Andrej Bauer | @ChristopherKing: what is the difference between "every total function" and "just those in the model"? In any case, the topos validates thge internal statement "$\forall f \in R^R . \text{$f$ is smooth}$". Also, are you dead set on using CZF, or would higher-order intuitionistic logic also fit the bill? | |
| Jan 11 at 9:21 | comment | added | Z. A. K. | @NoahSchweber: Christopher King seems to be asking something like "Is the first-order theory CZF + there is a structure (R,+,⋅,0,1) so that every function f:R→R obeys the Kock-Lawvere axiom consistent?" here, not "is there some topos where the SIA axioms stated at the level of the topos hold". I agree with his assessment that it at the very least need not be immediate from the Moerdijk-Reyes topos models that the answer to this particular question is positive - e.g. does every topos w/ NNO model CZF? | |
| Jan 10 at 21:41 | comment | added | Max New | The models in that book are non-trivial models of CZF + a ring R satisfying the principles of smooth infinitesimal analysis, e.g., that all total functions from R to R are differentiable. Since the model is non-trivial this proves that assuming one exists in CZF is consistent. | |
| Jan 10 at 21:19 | comment | added | Noah Schweber | I'm not sure I understand your question. How does a model distinguish between "every total function" and "every total function in the model [= itself]"? | |
| Jan 10 at 20:33 | comment | added | Christopher King | @MaxNew do those models show that every total function $R \mapsto R$ is differentiable, or just those in the model? My understanding is that those models just apply to functions "in the model", whereas I'm looking for a $R$ such that the axioms of SIA applies to all total functions. I may be misunderstanding though, since I'm not super familiar with the subject! | |
| Jan 10 at 20:19 | comment | added | Max New | Yes there's entire books about such models: link.springer.com/book/10.1007/978-1-4757-4143-8 | |
| Jan 10 at 20:11 | history | asked | Christopher King | CC BY-SA 4.0 |