3
$\begingroup$

In a constructive set theory such as CZF, it is consistent to assume that every function $f : \mathbb R \to \mathbb R$ is continuous. However, it is not consistent to assume that every such function is differentiable. CZF proves that the absolute value function exists and is a total function on $\mathbb R$.

But is it consistent to assume that there is some that there is some ring $R$ which models smooth infinitesimal analysis?

Improve this question
$\endgroup$
8
  • 3
    $\begingroup$ Yes there's entire books about such models: link.springer.com/book/10.1007/978-1-4757-4143-8 $\endgroup$
    – Max New
    Commented Jan 10 at 20:19
  • 2
    $\begingroup$ 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]"? $\endgroup$
    – Noah Schweber
    Commented Jan 10 at 21:19
  • 2
    $\begingroup$ 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. $\endgroup$
    – Max New
    Commented Jan 10 at 21:41
  • 2
    $\begingroup$ @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? $\endgroup$
    – Z. A. K.
    Commented Jan 11 at 9:21
  • 2
    $\begingroup$ @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? $\endgroup$
    – Andrej Bauer
    Commented Jan 11 at 9:45

0

Reset to default

You must log in to answer this question.