An Axiomatisation of a Pure Calculus of Names

A calculus of names is a logical theory describing relations between names. By a pure calculus of names we mean a quantifier-free formulation of such a theory, based on classical propositional calculus. An axiomatisation of a pure calculus of names is presented and its completeness is discussed. It is shown that the axiomatisation is complete in three different ways: with respect to a set theoretical model, with respect to Le?niewski??s Ontology and in a sense defined with the use of axiomatic rejection. The independence of axioms is proved. A decision procedure based on syntactic transformations and models defined in the domain of only two members is defined.