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: $\epsilon (a,b)\supset \epsilon (a,a),\epsilon (a,b)\wedge \epsilon (b,).\supset \epsilon (a,c)$ and $\epsilon (a,b)\wedge \epsilon (b,c).\supset \epsilon (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\epsilon (a,b)=F_{b}\imath xF_{a}x$ (Russellian-type definite description), $TA\vee B=TA\vee TB,T\sim A=\sim TA$ , etc. For the proof of this theorem use is made of a tableau method based upon the following reduction rules: $\frac{G[A\vee B_{-}]}{G[A\vee B_{-}]\vee \sim A|G[A\vee B_{-}]\vee \sim B},\frac{G[\epsilon (a,b)_{-}]}{G[\epsilon (a,b)_{-}]\vee \sim \epsilon (a,a)},\frac{G[\epsilon (a,b)_{-},\epsilon (b,c)_{-}]}{G[\epsilon (a,b)_{-},\epsilon (b,c)_{-}]\vee \sim \epsilon (a,c),}\frac{G[\epsilon (a,b)_{-},\epsilon (b,c)_{-}]}{G[\epsilon (a,b)_{-},\epsilon (b,c)_{-}]\vee \sim \epsilon (b,a),}$ , 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