4 ms·

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

by taneq 2y ago

lisper 2y ago
You'd be surprised at the number of things that appear to be self-evidently true that turn out to depend on tacit assumptions. For example, is 7 prime? Not if you're doing modular arithmetic.
- sebzim4500 2y ago
  It's a joke about `i` being imaginary.
  - fat_cantor 2y ago
    yes the joke is on i
- lohfu 2y ago
  i think they were joking, but i can't prove it
  - lisper 2y ago
    Maybe -i can.
  - taneq 2y ago
    Unfortunately the margin is too small to contain it.
- mathgradthrow 2y ago
  It's also independently pretty tedious to explain that 7 is prime to a proof checker.
  - amenghra 2y ago
    Is it? You can tell the checker about the remainder of division by 2 to 6.
    - deleted 2y ago
      [deleted]
    - kevhito 2y ago
      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?
      - someplaceguy 2y ago
        The first one can be trivially proved with automatic decision procedures and the second one is also very easy to prove, I believe.
  - drhodes 2y ago
    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_Structure_II.html#id32 https://hrmacbeth.github.io/math2001/04_Proofs_with_Structur... btw, that book is a lot of fun to work through.
    - mathgradthrow 2y ago
      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.
      - mathgradthrow 2y ago
        https://en.m.wikipedia.org/wiki/Primality_certificate https://en.m.wikipedia.org/wiki/Primality_certificate
olivierduval 2y ago
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 * 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
- ted_dunning 2y ago
  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 < 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.
  - olivierduval 2y ago
    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 < 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
gerdesj 2y ago
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-irrational https://math.stackexchange.com/questions/823970/is-i-irratio...
- BalinKing 2y ago
  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?
  - lupire 2y ago
    That's the point. When you use ambiguous definitions, you get stuck in a morass.
    - BalinKing 2y ago
      Still, I don't see how any such definition could even be called a "definition of √-1" in the first place, since the resulting object wouldn't actually have the properties of √-1.

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

by taneq 2y ago

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

lisper 2y ago

You'd be surprised at the number of things that appear to be self-evidently true that turn out to depend on tacit assumptions. For example, is 7 prime? Not if you're doing modular arithmetic.

sebzim4500 2y ago
It's a joke about `i` being imaginary.
- fat_cantor 2y ago
  yes the joke is on i
lohfu 2y ago
i think they were joking, but i can't prove it
- lisper 2y ago
  Maybe -i can.
- taneq 2y ago
  Unfortunately the margin is too small to contain it.
mathgradthrow 2y ago
It's also independently pretty tedious to explain that 7 is prime to a proof checker.
- amenghra 2y ago
  Is it? You can tell the checker about the remainder of division by 2 to 6.
  - deleted 2y ago
    [deleted]
  - kevhito 2y ago
    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?
    - someplaceguy 2y ago
      The first one can be trivially proved with automatic decision procedures and the second one is also very easy to prove, I believe.
- drhodes 2y ago
  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_Structure_II.html#id32 https://hrmacbeth.github.io/math2001/04_Proofs_with_Structur... btw, that book is a lot of fun to work through.
  - mathgradthrow 2y ago
    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.
    - mathgradthrow 2y ago
      https://en.m.wikipedia.org/wiki/Primality_certificate https://en.m.wikipedia.org/wiki/Primality_certificate

olivierduval 2y ago

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

ted_dunning 2y ago
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 < 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.
- olivierduval 2y ago
  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 < 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

gerdesj 2y ago

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-irrational https://math.stackexchange.com/questions/823970/is-i-irratio...

BalinKing 2y ago
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?
- lupire 2y ago
  That's the point. When you use ambiguous definitions, you get stuck in a morass.
  - BalinKing 2y ago
    Still, I don't see how any such definition could even be called a "definition of √-1" in the first place, since the resulting object wouldn't actually have the properties of √-1.