/sci/ - Science & Math

Regarding constructivism, for people interested, I had recently shown e.g. how to prove the law of non-contradiction [math] \neg( P\land \neg P) [/math] constructively, which classically is equivalent to the law of excluded middle [math] \neg P\lor P) [/math]. Generally, for every classically provable statement [math] Q [/math], there's a constructive proof of a statement [math] Q' [/math] that's classically equivalent to to it. So you don't lose anything (but making the proofs harder and more algorithmic) when you do things purely constructively. And at the same time there's some nice theories (e.g. differential geometric ones) that aren't consistent classically - so you lose something going classical.
More high level, there's also a survey on axiomatizations of constructive set theory, sorted by axiom strength

https://youtu.be/Fyfvwu1dejA
https://youtu.be/HrN7orXvu9k

>>10946723
At looked at that book (series) today at the library. Seems like he really loved to write very thick books in general. Actually makes me think he didn't bother much about sorting out and rewriting things, but I might well be wrong.

>>10952500
smells like something along the lines fitting of
f2(n) := n - f1(n) + g(n)
and turing f1 such that when g maps to the same thing, f1 doesn't. Just a blue guess

>>10952562
from the start