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

In this paper, we introduce a Ketonen-type Gentzen-style classical simple type theory $\mathbf{K}\mathbf{C}\mathbf{T}$. Also the tableau system $\mathbf{K}\mathbf{C}\mathbf{T}\mathbf{T}$ corresponding to $\mathbf{K}\mathbf{C}\mathbf{T}$ is introduced. Further inference-preserving Gentzen system $\mathbf{K}\mathbf{C}{\mathbf{T}}_{\mathbf{h}}$ (equivalent to $\mathbf{K}\mathbf{C}\mathbf{T}$) and tableau system $\mathbf{K}\mathbf{C}\mathbf{T}{\mathbf{T}}_{\mathbf{h}}$ (equivalent to $\mathbf{K}\mathbf{C}\mathbf{T}\mathbf{T}$) is introduced. We introduce the notion of Hintikka sequents for $\mathbf{K}\mathbf{C}\mathbf{T}{\mathbf{T}}_{\mathbf{h}}$.The completeness theorem and Takahashi-Prawitz’s theorem are proved for $\mathbf{K}\mathbf{C}\mathbf{T}{\mathbf{T}}_{\mathbf{h}}$.