{"id":"arxiv/2601.10026","url":"https://arxiv.org/abs/2601.10026","tags":["math.LO"],"score":0,"title":"A New Overture to Classical Simple Type Theory, Ketonen-type Gentzen and Tableau Systems","domain":"math.LO","source":"arxiv","authors":["Tadayoshi Miwa","Takao Inoué"],"reviews":0,"subject":"math.LO","summary":"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$.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-01-15","reactions":{}}