An axiomatisation of a pure calculus of names (Q1928489)

In this paper, by a pure calculus of names (PCN) is meant a quantifier-free fragment of Leśniewski's Ontology based on the classical propositional calculus. In contrast to [\textit{A. Ishimoto}, Stud. Log. 36(1977), 285--299 (1978; Zbl 0391.03004); \textit{M. Kobayashi} and \textit{A. Ishimoto}, Stud. Log. 41, 181--195 (1982; Zbl 0597.03015)], the author has chosen three primitive \(nn/s\) type functors: Leśniewski's \(\varepsilon\) and functors \(a\) and \(i\) of Aristotle's syllogistic (\(a\) with the so-called strong interpretation; vacuous names are admitted). An axiomatisation of, and a decision procedure for, PCN are presented; the axioms are shown to be independent. The main discussion concerns adequacy of PCN (only weak completeness is dealt with). PCN is enriched to an axiomatic rejection system; it is then proved that every formula in the language of PCN is either a thesis or a rejected one, and no formula is both proved and rejected. This allows to conclude that any extension of PCN must contain undesirable theses, and to prove that PCN is (sound and) complete with respect to a certain natural class of set-theoretical models. The latter result leads to the following conservativeness theorem: Every thesis of the so-called basic Ontology formulated in the language of PCN is a thesis of PCN. Here, basic Ontology is a first-order theory whose language is that of PCN enriched by quantifiers; its axioms are Leśniewski's \(\varepsilon\)-axiom and definitions for \(a\) and \(i\).