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

21–30 of 60 posts

Re: A proof of proof by infinite descent

#21

Post by ted_dunning »

olivierduval wrote: post #16
taneq wrote: post #2

> I imagine that one could also prove that √−1 is not rational I feel like this was a marvellous joke but I can’t prove it.

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 have chalk in hand, but do matter when speaking to a system like lean4.

Re: A proof of proof by infinite descent

#22

Post by lupire »

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. It can do apparently impossible things because ZFC flat out assumes that it can do apparently impossible things.

Re: A proof of proof by infinite descent

#23

Post by [deleted] »

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…

[deleted]

Re: A proof of proof by infinite descent

#24

Post by gizmo686 »

pdonis wrote: post #20
GrantMoyer wrote: post #11

I like that the article uses the concrete example of proving √2 is not rational to demonstrate the abstract priciples of induction, while also not hand-waving away the formal details of the general case. I got a little caught up on on the proof of (no) infinite descent by well-founded induction without a base case. I thought, "something is wrong; (∀y∈X.y⊏x⟹¬Φ(y)) only implies ¬Φ(x) if you assume (∀y∈X.y⊏x⟹¬Φ(y)) in t…

> 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.

Re: A proof of proof by infinite descent

#25

Post by pdonis »

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.

> 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.

Re: A proof of proof by infinite descent

#26

Post by BalinKing »

gerdesj wrote: post #17
taneq wrote: post #2

> I imagine that one could also prove that √−1 is not rational I feel like this was a marvellous joke but I can’t prove it.

Taking the square root of -1 is not only an irrational thing to do but bloody daft. QED 8) i tends to pop out as a construction so I suspect you can probably prove it is both rational and irrational or neither, depending on the fine print. Here's a discussion: https://math.stackexchange.com/questions/823970/is-i-irratio...

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?

Re: A proof of proof by infinite descent

#27

Post by mathgradthrow »

drhodes wrote: post #10
mathgradthrow wrote: post #5

Earlier quoted context omitted.

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

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.

Re: A proof of proof by infinite descent

#28

Post by agalunar »

How does infinite descent work using a proof assistant? It's been quite a while, so I may be remembering incorrectly, but this is my understanding:

Coq uses an inductive type like "N = 0 : N | S : N → N", and a first-order theory with integers axiomatized this way admits nonstandard models (whose prefixes are isomorphic to the naturals but have elements not reachable by repeated application of S, defeating infinite descent). But universal quantification in system F (inherited by the calculus of inductive constructions) corresponds to a fragment of second-order logic, where there is only one model (– the theory is categorical).

Is that right?

Re: A proof of proof by infinite descent

#29

Post by someplaceguy »

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 b^2) ⟹ ∃y ∈ Z. y |
The antecedent of this implication is true (when b = 0), so now you have to prove:

  ∃y ∈ Z. y |
However, this can't be proved because no `y` satisfies the |Therefore, this article's sentence doesn't seem to be true:

> Having satisfied the premises of the principle, we use it to deduce that no `a` satisfies the property

... which in fact cannot be true, because `a=0` does satisfy the property `∃b ∈ Z. a^2 = 2 b^2`, does it not? Consider `b=0`.

So what am I missing?

Edit: in fact, if the theorem could be applied in this case, then the conclusion of the theorem would be:

  ∀x ∈ Z. ¬(∃b ∈ Z. x^2 = 2 b^2)
Which is equivalent to:

  ∀x ∀y ∈ Z. ¬(x^2 = 2 y^2)
... which is clearly false when x=0 and y=0. So it seems like the theorem of infinite descent cannot be used to reach this conclusion. Some kind of false assumption would have to exist, but no false assumption was used to instantiate this theorem.

Re: A proof of proof by infinite descent

#30

Post by martin293 »

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…

Well how is it constructed?
Post reply on HN