Abstract:
New mathematics concepts are often introduced with some quantifier definitions. If we have a sufficiently large stock of such notions, it can allow to reformulate the new quantifier definitions in a quantifier-free form. This makes the problem of finding basic concepts, which make further quantifiable definition redundant, worth considering. Creating computer programs that automatically introduce such bases is also worth considering.
In this paper we observe $3$ simple cases of reducing the quantifier expressions to the quantifier-free ones. We investigate predicates and functions defined by $\in$ predicate on the set $Z\cup2^Z$, where $Z$ is the set of integers. We consider predicates expressed by $\mid$ predicate on the set of points of the plane and the lines lying in it. Finally, predicates expressed on the set of natural numbers by the predicate on it are also considered. Bases were found in all 3 cases.