Uniform Realizability Interpretations

Submitted to: CCC 2025 © U. Berger & P. Oliva This work is licensed under the Creative Commons Attribution License. Uniform Realizability Interpretations Ulrich Berger Swansea University Paulo Oliva Queen Mary University of London 1 Extended Abstract We report here on a novel framework of uniform realizability that unifies and generalizes various realizability interpretations of logic, particularly focussing on the treatment of atomic formulas and quantifiers. Traditional realizability interpretations (such as Kleene’s number realizability [7]) require explicit witnesses for existential quantifiers. In contrast, newer approaches, such as in the first author’s uniform Heyting arithmetic [2], Herbrand realizability of non-standard arithmetic [9], or in the “classical” realizability of arithmetic [3, 4], (some) quantifiers, are treated uniformly. The proposed notion of uniform realizability abstracts these differences, parametrising the interpretation by a given treatment of atomic formulas, accounting for both classical and modern variants. The approach is illustrated using several realizability interpretations of Heyting arithmetic, but in general we consider a realizability interpretation of an arbitrary source theory Sinto a some suitable target theory Twhich has an extra sort for potentially partial realizers with an application operation. Definition 1.1 (Base interpretation of L(S)into L(T))Abase interpretation of L(S)into L(T)associates to each n-ary predicate symbol P of the language of San (n+m)-ary relation x◁Pain the language of T, between tuples x(arity n) and a(arity m, for some m). We read this as xis P-bounded by a. We think of the tuple aas the realizers or witness of P(x). Either xor acould be the empty (nullary) tuple. We use the symbol ⟨⟩ for the empty tuple and write a↓to indicate that all elements of the tuple a are defined. Application of a tuple fto a tuple ais defined as the tuple f(a):=f1(a),..., fn(a). Definition 1.2 (Uniform realizability interpretation) Let a base interpretation of L(S)into L(T)be given. For each formula A of S, possibly with free-variables, associate a formula aur A (auniformly realises A) of T, by induction on A. For atomic formulas P(x)the interpretation is as in the base interpretation: aur P(x):≡x◁Pa. So, auniformly realizes P(x)if xis P-bounded by a. For composite formulas the interpretation is defined as follows: a,bur A ∧B:≡(aur A)∧(bur B)aur ∃xA(x):≡ ∃x(aur A(x)) fur A →B:≡ ∀a((aur A)→(f(a)↓)∧(f(a)ur B)) aur ∀xA(x):≡ ∀x(aur A(x)). Definition 1.3 (Realizable sequents and formulas) For a fixed base interpretation of L(S), we say that a sequent Γ⊢A of Sis realizable if for some λ-term t[γ]of T, with γas the only free-variables, we have (γ↓),(γur Γ)⊢T(t[γ]↓)∧(t[γ]ur A). A closed formula A is realizable if the sequent ⊢TA is realizable. 2Uniform Realizability Interpretations Theorem 1.4 (Soundness) Given a base interpretation of L(S), if all the non-logical axioms of Sare realizable then all the theorems of Sare realizable. Definition 1.2 describes how we can extend a given base interpretation to a full interpretation. Consider now a concrete source theory: Heyting (intuitionistic) arithmetic HA formulated with three predicate symbols: falsity ⊥(nullary), natural number N(unary), and equality =(binary). This means that in HA we have three kinds of atomic formulas: ⊥(falsity), N(n)(nis a number), and n=m(equality). We can then look at particular choices of base interpretation for HA and show that the full interpretations obtained coincide with (or are very close to) various well-known realizability interpretations of HA. We carry this out for the following five interpretations: Kleene’s number realizability [7]. This is based on the partial combinatory algebra K1, i.e. realizers are natural numbers and application is partial recursive function application {e}(a). The target theory is in this case HA (in the traditional formulation, i.e. without the predicate N) and the base interpretation of the three predicate symbols of HA is ⟨⟩ ◁⊥⟨⟩ :≡ ⊥ x◁Nn:≡x=n(x,y)◁=⟨⟩ :≡x=y. Due to the particular interpretation of equality, realizability for the ‘qualified’ quantifiers ∃NxA(x):= ∃x(N(x)∧A(x)) and ∀NxA(x):=∀x(N(x)→A(x)) is equivalent to the usual interpretation, i.e. writing “arA” for this instance of the uniform realizability interpretation, m,ar∃NxA(x)⇔arA(m)er∀NxA(x)⇔ ∀m({e}(m)↓∧{e}(m)rA(m). Kreisel’s modified realizability [8]. Here, the realizers are Gödel’s finite-type primitive recursive functionals, formalised in Gödel’s system T. The base interpretation as the same as for Kleene realizability, but, since the primitive recursive functions are total, definedness statements a↓can be omitted. Classical realizability [3, 4]. This is the same as modified realizability except that, to extract computational content from negated formulas, ⊥is given a computational meaning. The interpretation can be seen as a combination of modified realizability and Friedman and Dragalin A-translation [5, 6]. The base interpretation is ⟨⟩ ◁⊥a:≡P(a)x◁Nn:≡x=n(x,y)◁=a:≡(x=y)∨P(a). If we write “amr⊥A” for this instance of uniform realizability, we have a mr⊥A⇔A∨P(a)for every atomic formula A. Herbrand realizability [9]. In this case we have an extra predicate st, for standard natural numbers, with base interpretation x◁st S≡x∈S where Sranges over finite sets of (standard) natural numbers. Otherwise, the interpretation is as for modified realizability, except that internal quantifiers are treated as unqualified quantifiers (uniformly). Of major interest are the ‘external’ quantifiers ∃stxA(x):=∃x(st(x)∧A(x)) and ∀stxA(x):=∀x(st(x)→ A(x)) whose Herbrand realizability interpretations are S,ahr ∃stxA(x)⇔ ∃n∈Sahr A(n)fhr ∀stxA(x)⇔ ∀S∀n∈Sf(S)hr A(n) U. Berger & P. Oliva 3 Aschieri-Berardi learning realizability [1]. In this interpretation the goal is to extract computational content from proofs in HA plus the law of excluded middle for Σ0 1-formulas. To this end, Gödel’s primitive recursive functionals are extended by a new base type of states, where a state is a finite set of triples (P,n,m)such that mis a witness of the Σ0 1-formula ∃xP(n,x). The base interpretation depends now on a fixed state s: ⟨⟩ ◁s ⊥γ:≡γ(s)=s x ◁s Nα:≡α(s) = x(x,y)◁s =γ:≡γ(s) = s→(x=y). The intuition is that atomic formulas are realized by a state transformer γas long as sis not a fixed point of γ, and the property of being a natural number is realized by a a state-dependent number α. Aschieri and Berardi show that the realizer extracted from a proof of a Σ0 1-formula is a state transformer that, when iterated starting with the empty state, eventually reaches a fixed point of γwhich then contains a correct witness for the proven formula. References [1] F. Aschieri and S. Berardi. Interactive learning-based realizability for Heyting arithmetic with EM1.Logical Methods in Computer Science, 6 (issue 3, paper 19):1–22, 2010. [2] U. Berger. Uniform Heyting arithmetic. Annals of Pure and Applied Logic, 133:125–148, 2005. [3] U. Berger and P. Oliva. Modified bar recursion. BRICS Report Series RS-02-14 (23 pages), BRICS – Basic Research in Computer Science, 2002. http://www.brics.dk/RS/02/14/BRICS-RS-02-14.ps.gz. [4] U. Berger and P. Oliva. Modified bar recursion and classical dependent choice. Lecture Notes in Logic, 20:89–107, 2005. [5] A. G. Dragalin. New kinds of realizability and the Markov rule. Dokl. Akad. Nauk. SSSR (Russian), 251:534– 537, 1980. English translation: Soviet Math. Dokl. 21, pp. 461-464 (1980). [6] H. Friedman. Classically and intuitionistically provably recursive functions. In D. Scott and G. Müller, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21–28. Springer, Berlin, 1978. [7] S. C. Kleene. On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic, 10:109– 124, 1945. [8] G. Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101–128. North Holland, Amsterdam, 1959. [9] B. van den Berg, E. Briseid, and B. Safarik. A functional interpretation for nonstandard arithmetic. Annals of Pure and Applied Logic, 163(12):1962–1994, 2012.