A Constructive Completeness Proof for Intuitionistic Predicate Calculus
by Judith Underwood
In this week's Prl seminar, I'll present a version of a constructive completeness proof for intuitionistic predicate calculus. Since the predicate calculus (unlike the propositional calculus) is undecidable, this proof cannot give rise to a true decision procedure.
However, it does illustrate a constructive approach to undecidable problems, and also demonstrates the use of co-inductive definitions of infinite objects.Despite the density of the above description, the talk should be accessible to anyone familiar with constructive logic.