Nonstandard analysis in Coq

Using Coq
1

Hello,

I have recently been toying with the idea of doing nonstandard analysis in Coq, and I’m running into an issue. I can construct the hyperreals using ultrapowers (I use nonconstructive axioms so the use of Zorn’s lemma is perfectly fine to me), but I have no idea how to even state the transfer principle. The usual statements involve logic and model theory, but Coq uses its own foundations so I find it difficult to use the usual formulations of the transfer principle in Coq. I feel like I would want to have some kind of definition that would take propositions to their hyperreal variant, but I have no idea how that could even be done. I could maybe manage by just manually utilizing the properties of ultrapowers, but that seems to be removing most of the power of nonstandard analysis, since the transfer principle is so vital to it.

So my question is, is there some way of formulating the transfer principle in NSA in Coq? Or maybe, something similar that produces a similar result?

2

A way to do it would be to reify first-order formulas as an inductive type. Then you would define two interpretations of these formulas: one over the real numbers and the other one over the hyperreal numbers. And finally, you would prove that, for any first-order formula, the former interpretation implies the latter, by induction on the reified formula. This is not so different from manually using the properties of ultrapowers, except that you do it once and for all. Later, you can just reify whatever formula you want to prove, which can be done automatically if needed (e.g., in Ltac), and then apply this transfer theorem.

2 Likes