A propositional fragment of Leśniewski's ontology and its formulation by the tableau method

Abstract

The propositional fragment L ₁ of Leśniewski's ontology is the smallest class (of formulas) containing besides all the instances of tautology the formulas of the forms: ɛ(a, b) ⊃ ɛ(a, a), ɛ(a, b) ∧ ɛ(b,).⊃ ɛ(a, c) and ɛ(a, b) ∧ ɛ(b, c). ⊃ ɛ(b, a) being closed under detachment. The purpose of this paper is to furnish another more constructive proof than that given earlier by one of us for:

Theorem A is provable in L ₁ iff TA is a thesis of first-order predicate logic with equality, where T is a translation of the formulas of L ₁ into those of first-order predicate logic with equality such that Tɛ(a, b) = F_blxF_ax (Russeltian-type definite description), TA ∨ B = TA ∨ TB, T ∼ A = ∼TA, etc.

For the proof of this theorem use is made of a tableau method based upon the following reduction rules:

$$\begin{gathered} \frac{{G\left[ {A \vee B} \right]}}{{G\left[ {A \vee B{\text{\_}}} \right] \vee \sim A|G|[A \vee B\_] \vee \sim B,}}{\text{ }}\frac{{G[\varepsilon (a,b)\_]}}{{G[\varepsilon (a,b)\_] \vee \sim \varepsilon (a,a),}} \hfill \\ \frac{{G[\varepsilon (a,b)\_,\varepsilon (b,c)\_]}}{{G[\varepsilon (a,b)\_,\varepsilon (b,c)\_], \vee \sim \varepsilon (a,c),}}{\text{ }}\frac{{G[\varepsilon (a,b)\_,\varepsilon (b,c)\_]}}{{G[\varepsilon (a,b)\_,\varepsilon (b,c)\_] \vee \sim \varepsilon (b,a),}} \hfill \\ \end{gathered} $$

where F[A ₊] (G[A₋]) means that A occurs in F[A ₊] (G[A₋]) as its positive (negative) part in accordance with the definition given by Schütte.