Skip to main content
MathOverflow

Return to Answer

added 977 characters in body
Source Link
user21820
user21820
  • 2.9k
  • 1
  • 18
  • 35

From a logical viewpoint, this is frankly a trivial matter and has nothing to do with platonism, ZFC, or the cumulative hierarchy in ZFC. $ \def\nn{\mathbb{N}} \def\zz{\mathbb{Z}} \def\qq{\mathbb{Q}} \def\rr{\mathbb{R}} \def\cc{\mathbb{C}} $

Anyway, IVT is provable in HOA using only the axiomatization of the reals. And so are EVT (extreme value theorem), MVT (mean value theorem), Dini's theorem for real functions, ... You only need to go beyond HOA if you want to handle arbitrary types, such as general metric spaces, topological spaces and so on. Even then, every mathematical structure of interest will be defined via axiomatization, and all proofs based on that axiomatization alone would of course carry over to all those structures.

There is one possible snag, namely what if the proof was found by a computer rather than a human? Well, if the proof is really just one huge mess, then the easiest solution has been provided by Gareth McCaughan: We can tack on a proof of the equivalence of the desired theorem about Cauchy-reals with the same theorem stated for any isomorphic copy of the reals, and hence we can treat the given computer-generated proof as a black-box. More generally, we can write a computer program $P$ such that, given any desired statement $Q$ about a model $M$ of some second-order axiomatization $A$ that only uses $M$ via its interface $A$, $P(Q)$ outputs a proof that $Q(M)$ implies $Q(N)$ for every model $N$ of $A$. Then we do not even have to manually construct such kind of tack-on proofs but can just run that single program $P$ on any theorem that that 'wag' throws at you, and not just for those about reals. The exact details would depend on the chosen foundational system, but Z set theory certainly suffices.

From a logical viewpoint, this is frankly a trivial matter and has nothing to do with platonism, ZFC, or the cumulative hierarchy in ZFC. $ \def\nn{\mathbb{N}} \def\zz{\mathbb{Z}} \def\qq{\mathbb{Q}} \def\rr{\mathbb{R}} \def\cc{\mathbb{C}} $

Anyway, IVT is provable in HOA using only the axiomatization of the reals. And so are EVT (extreme value theorem), MVT (mean value theorem), Dini's theorem for real functions, ... You only need to go beyond HOA if you want to handle arbitrary types, such as general metric spaces, topological spaces and so on. Even then, every mathematical structure of interest will be defined via axiomatization, and all proofs based on that axiomatization alone would of course carry over to all those structures.

From a logical viewpoint, this has nothing to do with platonism, ZFC, or the cumulative hierarchy. $ \def\nn{\mathbb{N}} \def\zz{\mathbb{Z}} \def\qq{\mathbb{Q}} \def\rr{\mathbb{R}} \def\cc{\mathbb{C}} $

Anyway, IVT is provable in HOA using only the axiomatization of the reals. And so are EVT (extreme value theorem), MVT (mean value theorem), Dini's theorem for real functions, ... You only need to go beyond HOA if you want to handle arbitrary types, such as general metric spaces, topological spaces and so on. Even then, every mathematical structure of interest will be defined via axiomatization, and all proofs based on that axiomatization alone would of course carry over to all those structures.

There is one possible snag, namely what if the proof was found by a computer rather than a human? Well, if the proof is really just one huge mess, then the easiest solution has been provided by Gareth McCaughan: We can tack on a proof of the equivalence of the desired theorem about Cauchy-reals with the same theorem stated for any isomorphic copy of the reals, and hence we can treat the given computer-generated proof as a black-box. More generally, we can write a computer program $P$ such that, given any desired statement $Q$ about a model $M$ of some second-order axiomatization $A$ that only uses $M$ via its interface $A$, $P(Q)$ outputs a proof that $Q(M)$ implies $Q(N)$ for every model $N$ of $A$. Then we do not even have to manually construct such kind of tack-on proofs but can just run that single program $P$ on any theorem that that 'wag' throws at you, and not just for those about reals. The exact details would depend on the chosen foundational system, but Z set theory certainly suffices.

Source Link
user21820
user21820
  • 2.9k
  • 1
  • 18
  • 35

From a logical viewpoint, this is frankly a trivial matter and has nothing to do with platonism, ZFC, or the cumulative hierarchy in ZFC. $ \def\nn{\mathbb{N}} \def\zz{\mathbb{Z}} \def\qq{\mathbb{Q}} \def\rr{\mathbb{R}} \def\cc{\mathbb{C}} $

Almost all reasonable mathematical statements about the reals are actually about any structure that satisfies the axiomatization of the reals. It is clear that this axiomatization can be expressed in very weak foundational systems, whether or not compatible with ZFC. Of course, if you are only familiar with ZFC then you may have to look at how things go in ZFC (as François G. Dorais has explained). But ZFC is really a red herring here.

The Cauchy-sequence or Dedekind-cut constructions merely serve to prove the existence of such a structure that satisfies the axiomatization of the reals. From then on, we can literally forget the exact objects in the construction (which is precisely what $∃$-intro does), because we are only interested in theorems concerning the axiomatized properties (interface) of the reals. Similarly when you construct the complex numbers by a quadratic extension of $\rr$ by some object $i$ such that $i^2 = -1$ in the field extension $\rr(i)$, it is completely irrelevant what objects are 'used' as elements in the field extension. For instance, you could use linear polynomials in $X$ with addition and multiplication modulo $X^2+1$. All that matters is that you get an algebraically closed field containing an isomorphic copy of the reals. Relatedly, we can assume that $\rr ⊆ \cc$ because we only care about the axiomatized properties of $\rr$, which are preserved under isomorphism. One could manually preserve the original $\rr$ as an actual subset of its quadratic extension, but that is unnecessary for the reason I just stated.

Long before $\rr$, to even get from $\nn$ to $\zz$ we could either encode an integer as a sign with a magnitude, or as an equivalence class of pairs from $\nn$. Does it matter? No, because all we care about are certain properties.

If someone claims to have proved something about reals but their proof needs to look at the concrete implementation of reals, then that someone simply has taken a silly route. This is akin to expressing an algorithm in the SOAP assembly language for the IBM 650, instead of expressing it in at least a high-level language supporting loops and function calls. Good software is always written to separate interface from implementation, and so are good proofs (whether in a formal system or not).

Consider simple examples. The IVT (intermediate value theorem) concerns continuous functions on a closed bounded interval of the reals. To state it directly, we must be able to quantify over real functions. This only needs 3rd-order arithmetic (since a real can be naturally encoded as a function of naturals, which is 2nd-order, so a function from reals to reals would be 3rd-order). More generally, if you want to talk about objects in specific higher-order types where the 0th-order type is the naturals, then all you need is HOA (higher-order arithmetic). Practically any modern foundational system for mathematics can interpret HOA, namely that there is a computable translation of proofs from HOA into the system that interprets it. You can check that Z set theory for instance interprets HOA, and if you want some extra interesting sets you might want some form of AC (axiom of choice).

Anyway, IVT is provable in HOA using only the axiomatization of the reals. And so are EVT (extreme value theorem), MVT (mean value theorem), Dini's theorem for real functions, ... You only need to go beyond HOA if you want to handle arbitrary types, such as general metric spaces, topological spaces and so on. Even then, every mathematical structure of interest will be defined via axiomatization, and all proofs based on that axiomatization alone would of course carry over to all those structures.