Generalized realizability for extensions of the language of arithmetic (Q2287392)

The notion of \(V\)-realizability is introduced in the paper for a language \(L\) that contains the language of classical arithmetic, where \(V\) is a class of number-theoretical partial functions. This is a generalized realizability, in the sense that the functions used for realizing the implications and universal quantifiers of \(L\)-formulas are chosen from \(V\). In the framework of the paper, the implication and universal quantifiers are both of the form \(\forall\vec{x}[A(\vec{x})\rightarrow B(\vec{x})]\) for a possibly empty tuple \(\vec{x}\) of variables; the idea is taken from the basic quantifier calculus of \textit{W. Ruitenburg} [Notre Dame J. Formal Logic 39, No. 1, 18--46 (1998; Zbl 0967.03005)]. Negation is defined as \(\neg A = [A\rightarrow\bot]\). Now, the \(V\)-realizability of atomic \(L\)-formulas is equivalent to their truth in the standard model of natural numbers; for conjunction, disjunction, and existential quantifier it is defined as usual using the pairing (and their decoding) functions; and for the implication-universal quantifier the realizing function is chosen from the class \(V\). The main result of this short paper is that (i) if \(V\) contains all the \(L\)-definable functions, then being \(V\)-realizable of an \(L\)-sentence is equivalent to being true in the standard model; and (ii) if \(V\) does not contain all the \(L\)-definable functions, then some \(L\)-sentence of the form \(\forall z[\varphi(z)\vee\neg\varphi(z)]\) is not \(V\)-realizable.