/sci/ - Science & Math

>>15049092
>I'm >>15048954 >>15049031 >>15049034
Okay, I conjectured this already (which is why I asked) based on the fact that few people on /mg/ would care or know about the subject. But fyi the reply >>15049031 was written as if it came from another person and that doesn't help your cause.


Anyway,
>>15048954
if you want a setty formulation, a "justification" for the construction of g1, I think you can go with

[math] g_1 := \{ (y, g_{1y}) \in (Y \times \Omega) \mid g_{1y} = S_y\} [/math]

where I write [math] S_y [/math] for the subset of [math] \{0\} [/math] given by

[math] S_y := \{0 \in \{0\} \mid \exists(x\in X). f(x)=y\} [/math]
where
1:= {0}

It's a function in that [math] g_1(y) [/math] is always [math] S_y [/math], even if the predicate defining the set S_y is not decidable.

>>15049031
Note:
The above pattern is extremely common:
You got a term [math]z_0[/math] any predicate [math]P(x)[/math] (not necessarily actually depending on a parameter x, i.e. P can also be a proposition), and if your theory allows for comprehension/separation with P, then you define the set
[math] S_{z_0, P} := \{x\in\{z_0\}\mid P(x)\} [/math]
Unlike P, the set [math] S_{z_0, P}\subset\{z_0\} [/math] is an actual thing in your theory, namely a set, and that makes is possible to relate it to the axioms.
Notably, If you know [math] P(z_0) [/math] holds, then and only then you know [math] z_0\in S_{z_0, P} [/math].
The proposition has been translated to a set theoretical statement.

>apparently P(1)={0,1} would imply LEM
I think that's sort of the important thing to understand here, and it also relates to the above.
Say for example CH denotes the continuum hypothesis, which is not even decidable in ZFC.
Now consider a weakened theory (constructive ones are of interest here) of ZFC which nonetheless allows for comprehension with CH. Then define
[math]S_{CH}:=\{0\in 1\mid CH\}[/math]
This is a subset of {0} and if LEM, all such subsets are {} or {0} and P({0}) becomes {0,1}.