This meaning theory also justifies a variety of inductive, recursive, and inductive-recursive definitions. Although proof-theoretically strong notions can be justified, such as analogues of certain large cardinals, the system is considered predicative. Impredicative definitions of the kind found in higher-order logic, intuitionistic set theory, and topos theory are not part of the theory. Neither is Markov’s principle, and thus the theory is distinct from Russian constructivism.