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

A proof of proof by infinite descent

relatedwork.blogspot.com

Post reply on HN
Print view View original

51–60 of 60 posts

Re: A proof of proof by infinite descent

#51

Post by lupire »

someplaceguy wrote: post #29

I think I'm missing something... isn't there an error in the proof when applying the theorem of the principle of infinite descent? The theorem requires proving the following premise/antecedent (to deduce the consequent): ∀x ∈ X. Φ(x) ⟹ ∃y ∈ X. y ⊏ x ∧ (...) ... but I don't see how this can be proved when x=0. By substituting `x` for `0` (and using Z as the set X and | Φ(0) ⟹ ∃y ∈ Z. y | Unfolding Φ: (∃b ∈ Z. 0^2 = 2…

It's not wrong, but it skips some detail. (It's ironic that an article about "insight via precision" uses such imprecise language.)

This is demonstrated in a Lean tutorial for induction, where first it has you "prove" that √2 is "rational", before adding the requirement that the denominator is not 0, which then of course requires a totally different (semantically valid) proof.

0 does satisfy the theorem on integers, but it doesn't say anything about √2, because rational numbers do not allow a 0 denominator.

The √2 theorem assumes b >= 1, and infinite descent / well-foundedness is based on this subset of Z (and to the author's pedantic point about ordering, also works with Z\{0} and the magnitude ordering on |z|.)

Re: A proof of proof by infinite descent

#52

Post by someplaceguy »

lupire wrote: post #51
someplaceguy wrote: post #29

I think I'm missing something... isn't there an error in the proof when applying the theorem of the principle of infinite descent? The theorem requires proving the following premise/antecedent (to deduce the consequent): ∀x ∈ X. Φ(x) ⟹ ∃y ∈ X. y ⊏ x ∧ (...) ... but I don't see how this can be proved when x=0. By substituting `x` for `0` (and using Z as the set X and | Φ(0) ⟹ ∃y ∈ Z. y | Unfolding Φ: (∃b ∈ Z. 0^2 = 2…

It's not wrong, but it skips some detail. (It's ironic that an article about "insight via precision" uses such imprecise language.) This is demonstrated in a Lean tutorial for induction, where first it has you "prove" that √2 is "rational", before adding the requirement that the denominator is not 0, which then of course requires a totally different (semantically valid) proof. 0 does satisfy the theorem on integers,…

I would argue that technically, the proof has an error because the author says:

> Let X be the integers Z; for integers a,b, let `a ⊏ b` be `a|However, the theorem of infinite descent cannot be applied to this property with the set Z which the author specifically said he would use. Instead, it needs to be applied to the set Z\{0}, which you rightly pointed out (as well as the sibling poster).

Note that this has nothing to do with the rest of the proof about √2.

I do agree that even after this error is corrected, then the proof additionally needs to be fixed by adding a few more simple proof steps to analyze what happens when either `a` or `b` are zero, which was excluded from the set. At this point you'd probably realize that yes, there is an implicit assumption that ¬(b = 0) which should be made explicit, and then you also have to account for the `a = 0` case, which should also be easy.

But still, the error greatly confused me at first because it seemed like the theorem could not be applied in this case. I only realized the theorem could be used correctly in this case when the sibling poster suggested to use a different set.

Re: A proof of proof by infinite descent

#53

Post by [deleted] »

mathgradthrow wrote: post #5
lisper wrote: post #3

Earlier quoted context omitted.

You'd be surprised at the number of things that appear to be self-evidently true that turn out to depend on tacit assumptions. For example, is 7 prime? Not if you're doing modular arithmetic.

It's also independently pretty tedious to explain that 7 is prime to a proof checker.

[deleted]

Re: A proof of proof by infinite descent

#54

Post by mathgradthrow »

mathgradthrow wrote: post #27
drhodes wrote: post #10

Earlier quoted context omitted.

The proof is not too bad in Lean4. I'm nothing special and I've got it down to 9 lines. But, maybe that is considered pretty tedious vs. what expectations one might have. In any case, it is an exercise in Heather MacBeth's free book: The Mechanics of Proof, https://hrmacbeth.github.io/math2001/04_Proofs_with_Structur... btw, that book is a lot of fun to work through.

The obvious proof term for isprime p is exponential compared to the size of p. The AKS proof term is polynomial, but still very bad.

https://en.m.wikipedia.org/wiki/Primality_certificate

Re: A proof of proof by infinite descent

#55

Post by IsTom »

lupire wrote: post #48
IsTom wrote: post #44

In the step of √2 = a/b you can get away without asking for relatively prime, using GCD or this descent by asking for least a for which this holds. Then when you get a/b = 2c/2d = c/d, but c would be less than a, hence contradiction. Couldn't you always do this instead of doing this infinite descent? If relation is well-founded then there will be a least element.

What do you mean? Proof by contradiction with well-foundedness is exactly what "infinite descent" means.

I guess I got a little confused, because a different form with some de-morganing and contraposed implications feels more natural to me in plain-language proofs.

Re: A proof of proof by infinite descent

#56

Post by kccqzy »

lupire wrote: post #47
immibis wrote: post #38

Earlier quoted context omitted.

IIRC the real numbers are, roughly speaking, more-or-less isomorphic to infinite sequences of digits. If you believe real numbers are fantastical, I suppose you also believe infinite sequences are fantastical? We can't have one in the universe, because we'd run out of atoms, but we can't have circles either and that is rarely complained about.

An infinite computable sequence is fine. Making "choices" from an uncountable collection of uncomputable sequences is not fine. I'm embarrassed to have to write that out.

Historically the definition of computability came quite a bit later than ZFC. Zermelo might have formulated his set theory differently if computability came first.

Re: A proof of proof by infinite descent

#58

Post by BalinKing »

lupire wrote: post #50
BalinKing wrote: post #26

Earlier quoted context omitted.

I doubt you'd be able to prove that it's rational, regardless of how it's constructed, since wouldn't that imply that it's also (for example) a real number?

That's the point. When you use ambiguous definitions, you get stuck in a morass.

Still, I don't see how any such definition could even be called a "definition of √-1" in the first place, since the resulting object wouldn't actually have the properties of √-1.

Re: A proof of proof by infinite descent

#59

Post by taneq »

lohfu wrote: post #4
lisper wrote: post #3

Earlier quoted context omitted.

You'd be surprised at the number of things that appear to be self-evidently true that turn out to depend on tacit assumptions. For example, is 7 prime? Not if you're doing modular arithmetic.

i think they were joking, but i can't prove it

Unfortunately the margin is too small to contain it.

Re: A proof of proof by infinite descent

#60

Post by __rito__ »

bruce343434 wrote: post #40
__rito__ wrote: post #33

What is the best way to write LaTeX in Blogspot sites, like the author has here?

How do you evaluate "best"? FWIW this blog uses mathjax, I believe that's a pretty conventional approach, but the latex is rendered on the browser side leading to lots of reflows. There's also mathjax-node to pre-render the latex on the server side, and serve ready made html+css.

By best, I mean, most hassle-free for the writer.
Post reply on HN