59

The succinct question

The conjecture of Birch and Swinnerton-Dyer (to take a random example) mentions L-functions and hence the complex numbers and hence the real numbers (because the complexes are built from the reals). Two naive questions which probably just indicate that I don't understand logic well enough: (1) if we regard BSD as a statement about an explicit model of the real numbers (e.g. the one built from Cauchy sequences or the one built from Dedekind cuts), then why is it "obvious" that BSD is true for one iff it's true for the other? (2) Is it "obvious" that BSD can be formulated as a statement BSD(F) which makes sense for an arbitrary complete ordered archimedean field F? If so, is it also "obvious" that BSD in this sense is isomorphism-invariant, i.e. if F1 and F2 are isomorphic then BSD(F1) iff BSD(F2)?

I am interesting in learning the techniques behind why mathematicians treat these claims as obvious.

The original question(s)

Up to unique isomorphism, there is only one complete archimedean ordered field, and mathematicians refer to it as "the real numbers". There are two standard constructions for showing that such a field exists, one using Dedekind cuts and the other using Cauchy sequences. To be even more explicit, let me define "the Cauchy reals" in this question to mean the set of equivalence classes of Cauchy sequences modulo the usual equivalence relation (so if $x$ is a Cauchy real then $x$ is an uncountably infinite set) and let me define "the Dedekind reals" as being Kuratowski ordered pairs $\{\{L\}, \{L,R\}\}$ with $L$ and $R$ a partition of the rationals with every element of $L$ less than every element of $R$ and both non-empty and $L$ having no rational sup (so if $x$ is a Dedekind real then $x$ is a finite set).

Because these two constructions give canonically isomorphic objects, mathematicians think of these constructions as giving "the same answer" and never fuss about which version of the real numbers they are using. I guess there must be some underlying logical principle behind why this works, but I now realise I don't know it. What is it?

I am hoping that there is some theorem of logic that says that if I formulate a conjecture (in ZFC set theory, say) about all complete archimedean ordered fields and then I prove the conjecture for the Cauchy reals, then I can somehow deduce that it is also true for the Dedekind reals. But as it stands this is not true. For example, a stupid conjecture about all complete archimedean ordered fields is that they are all equal (as sets in ZFC) to the Cauchy reals. This conjecture is false in general, true for the Cauchy reals, and not true for the Dedekind reals. On the other hand, clearly any "sensible" (I don't know a formal definition of this) mathematical question about complete archimedean ordered fields will be true for the Cauchy reals iff it's true for the Dedekind reals. What would a proof look like? Does one need to give some kind of algorithm which changes a certain kind of proof about Cauchy reals to Dedekind reals? In what generality does this sort of thing work? What are the ingredients? Note that I cannot guarantee that my proof treats the Cauchy reals only as a complete archimedean ordered field, even though I "know in my heart" that there is no advantage in actually starting to look at elements of elements.

Here is a related question. Take a normal mathematical conjecture which mentions the reals (for example the Birch and Swinnerton-Dyer conjecture, which mentions L-functions, which are functions on the complex numbers, and a complex number is usually defined to be a pair of reals). Every mathematician knows that it doesn't matter at all whether we use the Dedekind reals or the Cauchy reals. So what is the proof that BSD is true for the L-functions built using the Dedekind reals iff it's true for the L-functions built using the Cauchy reals? It seems to me that we could attempt to use the preceding paragraph, but only once we know that some version of BSD can be formulated using any complete archimedean ordered field, and that the resulting formulation is "a sensible maths question". My gut feeling is that this is "obvious"; however I would rather hear some general principle which I can invoke than actually have to say something coherent about why this is true.

Background

A few years ago I would have found this kind of question extremely confusing to think about, and would have either dismissed it as trivial or just said that the real numbers were unique up to unique isomorphism and there were probably "theorems of logic" which resolved these issues. But I have a better understanding of what mathematics is now, and I realise that I am not quite sure about how all this works. Here is an attempt to explain what I think are the guts of the first question.

Let's say I am doing "normal" mathematics, and I come up with a "normal" mathematical conjecture that mentions real numbers in some way, e.g. the conjecture that pi + e is transcendental, or some much more complicated conjecture which mentions the real numbers implicitly, like the Birch and Swinnerton-Dyer conjecture (which mentions the complex numbers, which are built from the real numbers). No mathematician would ask me whether I mean the Cauchy reals or the Dedekind reals in my conjecture. Let's say I decide to offer $1,000,000 for a proof of my conjecture.

Now say some wag who is into computer proof formalisation asks me what foundational system I am using when I make my conjecture, so I say "ZFC set theory". And then they remark that the real numbers have two definitions in ZFC set theory, one using Cauchy sequences and one as Dedekind cuts, and which real numbers was my conjecture about? I am a mathematician, so I know it doesn't matter, so I say "the Cauchy reals" just to shut them up. The next day I realise I could have been more clever, so I take the trouble to reformulate my conjecture so that instead of explicitly mentioning "the real numbers" I make it into a conjecture about all complete archimedean ordered fields (the fact that this reformulation is possible could be thought of as a definition of "normal" mathematics in the paragraph above). Of course I "know" that this does not change my conjecture in any substantial way. I decide to get in touch with the wag to tell them my change of viewpoint, so I call them up, but before I can get a word in, they very excitedly tell me that they left their new deep learning AI ZFC computer proof generator system on all night working on my conjecture about the Cauchy reals, and it has managed to come up with a proof which is a billion lines long and incomprehensible, but each line is formally checked to be valid in ZFC, so it must be right, and can they please have the $1,000,000. I explain that I have now changed my conjecture and it's now a statement about all complete archimedean ordered fields, and ask them if their proof works for all such fields. "Definitely not!" they reply. "My AI needs to generate proofs of trivial things like 3 < 5 to prove your conjecture, and it does it by thinking about the definition of < on the Cauchy reals and coming up with a proof of 3 < 5 which is specific to Cauchy reals. My AI also does a bunch of other weird things with Cauchy reals, and some of them I don't understand at all; they are probably just weird ways of proving standard facts about complete archimedean ordered fields but I can't be sure". "Well, does everything you do for the Cauchy reals have some analogue for the Dedekind reals?" I ask. And they reply "I don't know, all I can guarantee is that my proof is valid in ZFC set theory, and therefore I have proved your conjecture in its Cauchy form. You are claiming that the Cauchy form and the complete archimedean ordered field form are obviously equivalent, hence I have proved your more general conjecture."

I think the wag must be right, but I do not understand the details of why.

Kevin Buzzard
  • 40,559
  • I am confused about your counterexample. If ZFC proves that any Dedekind-complete Archimedean field is also a Cauchy-complete field, with the isomorphism being unique. How is that claim true for Cauchy reals but not Dedekind reals? – Asaf Karagila Jul 15 '19 at 17:26
  • I know that in some constructive flavours of mathematics the two objects differ. But ZFC is not a constructive theory, is it? – Asaf Karagila Jul 15 '19 at 17:27
  • I am simply claiming that the predicate on complete archimedean ordered fields defined by saying "I am literally equal to the set of Cauchy reals" is true for the Cauchy reals but not for the Dedekind reals. – Kevin Buzzard Jul 15 '19 at 17:29
  • 1
    Yes, this has nothing to do with constructivism. I am simply saying that whilst the Cauchy reals and the Dedekind reals are isomorphic, they are not literally equal as sets. This is all about ZFC with classical logic, i.e. "normal maths". – Kevin Buzzard Jul 15 '19 at 17:30
  • 3
    Okay, but what is the set of Cauchy reals? Also, this all falls back to the usual silly "anti-ZFC" argument which says "Ohhhh!!!! There are two singletons which are not the same!!!!! IT IS NOT A GOOD FOUNDATION OF MATHEMATICS!!!!!!!!111oneone". I'm not trying to disparage your question, which I think is good, and worthy of discussion. I'm just drawing parallels with the "usual" stuff. It always baffled me that people who care so little about "up to isomorphism" suddenly don't know how to apply an isomorphism to save their lives. (And again, this is not a critique of your question.) – Asaf Karagila Jul 15 '19 at 17:37
  • See https://math.stackexchange.com/questions/437948/do-isomorphic-structures-always-satisfy-the-same-second-order-sentences You're asking about something maybe stronger than just second-order statements, but it's true for the same reason – Kevin Casto Jul 15 '19 at 17:39
  • I will add definitions to the question. I completely agree with you that there is more than one way to define the Cauchy reals. – Kevin Buzzard Jul 15 '19 at 17:39
  • 14
    For statements about complete archimedean ordered fields, why shouldn't your terms "sensible" and "normal" be taken to mean "invariant under isomorphism"? – Andreas Blass Jul 15 '19 at 17:43
  • 10
    I don't see why the answer isn't just "give a proof that the statement you care about is isomorphism-invariant." Is there a reason this is unsatisfying? – Noah Schweber Jul 15 '19 at 17:48
  • 1
    I like this idea but I don't see how to make it rigorous yet. If $Q(F)$ is a statement about complete ordered archimedean fields $F$, and $C\to D$ is an isomorphism of complete ordered archimedean fields...you want me to demand that $Q(C)$ is true iff $Q(D)$ is true? Is that checkable in practice? It is surely true for the BSD conjecture. How do I prove this though? – Kevin Buzzard Jul 15 '19 at 17:49
  • 1
    @NoahSchweber can you give a proof that (a) there is a version of BSD which makes sense for any complete ordered archimedean field and (b) this version isomorphism-invariant? What would go into such a proof? I know "it's obvious" but I am interested in what the proof looks like. – Kevin Buzzard Jul 15 '19 at 17:58
  • 7
    @KevinBuzzard A statement like BSD isn't a first-order statement within the field $F$, but it is a first-order statement about an appropriate "superstructure" built over that field (and possibly other auxiliary objects, like $\mathbb{N}$). Generally the set of all finite-type objects over this base is massive overkill already. The point now is that isomorphic bases yield isomorphic superstructures. – Noah Schweber Jul 15 '19 at 18:13
  • 4
    So what we'd do is the following. I have my "BSD-for-Cauchy-sequences" $\beta$. You would turn this straightforwardly into a first-order statement $\varphi_{BSD}$ in the language of the appropriate superstructures and would prove that $\beta$ iff the superstructure $S_{RC}$ associated to the Cauchy reals $RC$ satisfies $\varphi_{BSD}$. Now we prove that the construction taking a CAOF $F$ and outputting the appropriate superstructure $S_F$ is isomorphism-preserving. This then gives us the following: for any CAOF $F$ we have $S_F\models\varphi_{BSD}$ iff $S_{RC}\models\varphi_{BSD}$ iff $\beta$. – Noah Schweber Jul 15 '19 at 18:18
  • 1
    If you'd like I can turn this into an answer. – Noah Schweber Jul 15 '19 at 18:18
  • 7
    More often than not, when a statement such as "in $\mathbb{R}$, we have [...]" is proved, what's actually proved is "in any field satisfying this and that properties (which characterize $\mathbb{R}$), we have [...]". In this view, the validity of the statement for any given realization of $\mathbb{R}$ simply follows from the specialization of the universal statement to said realization. – nombre Jul 15 '19 at 18:28
  • 39
    When one introduces the reals in (say) ZFC, what one is really doing is passing to a conservative extension of ZFC in which there is a new object ${\bf R}$ that happens to be a complete ordered Archimedean field. To verify the metatheorem that this is indeed a conservative extension, one can produce an explicit example of such a field, such as the Cauchy construction or the Dedekind construction. But the conservative extension does not presume that ${\bf R}$ is equal to either of these two (or any other preferred construction), so any theorems in this extension do not depend on such choices. – Terry Tao Jul 15 '19 at 20:28
  • 2
    @KevinBuzzard : Is this really a proof-assistant question in disguise? If so, the answers you get might be more on-point if you dispense with the disguise. – Timothy Chow Jul 15 '19 at 20:46
  • 1
    (continued) Specifically, there are techniques for creating a layer of types that let you do what you want even if your assistant, at bottom, speaks ZFC, complete with all its weirdnesses like $0\in \pi$. – Timothy Chow Jul 15 '19 at 20:50
  • @TerryTao When I think about the reals in ZFC, I'm thinking about Dedekind cuts of the field of fractions of the Grothendieck ring of $\omega$; in what sense have I passed to an extension? Are you essentially saying that I have a preferred model I think about, but when most mathematicians think about them there is no model in mind which amounts to an extension of the language by a formal symbol and some axioms? – Alec Rhea Jul 15 '19 at 20:53
  • 4
    You say "a stupid conjecture about all complete archimedean ordered fields is that they are all equal to the Cauchy reals. This conjecture is false in general, true for the Cauchy reals, and not true for the Dedekind reals." If you have a statement involving a method of constructing real numbers (Cauchy real, Dedekind real, Eudoxus real, etc.) then the proof that two complete ordered fields are uniquely isomorphic lets you go between the constructions, e.g., "a real number is a Cauchy real" becomes "a real number is a Dedekind real". Why have you forgotten how to use isomorphisms? – KConrad Jul 15 '19 at 20:58
  • 14
    Two cyclic groups of the same size are isomorphic as abstract groups (usually in multiple ways). Does that make someone worry about the validity of statements for one cyclic group as an abstract group not being valid for another group of the same size? If you want to think of cyclic groups not as abstract groups but as something else then maybe cyclic groups of the same size are no longer isomorphic. For example, if $p$ is prime, $\mathbf Z/(p-1)$ and $(\mathbf Z/(p))^\times$ are isomorphic as abstract groups but there is a definite computable difference, which matters in cryptography. – KConrad Jul 15 '19 at 21:07
  • 5
    In the original setting Kevin gave, of different constructions of $\mathbf R$, they satisfy the same theorems expressed in the language of complete ordered fields but there's no reason to think different constructions satisfy "the same theorems" with no constraint at all. – KConrad Jul 15 '19 at 21:11
  • 1
    @Terry: That's an interesting approach to foundations. It has a problem, though, that now we could ask why is it the same when we interpret the new symbol as a Cauchy completion or a Dedekind completion. So you're not entirely avoiding the question Kevin asks. – Asaf Karagila Jul 15 '19 at 21:26
  • 6
    We are drowning in comments :-( – Kevin Buzzard Jul 15 '19 at 23:00
  • 1
    @TimothyChow the question was inspired by thoughts about rewriting along isomorphisms in proof assistants, however the more I thought about things the more I realised that I did not even understand the question I asked. – Kevin Buzzard Jul 15 '19 at 23:01
  • 6
    @KConrad You know as well as I do that isomorphism is not the same as equality. You also know as well as I do that the difference should not really matter. However the problem is that whilst all these different models of the reals are isomorphic as ordered fields, how do I know that my ZFC proof concerning one of them only uses facts about ordered fields? This is a silly set theory question. – Kevin Buzzard Jul 15 '19 at 23:04
  • @NoahSchweber I think that offering your thoughts as an answer is a good way of moving the conversation forward. Are you claiming that it is "obvious" that BSD for Cauchy reals iff BSD for Dedekind reals? – Kevin Buzzard Jul 15 '19 at 23:09
  • 2
    @nombre: I agree with your "more often than not" statement. What I am trying to understand is what happens in the situation where we don't know enough about a proof to be sure that we're in the "more often than not" situation. – Kevin Buzzard Jul 15 '19 at 23:15
  • @NoahSchweber I have updated the question based on your and Blass' comments suggesting I focus on isomorphism-invariance of the situation. – Kevin Buzzard Jul 15 '19 at 23:26
  • If I prove that every Dedekind-complete field is Cauchy complete, and that every Cauchy-complete field is Dedekind-complete. And if we agree that any two Dedekind-complete fields are isomorphic, and that any two Cauchy-complete fields are isomorphic. Where is the problem now? There is nothing more that talking about "structure" can get you. From here you get differences in implementations into the universe of sets... – Asaf Karagila Jul 15 '19 at 23:35
  • 3
    The problem is that the proof by my wag friend might use facts about the set of real numbers which are true for one model but not the other. The statement is "sensible" but I have no guarantee that the proof is. They are isomorphic as fields but not equal as sets, and I do not immediately see how to port the proof from one to the other. I'm worried about how a proof might use some specifics of an implementation. – Kevin Buzzard Jul 15 '19 at 23:37
  • 1
    @KevinBuzzard I'll post an answer when I have a bit more time, but briefly: "Are you claiming that it is "obvious" that BSD for Cauchy reals iff BSD for Dedekind reals?" Ultimately, yes (modulo the inherent rudeness of the word "obvious," especially in a context where we're actually considering being fully formal). "I do not immediately see how to port the proof from one to the other." You don't need to port the proof; instead, you'll have a theorem which yields one version from the other as a corollary. It doesn't matter what the wag does or doesn't do in their proof - treat it as a blackbox. – Noah Schweber Jul 16 '19 at 00:00
  • Kevin, I understand the concern. But let me work from the other direction for a moment, and make what might seem like a logical fallacy. Do you have an example for a statement which is "structural" whose proof crucially depends on the implementation of the structure into sets? I know one example that I saw Joel Hamkins present a few months ago where the proof relied on a specific way we code ordered pairs (if my memory is correct), but even that is arguably not an example, since it was a foundational theorem, and implementation is foundation. – Asaf Karagila Jul 16 '19 at 00:13
  • 18
    @AlecRhea Most mathematicians in fact do not reason directly in ZFC, for much the same reason most programmers do not program directly in machine code. Instead they almost all use a much higher level and dynamic mathematical language, which Andreas Blass calls "T" in this MathOverflow answer: https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems/90945#90945 . The foundation of dynamically extending one's working language as needed is much closer to how mathematicians work in T than the orthodox foundational approach of always working purely in ZFC. – Terry Tao Jul 16 '19 at 00:54
  • @TerryTao Your original comment began with "when you introduce the reals in (say) ZFC...", so I presented the way I think about them in ZFC (or MK in my case usually) -- how is this related to your assertions about T above? It seems we're talking across eachother; I was wondering why someone "introducing the reals in ZFC" would pass to an extension, and you seem to be addressing why someone introducing the reals in an intuitively familiar manner would avoid a particularly cumbersome axiomatization. – Alec Rhea Jul 16 '19 at 05:19
  • 1
    Sorry, I was using the usual abuse of notation (also noted in Blass's post that I linked to) of using ZFC as a shorthand for T (which I did not have space to explain about in my first comment). In other words, I was referring to the ZFC-like theory that mathematicians actually use in practice, rather than the low-level ZFC that appears in orthodox foundations. – Terry Tao Jul 16 '19 at 05:23
  • @TerryTao Ah, I see now, much appreciated. (I think the route you suggest is the most satisfying response to the question I've seen thus far) – Alec Rhea Jul 16 '19 at 05:33
  • @AsafKaragila "Do you have an example for a statement which is "structural" whose proof crucially depends on the implementation of the structure into sets?" -- absolutely not. I have never seen an example in number theory. – Kevin Buzzard Jul 16 '19 at 15:43
  • 1
    Is it really clear how to state "BSD for Cauchy reals" and "BSD for Dedekind reals" in a formal way? I think formally stating them might be equally as hard as proving the equivalence, or the difficulty of proving the equivalence might vary greatly with the choice of statement. – Will Sawin Jul 16 '19 at 19:53
  • 1
    @KevinBuzzard I think Francois' answer captures everything I was going to say, so for now I'm not going to post an answer of my own. But let me know if there's something in my comments above that you feel Francois doesn't address, and I can expand that. – Noah Schweber Jul 16 '19 at 23:40
  • 1
    There used to be an interesting answer on homotopy type theory from (I think) @AndrejBauer , but now I cannot see it anymore. Was it cancelled? – Andrea Ferretti Jul 17 '19 at 08:15
  • 3
    @AndreaFerretti: I deleted the answer because I refuse to participate in flame wars. The comments were too toxic for my taste. Also, I realized that the answer needs more work and references (I am pretty sure it's known that Church's simple type theory is isomorphism-invariant), and it exceeds the scope of an MO answer. I might write a blog post about it. – Andrej Bauer Jul 17 '19 at 14:02
  • @AndrejBauer If you ever do that, please let me know :-) – Andrea Ferretti Jul 17 '19 at 14:24
  • I am fortunate enough to still be able to see Andrej's answer :P I thank you for the answer Andrej and I will not comment on the flame war. – Kevin Buzzard Jul 17 '19 at 18:29
  • I think the difficulty here is being exaggerated a bit. For mathematicians, sure, we all know that Cauchy-BSD is equivalent to Dedekind-BSD. We know that because we know all the definitions BSD builds on and that all of these make no reference to the internal structure of the reals. This is also easy to verify mechanically (it's a simple parsing problem). What is difficult is actually formalising all those definitions for a machine: but if you don't do that, you can't verify any-BSD anyway. If you already formalised some-BSD (statement) then verifying any-BSD is easy. – user36212 Jul 17 '19 at 18:34
  • @WillSawin "Is it really clear how to state "BSD for Cauchy reals" and "BSD for Dedekind reals" in a formal way? " It is to me -- but this is what I have spent the last two years of my life learning about. You can make a type in dependent type theory that is equivalent to BSD for Cauchy reals, and you can make another one which is equivalent to BSD for Dedekind reals. – Kevin Buzzard Jul 18 '19 at 06:23
  • @KevinBuzzard But you asked in ZFC, where it's less obvious. Let me ask two very stupid questions. 1. Does this formalization use the type of types at all (as a base for constructing further types like equality types). 2. Do you know of an example of a statement not using the type of types which is not isomorphism-invariant in this way? – Will Sawin Jul 18 '19 at 11:39
  • Oh sorry, I misunderstood the comment. I thought you were saying "formalisation of BSD in any foundations is surely hard". I have no experience formalising within ZFC. I formalise in dependent type theory and you can prove that the type of types exists; I don't really know what it means to say I am "using it". Recursors mention these kinds of sets. The principle of mathematical recursion, used everywhere, is a claim about constructing terms f n of type F n where F some map from the naturals to some big type universe. – Kevin Buzzard Jul 18 '19 at 11:53
  • 1
    I have now read the question, the comments, and the answers several times, and I have to confess that I still don't understand what's happening here. I went back and looked through several textbooks / papers on number theory, differential geometry, functional analysis, and a few other areas and I was unable to locate a single example that used a specific construction of the real numbers rather than their axioms. I get that constructing an object which satisfies the axioms is difficult, but given that we're allowed to use these axioms in the rest of mathematics what is left of this question? – Paul Siegel Jul 20 '19 at 02:06
  • @PaulSiegel The point is ZFC as such doesn't contain a set 'the real numbers'. It contains several different sets on which you can define operations+relations satisfying the axioms. While a mathematician is more or less never going to use the details of some construction in a proof or definition (note, by the way, that sometimes basic analysis does use explicitly one or another construction..!), if you want to write your proofs and definitions in ZFC you have to do that. I think the conclusion is that doing it in a proof is fine, but doing it in definitions (if you want to make sense) requires – user36212 Jul 20 '19 at 15:30
  • that you also check your definitions do not change meaning when you change the construction of the reals you're using. This is not completely trivial, though I think it is not so hard as suggested (once you already formalised definitions in the first place).

    I think the main point is that ZFC formalisation of the reals is a toy example of the more general problem: what do we do about formalising any proof in some more useable system when we want to work with a structure unique up to isomorphism but which isn't actually unique?

    – user36212 Jul 20 '19 at 15:33
  • 1
    And the reason this is a real issue is that 'unique up to isomorphism' is only useful as long as whatever you want to do is also isomorphism invariant. But there are examples where this is just not true. For example R[x] is the same as R[y], except when x and y already play different roles in your structure, or more to the point except when they will later be used differently. That's a nice source of undergraduate errors. So how do we make sure a computer is not making this kind of error, while also not having to do all the stupid work with isomorphisms ourselves? – user36212 Jul 20 '19 at 15:39
  • "The problem is that the proof by my wag friend might use facts about the set of real numbers which are true for one model but not the other. The statement is "sensible" but I have no guarantee that the proof is. They are isomorphic as fields but not equal as sets, and I do not immediately see how to port the proof from one to the other. I'm worried about how a proof might use some specifics of an implementation."

    Would the following toy example be analogous?

    – Adam Epstein Dec 13 '21 at 09:14
  • Consider the silly, yet still sensible set-theory assertion $\forall x \exists y (,(x\times {y} )\cap x = \varnothing)$. Here, $\times$ is with reference to a fixed, but otherwise arbitrary notion of ordered pairing - so what I really have here is a theorem schema. There is a natural proof schema, which proceeds via consideration of $X\times \mathcal{P}X$ and argues by Cantor's Theorem. Quoting from my homework solutions: – Adam Epstein Dec 13 '21 at 09:22
  • "Let $Z={z\in X: \exists x\exists y (z=(y,x)\wedge (x\in X\wedge y\in \mathcal{P}X))}$ and consider $g:Z\rightarrow \mathcal{P}X$ given by $g(z)=y$ for $z=(y,x)$. It suffices to show that $g$ is not surjective. Let $h:X\rightarrow \mathcal{P}X$ be given by $h(x)=g(x)$ for $x\in Z$ and $h(x)=\varnothing$ otherwise. If $g$ is surjective then $h$ is surjective, which is impossible, by Cantor's Theorem." – Adam Epstein Dec 13 '21 at 09:23
  • The preceding argument is valid for any implementation of ordered pairing. We regard the following argument as unhygenic:

    "Under the Kuratowski convention, $X$ is disjoint from ${X}\times X$: if $z=(X,x)$ for some $x,z\in X$ then $z\in X\in{X}\in {{X},{X,x}}=z$ which contradicts Foundation."

    – Adam Epstein Dec 13 '21 at 09:24

8 Answers8

28

Here is a way to do this in ZFC. Similar ideas work in a bunch of other contexts.

First, given any set $A$ in the universe of sets $V$ we can form the set theoretic universe $V(A)$ by mimicking the cumulative hierarchy, where the elements of $A$ are considered to be atoms. Start with $V_0(A) = A$, at successors $V_{\alpha+1}(A) = V_\alpha(A) \cup \mathcal{P}(V_\alpha(A))$, at limits $V_\delta(A) = \bigcup_{\alpha<\delta} V_\alpha(A)$. (Some care must be taken to carefully distinguish atoms. Indeed, $A$ will appear at some point in the pure part of $V(A)$ and we don't want to confound this pure $A$ with the set of atoms $A$. Fortunately, it is well-understood how to do this formally. Since these details are irrelevant, I will not mention them further.)

If $A$ has additional structure, say it's a complete ordered field, then that structure will appear quickly in the hierarchy since we add all possible subsets at each step. Therefore $A$ has all the same ordered field structure it originally had in $V$. Even completeness carries through since the subsets of $A$ in $V(A)$ come from subsets of the original $A$ in $V$. The difference is that $A$ has no internal structure in $V(A)$ since we can't inspect the innards of atoms: all we can say about atoms is whether two atoms equal or not. The main kicker is that if $A'$ is any isomorphic structure to $A$, then the isomorphism of $A'$ and $A$ lifts uniquely to an isomorphism of $V(A')$ and $V(A)$!

A normal mathematical statement about $A$ in $V$, say BSD, makes perfect sense about the structure $A$ in $V(A)$. This is because BSD makes no mention at all of the innards of the elements of $A$. Furthermore, if BSD holds of the original $A$ in $V$ then it will hold of the $A$ in $V(A)$ since they have identical external structure. Because $V(A')$ is isomorphic to $V(A)$, the isomorphism ensures that BSD holds of $A'$ in $V(A')$. Then, for the reverse reason explained above, BSD holds of the original $A'$ in $V$.

For this transfer from $A$ to $A'$, we only needed that BSD was a normal mathematical statement in the sense that it relies only on the external structure of $A$ and $A'$ and not on the innards of these structures. Whether some proof of BSD for $A$ relies heavily on the innards of $A$ is irrelevant since the statement proven makes no mention of the internal structure of $A$ and will therefore transfer to any isomorphic structure as described above.

  • 2
    But what if the mathematical statement, in addition to mentioning $A$, mentions some other mathematical structures, such as the integers, and some sheaf cohomology, and half of Lange's algebra book? Will you just keep accummulating stuff and build $V(\mathrm{stuff})$? If so, how are we ever going to relate theorems stated in $V(\mathrm{stuff}_1)$ from Paper 1 to theorems stated in $V(\mathrm{stuff}_2)$ from Paper 2? – Andrej Bauer Jul 16 '19 at 14:03
  • 2
    @AndrejBauer: The pure set part of any $V(A)$ is a copy of $V$. So $V(A)$ knows everything that happens in $V$. – François G. Dorais Jul 16 '19 at 14:34
  • I am afraid that does not answer my question. If my theorem and proof mention structures $A$, $B$ and $C$, then I need $V(A,B,C)$ so that I can replace either one with an isomorphic copy. If you are suggesting that I should use $V(A)$, inside of which I can find $B$ and $C$ as elements of $V$, then I cannot vary $B$ and $C$ isomorphically. – Andrej Bauer Jul 16 '19 at 15:55
  • 3
    Ok. What's the issue with $V(A,B,C)$? You can iterate the construction as much as you want. But that's not necessary, the Theorem proved by this argument is that if you have any set theoretic statement about a structure $A$ that doesn't contain $\in a$ for $a \in A$, then the statement holds for any isomorphic structure $A'$. You can apply this to all the parameters of a statement. – François G. Dorais Jul 16 '19 at 17:42
  • Does your theorem cover topological spaces as structures? The topology is a family of opens, and there will be theorems that look at elements of those opens, so will have "$\Box \in a$" thingy in them, no? – Andrej Bauer Jul 17 '19 at 14:05
  • There is a general problem with any suggestion that tailors the formal system, the language, or the model, to the theorem or structure at hand, namely, that it becomes unclear how we're going to combine all these custom-made gadgets together into a beautiful cathedral of mathematics. A computer scientists would say that such solutions are not modular or composable. I would be deligthed to be wrong about this point. – Andrej Bauer Jul 17 '19 at 14:08
  • @AndrejBauer This seems very similar to the Bourbaki structured set approach, which can handle topological spaces but not certain other stuff like sheaves IIRC. One doesn't view the open sets as elements of the structured set $A$, but rather as part of the structure. – Will Sawin Jul 17 '19 at 15:06
  • 2
    @AndrejBauer i.e. a topological space is a set $A$ with a distinguished element of $\mathcal P (\mathcal P(A))$ satisfying some axioms, and all statements in the language of $V(A)$ with an extra constant symbol for this distinguished element are invariant under the usual notion of isomorphism of topological spaces. – Will Sawin Jul 17 '19 at 15:12
  • 1
    I feel like I am programming in a mix of assembly and COBOL. – Andrej Bauer Jul 17 '19 at 15:24
  • 1
    @WillSawin is right, there is no need to atomize any external structure. Any set theoretic construct on top of $A$ is literally in $V(A)$, no matter how complex that construct is. Everything about $A$ in $V$ transfers exactly to $V(A)$. That's the point of going to the length of building the entire hierarchy on top of $A$ rather than stopping after 15 steps, or selecting what you want or don't want, or doing anything specific to the statement to be transferred. – François G. Dorais Jul 17 '19 at 15:24
  • 1
    Also keep in mind that the point is not to move into $V(A)$. The point is to transfer a statement $\phi(A)$ to a statement $\phi(A')$ where $A$ and $A'$ are isomorphic structures in $V$. The point of $V(A)$ is to do this in three easy steps: the transfer from $\phi(A)$ in $V$ to $\phi(A)$ in $V(A)$ is literal (modulo some cosmetic stuff implementing the parenthetical note in the second paragraph), the transfer from $\phi(A)$ in $V(A)$ to $\phi(A')$ in $V(A')$ is through the isomorphism $V(A) \cong V(A')$, and the transfer from $\phi(A')$ in $V(A')$ to $\phi(A')$ in $V$ is again literal. – François G. Dorais Jul 17 '19 at 15:40
  • 4
    @AndrejBauer I don't think anyone claimed that formalizing mathematics in ZFC was a fun and relaxing experience. – Will Sawin Jul 17 '19 at 15:46
  • @WillSawin: nobody knows because nobody's ever formalized any decent amount of mathematics in ZFC (extended with definitions of new symbols and operations, say), as far as I know. Who knows, perhaps it's enjoyable. – Andrej Bauer Jul 17 '19 at 17:15
  • 2
    @AndrejBauer Umm... I guess that depends on what counts as "decent", but Metamath and Mizar are both significant formalized bodies in ZFC or a very close cousin. Not all formalized systems use type theory. As for "enjoyable", there's no accounting for taste but I enjoy it quite a bit. Frankly the foundational system doesn't matter too much when it comes to the game-like feeling of formalization, so I would guess you are already familiar with it. – Mario Carneiro Jul 18 '19 at 01:08
  • 1
    Mizar is written in something that is more type theory than set theory, even though at the bottom there is ZFC. This is not meant as a criticism, only an observation. People who have never tried to formalize mathematics are unaware of many "engineering" problems that crop up, and some may even underestimate them or dismiss them. That's why I am interested in @FrançoisG.Dorais suggestion: I don't see how to make it scale. It solves nicely a single problem, but how would it work if many people used it to formalize many chapter of mathematics? How would they combine their work? – Andrej Bauer Jul 18 '19 at 07:27
  • @FrançoisG.Dorais - What do you exactly mean by "if $A'$ is any isomorphic structure to $A$, then the isomorphism of $A'$ and $A$ lifts uniquely to an isomorphism of $V(A')$ and $V(A)$"? [I'm asking this because it seems to me that $A'$ equipotent to $A$ does not imply $V_1(A')$ equipotent to $V_1(A)$ --- take $A={\varnothing},A'={{\varnothing}}$.] – Pierre-Yves Gaillard Jul 18 '19 at 11:55
  • 1
    @Pierre-YvesGaillard $V(A)$ is a model of ZFA, where the elements of $A$ are the atoms. In ZFA, atoms have no elements (and extensionality is slightly modified to allow this). Inside $V(A)$ there is no way to know what the atoms originally contained. In both cases you propose $V_1(A) = {\ast,\varnothing,{\ast}}$, where $\ast$ denotes the atom. – François G. Dorais Jul 18 '19 at 14:04
  • 1
    @AndrejBauer It looks like we're trying to solve different problems. From my point of view, scaling isn't an issue at all but from your perspective it looks like a major endeavor. But something you said in passing gave me a hunch... In my view, I prove a metatheorem: If $\phi(A)$ is a statement in the language of set theory meeting this and that syntactic requirement, then ZFC proves the universal closure of $(\forall A, A')(A \cong A' \to \phi(A) \to \phi(A'))$. I'm being deliberately vague about the syntactic requirements and I originally thought that was the issue but I now think ... – François G. Dorais Jul 18 '19 at 14:27
  • 4
    ... the issue is that I require $\phi(A)$ to be a formula in the language of set theory. I do not allow new symbols for then I would have to factor these into the (otherwise trivial) translation from $V$ to $V(A)$. This is important but it is not restrictive. It does, however, put additional burden on the "formalizer" who has to fully translate BSD (to keep the same example) in the language of set theory prior to applying the metatheorem. That is a massive task! – François G. Dorais Jul 18 '19 at 14:35
  • 1
    I rest my case :-) – Andrej Bauer Jul 19 '19 at 08:25
21

Here's a low-tech way to look at it, which to me seems perfectly convincing.

Let C be some implementation of the reals via Cauchy sequences and D be some implementation of the reals via Dedekind cuts. Here C is "really" something like a tuple consisting of the set of reals, a relation corresponding to addition, etc.; D is a tuple with (allegedly) equivalent things implemented differently.

Let P(X) be the proposition that X is a tuple of the right size and that, when considered as an implementation of the real numbers, X satisfies the Birch-Swinnerton-Dyer conjecture. We have a proof -- perhaps a bizarre incomprehensible implementation-dependent one -- of P(C), in ZFC.

I claim that (again, in ZFC) P(C) iff P(D). Sketch of proof: 1. Up to canonical isomorphism there is only one complete ordered field. 2. C and D are complete ordered fields. 3. Therefore there is an isomorphism between C and D; in fact we can even write it down. 4. We can use this to build an isomorphism between C's complex numbers and D's complex numbers, and then between C's L-functions and D's L-functions, and C's elliptic curves and D's elliptic curves, and so on for every object required to state the BSD conjecture. 5. If we have a specific elliptic curve over D, these isomorphisms yield its equivalent over C (and vice versa); they pair up the groups of rational points in the two cases, showing that they have the same rank; they pair up the corresponding L-functions, showing that they have the same order of zero at s=1. 6. And we're done.

None of this requires that these isomorphisms be applied to the proof of P(C). That proof can be as C-specific as you like. What the isomorphisms show is that the things BSD says are equal come out the same way however you implement the real numbers.

How do we know that we can actually construct this pile of isomorphisms? By thinking about what objects we need in order to state the BSD conjecture, and how we build them, and noting that nothing in the process cares about "implementation details" of the real numbers. If you're sufficiently confident of your memory, you could do this "negatively" by noting that if when you were learning about elliptic curves and L-functions a lecturer had said something like "and of course this is true because the number 1 is just the same thing as the set containing just the empty set" you'd have noticed and been horrified. Otherwise, you can (tediously but straightforwardly) go through the usual textbooks and check that the constructions are all "sane".

EDITED to add:

Although I stand by everything above, I can't escape the feeling that Kevin already knows all that and I'm therefore not answering quite the question he's meaning to ask. Let me put some words into Kevin's mouth:

Yes, yes, of course. Every mathematician who thinks about this stuff at all has something like that mental picture. But what really justifies that breezy confidence that that big pile of isomorphisms is really there? I understand that it feels obvious that none of the machinery you need to state something like the BSD conjecture depends on "implementation details". But this is the sort of thing mathematicians are good at getting wrong. It wasn't until the 20th century that we noticed how many extra axioms you really need to add to Euclid's system to make the proofs in the Elements rigorous. The axiom of comprehension probably seemed obviously innocuous until Bertrand Russell asked whether the set of non-self-membered sets shaves itself. A more isomorphism-y example: it seems transparently obvious that a set $X$ is the same size as $\{\{x\}\,:\,x\in X\}$, but this fails if you work in NF instead of ZFC. Maybe there's some implementation detail no one ever noticed we were assuming. How can we be sure?

Again, personally I'm very confident that I'd have noticed if some implementation detail were being slipped into anything in "normal" mathematics (or at least, I'm as confident as that I'd have noticed any other sort of gap in the proofs -- I don't think there's anything special here), and very confident that if I missed one some of the many many other mathematicians, some of them much smarter than I am, who have read the same textbooks and been to the same lectures would have noticed. But I think Kevin's asking whether there's some simple principle that makes it obvious without any need either to trust that sort of thing, or to check in detail through everything in the textbooks, and I want to be clear that this answer doesn't purport to give one; my feeling is that there couldn't possibly be one, any more than there could be some simple principle that makes it obvious (with the same restrictions) that there are no other logical holes in those same textbooks, and for essentially the same reason.

  • Very nice! Can't you even start with two complete ordered fields and show that if the Birch-Swinnerton-Dyer Conjecture holds over one, it holds over the other? – Pierre-Yves Gaillard Jul 16 '19 at 13:52
  • 1
    Yup, same process as I described. All it depends on is that we have an isomorphism between our fields out of which we can build isomorphisms of the other structures we need to state BSD. – Gareth McCaughan Jul 16 '19 at 13:54
  • 1
    I see someone gave this a downvote. It's very likely that they spotted something bad about my answer that I missed; I'd be very interested to know what. (This isn't a snarky way of complaining about downvotes; I really do think it most likely indicates a deficiency I'm unaware of.) – Gareth McCaughan Jul 16 '19 at 15:01
  • 1
    I didn't read it carefully, but the general idea is certainly correct, as I also said in my answer, so I don't see any reason for a downvote. Anyway, welcome to Math Overflow and hope to see more of your answers! – user21820 Jul 16 '19 at 15:10
  • My current best guess is that the downvoter either (1) thinks my answer doesn't really add anything to others, or (2) just dislikes this sort of foundational angst and has downvoted the question and all the answers for good measure :-). Thanks for the kind words! – Gareth McCaughan Jul 16 '19 at 15:24
  • 1
    Hi Gareth [I assume you're the Gareth I went to the IMO with all those years ago!] Yes, this is the conclusion I've come to. So the actual proof is never written down, but its existence is some kind of consequence of a "mathematician's agreement" that we don't break the interface of the real numbers when using them. I have never seen a proof of this nature before, but now I realise that mathematics is full of them. I know a completely different example involving localisations of rings where the proof is just the same -- this works because we would definitely have complained if it didn't. – Kevin Buzzard Jul 16 '19 at 15:52
  • 18
    While all this is a nice idea, it's an entirely different matter to try to actually carry it out. People have tried and failed. It is not at all easy to "just insert the correct isomorphisms" everywhere. Not at all! I speak from experience. When you formalize mathematics with a proof assistant, you have to insert such isomorphisms (they're actually applications of Leibniz's law translated to type theory). The activity is known as "coherence hell" by those who have had the misfortune to try to do it. – Andrej Bauer Jul 16 '19 at 15:58
  • Yup, same Gareth. It may amuse you to know that about 1/3 of the way into the question I thought "I wonder if Kevin wrote this" -- though that's more from seeing your other stuff on MO than from any recollection of how you wrote all those years ago. – Gareth McCaughan Jul 16 '19 at 16:07
  • @AndrejBauer Yeah, actually doing it in full detail would be extremely painful -- but don't most things become extremely painful when you try to do them in full detail? This isn't the only thing that hurts when you switch from just proving things to trying to cram them into an automated proof assistant, right? I think the key question here is how you know that it can be done, and (though I'm willing to be refuted) I think what I've said is correct on that point. – Gareth McCaughan Jul 16 '19 at 16:09
  • I absolutely agree with you. My localisation story can be summarised with the following meme: https://twitter.com/XenaProject/status/1136973391280377856 and fixing this issue took me a very long time; only later on did I realise that was proving the wrong things because I was thinking about stuff the wrong way. The ongoing thread about this sort of thing at the Lean Zulip chat https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/transport.20and.20parametricity contains comments by computer scientists making exactly Andrej's point. – Kevin Buzzard Jul 16 '19 at 16:13
  • @GarethMcCaughan "but don't most things become extremely painful when you try to do them in full detail?" I suppose they do -- I never have to do this, the proof assistant I use has a bunch of tactics which do the dirty work for me in most cases. However it does not currently have a tactic which switches out an object for an isomorphic one. To write such a tactic one would need a clear understanding of the algorithm, which is what I'm trying to develop. – Kevin Buzzard Jul 16 '19 at 16:15
  • 5
    @KevinBuzzard: you should take note of what people in type theory did before Univalence axiom came along, and aks them why they were so excited about Univalence. I don't actually know of any proofs that type theory is isomorphism-invariant (which is what your tactic is supposed to do), althought people belive this to be the case. – Andrej Bauer Jul 16 '19 at 16:20
  • 1
    The problem is that type theory is not isomorphism-invariant (at least Lean's dependent type theory isn't) -- however there is this weird notion of being "acceptable to mathematicians", and many things which are acceptable to mathematicians are isomorphism-invariant. – Kevin Buzzard Jul 16 '19 at 21:36
  • 1
    Really, Lean is not isomorphism invariant? – Andrej Bauer Jul 17 '19 at 14:22
  • Lean cannot rewrite along isomorphisms. If R and S are isomorphic rings, and P is a predicate on rings, then it might be the case that P(R) is true and P(S) is not provable; for example P(X) might be the predicate "X=R". This predicate is "non-mathematical". – Kevin Buzzard Jul 17 '19 at 18:20
  • @GarethMcCaughan yes you're thinking exactly how I'm thinking. Isn't life crazy? All these secret theorems being implicitly proved. I have a more interesting example of this involving localisations of rings. Basically if you prove a theorem for R[1/S] (defined as pairs (r,s) modulo the usual equivalence) then in a formal proof verification system which does not use HoTT you can't apply the theorem to any ring isomorphic to R[1/S]. You should instead prove results about rings isomorphic to R[1/S]. But I know explicit examples in the literature where people (Grothendieck!) do not do this. – Kevin Buzzard Jul 17 '19 at 18:23
  • One has to then think a little bit to actually ensure that what is going on is valid mathematics. This is a bore, because I am trying to design a tactic which does all the rewriting in a formal proof system automatically. I think you're seeing, like me, that this is a little delicate. – Kevin Buzzard Jul 17 '19 at 18:25
  • 4
    @KevinBuzzard, @ AndrejBauer: Regarding “Is Lean isomorphism-invariant?”, there are two different kinds of isomorphism-invariance properties to distinguish. The stronger one is that any postulated predicate on types must be isomorphism-invariant; this is roughly univalence, and as Kevin points out, it fails in Lean and many other reasonable type theories. The other is that any definable predicate must be isomorphism-invariant; this is roughly parametricity, and such properties have been proven for various type theories and seem likely for many others, including Lean as far as I know. – Peter LeFanu Lumsdaine Jul 17 '19 at 18:36
  • @PeterLeFanuLumsdaine could you give a rough idea of the difference between a postulated and definable predicate, for the interested outsider? – Michael Bächtold Jul 17 '19 at 20:52
  • @KevinBuzzard - I wonder if you should be trying to design a completely automatic tactic or something rather semi-automatic? What I mean (I think) is that some of these things are really implementation details (what are the real numbers), some are a bit intermediate (R[1/s]) and some are genuine problems (changing measure on a probabiliy space comes to mind) where what you would like to do either requires serious justification or is just not true. I don't see a great way to distinguish automatically, so perhaps one should ask the computer to change one at a time – user36212 Jul 17 '19 at 22:47
  • and then check whether what is coming out looks like what it is supposed to be? (I realise that something actively wrong will be rejected, but you can easily prove something you did not want to prove..!) – user36212 Jul 17 '19 at 22:48
  • 4
    @MichaelBächtold In type theory there is more than one kind of equality; more generally there are several distinct equivalence relations on the category of all types, none of which quite agree with the mathematician's notion of "equal". Mathematicians have weird super-powers where they know to only treat objects via their interfaces but never explicitly mention this fact; there is a public interface which we use and a private interface that we never touch and which is invariant under some of the equivalences but not all of them. – Kevin Buzzard Jul 17 '19 at 22:55
  • 2
    The reason this is an issue is a foundational one. If someone had asked me 10 years ago what my foundations are, I would have said "ZFC set theory", but if that's really true then are my reals the Cauchy reals or the Dedekind reals? I don't care because I'm actually working in a different and much more subtle theory than ZFC set theory, where the reals have a public interface and a private interface, and we have all promised not to touch the private interface (e.g. asking how many elements $\pi$ has is part of the private interface of the real numbers; one can only treat numbers as "atoms") – Kevin Buzzard Jul 17 '19 at 22:57
  • 2
    @PeterLeFanuLumsdaine Parametricity fails in lean as well, because of the presence of a global choice function. If you avoid choice then I believe parametricity holds, but people like Kevin absolutely do not want to work in this kind of intuitionistic system. To me the interesting question is what to do when the ambient theory does not give you univalence or parametricity for free, such as in ZFC. – Mario Carneiro Jul 18 '19 at 00:54
  • 2
    Here's a mistake in your post, but I doubt this is why you got a downvote: you wrote "they pair up the groups of integer points in the two cases, showing that they have the same rank" instead of "they pair up the groups of rational points in the two cases, showing that they have the same rank". – KConrad Jul 18 '19 at 04:41
  • Oooops! Will fix. Thanks. – Gareth McCaughan Jul 18 '19 at 09:56
  • @KevinBuzzard: Your last comment contains a good question, but it is more a matter of precision than a matter of foundations. Any mathematical claim has to be 100% precise, regardless of foundations, and we cannot use the term "real" without having defined it. So for complete precision every claim must be made under the context of certain definitions. The correct approach is to prove that there is a model of the axiomatization $A$ of the reals, by ∃-intro after the hard work, and then define $\mathbb{R}$ to be some structure that satisfies $A$, by ∃-elim. This forces encapsulation. – user21820 Jul 18 '19 at 15:00
  • Equivalently, all subsequent theorems would be proven under the context of $\mathbb{R}$ being a model of $A$, but nothing else, so we have no idea exactly what objects are in $\mathbb{R}$. It is possible for someone to use a wrong approach, and prove facts about some specific model of $A$, but that is not a problem with the foundational system or its underlying logic, as much as it is a problem with the bad choice of what kind of facts to prove. Nothing more subtle than any standard deductive system for ZFC over FOL is needed (but Fitch-style is good for humans), but we must use it right. – user21820 Jul 18 '19 at 15:05
  • 2
    @MichaelBächtold: “postulated” vs “definable” is a distinction made when looking at a logical system from outside, not within the system itself. “Definable” means just what you probably think it does: e.g. given a ring R, the predicates “R is an integral domain”, “R is uncountable”, and “R is Noetherian” are all definable in ZFC (or any reasonably strong foundational system), and you can prove (in ZFC or other systems) that these all respect isomorphism. You can also postulate an arbitrary predicate P of rings, and ask whether the system must prove “P respects isomorphism”, or [cont’d] – Peter LeFanu Lumsdaine Jul 18 '19 at 15:30
  • 1
    roughly equivalently, whether the system proves or disproves “every predicate on rings respects isomorphism”. In ZFC, you can also define predicates that don’t respect isomorphism, like “the empty set is an element of R”. So ZFC refutes “every predicate on rings respects isomorphism”. Type theory with univalence proves “every predicate on rings respects isomorphism”. In a type theory without univalence but that satisfies parametricity, you can’t prove “every predicate on rings respects isomorphism”, since it’s consistent that there could exist some predicate that doesn’t, but [cont’d] – Peter LeFanu Lumsdaine Jul 18 '19 at 15:34
  • 1
    …you know that for and specific predicate you can define, you’ll also be able to prove that it respects isomorphism. – Peter LeFanu Lumsdaine Jul 18 '19 at 15:35
18

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}} $

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.

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.

user21820
  • 2,733
  • 3
    "because we are only interested in theorems concerning the axiomatized properties (interface) of the reals." Yes! However we never seem to formally state this fact, and after so many years of mathematics has piled up, it seems almost impossible to start to formally check this, and it's also pointless because everyone knows it's true. There just appears to be no reference, in some sense. It's just something we all know. – Kevin Buzzard Jul 16 '19 at 21:37
  • @KevinBuzzard: I'm pretty sure it must have been stated somewhere, even if I've no idea how to find a reference. I'm not sure what it means to formally state it, because what we are interested in is not something provable. But one can quite systematically identify when this is done, because whenever people refer to "the naturals" or "the reals" they are actually referring to a model of its usual axiomatization, and never a specific implementation. The only possible catch I am aware of is that in ZFC we frequently use $ω$ and not other representation of naturals, because it is an ordinal. – user21820 Jul 17 '19 at 18:20
  • 1
    We certainly cannot prove "for all mathematically interesting statements about objects which involve what a mathematician would call 'the real numbers', the statement is true for the Cauchy reals iff it's true for the Dedekind reals". One could however ask for a proof in any specific case e.g. BSD, and I think that in that case one has to simply grind out the formal assertions that every object defined and every lemma proved along the way to stating BSD is isomorphism-invariant. Every single proof is essentially "it's trivial from what we have already proved", but the pile is huge! – Kevin Buzzard Jul 17 '19 at 18:33
  • @KevinBuzzard One can do something in between, also. One can give a language L, and argue that everything stated in that language is isomorphism-invariant, then check that BSD can be formalized in this language. If one chooses the language well then this should be easier than doing the proof step-by-step, but choosing the language well could be tricky. For BSD I think the pile is not so huge, but for other statements it surely is. – Will Sawin Jul 17 '19 at 20:52
  • @WillSawin: Well, almost all mathematics is expressed clearly in terms of structures defined by their axiomatizations, so almost every mathematical statement can be easily stated in a manner that the last paragraph of my answer would systematically and uniformly deal with. If someone feeds a computer prover with a lousy form of a mathematical statement, it is that someone's mistake, and not an issue with the foundational system at all, because such mistakes can be made with any foundational system! – user21820 Jul 18 '19 at 15:14
  • For instance, we can and should state Fermat's little theorem (FLT) in terms of any structure $\mathbb{N}$ that is a model of PA. Why? Because that is in fact what we want. We should definitely not state Fermat's little theorem in terms of the least infinite ordinal (and appropriate functions), nor should we state it about finite binary strings (even though that is how it would look like in our computers that rely on FLT to decode HTTPS). Anyone who gives a perverse form of FLT to a computer prover is just asking for trouble. Same for statements in real/functional analysis. CC @KevinBuzzard – user21820 Jul 18 '19 at 15:19
  • @user21820 Well suppose I have a proof of some combinatorial theorem about natural numbers that involves passing back and forth often between natural numbers and finite steps. It might be easier to prove that theorem using the least infinite ordinal notion of natural numbers, and put a short argument on the end showing that, if it is true for the least infinite ordinal notion, it's true for all models of second-order arithmetic. Do you think nothing like that could ever happen, so it's not worth figuring out how to write this short argument at the end? – Will Sawin Jul 18 '19 at 18:00
  • @WillSawin you could ask that at the Lean chat. – Kevin Buzzard Jul 19 '19 at 00:39
  • @WillSawin: Are you aware that the well-ordering principle for $\mathbb{N}$ is a purely logical and trivial consequence of PA? It would never be easier to prove any statement expressed in higher-order arithmetic via isomorphism between $\mathbb{N}$ and the appropriate structure on $ω$ than to prove it via the well-ordering principle for $\mathbb{N}$. So automated provers would never have an advantage in doing so. That said, I don't claim it isn't worth knowing how to do it. It is worth knowing, otherwise I wouldn't have included my last paragraph. – user21820 Jul 19 '19 at 06:42
  • @KevinBuzzard: It's not related to Lean; it's a simple fact about PA. Anyway the lean chat has been frozen for lack of activity. For extended discussion, feel free to come to the logic chat-room to continue. – user21820 Jul 19 '19 at 06:47
  • 1
    Oh I mean the lean chat at Zulip – Kevin Buzzard Jul 19 '19 at 14:27
  • @user21820 : Is it really true that we want to prove Fermat's little theorem in terms of any model of PA? Isn't there a lot of overhead associated with precisely formulating PA and its model theory? Why PA rather than some weaker formal theory? – Timothy Chow Jul 29 '19 at 14:12
  • @TimothyChow: It's really true, and I don't know what you mean by "a lot of overhead", since there is almost no overhead... FLT says "For every set $N$ and binary operations $+,·$ on $N$ and binary relation $<$ on $N$ and $0,1∈N$ such that ... [insert axiomatization of PA here] ... , FLT is true for $⟨N,+,·,<,0,1⟩$." To evade having to deal with the induction schema, you can use a finite axiomatization of ACA0, but that is arguably unnatural. Or you can work in higher-order logic so that the induction schema becomes a single axiom. To evade coding exponentiation, you can add ${^∧}$. – user21820 Jul 29 '19 at 14:38
  • @TimothyChow: So if what concerns you is that to have the 'real' induction schema we need to at least include a recursive definition of satisfaction of a formula of a certain form, then that is a valid point on the inadequacy of a foundational system that is unable to express the 'true' higher-order notion behind the schema. It does not change the fact that whenever we make any claim about "the natural numbers" we are in fact talking about any model of PA. – user21820 Jul 29 '19 at 14:44
  • @user21820 : Part of what concerns me is that if, in the course of proving some other theorem, someone wants to invoke (say) Paris-Harrington, then they may be unpleasantly surprised that the codebase is framed entirely in terms of models of PA. Even if they're willing to put in some work to implement P-H itself, they may be annoyed at having to grapple with the distinction between $\mathbb N$ and models of PA just to be able to invoke basic facts about the natural numbers. – Timothy Chow Jul 30 '19 at 14:58
  • @TimothyChow: Ah that's what you're concerned about. In my (personal) view, PH is (as you say) a statement that first-order PA cannot prove some sentence that is true about the structure of naturals (i.e. the one that the foundational system has). On the surface, one may think that it requires painful dealing with schemas, but actually it doesn't; ACA0 is conservative over PA and arguably PH should be about ACA0 phrased over HOL rather than PA over FOL (so that arithmetical predicates are second-order objects that can be constructed via the HOL that underlies the foundational system). – user21820 Jul 30 '19 at 15:22
  • @TimothyChow: As for the distinction between the naturals and models of PA, this will occur in any foundational system, whose naturals are never just an arbitrary model of PA, so it is unclear why this kind of distinction should be annoying. After all, such a distinction is intrinsic to the incompleteness phenomena. And I cannot believe that PH will ever be needed in a proof that doesn't already need fine distinctions. – user21820 Jul 30 '19 at 15:29
12

There is no need to even go as far as $\mathbb{R}$ for an example of this type of phenomena. Even $\mathbb{Z}$ could be defined as different sets in ZFC. Let $\omega$ be the first infinite cardinal, as usual

Option 1: We could take $\mathbb{Z}=(\omega\times \{0\})\cup ((\omega-\{0\})\times \{1\}),$ where the second coordinate tells us whether the integer is positive or negative.

Option 2: Switch second coordinates.

Now, if our background theory is ZFC, we can certainly create statements about $\mathbb{Z}$ that are true for one of our constructions, and false for the other. (For instance, consider the statement: The additive identity of $\mathbb{Z}$ is an ordered pair whose second coordinate is the empty set.)

What makes BSD and other questions often avoid this kind of problem, is that they are stated in a language of rings, or topological rings, etc... where the derived objects (like analytic rank) will be invariant when extended to a language allowing multiple identical copies of the structure at hand. (When it isn't immediately clear whether or not a definition or property is well-defined/invariant for the given context, good mathematical writing requires one to point this out.) And, yes, it is obvious that BSD only requires $\mathbb{R}$ to be a completion of $\mathbb{Q}$ at the archimedean place. (Obvious, because we would otherwise have required more in the statement of BSD.) And, yes, you can show that analytic ranks and algebraic ranks are preserved by isomorphisms between completions.

Pace Nielsen
  • 18,047
  • 4
  • 72
  • 133
  • 4
    But the statement "the additive element of $\Bbb Z$ is $\varnothing$" is not a statement about $\Bbb Z$ in the language of groups/rings/whatever, it is a statement about its implementation in set theory. If you add your language $\in$ and all the axioms you expect it to satisfy you can ask if the identity is $\varnothing$, but that would again be an internal statement and would tell you nothing about the implementation... – Asaf Karagila Jul 16 '19 at 07:39
  • 4
    @AsafKaragila I think that's the point Pace was trying to make in the last paragraph : "they are stated in the language of rings" – Maxime Ramzi Jul 16 '19 at 16:54
12

I see a lot of confusion in the comments about what you are asking and why. The way I interpret your question is this:

Given the fact that mathematical statements about (or involving) the reals can be divided into two classes,

A. those that are “isomorphism invariant” (their truth does not depend on which model of the reals you’re using) and

B. those that aren’t,

what is a way to decide whether a given statement belongs to class A or to class B?

I’ll offer a sociological rather than mathematical criterion: if the statement is (as in your example) an open problem with a $1,000,000 prize, or is otherwise a famous/important question, you can be pretty darn sure that it’s in class A; or, conceivably (but with a much lower likelihood) that it’s in class B but that the statement of the question would make very clear which model of the reals it pertains to.

The remaining possibility, that the question contains some kind of hidden ambiguity that makes it belong in class B but in a way that isn’t formally stated, seems essentially inconceivable to me in the context of well-known open problems. The reason is that most working mathematicians are Platonists who, when they think of the real numbers, think of some ideal set satisfying the properties they know the real numbers satisfy, and never concern themselves with pesky foundational issues regarding the actual model of the reals underlying the discussion. For such people, the statements in class A are the only interesting statements (and in some Platonist sense, the only “real” statements) about the reals. A model-dependent question would likely never deserve to be labeled as important, unless it was in some explicit foundations of math context where that model dependence would be an explicit part of the statement of the problem.

As for a formal mechanism that you are asking about for distinguishing between class A and class B statements, as others have said, you need to check that the statement will survive being passed through an isomorphism. How this is done in practice for something like BSD would probably be extremely tedious (and in my opinion isn’t worth the trouble), but an intuitive level, if the statement is phrased in a “coordinate-free” manner that doesn’t appeal to Dedekind cuts or other objects used in a specific realization of the reals, that’s probably good enough to declare “it’s obvious” and go and do something more productive with your time. Well, at least it would be for a Platonist like me.

Dan Romik
  • 2,480
  • "most working mathematicians are Platonists who, when they think of the real numbers, think of some ideal set satisfying the properties they know the real numbers satisfy, and never concern themselves with pesky foundational issues regarding the actual model of the reals underlying the discussion." i.e. maths for maths sake, or maths for applied use. e.g. Furey C (2015) "A physics from Algebra". Do the reals represent the real word, or are they an abstract concept... – Philip Oakley Jul 16 '19 at 07:09
  • 6
    I took Kevin to mean not the statement of the theorem falls into A. or B., but the proof mutatis mutandis, does ("The problem is that the proof by my wag friend might use facts about the set of real numbers which are true for one model but not the other. The statement is "sensible" but I have no guarantee that the proof is.") – David Roberts Jul 16 '19 at 08:06
  • 1
    This answer indicates a point which had not crystallised in my head until very recently. BSD is in class A, for sure, but there is no proof of this in the literature, and some mathematicians are simply not equipped to supply such a proof (my impression is that many do not even really understand the question), whereas others (perhaps the minority?) are well aware that such a proof exists but can understand the enormity of the task to actually supply such a proof. I'm a number theorist and I understand the statement of BSD. Along the way, I "instinctively" verified it was in A, without noticing. – Kevin Buzzard Jul 16 '19 at 10:56
  • 5
    In my mind, one interesting part of the story is that essentially all mathematicians are united in claiming that nobody cares about the proof. Now pity the poor computer proof verification person... – Kevin Buzzard Jul 16 '19 at 11:06
  • 1
    @KevinBuzzard: Let me just say that in my opinion as a logician and computer scientist, I do not think a computer program can find very complicated long proofs of a theorem about reals that unpacks the particular instantiation of the axiomatization of reals, even if it is not encapsulated behind the interface. It is much more likely that a proof utilizing solely the interface would be much shorter than a proof that unpacks at any point, so a good automated prover ought to find the axiomatization-based proof first. But this is an opinion, not a provable mathematical claim. – user21820 Jul 16 '19 at 15:19
  • I'm reminded of a discussion (on the Foundations of Mathematics mailing list, I think) about Univalent Foundations. To oversimplify a bit, the way UF is set up, proofs are "automatically" isomorphism-invariant, so peculiar conversations with the wag will never happen. The cost of doing things this way is that if you really want to prove the ZFC, fully set-theoretic version of the theorem, then you'll still have to do extra work. But arguably, once the isomorphism-invariant version is proved, nobody cares about proving the gory set-theoretic version anyway... – Timothy Chow Jul 16 '19 at 15:40
  • 1
    ...except maybe the poor schmuck tasked with maintaining the ZFC code base! Anyway, I think this discussion can give one a better appreciation for the univalence axiom in homotopy type theory, and why such a trivial-sounding axiom can make a big practical difference in a proof assistant. – Timothy Chow Jul 16 '19 at 15:42
  • 1
    @TimothyChow as I'm sure you know, I've been trying to understand dependent type theory and homotopy type theory recently. And as I know you've guessed, the genesis of this question is exactly trying to understand what needs to be done in dependent type theory to work around the fact that the univalence axiom is not present. But once I realised that actually the issue was present in ZFC as well, that's what gave me the idea to ask on MO. – Kevin Buzzard Jul 16 '19 at 15:47
  • @Timothy: It sounds to me that the people who "should" appreciate UF, based on your comments here, are exactly those people who care about UF to begin with... – Asaf Karagila Jul 16 '19 at 15:58
  • 3
    @AsafKaragila: I don't understand your point. For everyone who currently cares about UF, there was a time $t$ in the past when they did not care about it, so by the intermediate value theorem there was a point where they came to care about UF, presumably for some reason, and presumably sometimes those reasons were justified. You're saying that the considerations I mentioned cannot be regarded as justifiable reasons for coming to care about UF? Or that there can never be a justifiable reason for making that transition? – Timothy Chow Jul 16 '19 at 17:11
  • @Timothy: Yes, in other words, having a maintainable code base is not of any interest of those not interested in UF (and Coq, or some other proof assistant, since I suppose one can care about UF without caring about formal proof verification and whatnot). – Asaf Karagila Jul 16 '19 at 17:13
  • 3
    @AsafKaragila : Well, it's just my opinion, but I think that the day is coming when almost every working mathematician is going to be relying on proof assistants, and is going to have to grasp these sorts of distinctions at some level, much as today's mathematicians need to grasp whether (say) learning Sage is worth the time if they want to perform a certain computation. – Timothy Chow Jul 16 '19 at 17:21
  • 2
    @Timothy: Yes, some people, at some point, might have to resort to proof assistant. For example, people who rely on UF for their work (I am not trying to disparage anyone here). I don't know if "almost every working mathematician" is right. Either I am not a working mathematician (did I take a holiday?) but I never thought about using Sage for anything other than making a nice herbal tea, or a nice tray of roasted potatoes. – Asaf Karagila Jul 16 '19 at 17:26
  • 1
    @AsafKaragila just a bit of nitpicking... I think Sage is not an optimal tool for those jobs. FWIW, I recommend using Wolfram alpha – polfosol Jul 17 '19 at 12:15
  • 1
    @polfosol: I don't need to know the nutrition values of a tray of roasted potatoes. If anything, I need to know the amount of starch in the potatoes and whether or not I want to preboil, cut, peel, or otherwise tend to the potatoes before I roast them. With sage, rosemary, garlic, and for the advanced class also put a handful of mint and peppercorns when preboiling. – Asaf Karagila Jul 17 '19 at 12:18
9

There is no need to use explicit models of $\mathbb R$ in formulations of Swinnerton-Dyer conjecture. You could extend $\mathbf{ZFC}$ with symbols $(\mathbb R,+_\mathbb R,\times_\mathbb R,<_\mathbb R,0_\mathbb R,1_\mathbb R)$ (in addition to symbols $=,\in$) and add obvious axioms of Reals. After that you obtain new system, say $\mathbf{ZFC}+\mathbb R$ in which you able to formulate any theorem about Reals model-independently using those new symbols. To be sure that $\mathbf{ZFC}+\mathbb R$ is conservative extension of $\mathbf{ZFC}$ you should to justify your axioms by construction of either Dedekind or Cauchy reals. So, you should to proof in $\mathbf{ZFC}$ statement $$\exists \mathbb R_{Cauchy}, +_{\mathbb {R}_{Cauchy}},\times_{\mathbb {R}_{Cauchy}},<_{\mathbb R_{Cauchy}},0_{\mathbb R_{Cauchy}},1_{\mathbb R_{Cauchy}} ({axiom}_1 \wedge {axiom}_2 \wedge ... \wedge {axiom}_n)$$ where ${axiom}_1,...,{axiom}_n$ is axioms of real numbers rewritten in terms of Cauchy reals, for example ${axiom}_1$ is $$0_{\mathbb R_{Cauchy}} \in \mathbb{R}_{Cauchy}$$ ${axiom}_2$ is $$\forall x \forall y (x \in \mathbb R_{Cauchy} \wedge y \in \mathbb R_{Cauchy} \to x+_{\mathbb R_{Cauchy}} y = y +_{\mathbb R_{Cauchy}} x)$$ and so on (of course you additionaly need to state that $+_{\mathbb R_{Cauchy}}$ is well-defined function on $\mathbb {R}_{Cauchy}$ and write $((x,y),t) \in +_{\mathbb{R}_{Cauchy}}$ rather than $x +_{\mathbb{R}_{Cauchy}} y = t$) . After that you could (externally, on metalevel) deduce that your system $\mathbf{ZFC}+\mathbb{R}$ is conservative extension of $\mathbf{ZFC}$ so you could work now inside $\mathbf{ZFC} + \mathbb{R}$ instead of $\mathbf{ZFC}$ and formulate statements about Reals model-independently.

Maybe it sounds a little bit artificial but this is exactly how proof-checkers work see Note on definitions on Metamath Proof Explorer. Also, for example, see axiom ax-resscn and construction-dependent theorem axresscn which is justification of axiom ax-resscn and "should not be referenced directly".

  • 1
    Wonderful answer! Beautifully explained! This should be the marked as correct, if only the timing was correct. – Chan Kha Vu Aug 21 '19 at 23:19
6

I think it is essentially the Frege–Hilbert controversy on the nature of mathematical axioms, cf. e.g. https://plato.stanford.edu/entries/frege-hilbert/ :

The central difference between Frege and Hilbert over the nature of axioms, i.e., over the question whether axioms are determinately true claims about a fixed subject-matter or reinterpretable sentences expressing multiply-instantiable conditions, lies at the heart of the difference between an older way of thinking of theories, exemplified by Frege, and a new way that gathered strength at the end of the nineteenth century.

Frege (i) understands the consistency and independence of thoughts to turn not just on the surface syntax of the sentences that express them but also on the contents of the simple terms used in their expression, and (ii) consistency and independence, so understood, are not demonstrable in Hilbert’s manner.

[On] Frege’s conception of logic … given a good formal system, a sentence σ is deducible from a set Σ only if the thought expressed by σ is in fact logically entailed by the thoughts expressed by the members of Σ. (This simply requires that one’s axioms and rules of inference are well-chosen.) But the converse is false: that σ is not deducible in such a system from Σ is no guarantee that the thought expressed by σ is independent of the set of thoughts expressed by the members of Σ. For it may well be, as in the cases treated explicitly by Frege’s own analyses, that further analysis of the thoughts and their components will yield a more-complex structure. When this happens, the analysis may return yet-more complex (sets of) sentences σ′ and Σ′ such that σ′ is, after all, deducible from Σ′. … This is the explanation of Frege’s rejection of Hilbert’s treatment of consistency and independence …

Taking a theory to be axiomatized by a set of multiply-interpretable sentences, Hilbert’s view is that the consistency of such a set suffices for the existence of the (or a) collection of mathematical entities mentioned in the theory. The consistency, for example, of a theory of complex numbers is all that’s needed to justify the mathematical practice of reasoning in terms of such numbers. For Frege on the other hand, consistency can never guarantee existence. His preferred example to make this point is that the consistency (in Hilbert’s sense) of the trio of sentences 1. A is an intelligent being, 2. A is omnipresent, 3. A is omnipotent is insufficient to guarantee their instantiation. (See, e.g., Frege’s letter to Hilbert of 6 January 1900.)

Hilbert is clearly the winner in this debate, in the sense that roughly his conception of consistency [and logic] is what one means today by consistency [and logic] in the context of formal theories.

David Roberts
  • 33,851
  • 2
    While I think the Frege-Hilbert "controversy" may be somewhat related, I feel the question is more of a "logical engineering" nature, i.e., how to organize mathematics so that certain we can guarantee the validity of certain desirable principles. A hundred years ago such a question would very likely be cast in philosophical and foundational terms, but nowadays there is a clear practical motivation behind the question (how to get a proof assistant to do more work). – Andrej Bauer Jul 17 '19 at 14:01
  • As you commented earlier “it is not at all easy to insert the correct isomorphisms everywhere” i.e. to translate the proof from one interpretation to another. Frege’s position (in the controversy) is that it is even impossible, as implied by the 3rd paragraph I cited. – Zvonimir Sikic Jul 17 '19 at 14:32
  • 1
    It is even clearer in a letter to Hilbert on January 6, 1900.: “Given that the axioms in special geometries (i.e. special interpretations; my add) are all special cases of general axioms, one can conclude from lack of contradiction in a special geometry (i.e. a special interpretation; my add) to lack of contradiction in the general case, but not to lack of contradiction in another special case (i.e. another special interpretation; my add).” – Zvonimir Sikic Jul 17 '19 at 14:32
  • Many thanks for this answer. I was well aware when I wrote the question that this sort of issue would be very well-understood but I had no idea about the history of this sort of concept -- I am not a logician and certainly not a philosopher. – Kevin Buzzard Jul 17 '19 at 18:27
  • 1
    It's not clear now where the quote from the SEP ends, and, checking the source, everything after the first sentence is cut and pasted. I'm going to edit again to make it clear the whole entry is a quote, to avoid any attribution worries. – David Roberts Jul 18 '19 at 11:33
  • It ends at the end i.e. everything after the first sentence is quote. – Zvonimir Sikic Jul 18 '19 at 16:11
0

I have a proposal for a (Nearly trivial) instance of such a theorem. Let $Form_{(+,\cdot,\lt)}$ be the set of a logical formulas constructed from the atoms $x+y$, $x\cdot y$, and $x\lt y$, with $x=y$ defined as $\forall z(z\lt x\leftrightarrow z\lt y)$. Then it is a simple to see (Though I will write it here anyway) that if $(\mathbb R,+,\cdot,\lt)$ and $(\mathbb R',+,\cdot,\lt)$ are Dedkind complete ordered fields, then $(\mathbb R,+,\cdot,\lt)\prec(\mathbb R',+,\cdot,\lt)$, where "$\prec$" denotes elementarity in $Form_{(+,\cdot,\lt)}$.

Given an ismorphisim $\pi: (\mathbb R,+,\cdot,\lt)\rightarrow(\mathbb R',+,\cdot,\lt)$, it is immediate that the relation holds for atomic formula, and inductively for logical connectives. Let $\exists x(\phi(x,x_0...x_n))$ be a $Form_{(+,\cdot,\lt)}$ formula, such that $(\mathbb R,+,\cdot,\lt)\vDash \exists x(\phi(x,x_0...x_n))$, and let $z$ be a witness to this. $$(\mathbb R,+,\cdot,\lt)\vDash\phi(z,x_0...x_n)\leftrightarrow(\mathbb R',+,\cdot,\lt)\vDash\phi(\pi(z),\pi(x_0)...\pi(x_n))$$

Therefore $(\mathbb R',+,\cdot,\lt)\vDash\exists x(\phi(x,\pi(x_0)...\pi(x_n)))$, and so $(\mathbb R,+,\cdot,\lt)\prec(\mathbb R',+,\cdot,\lt)$. Why is this important? Well every formula about the Reals in $Form_{(+,\cdot,\lt)}$ is therefore absolute between Dedkind complete ordered fields.

They also satisfy the same second order assertions. Extend the language $Form_{(+,\cdot,\lt)}$ with an atomic formula $x\in X$, and call $x$ a real if $M(x)\leftrightarrow \exists X(x\in X)$. For a non-real $X$, then extend the isomorphisim $\pi$ to $\pi'$ by $\pi'(X)=\{\pi(x)|x\in X\}$, and say $X=Y$ if and only if $\forall x(x\in X\leftrightarrow x\in Y)$. Note that then $x\in X\leftrightarrow \pi'(x)\in \pi'(X)$, and so by the same argument as before $(\mathbb R,+,\cdot,\lt,\in)\prec(\mathbb R',+,\cdot,\lt,\in)$.

So in order to get a result you want what we really want to show is that nearly every sensible statement about the Reals can be coded in just $Form_{(+,\cdot,\lt,\in)}$. This can be verified individually, but a will give you an example: $x=0$, $x=1$, $x\in \mathbb N$, $x\in \mathbb Z$, $x\in \mathbb Q$, $x\in \mathbb {CR}$ (Constructible numbers), as well as algebraic functions can be written in $Form_{(+,\cdot,\lt,\in)}$. First off, $x=0\leftrightarrow \forall y(M(y)\rightarrow x+y=y)$, and similarly with $x=1$.

$$x\in\mathbb N\leftrightarrow \forall X(0\in X\land\forall n\in X(n+1\in X))$$

$$x\in\mathbb Z\leftrightarrow x\in\mathbb N\lor\exists y\in\mathbb N(x+y=0)$$

$$x\in\mathbb Q\leftrightarrow \forall X((X\supseteq\mathbb Z\land\forall y,z\in X({y\over z}\in X))\rightarrow x\in X)$$ (See below)

$$x\in\mathbb {CR}\leftrightarrow \forall X((X\supseteq\mathbb Q\land\forall y\in X(\sqrt{y}\in X))\rightarrow x\in X)$$ (See below)

For the rest, $x={y\over z}\leftrightarrow x\cdot y=z$ and $x=\sqrt y\leftrightarrow x\cdot x=y$. This process is just a couple examples. In fact, you could even though this for the Riemann Hypothesis and other complex mathematical problems. Therefore, your conjecture would almost certainly be absolute between the Cauchy and Dedkind reals.

Master
  • 1,103