/sci/ - Science & Math

https://youtu.be/UulqkJzpSaA

Gonna try a science themed tea & chill session in 5 hours here, if you're quarantine and bored.
Currently thinking of broad topics, ideas?

>>11193986
nice, thanks!

>>10986523
https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf
https://discord.gg/UqgjEN

By then, it's its possible conscious life will be encoded on more durable material, such as germanium or silicon circuitry. This will allow conscious life to be miniaturized and robust enough to move freely in the depths of space.

It is much more easier to put a chip into space than carbon-based biological entity.

But this can only be possible in the distant future.

>>10904116
smart

>>10855578
Nevermind the formal syntax if you don't know it.
The point is that for each x, you have that x=x. The truth of x=x follos from the definition of equality (it's an axiom that equality is reflective).
The empty set just says that you don't need any assumptions.

The notation comes from reading the claim constructively via
https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation

Forall x gets translated into wanting an explicit map from x (and that's what the lambda is, it just binds x) and Exists says you need an explicit term (y is x here) together with a proof of the proposition (and refl generally comes with equality wherever it's implemented - refl is the incarnation of the axiom). See also
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
In full,
[math] \lambda A. \lambda x. \langle x, \mathrm{refl_x} \rangle \ : \ \Pi_{x:A} \Sigma_{y:A} Id_A(x, y) [/math]

The proof term is

[math] \lambda A. \lambda x. \langle x, \mathrm{refl_x} \rangle \ : \ \Pi_{x:A} \Sigma_{y:A} Id_A(x, y) [/math]

i.e. for each x take y:=x, assuming reflectivity of equality.