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.


Here are all the notes in this garden, along with their links, visualized as a graph.