We present a cut-free tableau system for a version of Church's simple type theory with primitive equality. The system is formulated with an abstract normalization operator that completely hides the details of lambda conversion. We prove completeness of the system relative to Henkin models. The proof constructs Henkin models using the novel notion of a value system.
Download PDF Show BibTeX
Login to edit