# * Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus *

## by Robert L. Constable, Robert L. Constable

1992-1993

I will contrast the predicative (or ramified, Nuprl-like) higher-order PROPOSITIONAL logic with the impredicative (Coq-like) propositional calculus. I will relate this to the well-known polymorphic lambda calculus of Girard/Reynolds, and then discuss its extension to predicate logic and type theory.

I may also discuss contructive set theory and its role in providing models for the polymorphic calculus and its foundation role vis a vis type theory.

I hope to also discuss the relationship of foundational concerns to the on-going projects using Nuprl.