Moscow University Mathematics Bulletin

, Volume 72, Issue 3, pp 129–132 | Cite as

The semantics of realizability for the constructive set theory based on hyperarithmetical predicates

  • A. Yu. Konovalov
Brief Communications


A semantics of realizability based on hyperarithmetical predicates of membership is introduced for formulas of the language of set theory. It is proved that the constructive set theory without the extensionality axiom is sound with this semantics.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    H. Rogers Jr., Theory of Recursive Functions and Effective Computability (McGraw–Hill Book Comp., N.Y., St. Louis, San Francisco, Toronto, L., Sydney, 1967; Mir, Moscow, 1972).MATHGoogle Scholar
  2. 2.
    P. Aczel, “The Type Theoretic Interpretation of Constructive Set Theory,” Log. Coll. 77, 55 (1978).MathSciNetMATHGoogle Scholar

Copyright information

© Allerton Press, Inc. 2017

Authors and Affiliations

  1. 1.Moscow State UniversityFaculty of Mechanics and MathematicsLeninskie Gory, MoscowRussia

Personalised recommendations