/sci/ - Science & Math

>>12141295
The point is that for all classically provable statements, there is always intuitionistically provable statment that's classically equivalent to it.

Example: Noncontradiction is intuitionistically provable, i.e.
[math] \neg (A \and \neg A) [/math]
is a constructive theorem
(Proof: given a reason x to believe A and a reason f to believe A leads to absurdum, apply the procedure f to x and thus an absurd conclusion f(x) is obtained)

Now there's a classical rule that
[math] \neg (P \and Q) [/math]
is equivalent to
[math] \neg P \or \neq Q [/math]
and classically we also have the double negation elimination saying
[math] \neg \neg A [/math]
is equivalent to just
[math]A [/math].
So the constructively proven
[math] \neg(A\and\neg A) [/math]
is classically equivalent to
[math]\neg A\or A[/math]

There are several schemes of translations (rewritings) that each map any classically provable statement to one that's constructively provable in this way.
If we view theorems connected via such short rewriting procedures as equivalence class, then dropping LEM does not make any such class empty. No theorem is lost in that sense.

Compare it to me discarding the possibility to use "9+5=14" but still allowing the rules "9+4=13" and "13+1=14". You then have to make syntactical detours, but the theorems you prove remain the same.

More concretely, some existence claims will constructively only survive as non-rejectibility claims. The constructive frameworks however allows for a nicer range of semantics.

* Classical reasoning example (common sense application of LEM):
"After the car accident, I found myself waking up in a hospital room without windows and I knew that either it was day, or it was night!"

* Epistemic logic semantics (out of place use of LEM):
"After the car accident, I found myself waking up in a hospital room without windows and I knew that either I had a reason to believe it was day, or I had a reason to believe it was night!"

Which is just bullshit.