Examines models of universal first-order formulas without functional symbols. We prove the existence of a limited number of types of submodels, which are formed from logical models of these formulas. Based on this, we prove the solvability of problems generally valid for a class of formulas, representing an implication of the following form. Their package is a universal formula, and the conclusion — formulas of the first order, the signature included in the signature parcels, and occurrences of atoms of one sign — either positive or negative. It is shown that the attenuation requirements on the type of conclusion of an implication leads to the insoluble class.

logical formula, formula of the first order, logical model, universal formula, solvable class

Mathematical problems and theory of numerical methods