4 ms·

A lot of things aren't that rigorous and people like to skip steps. Here's what happens if you try to prove that 2+2=4 with a computer program that refuses to

by Natsu 4y ago

A lot of things aren't that rigorous and people like to skip steps. Here's what happens if you try to prove that 2+2=4 with a computer program that refuses to skip any steps (granted, it's treating them as complex numbers with zero imaginary parts): http://us.metamath.org/mpeuni/mmset.html#trivia http://us.metamath.org/mpeuni/mmset.html#trivia Math is just a matter of transforming one thing into another using the operations allowed by the system starting from the ground truths stipulated by the system

lisper 4y ago
> … a total of 26,323 steps—this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms of ZFC set theory I can’t help but shake the feeling that if it takes this many steps to prove 2+2=4 then you’ve done something wrong in the design of your formalism.
- HL33tibCe7 4y ago
  > One of the reasons that the proof of 2 + 2 = 4 is so long is that 2 and 4 are complex numbers—i.e. we are really proving (2+0i) + (2+0i) = (4+0i) Yeah, this is why
  - lisper 4y ago
    Right. That seems like an unnecessary detour to me.
    - Natsu 4y ago
      It's necessary to go down to the level of axioms and do one step at a time. It's obviously not needed for us to see that this proof is correct. A human proof would probably not generally go beyond something like: 2+2=4 1+1+1+1 = 1+1+1+1 // Substitute the definitions of 2 (1+1) and 4 (1+1+1+1)
      - lisper 4y ago
        Except that 4 is not 1+1+1+1, it's the successor of 3, which is the successor of 2 which is the successor of 1 which is the successor of 0. So you'd have to show that: S(S(0)) + S(S(0)) = S(S(S(S(0)))) and that is non-trivial. (But it's not 26,000 steps either.)
        Natsu 4y ago
        I'm assuming those steps in the definitions of 2 and 4, but you're right that this is part of why it gets so tedious.
        WastingMyTime89 4y ago
        It is trivial in most axiomatic systems. It’s directly linked to how + is defined and will mostly boil down to applying it. The 26000 steps proof is extremely convoluted.

by Natsu 4y ago

lisper 4y ago

> … a total of 26,323 steps—this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms of ZFC set theory I can’t help but shake the feeling that if it takes this many steps to prove 2+2=4 then you’ve done something wrong in the design of your formalism.

HL33tibCe7 4y ago
> One of the reasons that the proof of 2 + 2 = 4 is so long is that 2 and 4 are complex numbers—i.e. we are really proving (2+0i) + (2+0i) = (4+0i) Yeah, this is why
- lisper 4y ago
  Right. That seems like an unnecessary detour to me.
  - Natsu 4y ago
    It's necessary to go down to the level of axioms and do one step at a time. It's obviously not needed for us to see that this proof is correct. A human proof would probably not generally go beyond something like: 2+2=4 1+1+1+1 = 1+1+1+1 // Substitute the definitions of 2 (1+1) and 4 (1+1+1+1)
    - lisper 4y ago
      Except that 4 is not 1+1+1+1, it's the successor of 3, which is the successor of 2 which is the successor of 1 which is the successor of 0. So you'd have to show that: S(S(0)) + S(S(0)) = S(S(S(S(0)))) and that is non-trivial. (But it's not 26,000 steps either.)
      - Natsu 4y ago
        I'm assuming those steps in the definitions of 2 and 4, but you're right that this is part of why it gets so tedious.
      - WastingMyTime89 4y ago
        It is trivial in most axiomatic systems. It’s directly linked to how + is defined and will mostly boil down to applying it. The 26000 steps proof is extremely convoluted.