Let EOA be the elementary ontology augmented by an additional axiom S (S S), and let LS be the monadic second-order predicate logic. We show that the mapping which was introduced by V. A. Smirnov is an embedding of EOA into LS. We also give an embedding of LS into EOA.

LetEO be the elementary ontology of Leniewski formalized as in Iwanu [1], and letLS be the monadic second-order calculus of predicates. In this paper we give an example of a recursive function , defined on the formulas of the language ofEO with values in the set of formulas of the language of LS, such that EO A iff LS (A) for each formulaA.

The propositional fragment L 1 of Leniewski'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 1 iff TA is a thesis of first-order (...) predicate logic with equality, where T is a translation of the formulas of L 1 into those of first-order predicate logic with equality such that T(a, b) = FblxFax (Russeltian-type definite description), TA B = TA TB, T A = TA, etc. (shrink)

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. (shrink)

A structure A for the language L, which is the first-order language (without equality) whose only nonlogical symbol is the binary predicate symbol , is called a quasi -struoture iff (a) the universe A of A consists of sets and (b) a b is true in A ([p) a = {p } & p b] for every a and b in A, where a(b) is the name of a (b). A quasi -structure A is called an -structure iff (c) {p (...) } A whenever p a A. Then a closed formula in L is derivable from Leniewski's axiom x, y[x y u (u x) u; v(u, v x u v) u(u x u y)] (from the axiom x, y(x y x x) x, y, z(x y z y x z)) iff is true in every -structure (in every quasi -structure). (shrink)