Modified realizability and predicate logic

Semantics of predicate formulas based on the notion of modified realizability for arithmetic formulas and interpretations of the language of arithmetic in all finite types are considered. For a number of natural constructive interpretations, the corresponding predicate logic of modified realizability is proved to be nonarithmetical. Translated fromMatematicheskie Zametki, Vol. 61, No. 2, pp. 259–269, February, 1997. This research was supported by the Russian Foundation for Basic Research under grant No. 95-01-00416 and by the International Science Foundation under grant No. NFQ000. Translated by V. N. Dubrovsky