Axiomatic Rejection for the Propositional Fragment of Leśniewski's Ontology

Abstract

A Hilbert-type axiomatic rejection $\mathbf{HAR}$ for the propositional fragment ${\mathbf{L}}_1$ of Leśniewski's ontology is proposed. Also a Gentzen-type axiomatic rejection $\mathbf{GAR}$ of ${\mathbf{L}}_1$ is proposed. Models for ${\mathbf{L}}_1$ are introduced. By axiomatic rejection, Ishimoto's embedding theorem will be proved. One of our main theorems is: \noindent \textsc{Theorem} \rm (Main Theorem) \it ${⊢}_{T}A⟺{⊢}_{H}A$ $\enspace \enspace \enspace \enspace \enspace \enspace \Longleftrightarrow \enspace TA \enspace \mbox{is valid in first-order predicate logic with equality}$ $⟺not{⊣}_{H}A.$ \noindent where ${⊢}_{T}A$ means that $A$ is provable in the tableau method of ${\mathbf{L}}_1$, while ${⊢}_{H}A$ means that $A$ is provable in the Hilbert-type ${\mathbf{L}}_1$. \rm \smallskip In the last section, as the chracterization theorem, we shall show the theorem which contains six equivalent statements with the cut elimination theorem etc.

53 pages