On undecidability of subset theories of some unars

This paper is dedicated to studying of the algorithmic properties of unars with an injective function. We prove that the theory of every such unar admits quantifier elimination if the language is extended by a countable amount of predicate symbols. Necessary and sufficient conditions are established for the quantifier elimination to be effective, and a criterion of decidability of theories of such unars is formulated. Using this criterion we build a unar such that its theory is decidable, but the theory of the unar of its subsets is undecidable.