Timeline for Cauchy reals and Dedekind reals satisfy "the same mathematical theorems"
Current License: CC BY-SA 4.0
35 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 18, 2019 at 15:35 | comment | added | Peter LeFanu Lumsdaine | …you know that for and specific predicate you can define, you’ll also be able to prove that it respects isomorphism. | |
| Jul 18, 2019 at 15:34 | comment | added | Peter LeFanu Lumsdaine | 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] | |
| Jul 18, 2019 at 15:30 | comment | added | Peter LeFanu Lumsdaine | @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] | |
| Jul 18, 2019 at 15:05 | comment | added | user21820 | 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. | |
| Jul 18, 2019 at 15:00 | comment | added | user21820 | @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. | |
| Jul 18, 2019 at 9:57 | history | edited | Gareth McCaughan | CC BY-SA 4.0 |
duh, rational points not integer points
|
| Jul 18, 2019 at 9:56 | comment | added | Gareth McCaughan | Oooops! Will fix. Thanks. | |
| Jul 18, 2019 at 4:41 | comment | added | KConrad | 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". | |
| Jul 18, 2019 at 0:54 | comment | added | Mario Carneiro | @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. | |
| Jul 17, 2019 at 22:57 | comment | added | Kevin Buzzard | 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") | |
| Jul 17, 2019 at 22:55 | comment | added | Kevin Buzzard | @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. | |
| Jul 17, 2019 at 22:48 | comment | added | user36212 | 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..!) | |
| Jul 17, 2019 at 22:47 | comment | added | user36212 | @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 | |
| Jul 17, 2019 at 20:52 | comment | added | Michael Bächtold | @PeterLeFanuLumsdaine could you give a rough idea of the difference between a postulated and definable predicate, for the interested outsider? | |
| Jul 17, 2019 at 18:36 | comment | added | Peter LeFanu Lumsdaine | @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. | |
| Jul 17, 2019 at 18:25 | comment | added | Kevin Buzzard | 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. | |
| Jul 17, 2019 at 18:23 | comment | added | Kevin Buzzard | @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. | |
| Jul 17, 2019 at 18:20 | comment | added | Kevin Buzzard | 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". | |
| Jul 17, 2019 at 18:18 | vote | accept | Kevin Buzzard | ||
| Jul 17, 2019 at 14:22 | comment | added | Andrej Bauer | Really, Lean is not isomorphism invariant? | |
| Jul 17, 2019 at 11:59 | history | edited | Gareth McCaughan | CC BY-SA 4.0 |
added 2283 characters in body
|
| Jul 16, 2019 at 21:36 | comment | added | Kevin Buzzard | 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. | |
| Jul 16, 2019 at 16:20 | comment | added | Andrej Bauer | @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. | |
| Jul 16, 2019 at 16:15 | comment | added | Kevin Buzzard | @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. | |
| Jul 16, 2019 at 16:13 | comment | added | Kevin Buzzard | I absolutely agree with you. My localisation story can be summarised with the following meme: 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 leanprover.zulipchat.com/#narrow/stream/113488-general/topic/… contains comments by computer scientists making exactly Andrej's point. | |
| Jul 16, 2019 at 16:09 | comment | added | Gareth McCaughan | @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. | |
| Jul 16, 2019 at 16:07 | comment | added | Gareth McCaughan | 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. | |
| Jul 16, 2019 at 15:58 | comment | added | Andrej Bauer | 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. | |
| Jul 16, 2019 at 15:52 | comment | added | Kevin Buzzard | 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. | |
| Jul 16, 2019 at 15:24 | comment | added | Gareth McCaughan | 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! | |
| Jul 16, 2019 at 15:10 | comment | added | user21820 | 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! | |
| Jul 16, 2019 at 15:01 | comment | added | Gareth McCaughan | 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.) | |
| Jul 16, 2019 at 13:54 | comment | added | Gareth McCaughan | 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. | |
| Jul 16, 2019 at 13:52 | comment | added | Pierre-Yves Gaillard | 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? | |
| Jul 16, 2019 at 12:16 | history | answered | Gareth McCaughan | CC BY-SA 4.0 |