/sci/ - Science & Math

>>9802160
>But if stuff like Weierstrass' approximation theorem, the fundamental theorem of algebra, pretty much every foundational result in analysis with Cauchy's name on it or hell even basic shit like the mean value theorem or Pythagoras' theorem isn't valid on your theory it is just a neat thing and nothing more.

If you drop the law of excluded middle (LEM), i.e. if you work only constructively, then you can prove just as many theorems as when you assume LEM.
More concretely (via Gödels double negation), you have that for every classical theorem CL, there is a constructive theorem CO, which is classically equivalent to CL. The LEM just collapses a bunch of theorems, making semantics of the sentences less rich.

For example, LEM states
A ∨ ¬A
>Either A is true or A is absurd
and this is not constructively provable.
However, the sentence
¬(¬A ∧ ¬(¬A))
>If it's the case that 'A leads to an absurdity' and also that the statement 'A leads to an absurdity' does lead to an absurdity, then this together leads to an absurdity.
Is constructively provable.
And in classical logic, the later sentence reduces to the former.

That is to say, if you work constructively, you don't lose any theorems. However, all proves have computational content (and are harder to obtain, because you didn't axiomize stuff you'd like to be true).

Pic also related, regarding your complains.