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.

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

by Robert L. Constable, Robert L. Constable 1992-1993

by Robert L. Constable, Robert L. Constable
1992-1993