> My computer can manipulate and prove things about real numbers just fine.
If you mean it can, with appropriate software, do symbolic manipulations of general formulas that are valid for real numbers, yes, of course. But that's not the same as doing specific concrete computations with them.
> What I was mostly responding to in your previous comment is the idea of "emulating" multiplication for whole numbers by repeated addition. What I got from that is that you were thinking of the whole numbers as being inside the real numbers. My point was that to get the real numbers you usually have to start with the whole numbers and build up to the reals (say by Dedekind cuts or Cauchy sequences)
Ah, I see. As far as I know the axiomatic reasoning involved can go either way. But in any case, that wasn't what I was trying to get at with the term "emulating"; I'm sorry if my use of that term caused confusion, and I agree with you that telling a child something like "the whole numbers are inside the real numbers" without qualification would also be a misrepresentation. My point was simply that teaching a child a specific computational procedure, repeated addition, in order to get an answer to particular multiplication problems does not require telling the child that multiplication is repeated addition, without qualification. The two things are distinct, and I am fine with the former; I only object to the latter.
> If you mean it can, with appropriate software, do symbolic manipulations of general formulas that are valid for real numbers, yes, of course. But that's not the same as doing specific concrete computations with them.
No, I don't mean computer algebra systems, if that's what you mean. In something like Lean, you can set up an actual construction of the system of real numbers (in mathlib it's the Cauchy completion of the rationals, which in turn are a given by a numerator and positive nonzero denominator that are coprime; an integer is essentially a natural number and a sign bit, and natural numbers are inductively constructed from zero and taking successors). Maybe this will convince you that these are "the" real numbers: you can prove there are uncountably many of them, and more importantly that it is the unique complete ordered field (up to isomorphism).
> In something like Lean, you can set up an actual construction of the system of real numbers
I'm not familiar with Lean, but from what I can gather, it's a theorem proving system. That is included in what I was referring to. Proving general theorems is still not the same as doing specific concrete computations.
Yes, it's a theorem proving system, and it's based on foundations that are powerful enough to represent all of (formal) math. Including something like Lean excludes math itself from being able to do "specific concrete computations," which is absurd.
Here are some examples to give you an idea of concrete calculations. Lean is not a CAS, so it needs some help in the form of tactic proofs (which are unreadable without an IDE, but their structure sort of mirrors work you'd do on paper):
import data.real.basic
import data.real.sqrt
import tactic
-- that 2^2 - 2 = 0
example : (real.sqrt 2)^2 - 2 = 0
:= by norm_num
-- that if x solves x^2 - 2x + 1, then x = 1.
example (x : ℝ) (h : x^2 - 2*x + 1 = 0) : x = 1
:= begin
have : x^2 - 2*x + 1 = (x - 1)*(x - 1), ring,
rw this at h,
cases eq_zero_or_eq_zero_of_mul_eq_zero h with h' h',
repeat {
convert_to x - 1 + 1 = 1,
norm_num,
rw h',
norm_num,
},
end
These were just some quick examples, but what I'm trying to show you is that in Lean you are working with the real numbers. They're just as real as the ones defined in a real analysis textbook, maybe moreso. They're just more tedious to deal with because the computer needs every calculation to come with some sort of proof of correctness, which thankfully can be filled in automatically sometimes with tactics like norm_num.
(A meta-comment: I'm not sure why if you're not familiar with Lean you'd tell me what it can and cannot do. Maybe someone told you at some point "theorem prover systems prove general theorems" or "theorem provers can only prove things about computable reals" and you had no reason to believe that they weren't telling you the whole story? Don't take this too seriously, I'm just riffing on your original point.)
p.s. Looking back to the beginning of this thread, I realize my saying "I'm not understanding what all the fuss is" could be misinterpreted -- I didn't meant to refer to you in particular. This was meant to be in the context of all the comments and the original article, and somehow I ended up replying to yours. Maybe one thing that caught my eye was the idea that there was much to unlearn here, but I ended up not addressing that point because I didn't have anything cogent to say. I think the sibling comment put it well, that there's value in learning to unlearn.
If you mean it can, with appropriate software, do symbolic manipulations of general formulas that are valid for real numbers, yes, of course. But that's not the same as doing specific concrete computations with them.
> What I was mostly responding to in your previous comment is the idea of "emulating" multiplication for whole numbers by repeated addition. What I got from that is that you were thinking of the whole numbers as being inside the real numbers. My point was that to get the real numbers you usually have to start with the whole numbers and build up to the reals (say by Dedekind cuts or Cauchy sequences)
Ah, I see. As far as I know the axiomatic reasoning involved can go either way. But in any case, that wasn't what I was trying to get at with the term "emulating"; I'm sorry if my use of that term caused confusion, and I agree with you that telling a child something like "the whole numbers are inside the real numbers" without qualification would also be a misrepresentation. My point was simply that teaching a child a specific computational procedure, repeated addition, in order to get an answer to particular multiplication problems does not require telling the child that multiplication is repeated addition, without qualification. The two things are distinct, and I am fine with the former; I only object to the latter.