Analytic Tableaux for Simple Type Theory and its First-Order Fragment

TL;DR

This paper develops a cut-free tableau calculus for simple type theory and its first-order fragment, establishing key logical properties and decision procedures for specific fragments.

Contribution

It introduces a tableau calculus for STT and EFO, proving completeness, compactness, and decision procedures, advancing the understanding of their model-theoretic and proof-theoretic aspects.

Findings

Proved completeness and compactness for STT and EFO.

Established decision procedures for three EFO fragments.

Demonstrated the existence of countable models for these theories.

Abstract

We study simple type theory with primitive equality (STT) and its first-order fragment EFO, which restricts equality and quantification to base types but retains lambda abstraction and higher-order variables. As deductive system we employ a cut-free tableau calculus. We consider completeness, compactness, and existence of countable models. We prove these properties for STT with respect to Henkin models and for EFO with respect to standard models. We also show that the tableau system yields a decision procedure for three EFO fragments.