A New Overture to Classical Simple Type Theory, Ketonen-type Gentzen and Tableau Systems

TL;DR

This paper introduces a new classical simple type theory system, along with corresponding Gentzen and tableau proof systems, and establishes their completeness and equivalence properties.

Contribution

It presents a novel Ketonen-type Gentzen system and tableau system for classical simple type theory, including inference-preserving variants and completeness results.

Findings

Introduction of the Ketonen-type Gentzen system $f KCT$

Development of the tableau system $f KCTT$ and its variants

Proof of completeness and Takahashi-Prawitz's theorem for the systems

Abstract

In this paper, we introduce a Ketonen-type Gentzen-style classical simple type theory $\bf KCT$. Also the tableau system $\bf KCTT$ corresponding to $\bf KCT$ is introduced. Further inference-preserving Gentzen system $\bf KCT_h$ (equivalent to $\bf KCT$) and tableau system $\bf KCTT_h$ (equivalent to $\bf KCTT$) is introduced. We introduce the notion of Hintikka sequents for $\bf KCTT_h$.The completeness theorem and Takahashi-Prawitz's theorem are proved for $\bf KCTT_h$.