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

41–50 of 60 posts

Re: A proof of proof by infinite descent

#41

Post by bubblyworld »

agalunar wrote: post #28

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 d…

Not my area at all, but surely you would just add the relevant induction schema as an axiom? Are nonstandard models relevant to proof assistants?

(to be clear - I know what nonstandard models are and how they work, and I've mucked around in coq/lean, just wondering why it matters to a proof assistant)

Re: A proof of proof by infinite descent

#42

Post by agalunar »

bubblyworld wrote: post #41
agalunar wrote: post #28

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 d…

Not my area at all, but surely you would just add the relevant induction schema as an axiom? Are nonstandard models relevant to proof assistants? (to be clear - I know what nonstandard models are and how they work, and I've mucked around in coq/lean, just wondering why it matters to a proof assistant)

My line of thinking roughly was, "each type system corresponds to a particular logic system and vice versa; in a proof by induction, the different cases correspond to the type constructors, but what does the necessary axiom schema or second-order axiom of induction correspond to? (in order to avoid the problem of nonstandard elements). And proof by infinite descent seems to require something other than induction, so where does well-foundedness come from?"

I realize these questions may not even be posed sensibly; maybe the answer is as simple as, "the naturals are defined constructively here; of course they are the naturals and therefore are well-founded". As I said, it's been a while, so things are hazy in my mind.

Re: A proof of proof by infinite descent

#43

Post by [deleted] »

martin293 wrote: post #30
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?

[deleted]

Re: A proof of proof by infinite descent

#44

Post by IsTom »

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.

Re: A proof of proof by infinite descent

#45

Post by kccqzy »

martin293 wrote: post #30
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?

The existence proof uses the axiom of choice so it's not a constructive proof. You cannot deduce how it's constructed from its existence.

Re: A proof of proof by infinite descent

#46

Post by bubblyworld »

agalunar wrote: post #42
bubblyworld wrote: post #41

Earlier quoted context omitted.

Not my area at all, but surely you would just add the relevant induction schema as an axiom? Are nonstandard models relevant to proof assistants? (to be clear - I know what nonstandard models are and how they work, and I've mucked around in coq/lean, just wondering why it matters to a proof assistant)

My line of thinking roughly was, "each type system corresponds to a particular logic system and vice versa; in a proof by induction, the different cases correspond to the type constructors, but what does the necessary axiom schema or second-order axiom of induction correspond to? (in order to avoid the problem of nonstandard elements). And proof by infinite descent seems to require something other than induction, so…

I see, that's interesting. You inspired me to go read up about CIC, it's really cool, thanks! And in hindsight I realise my reply was totally wrong anyway haha.

Re: A proof of proof by infinite descent

#47

Post by lupire »

immibis wrote: post #38
lupire wrote: post #22

Earlier quoted context omitted.

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.

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.

Re: A proof of proof by infinite descent

#48

Post by lupire »

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.

Re: A proof of proof by infinite descent

#50

Post by lupire »

BalinKing wrote: post #26
gerdesj wrote: post #17

Earlier quoted context omitted.

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?

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