Standard first-order modal logic is a convenient family of formalisms for studying modalities and their relationships to quantification and predication. The standard semantics for such logics is the semantics of possible worlds. However, as regards predication, it is formulated in such a way that it does not allow an adequate analysis of expressions containing comparisons of objects associated with different possible worlds. However, in some cases, it is necessary to refer to the comparison of objects associated with different possible worlds. Cross-world predication (as opposed to intra-world predication) seems to have a number of obvious ontological advantages. In a natural language, statements with cross-world predication are correct and can be intuitively understood by native speakers of a particular language. Such statements involve comparing what is with what it could be. In addition, we are able to compare objects from different possible worlds with each other, even if there are no such objects in the actual world. However, cross-world predication is not limited to comparisons in general and comparisons of two objects in particular. Comparisons of three or more objects from different possible worlds are allowed, and statements are allowed that say that an arbitrary set of objects from different possible worlds satisfies some criteria. The present article considers the features of CPL. It discusses various standard and non-standard formulas used as axioms of quantification in the formulation of the axiomatic calculus of first-order logic and for standard constant-domain modal logics, as well as formulas expressing the semantic features of quantifiers and their relationships with modalities. The second part of the article discusses the features of CPL in the case of intra-world predication. The third part touches upon the features of cross-world predication. The fourth part gives a brief conclusion. In contrast to standard modal logic, the truth (respectively, validity) of formulas in CPL is determined by a larger number of factors, which primarily include VP-functions used to associate variables with possible worlds. CPL uses a variable domain, so it is important to pay attention to how (with respect to which possible world) values are assigned to one or another formula variable. The latter is affected by VP-functions: if a VP-function is not defined for some variable, then this variable is associated with the current world of evaluation using a "grounded" VP-function. In addition, CPL inherits a number of features that some modal logics without cross-world predication have: variable domain and lambda operators. Also, in CPL, the interpretation of predicate symbols, variables, and individual constants is given in the domain of the model, while quantified variables are assigned values from the domain of the world of evaluation (also associated by VP-functions with the world of evaluation). All these features of CPL must be taken into account when formulating calculi, for example, natural, sequential, and axiomatic.
