Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Tadayoshi Miwa, Takao Inoué

TL;DR

This work develops a Ketonen-type Gentzen framework for classical simple type theory, introducing both Gentzen ($KCT$, $KCT_h$) and tableau ($KCTT$, $KCTT_h$) systems and establishing a deep correspondence between them. It furthermore introduces Hintikka sequents as a semantic-structural bridge and proves completeness and a Takahashi-Prawitz-style theorem for the tableau-variant, thereby reconciling tableau methods with sequent-calculus reasoning. Semantics are given via total valuations over systems of sets, with robust reduction chains and partial valuations underpinning soundness and cut-elimination. Collectively, the results offer a uniform, inference-preserving proof-theoretic account of classical simple type theory and reinterpret Schütte’s foundational program through the Ketonen tableau lens.

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$.

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

TL;DR

This work develops a Ketonen-type Gentzen framework for classical simple type theory, introducing both Gentzen (, ) and tableau (, ) systems and establishing a deep correspondence between them. It furthermore introduces Hintikka sequents as a semantic-structural bridge and proves completeness and a Takahashi-Prawitz-style theorem for the tableau-variant, thereby reconciling tableau methods with sequent-calculus reasoning. Semantics are given via total valuations over systems of sets, with robust reduction chains and partial valuations underpinning soundness and cut-elimination. Collectively, the results offer a uniform, inference-preserving proof-theoretic account of classical simple type theory and reinterpret Schütte’s foundational program through the Ketonen tableau lens.

Abstract

In this paper, we introduce a Ketonen-type Gentzen-style classical simple type theory . Also the tableau system corresponding to is introduced. Further inference-preserving Gentzen system (equivalent to ) and tableau system (equivalent to ) is introduced. We introduce the notion of Hintikka sequents for .The completeness theorem and Takahashi-Prawitz's theorem are proved for .
Paper Structure (32 sections, 31 theorems, 12 equations)

This paper contains 32 sections, 31 theorems, 12 equations.

Table of Contents

  1. Introduction
  2. General introduction: Proposed systems and the results
  3. Main contributions.
  4. Why Type Theory?---Russell's Paradox, Syntactic Stratification, and Foundations
  5. Preparations for Our Formal Systems
  6. The Formal Language
  7. Chains of Subterms
  8. Basic preliminaries on inferences
  9. (1) Basic inferences
  10. (2) deducibility
  11. (3) reducibility
  12. (4) The turnstile $\vdash$ in this paper (a caution).
  13. (6) permissible inference
  14. (7) weak inference
  15. Ketonen-type Gentzen classical simple type theory $\bf KCT$
  16. ...and 17 more sections

Key Result

Proposition 2.1

$$ 1. If $\forall x^{\sigma} \mathscr{F}[x^\sigma]$ is a formula and $t^{\sigma}$ is a term of type $\sigma$, then $\mathscr{F}[t^\sigma]$ is a formula. 2. If $\lambda x^\tau \mathscr{A} [x^\tau]$ is a term of type $(\tau) = (\tau_1, \ldots, \tau_n)$ and if $t^\tau = t_1^{\tau_1}, \ldots, t_n^{\tau_

Theorems & Definitions (65)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 2.7
  • Proposition 2.1
  • Definition 2.8
  • Definition 2.9
  • ...and 55 more