PRL Seminars

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.