Re: Cum Hoc, Ergo Propter Hoc

From: Jesse F. Hughes (jesse_at_phiwumbda.org)
Date: 08/30/04 

Date: Mon, 30 Aug 2004 09:31:02 +0200

jstevh@msn.com (James Harris) writes:

> Hmmm...I can't seem to remember offhand the proof that sqrt(2) is not
> rational, so I'll just figure something out, which I think is kind of
> how it goes.
>
> Let b/a = sqrt(2), and assume that 'b' and 'a' are coprime naturals.
>
> Then b = sqrt(2) a, and squaring both sides gives
>
> b^2 = 2a^2
>
> which means that 'b' must be even by the assumption that it is a
> natural, as all naturals are either even or odd, but no square has
> only 2 as a factor; therefore 'a' must also be even, but that
> contradicts with 'b' being coprime to 'a' therefore, b/a is not
> rational.
>
> Now then, how do you null test?
>
> Assume that b/a is rational, but that was done to make the proof as
> it's a proof by contradiction.
>
> Null test passed with a contradiction with the last logical step
> before the conclusion.

I realize that I wasn't specific enough. Your answer is too hard to
understand as stated. Let's be a touch more formal.

Below, I've included a partially formalized proof that sqrt(2) is
irrational. I give the rules of inference as well, with the following
abbreviations.

Theorem -- A theorem quoted
UE -- Universal elimination
EE -- Existential elimination
&E -- Conjunction elimination
&I -- Conjunction introduction
EI -- Existential introduction
Defn -- A definitional replacement
Subst -- Substitution
alg -- Algebraic manipulations
(***) -- Skipping a few steps
NOT I -- "Not" introduction, i.e. proof by contradiction

I use (***) to go from a step in which I've proved that some value x
is greater than or equal to 2 to conclude x is not equal to 1. I'll
expand that step if desired.

Here's the proof, sorry for the overly long line.

1. sqrt(2) in Q Assumption

,----
| 2. (A x)(x in Q -> (E a,b)( a in Z & b in Z & x = a/b & gcd(a,b) = 1 )) Theorem
| 3. sqrt(2) in Q -> (E a,b)( a in Z & b in Z & sqrt(2) = a/b & gcd(a,b) = 1 ) UE
| 4. (E a,b)( a in Z & b in Z & sqrt(2) = a/b & gcd(a,b) = 1 ) MP
| 5. a in Z & b in Z & sqrt(2) = a/b & gcd(a,b) = 1 EE
| 6. sqrt(2) = a/b &E
| 7. 2 = a^2 / b^2 alg
| 8. 2 b^2 = a^2 alg
| 9. (E k)( 2 k = a^2) EI
| 10. 2 | a^2 Defn
| 11. (A c)(( c in Z & 2 | c^2) -> 2 | c) Theorem
| 12. ( a in Z & 2 | a^2 ) -> 2 | a UE
| 13. a in Z &E
| 14. a in Z & 2 | a^2 &I
| 15. 2 | a MP
| 16. (E k)( k in Z & 2 k = a ) Defn
| 17. k in Z & 2 k = a EE
| 18. 2 k = a &E
| 19. 2 b^2 = (2 k)^2 Subst
| 20. 2 b^2 = 4 k^2 alg
| 21. b^2 = 2 k^2 alg
| 22. (E l)( 2 l = b^2 ) EI
| 23. 2 | b^2 Defn
| 24. ( b in Z & 2 | b^2 ) -> 2 | b UE
| 25. b in Z &E
| 26. b in Z & 2 | b^2 &I
| 27. 2 | b MP
| 28. 2 | b & 2 | a &I
| 29. gcd(a,b) >= 2 Defn
| 30. gcd(a,b) != 1 (***)
| 31. gcd(a,b) = 1 &E
`----

32. NOT (sqrt(2) in Q) NOT I

Now *which* step is your so-called keystone step? What do you mean
"assume sqrt(2) is rational and look for the step it contradicts"?
Contradicts in what sense? Why the step *you* choose and not any
other step?

If you say that one of the theorem steps is the keystone step, then I
will insert their respective proofs and ask the question again. If
you say that it's the (***) step, I will do the same. It surely
cannot be a Defn step.

So, I ask you to please answer the question again, now that the answer
will be a bit more specific and harder to misunderstand. I have taken
the time to formalize the proof, so I ask that you take just a smidgen
of time to answer again. 

-- 
"Now I realize that he got away with all of that because sci.math is
not important, and the rest of the world doesn't pay attention.
Like, no one is worried about football players reading sci.math
postings!" -- James S. Harris on jock reading habits

Relevant Pages

  • Re: Predominant philosophy of mathematics today
    ... there is an actual derivable contradiction from it's axioms. ... is a derivation of a contradiction in Robinson arithmetic" is of course ... proof machinery is very minimal: like "finite", negation of a meta statement, ... possibly formalize. ...
    (sci.logic)
  • Re: Review of Mueckenheims book.
    ... relevant to the question of how best to formalize the informal concept. ... Not only needlessly complicate, but needlessly CONTRADICT. ... CONTRADICTION to define it that way since ALREADY, in those contexts, ... Because, as YOU JUST RECOGNIZED, in set theory, it would "needlessly ...
    (sci.math)
  • Re: Amateur takes on Wiless work
    ... > jstevh@msn.com (James Harris) writes: ... Assume in contradiction to the conclusion that ... logical statement leading up to the conclusion? ... Surprise. ...
    (sci.math)
  • Re: JSH: Curious, Wiless work, null test
    ... > jstevh@msn.com (James Harris) writes: ... >> that assumption leads to a contradiction. ... Since my first example involved an indirect ... > We'll also take the axiom scheme of induction as given, ...
    (sci.math)
  • Re: Null test, Wiless work
    ... jstevh@msn.com (James Harris) writes: ... > where you get a contradiction. ... What does invalidate mean? ... Mother Mathematics is a harlot! ...
    (sci.math)