/sci/ - Science & Math

>>11772381
He wrote a lot of book, that's obviously prove he existed.
(Actually, I think I didn't even make the point he/she/xe was a person)

>>11772345
Mhm, yeah try
>https://plato.stanford.edu/entries/intuitionism/
and go from there.

What's fun to read is also pic related
https://en.wikipedia.org/wiki/Brouwer%E2%80%93Hilbert_controversy

Sort of the origin of why Russel made his original type theory (now pretty much forgotten, but strongly revived of course 50 years ago) is how the debate about the Russel paradox was had 120 years ago.
E.g. there's the impredicativity discussion, about which I however never found a good text myself.

Namely that people back then argued that "set of all sets" and notions like this have the underlying conceptual problem that they are not "predicative":
What would it mean to compute
[math] T := \{n \in {\mathbb N} \mid \forall(S \subset {\mathbb N}). \phi(n, S)\} [/math]
?
The issue is that to assemble all elements of T to a set, you'd have to check all subsets S of N, but T is one of those.
With unbounded comprehension, of course writing down this set is no issue in e.g. ZF, but logicans took (or take) issue with that.

The theory called IZF is just ZF in a context without LEM (and regularity replaced with set indcution, for the mentioned technical reasons), but the impredicativity issue is why people actually looked at CZF, which is roughly what I outline above.
It's IZF, but with power set replaced with a weaker axiom and separation make predicative (no forall over all sets.)

>>11772397
Not from me, but there's texts on topology without LEM and the prove are hard as far as I could tell. Things just get cumbersome there. So I think the Lie theory will look more like algebra and less like differential geometry.