SSequence said:
Are you sure about this? I don't know much about this stuff formally. But what I do know is that LEM (law of excluded-middle) is closely related to both incompleteness and how the humans mind mentally carries out processes (in a general sense).
Qualitatively (not going to every detail) a lot of what Brouwer said about mathematics seems to be spot on (in my opinion of course). I am not sure though whether Brouwer (or Bishop) ever wrote (I haven't read any of their technical work) that they doubt mathematical induction (for natural numbers). I would certainly be very surprised to see that.
Now if some one doubts that numbers that are larger than scale of universe (in some sense) don't exist or make sense (or something like that), then it would be expected for them to doubt mathematical induction (for natural numbers). Anyway, what I wanted to point out (correct me if I am wrong) that this certainly isn't necessarily a consensus opinion about this among those working on some non-classical logic.
Yes, the OP is wrong. Constructivists do not reject the axiom of infinity. Some do though, but most definitely not all.
Anyway, the plan in the OP is totally insane. Seriously, I recommend you to get more in touch with the the typical student. Why don't you try to make some money by tutoring high school or calculus students, or why don't you get a job as a TA of elementary math classes. I highly recommend you do this because then you will see that your very interesting math plans will fall on deaf ears with the students. It just can't be done practically.
Now, I live in a country where the curriculum is known to be more abstract than in the US. Not too abstract, but we see basic sets in elementary school and we cover some group theory in high school. In particular, we are shown that the real numbers form a field. And you know, I have always been mathematically inclined in my life, and of all the kids in my class I was probably the most interested and perhaps even the best at mathematics. And you know what? I found fields to be something quite abstract and something that made math more difficult than it actually is. It took me years before I could appreciate what a field is!
You seem to like a foundations first approach. But it is a very bad idea to teach mathematics this way. You can't possibly study category without studying abstract mathematics for years. You need to know group theory, ring theory, field theory, topology, etc. in order to really grasp category theory. Teaching it in the very beginning is being an abusive teacher. I
am a category theorist by profession, and I wouldn't have understood one single bit of it without studying abstract mathematics for years already. The same holds true for logic. The same holds true for set theory. The same holds true for foundational issues like constructivism.
And about ##\mathbb{R}^n##, you don't fully realize the genius of the notation I see. In set theory given sets ##A## and ##B##, we have that ##A^B## is the set of functions from ##B## to ##A##. In set theory also, the natural number ##n## is defined as a set containing ##n## numbers. More precisely, you can define recursively ##0=\emptyset## and ##n+1 = \{0,1,...,n\}##. Then ##\mathbb{R}^n## is the set of functions from ##\{0,...,n-1\}## to ##\mathbb{R}##. Given such a function ##f:n\rightarrow \mathbb{R}##, we can write it symbolically as ##(f(0), f(1), ..., f(n-1))##. So this is the full explanation of the ##\mathbb{R}^n## notation: it should not be interpreted as you say as ##\mathbb{R}\times ...\mathbb{R}## ##n## times. Not that I would tell high schoolers all of this, or even undergraduates in mathematics...