Basic Predicate Calculus is Sound with Respect to a Modified Version of Strictly Primitive Recursive Realizability

A. Yu. Konovalov

Lomonosov Moscow State University

Abstract: A version of strictly primitive recursive realizability for the language of the basis predicate logic $\mathsf{BQC}$ is defined, which takes into account specific features of the language. It is proved that $\mathsf{BQC}$ is sound with respect to this version of strictly primitive recursive realizability.

Keywords: strictly primitive recursive realizability, basis predicate logic BQC, constructive semantics, realizability.

UDC: 510.25+510.64

Received: 14.09.2022
Revised: 27.04.2023

DOI: 10.4213/mzm13723

 English version: Mathematical Notes, 2023, 114:6, 1260–1276

Bibliographic databases:

•