Timeline for Cauchy reals and Dedekind reals satisfy "the same mathematical theorems"
Current License: CC BY-SA 4.0
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 30, 2019 at 15:29 | comment | added | user21820 | @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. | |
| Jul 30, 2019 at 15:22 | comment | added | user21820 | @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). | |
| Jul 30, 2019 at 14:58 | comment | added | Timothy Chow | @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. | |
| Jul 29, 2019 at 14:44 | comment | added | user21820 | @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. | |
| Jul 29, 2019 at 14:38 | comment | added | user21820 | @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 ${^∧}$. | |
| Jul 29, 2019 at 14:12 | comment | added | Timothy Chow | @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? | |
| Jul 19, 2019 at 14:27 | comment | added | Kevin Buzzard | Oh I mean the lean chat at Zulip | |
| Jul 19, 2019 at 6:47 | comment | added | user21820 | @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. | |
| Jul 19, 2019 at 6:42 | comment | added | user21820 | @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. | |
| Jul 19, 2019 at 0:39 | comment | added | Kevin Buzzard | @WillSawin you could ask that at the Lean chat. | |
| Jul 18, 2019 at 18:00 | comment | added | Will Sawin | @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? | |
| Jul 18, 2019 at 15:19 | comment | added | user21820 | 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 | |
| Jul 18, 2019 at 15:14 | comment | added | user21820 | @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! | |
| Jul 17, 2019 at 20:52 | comment | added | Will Sawin | @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. | |
| Jul 17, 2019 at 18:33 | comment | added | Kevin Buzzard | 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! | |
| Jul 17, 2019 at 18:20 | comment | added | user21820 | @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. | |
| Jul 16, 2019 at 21:37 | comment | added | Kevin Buzzard | "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. | |
| Jul 16, 2019 at 15:08 | history | edited | user21820 | CC BY-SA 4.0 |
added 977 characters in body
|
| Jul 16, 2019 at 14:09 | history | answered | user21820 | CC BY-SA 4.0 |