Timeline for Don't the axioms of set theory implicitly assume numbers?
Current License: CC BY-SA 2.5
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 8, 2022 at 13:26 | comment | added | Todd Trimble | @MartinSleziak Yes, that was the one. Maybe some day I'll get back to it (although I think the nLab has disabled some of the personal pages). | |
| Aug 7, 2022 at 8:44 | comment | added | Martin Sleziak | I was wondering whether this is the article mentioned in the post (which was a draft at the time): Todd Trimble: Notes on predicate logic. (Maybe it would be worth including a link into the answer? Although I know that some MO users are not too keen on bumping old questions.) | |
| Oct 7, 2017 at 17:07 | comment | added | user21820 | @LSpice: I think I understood your point. My point above was that you are going to have a tough time explaining how billions of people and probably trillions of HTTPS connections per year are made and none of them seem to fail inexplicably. If you understand HTTPS, you would know that successful connections require Fermat's little theorem to work for a particular instance unique to each webpage, and failure would mean that you can't decrypt, not to say read the webpage. This is empirical verification far better than almost all scientific theories, so you shouldn't bring up "falsifiable". | |
| Oct 7, 2017 at 17:01 | comment | added | LSpice | @user21820, I am not claiming that theorems have no real-world consequences, only that I am not prepared to judge the theorems' meanings by those real-world consequences—especially if they are tied to highly fallible things like a specific piece of software. (I would be equally sceptical if the mathematical meaning of a theorem were to be judged completely by one person's proof of it.) I don't even know what it means to say that a piece of software would work if it had no bugs, and that that verifies the mathematics; that seems too circular an argument to be falsifiable. | |
| Oct 7, 2017 at 10:23 | comment | added | user21820 | @LSpice: Incidentally, the fact that you can read MathOverflow pages is something that you'll not be able to explain without agreeing that Fermat's little theorem (which is provable in PA) has real-world meaning in much the same manner as I claimed for Fermat's last theorem, at least for numbers up to $2^{2048}$. Don't forget that HTTPS was designed based on Fermat's little theorem, after it was proven by mathematicians, and would not have been discovered otherwise. So there is indeed some abstract nature of programs that PA captures at small scales. | |
| Oct 7, 2017 at 10:14 | comment | added | user21820 | @LSpice: I also wish to address your last point, which is that it is simply irrelevant. Any compiler that does not implement Python 3, exactly as it was designed, is by definition not a compiler of Python 3. It should have been clear that I made a claim about real Python-3 compilers, not fakes. Just saying that compilers can have bugs in them is actually an evasion of the real issue, just as I can equally say that your browser's implementation of HTTPS could have bugs in it. But see, HTTPS would work if there are no bugs, and that fact verifies the mathematics behind it. | |
| Oct 7, 2017 at 4:36 | comment | added | user21820 | @LSpice: Yes Python 3 supports big integers natively. Anyway if you know computability theory you will know that that's clearly not the point; we all assume the existence and basic properties of finite binary strings precisely because we have some real-world notion of them. If we did not in the first place have finite binary strings in any physical media, we would not even have come up with axioms stating their properties (nor the axioms of PA−, which are interpretable in TC). See also this for more related points. | |
| Oct 6, 2017 at 17:22 | comment | added | LSpice |
@user21820, I don't know enough about Python 3 to know whether the most trivial objection to that meaning is valid: does Python support bigints natively? Even if this trivial objection isn't satisfied, I'm not sure that I want the meaning of Fermat's theorem to be tied to a particular piece of software, necessarily (not anything to do with Python, just with software) with its own bugs. If it comes down to that, what if I compile Python with a version of Ken Thompson's compiler designed specifically to make Python programs report true when they detect attempts to probe FLT?
|
|
| Feb 25, 2017 at 7:00 | comment | added | user21820 |
@FanZheng: That's an easy question to answer! It means that there are no four decimal integer strings $x,y,z,n$ such that the Python-3 program n>2 and x**n+y**n==z**n returns true.
|
|
| Oct 15, 2016 at 1:35 | comment | added | Fan Zheng | Regarding meaning in the real world, that is not the requirement of theorems: what is the meaning of Fermat's last theorem? | |
| Dec 29, 2015 at 7:09 | comment | added | user21820 | @Deniz: An alternative would be to claim that our mathematical notion of $\mathbb{N}$ is merely an approximation to some manifestation in the real world, but we then have to admit that our formal systems are not necessarily embeddable in the real world, which means that either we accept that many theorems are simply meaningless or wrong in the real world, or we resign mathematics to being a symbol-pushing game. Note that if you claim that the natural numbers actually embed into the universe, then as in my first comment we are assuming even more than Con(PA), essentially. | |
| Dec 29, 2015 at 7:02 | comment | added | user21820 | @Deniz: Worse still, if the universe has finitely many particles, then no such physical procedure for checking proofs over first-order logic can even exist! The conventional response is that we are talking about an ideal computer, such as a Turing machine, but that is self-defeating because any idealization can only be done in yet another logic system, and precisely because it is once again estranged from the real world, the same reliance on the abstract notion of natural numbers and their properties is an obviously unjustifiable one. | |
| Dec 29, 2015 at 6:56 | comment | added | user21820 | @Deniz: I do not agree with Todd's proposed escape from circularity. His proposal implicitly assumes that there is a purely deterministic procedures to check a proof encoded as a string and stored in some physical medium. That is in fact assuming more than the consistency of PA. How do you know that the computer actually does what is claimed? You don't, unless you assume that the computer is in a world governed by some underlying system that already contains a manifestation of the natural numbers. | |
| Apr 1, 2014 at 7:13 | comment | added | Deniz | Is it complete now? | |
| Nov 27, 2010 at 21:46 | vote | accept | Deniz | ||
| Nov 27, 2010 at 21:46 | |||||
| Nov 26, 2010 at 14:50 | comment | added | Urs Schreiber | Am very glad that you are working on writing this up. | |
| Nov 26, 2010 at 14:13 | history | answered | Todd Trimble | CC BY-SA 2.5 |