Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Fermat's Last Theorem – how it’s going

xenaproject.wordpress.com

Post reply on HN
Print view View original

171–180 of 216 posts

Re: Fermat's Last Theorem – how it’s going

#171

Post by Tainnor »

gedpeck wrote: post #164
semolinapudding wrote: post #150

Earlier quoted context omitted.

If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the second-order induction axiom (in your first mathoverflow link, this is called Z_2): https://en.wikipedia.org/wiki/Second-order_arithmetic#The_fu... An other equivalent option would be to use the language…

You know more than me on logic so I defer to your expertise. https://math.stackexchange.com/questions/4753432/g%C3%B6dels... Andreas Blass in the comments says that the Incompleteness results don’t apply to the second order Axioms (tabling about PA_2 here and not Z_2) and that the second order axioms are not computably enumerable. Maybe that’s the correct concept I was remembering from mathematical logic class. Don’t…

> and that the second order axioms are not computably enumerable

He says that true sentences in second order logic aren't computably enumerable, he's not talking about the axioms.

> Don’t know if computably enumerable is the same as recursively enumerable

I've only ever seen them used as synonyms.

> Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.

What you call "Super PA" is called "the theory of PA". Its axioms are indeed not computably enumerable. That doesn't mean that the axioms of PA themselves aren't computably enumerable. And this much is true both for first and second order logic.

(edit: in fact, the set of Peano axioms isn't just computably enumerable, it's decidable - otherwise, it would be impossible to decide whether a proof is valid. This is at least true for FOL, but I do think it's also valid for SOL)

Re: Fermat's Last Theorem – how it’s going

#172

Post by bell-cot »

gjm11 wrote: post #137
bell-cot wrote: post #73

Earlier quoted context omitted.

Yep. Here's an easy-looking one, that lasted just under 2 centuries (quoting Wikipedia) - > In number theory, Euler's conjecture is a disproved conjecture related to Fermat's Last Theorem. It was proposed by Leonhard Euler in 1769. It states that for all integers n and k greater than 1, if the sum of n many kth powers of positive integers is itself a kth power, then n is greater than or equal to k... > ... > Euler's…

What exactly are you saying this is an example of? It's certainly not something that people believed and built stuff on the basis of; it was never regarded as anything more than a conjecture and I would be a little surprised if even one paper was published that took the conjecture as a hypothesis, even explicitly (i.e., "We show that if Euler's conjecture is true then ..."). It's also not, so far as I know, a case wh…

> What exactly are you saying this is an example of?

A prominent conjecture in number theory, taken quite seriously for centuries, but which was quickly and rather easily disproven once computers became powerful enough.

No, it is not a exact analogy for Fermat, nor BSD, nor Riemann, nor ...

My initial point of interest was u/bootby's comment - why the heck would a room full of experts (presumably noteworthy math professors) become so angry at some grad student's comment? Then /usr/baruz's comment, about things which "seem proven and make intuitive sense, but needed formal buttressing". On occasion, "seemed" and "intuition" prove to be wrong, and Euler was a pretty-good example that.

Re: Fermat's Last Theorem – how it’s going

#173

Post by saberience »

impendia wrote: post #48
vouaobrasil wrote: post #24

> The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to…

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone w…

log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) I don't get why this is true. If C is 1 and x is 2

log(x^2+1) sqrt(2) + x/exp(sqrt(4*2 + 3)) is not less than 2.

Re: Fermat's Last Theorem – how it’s going

#174

Post by Tainnor »

gedpeck wrote: post #170
Tainnor wrote: post #168

Earlier quoted context omitted.

> Take the collection of all true statements and make that your axiomatic system. A complete proof system needs to be able to derive Γ |- φ for every pair Γ, φ such that Γ |= φ. Not just when Γ is the complete theory of some structure. Completeness of first-order logic (and its failure for second-order logic) is about the logical system itself, while the incompleteness theorems are about specific theories - people of…

You know more than me. That is certain. However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this. If I take the standard model of ZFC and collect all true statements in the one model of PA_2 and make that my axiomatic system then I have an axiomatic system that is not recursively enumerable and contains PA_1. It’s not a nice se…

> However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this.

That's a matter of semantics as to what you consider the first incompleteness theorem to be precisely (of which there are several variants). Gödel's proof itself doesn't directly work for second-order logic. But the statement "if Γ is some axiomatic system that satisfies certain conditions, then for any sound proof calculus there is a sentence that isn't provable from Γ in this calculus" is true in second order logic too, it's just that the "failure" happens much "earlier" (and is in some sense obvious) than in the case of FOL.

> PA_2 is not such a system and as such the Incompleteness Theorems don’t apply.

I'm really not all that familiar with second-order PA, but it is my understanding that the set of its axioms is decidable. It consists of a finite collection of axioms plus one schema (comprehension axiom) which is valid when it's instantiated by any given sentence - but deciding whether something is a valid sentence is easy. Therefore, what you quoted applies to second-order PA too.

Re: Fermat's Last Theorem – how it’s going

#175

Post by imprime »

impendia wrote: post #48
vouaobrasil wrote: post #24

> The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to…

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone w…

To prove that you divide both sides by x and take the limit for x -> inf, applying L'Hopital rule the limit is zero, so there is such a C, any number greater than zero. The existence of such X is just the definition of limit when x tends to inf.

Another way, just using a cas (like maxima) to compute such limit: (%i1) limit( (log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4*x + 3)))/x,x,inf); the result is zero.

Re: Fermat's Last Theorem – how it’s going

#176

Post by semolinapudding »

gedpeck wrote: post #164
semolinapudding wrote: post #150

Earlier quoted context omitted.

If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the second-order induction axiom (in your first mathoverflow link, this is called Z_2): https://en.wikipedia.org/wiki/Second-order_arithmetic#The_fu... An other equivalent option would be to use the language…

You know more than me on logic so I defer to your expertise. https://math.stackexchange.com/questions/4753432/g%C3%B6dels... Andreas Blass in the comments says that the Incompleteness results don’t apply to the second order Axioms (tabling about PA_2 here and not Z_2) and that the second order axioms are not computably enumerable. Maybe that’s the correct concept I was remembering from mathematical logic class. Don’t…

There's a bit of a definition issue at play here. When Andreas Blass and Noah Schweber say that there is no proof system for PA_2, they mean that there is no effective proof system that is complete for the full semantics. If you subscribe to their definition of a proof system, you end up saying that there is no such thing as a proof in PA_2, and thus that incompleteness is meaningless -- which I personally find a bit silly.

On the other hand, proof theorists and computer scientists are perfectly happy to use proof systems for second order logic which are not complete. In that case, there are many effective proof systems, and given that the axioms of PA_2 are recursively enumerable (they are in finite number!), Gödel's incompleteness will apply.

If you are still not convinced, I encourage you to decide on a formal definition of what you call PA_2, and what you call a proof in that system. If your proof system is effective, and your axioms are recursively enumerable, then the incompleteness theorem will apply.

Re: Fermat's Last Theorem – how it’s going

#177

Post by naasking »

gedpeck wrote: post #166
naasking wrote: post #163

Earlier quoted context omitted.

> There are non-computable objects that mathematicians study. What's an example of such a non-computable object? Constructionism is based on the fact that every proof is a construction, which corresponds to a program, so you're claiming that there are proofs that do not correspond to any construction/program, and I'm curious what that might look like.

The set of statements about natural numbers that are true.

Using the law of the excluded middle is definitely a shortcut in such proofs, but there is no proof I'm aware of that shows no comparable constructive proof is possible. We reason with non-computable objects all of the time, such constructions are simply never fully materialized, and the need to materialize them are typically eliminated in later stages to prove concrete results. It's a good example but I don't think it's sufficient to exclude math from computer science.

Re: Fermat's Last Theorem – how it’s going

#178

Post by jsvlrtmred »

saberience wrote: post #173
impendia wrote: post #48

Earlier quoted context omitted.

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone w…

log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) I don't get why this is true. If C is 1 and x is 2 log(x^2+1) sqrt(2) + x/exp(sqrt(4*2 + 3)) is not less than 2.

The statement wasn't that it's true in general - only that there existing constants C and X>0 for which it is true for all x>X.

Re: Fermat's Last Theorem – how it’s going

#179

Post by rateofclimb »

williamstein wrote: post #82
rateofclimb wrote: post #72

Earlier quoted context omitted.

As a CS undergrad at Berkeley in the 90's I took an upper division math class in which we worked through the "old school" proof which was brand new and exciting then. Pretty much everyone else in the class was a math grad student. I don't think I understood more than 20% of the material! :)

I took that class with you! It was amazing. Here are my notes: https://wstein.org/books/ribet-stein/

Thanks for sharing that! Very cool.

Re: Fermat's Last Theorem – how it’s going

#180

Post by paulddraper »

vouaobrasil wrote: post #24

> The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to…

Has that ever blown up their faces?

I.e. a widely accepted proof that had a critical flaw due to hand waving?

If it hasn't, I would understand why they'd be cavalier about explicit details.

Post reply on HN