Abstract:As an introduction to the necessary modality □, the truth values of formulas of the predicate modal logic in a possible world may rely on its alternative worlds. So there is a problem of the transworld identity of individuals in the predicate modal logic. According to this problem, Lewis proposed the counterpart theory and used the counterpart relation to represent the transworld identity of individuals in the counterpart theory. When an object has more than one counterpart, the transworld identity cannot have a one-to-one correspondence with the counterpart relation. By limiting the scope of the universal quantifier ∀ in the predicate modal logic, this paper gives a formula- layered predicate modal logic, which is a sublogic of the predicate modal logic, and which language is the same as that of the predicate modal logic. But the definition of its formulas is decomposed into layers such that ∀ may occur in the scope of □, and □ cannot occur in the scope of ∀. Since any expression in the form of ∀x□φ(x) is not a formula of this logic, the truth value of any formula which begins with a quantifier in a possible world w only relies on w, and this logic avoids the problem of the transworld identity of individuals. This paper gives the language, the syntax and the semantics of this logic, and proves that this logic is sound and complete.