A Minimal Propositional Type Theory

TL;DR

This paper demonstrates that propositional type theory can be fully characterized using only two constants, falsity and implication, achieving both denotational and deductive completeness.

Contribution

It establishes that a minimal set of constants suffices for complete propositional type theory, simplifying its foundational understanding.

Findings

Two constants (falsity and implication) are enough for completeness.

Every value in the type hierarchy can be represented by a closed term.

A proof system with lambda conversion and Boolean replacement is deductively complete.

Abstract

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.