Publication details

Saarland University Computer Science

A Minimal Propositional Type Theory

Mark Kaminski, Gert Smolka

Technical Report, Saarland University, July 2008

Propositional type theory, first studied by Henkin, is the restriction of simple type theory to a single base type that is interpreted as the set of the two truth values. We show that two constants (falsity and implication) suffice for denotational and deductive completeness. Denotational completeness means that every value of the full set-theoretic type hierarchy can be described by a closed term. Deductive completeness is shown for a sequent-based proof system that extends a propositional natural deduction system with lambda conversion and Boolean replacement.

Also available at arXiv (arXiv:1001.4021).

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy