В статье описываются некоторые потенциальные проблемы теории кросс-мировой предикации Е. Борисова и предлагаются альтернативные формализации в терминах теории типов с зависимыми типами и теории множеств. Преимущество теоретико-типовой формализации состоит в её простоте, связанной с наличием в теории типов функций в зависимые типы. Преимущество предлагаемой теоретико-множественной формализации состоит в большей близости к традиционным подходам и отсутствии некоторых неинтуитивных следствий, таких как предикация по несуществующим объектам. The paper examines some potential problems of the theory of cross-world predication by E. Borisov and suggests alternative formalizations in terms of type theory with dependent types and set theory. The advantage of the type-theoretical formalization lies in its simplicity based on the presence of functions to dependent types. The advantage of the proposed set-theoretical formalization is a greater closeness to traditional approaches and the lack of some non-intuitive effects such as the predication on non-existing objects.