A proof of proof by infinite descent
relatedwork.blogspot.com
relatedwork.blogspot.com
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 the firsts place". But that's actually fine, because the principle of well-founded induction lets you assume it out of thin air, and as long as it implies ¬Φ(x), you're good.
The intuition of this, to me at least, is that well-founded induction has an implicit base case of the empty set. (∀y∈X.y⊏x⟹Ψ(y))⟹Ψ(x) means Ψ(x) is required to be automatically true if ∄y∈X, so (∀y∈X.y⊏x⟹Ψ(y)) may be assumed out of thin air and then used inductively for all the cases where ∃y∈X.
Back to the specific example, ¬Φ(x) is automatically true if ∄y∈X because Φ(x) implies ∃y∈X. However note that this base case doesn't need to be explicitly shown, because it's included in the general case.
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.
I suppose this is technically correct, but it doesn't seem like a good basis for doing induction.
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.
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 always divide it by 2 to get a lesser element. So there's no least element in the set of positive reals using the conventional < ordering. However, the amazing thing is that assuming axiom of choice, such a well ordering exists.
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.
Making "choices" from an uncountable collection of uncomputable sequences is not fine.
I'm embarrassed to have to write that out.
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?
(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)
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.
I feel like this was a marvellous joke but I can’t prove it.
* 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
* sign(a) = 1 or -1 for any a so sign(a)^2 = 1 (either 1*1 or -1*-1)
* so a^2 >= 0
The second one may be proved:
* Assume a is even, then a=2n, then a^2=4n^2=2*(2n^2) so a is even => a^2 is even
* Assume a is odd, then a=2n+1, then a^2=4n^2+4n+1=2*(2n^2+2n)+1, then a^2 is odd
* a is either even or odd
* So the only possibility for a^2 to be even is for a to be even
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 < 0, there is an integer abs(n) and n = -1 * abs(n)? If so, don't you need to include that (or at least reference it)?
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.
* abs(x) is usually defined as "x if x >=0 and -x if x < 0"
* sign(x) is usually defined as "1 if x >=0 and -1 if x < 0"
* with these definitions, it follows that for any x, x = sign(x) * abs(x) (by definition applied for each cases >=0 and <0, assuming that all integer are either >=0 or <0)
Showing that any integer is either even or odd seem less obvious
https://hrmacbeth.github.io/math2001/04_Proofs_with_Structur...
btw, that book is a lot of fun to work through.
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...
The theorem requires proving the following premise/antecedent (to deduce the consequent):
∀x ∈ X. Φ(x) ⟹ ∃y ∈ X. y ⊏ x ∧ (...)
Φ(0) ⟹ ∃y ∈ Z. y |<| 0
(∃b ∈ Z. 0^2 = 2 b^2) ⟹ ∃y ∈ Z. y |<| 0
∃y ∈ Z. y |<| 0
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)
∀x ∀y ∈ Z. ¬(x^2 = 2 y^2)
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|.)
> Let X be the integers Z; for integers a,b, let `a ⊏ b` be `a|<|b`; and let the property Φ(a) be “a^2=2 b^2 for some integer b” (formally, `∃b ∈ Z. a^2=2 b^2`).
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.
Couldn't you always do this instead of doing this infinite descent? If relation is well-founded then there will be a least element.