Curry Howard correspondence

classical logic semantics: we need a lattice with negation/complement constructive logic semantics: we don’t have negation, so we define the relative pseudo-compelement

Proof system = syntax, inductively defined Proving soundness (true in syntax implies true in semantics) is easy because syntax is inductive Proving completeness (true in semantics implies true in syntax) is hard because we quantify for all Heyting algebras and attribution function, which have properties but no syntax