Intuitionistic logic (Heyting)

Layer 0 — Mathematicsin the proof-theory subtree

Heyting 1930 formalisation of Brouwer intuitionism. Reject law-of-excluded-middle. Kripke-semantics 1965. BHK interpretation. Foundation of constructive-mathematics + computational-content.