Tadayoshi Miwa | arXiv Science

arXiv2026

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

math.LO↗

arXiv2025

Nontrivial single axiom schemata and their quasi-nontriviality of Leśniewski-Ishimoto's propositional ontology $\bf L_1$

On March 8, 1995, was found the following \it nontrivial \rm single axiom-schema characteristic of Leśniewski-Ishimoto's propositional ontology $\bf L_1$ (Inoué, 1995b \cite{inoue16}). $$(\mathrm{A_{M8})} \enspace εab \wedge εcd . \supset . εaa \wedge εcc \wedge (εbc \supset . εad \wedge εba).$$ In this paper, we shall present the progress about the above axiom-schema from 1995. Here we shall give two criteria \it nontiriviality \rm and \it quasi-nontriviality \rm in order to distinguish two axiom schemata. As main results, among others, in §6 - §8, we shall give the simplified axiom schemata ($\rm A_{S1}$), ($\rm A_{S2}$), ($\rm A_{S3N}$) and ($\rm A_{S3Nd}$) based on ($\mathrm{A_{M8}}$), their nontriviality and quasi-nontriviality. In §9 - §11, we shall give a lot of conjectures for nontrivial single axiom schemata for $\bf L_1$. We shall conclude this paper with summary and some remarks in §12.

math.LO↗