Part 2. Special Issues in Intellectual Systems Theory

The non-extensional constructive set theory is sound with respect to the sematics of the arithmetic realizability based on hyperarithmetic sorts

A. Yu. Konovalov

Lomonosov Moscow State University, Faculty of Mechanics and Mathematics

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

Keywords: constructive semantics, realizability, arithmetical realizability, axiomatic set theory, hyperarithmetical sorts.