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
There are no notes linking to this note.
There are no papers linking to this note.