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

31–40 of 60 posts

Re: A proof of proof by infinite descent

#31

Post by bubblyworld »

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…

Yeah, I think you have to exclude 0 to push that proof through. Your relation is still well-ordered in that case so it's fine I think.

Re: A proof of proof by infinite descent

#34

Post by DevelopingElk »

pdonis wrote: post #25
gizmo686 wrote: post #24

Earlier quoted context omitted.

If there are no y less than x, then any statement about all y less than x is vacuously true.

> If there are no y less than x, then any statement about all y less than x is vacuously true. I suppose this is technically correct, but it doesn't seem like a good basis for doing induction.

I think it's fine. It's analogous to starting induction from 0 over the natural numbers.

It does feel a bit tricky though because there are two nested foralls instead of just one in standard induction. I think to derive it from standard induction you need to perform induction over sets of statements, which takes more power than first order logic. This additional power is generally accepted in math courses. It isn't necessary though, you can prove the irrationality of sqrt 2 using standard induction.

The article discussed how additional techniques can be made rigorous in the opening paragraph. I agree that the author didn't fully justify the assumptions in the proof system used, instead bringing this well ordered induction as an axiom. This is an article, I think a full aximization would have taken too long.

Re: A proof of proof by infinite descent

#36

Post by someplaceguy »

kevhito wrote: post #19
amenghra wrote: post #6

Earlier quoted context omitted.

Is it? You can tell the checker about the remainder of division by 2 to 6.

Maybe also need to show that there are no other naturals between 1 and 7? And also that numbers greater than 7 can't be a divisor of 7?

The first one can be trivially proved with automatic decision procedures and the second one is also very easy to prove, I believe.

Re: A proof of proof by infinite descent

#37

Post by immibis »

gizmo686 wrote: post #24
pdonis wrote: post #20

Earlier quoted context omitted.

> well-founded induction has an implicit base case of the empty set Yes, but that still means the reasoning that proves the induction has to be valid for the empty set--i.e., "if P is true for all y less than x, then P is true for x" has to be validly proven for the case that there are no y less than x--which of course is the case for the natural number 0 in ordinary mathematical induction.

If there are no y less than x, then any statement about all y less than x is vacuously true.

But the second half, "P is true for x", still has to be proven and is not vacuous.

Re: A proof of proof by infinite descent

#38

Post by immibis »

lupire wrote: post #22
kccqzy wrote: post #12

> a well-founded relation ⊏ is a well-ordering if and only if it relates every distinct pair of elements, i.e. x1≠x2 implies either x1⊏x2 or x2⊏x1. The author here explains well-founded relation prior to this. I want to add an example here. Consider the set of positive real numbers. If we use the natural ordering < then we have a total order. But that's not a well-ordering. If x were to be the least element you could…

Recall that the set R of real numbers R is defined as the set of numbers that can be shown to exist, plus an uncountable collection of "numbers" that are assumed to be near the set of numbers that can be shown to exist. It's not amazing that assuming something unnatural (Uncountable Choice) gives an equally unnatural consequence. The set R of "Real" numbers is a fantastical "object" that has fantastical properties. I…

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.

Re: A proof of proof by infinite descent

#39

Post by olivierduval »

ted_dunning wrote: post #21
olivierduval wrote: post #16

Earlier quoted context omitted.

I think that the reasoning is the same: * sqrt(-1) = a/b * a^2 = -1 * b^2 Then either a^2 or b^2 are negative but a square can't be negative, so contradiction and sqrt(-1) is not rational. The main "problem" with this proof (and the original with sqrt(2)) is "how to prove that a^2 >= 0" (or that "if a^2 is even, then a is even") The first one is easy to prove: * a^2 = sign(a)^2 * abs(a)^2 * abs(a) >= 0 for any a * si…

There are lots of missing bits here. For instance, you seem to assume that a = sign(a) * abs(a). Why? And both sign and abs are not defined. So you say abs(a) >= 0 and sign(a) \in {-1, 1}. Why? For instance, what is sign(0)? Are you assuming a construction of integers from the natural numbers such that for any n Later you assume that all integers are even or odd. Why? These are niggling details that don't matter when…

You're right that a lot that is "usually defined" in math has to be explicitly defined in theorem prover/proof assistant

* abs(x) is usually defined as "x if x >=0 and -x if x * sign(x) is usually defined as "1 if x >=0 and -1 if x * with these definitions, it follows that for any x, x = sign(x) * abs(x) (by definition applied for each cases >=0 and =0 or Showing that any integer is either even or odd seem less obvious

Re: A proof of proof by infinite descent

#40

Post by bruce343434 »

__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.
Post reply on HN