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

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.