minus-squareCHINESEBOTTROLL@lemm.eetoNo Stupid Questions@lemmy.world•What are the most mindblowing things in mathematics?linkfedilinkarrow-up13·edit-21 year agoMaybe a bit advanced for this crowd, but there is a correspondence between logic and type theory (like in programming languages). Roughly we have Proposition ≈ Type Proof of a prop ≈ member of a Type Implication ≈ function type and ≈ Cartesian product or ≈ disjoint union true ≈ type with one element false ≈ empty type Once you understand it, its actually really simple and “obvious”, but the fact that this exists is really really surprising imo. https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence You can also add topology into the mix: https://en.m.wikipedia.org/wiki/Homotopy_type_theory linkfedilink
Maybe a bit advanced for this crowd, but there is a correspondence between logic and type theory (like in programming languages). Roughly we have
Proposition ≈ Type
Proof of a prop ≈ member of a Type
Implication ≈ function type
and ≈ Cartesian product
or ≈ disjoint union
true ≈ type with one element
false ≈ empty type
Once you understand it, its actually really simple and “obvious”, but the fact that this exists is really really surprising imo.
https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
You can also add topology into the mix:
https://en.m.wikipedia.org/wiki/Homotopy_type_theory