A TOPOS FOR A NONSTANDARD FUNCTIONAL INTERPRETATION BENNOVANDENBERG 3 1 0 2 Abstract. Weintroduceanewtoposinordertogiveasemanticaccountofthenonstandard n functionalinterpretationintroducedbyEyvindBriseid,PavolSafarikandtheauthor. a J 6 1. Introduction 1 The aimof this short note is to give a semantic,topos-theoretic accountof the nonstandard ] T functional interpretation which the author, together with Eyvind Briseid and Pavol Safarik, C introduced in [2], thus answering a question the author left open in [1]. In this way this note is similar to the author’s paper on the Herbrand topos [1], which did the same for Herbrand . h realizability,arealizabilityinterpretationwealsointroducedin[2]. Indeed,agoodwaytothink t a about the topos to be defined here is as a Herbrandized version of the modified Diller-Nahm m topos (for which see [4, 3]). [ 1 2. Notation v 9 Let us first establish some notation. We assume that we have fixed some pairing function, 7 coding pairs of natural numbers as natural numbers. We will not distinguish notationally 6 between pairs and codes of pairs and write (n,m) for both the pair consisting of n and m 3 . and its code. Also, Kleene application will be written as ordinary application, so the result 1 of applying the nth recursive function to the argument m is written as n(m), whenever it is 0 3 defined. 1 For X,Y ∈Pow(N), we will write : v X ×Y = {(x,y)∈N: x∈X,y ∈Y}, i X X +Y = {(0,x):x∈X}∪{(1,y): y ∈Y}, r a X →Y = {a∈N: (∀x∈X)a(x) is defined and a(x)∈Y}, as usual. In addition, we will write X∗ ={a∈N: a codes a finite set all whose elements belong to X}. Note that the empty set always belongs to X∗. We will use common set-theoretic notation when manipulating elements of X∗. We will always regard X∗ as a (pre)order, ordered by inclusion. Also note that we have an “exponential isomorphism” (X +Y)∗ ∼= X∗ ×Y∗, which is not just a bijection, but also an order-isomorphism (if we order X∗×Y∗ in the standard way). In what follows, we will often implicitly use this isomorphism and regard elements of (X +Y)∗ as pairs (a,b) with a ∈ X∗ and b∈Y∗. Date:January16,2013. 1 2 BENNOVANDENBERG It will also be convenientto introduce the following piece of notation: if x∈(S →T∗)∗ and y ∈S, then we will write x[y]:= [ z(y)∈T∗. z∈x Another thing which we often implicitly use is that x⊆x′ implies x[y]⊆x′[y] for all y. 3. Definition of the tripos We define an preorder indexed over the category of sets and then show it is a tripos. First of all, we put Σ = {(X,Y,R)∈Pow(N)2×Pow(N×N): R⊆X∗×Y st and (∀x,x′ ∈X∗,y ∈Y)(x,y)∈R,x⊆x′ →(x′,y)∈R}. For p=(X,Y,R)∈Σ we will write st p+ = X, p++ = X∗, p− = Y, p(x,y) = R(x,y), respectively. Definition 3.1. For any set I the preorder above I consists of functions I → Σ . We write st ⊢ for its preorder structure and we will have ϕ⊢ ψ iff there exist I I e+ ∈ \ϕ+i + →ψi++ i∈I e− ∈ \ϕ+i +×ψi− →(ϕ−i )∗ i∈I such that ∀i∈I,a∈ϕ++,b∈ψ−[∀c∈e−(a,b)ϕ (a,c)→ψ (e+(a),b)]. i i i i Reindexing is simply given by precomposition. Lemma 3.2. This defines an indexed preorder. Proof. p⊢p is realizedby e+(x)=x,e−(x,y)={y}. In addition, if (e+,e−) realizes p⊢q and (f+,f−) realizes q ⊢ r, then p ⊢ r is realized by (g+,g−) with g+(x) = f+(e+(x)),g−(x,z) = e−(x,y). The preorder structure is obviously stable along reindexing. (cid:3) Sy∈f−(e+(x),z) Theorem 3.3. The indexed preorder defined above is a tripos. WewillcalltheassociatedtopostheD -topos anddenoteitbyDst. Thefollowingsequence st of lemmas will prove Theorem 3.3. Lemma 3.4. Truth is given by (∅,∅,∅) and falsity by (∅,{0},∅). Lemma 3.5. The conjunction p∧q is given by (p∧q)+ = p++q+, (p∧q)− = p−+q−, (p∧q)((n,m),(i,k)) ⇔ i=0∧p(n,k) or i=1∧q(m,k) . (cid:0) (cid:1) (cid:0) (cid:1) A TOPOS FOR A NONSTANDARD FUNCTIONAL INTERPRETATION 3 Proof. Note that we have used the exponential isomorphism (X +Y)∗ ∼=X∗×Y∗ in order to identify (p∧q)++ with p++×q++. We will keep on making this identification. Theprojectionp∧q ⊢pisrealizedbye+(a,b)=aande−((a,b),c)=({c},∅),whilep∧q ⊢q is realized by e+(a,b)=b and e−((a,b),c)=(∅,{c}). Now suppose r ⊢ p is realized by (e+,e−), while r ⊢ q is realized by (f+,f−). Then r ⊢p∧q is realized by g+(x)=(e+(x),f+(x)) and g−(x,(0,y))=e−(x,y) and g−(x,(1,y))= f−(x,y). (cid:3) Lemma 3.6. The disjunction p∨q is given by (p∨q)+ = p++q+, (p∨q)− = p−×q−, (p∨q)((n,m),(k,l)) ⇔ p(n,k) or q(m,l). Proof. Again, we identify (p∨q)++ with p++×q++. First, the inclusions. p ⊢ p∨q is realized by e+(x) = (x,∅) and e−(x,(y,z)) = {y}, while q ⊢p∨q is realized by e+(x)=(∅,x) and e−(x,(y,z))={z}. Now suppose p⊢r is realized by (e+,e−), i.e., ∀a∈p++,b∈r−[∀c∈e−(a,b)p(a,c)→r(e+(a),b)], while q ⊢r is realized by (f+,f−), i.e., ∀a∈q++,b∈r−[∀c∈f−(a,b)q(a,c)→r(f+(a),b)]. Then,weclaim,p∨q ⊢r isrealizedbyg+(x,y)=e+(x)∪f+(x)andg−((x,y),z)={(s,t): s∈ e−(x,z),t∈f−(y,z)}. Because we have for all x∈p++,y ∈q++,z ∈r− that: ∀(s,t)∈g−((x,y),z) p(x,s)∨q(y,t) → (cid:0) (cid:1) ∀s∈e−(x,z),t∈f−(y,z) p(x,s)∨q(y,t) → (intuitionistic logic) (cid:0) (cid:1) ∀s∈e−(x,z)p(x,s)∨∀t∈f−(y,z)q(y,t) → r(e+(x),z)∨r(f+(y),z) → (upwards closure in first component) r(g+(x,y),z). (cid:3) Lemma 3.7. The implication p→q is given by (p→q)+ = (p++ →q++)+(p++×q− →(p−)∗) (p→q)− = p++×q−, (p→q)((e+,e−),(a,b)) ⇔ ∀c∈e−[(a,b)]p(a,c) →q(e+[a],b). (cid:0) (cid:1) Proof. Suppose (e+,e−) realizes r∧p⊢q. Then r ⊢(p→q) is realized by f+(x) = ({λy.e+(x,y)},{λy,z.π e−((x,y),z)}), 2 f−(x,(y,z)) = π e−((x,y),z). 1 Conversely, if (e+,e−) realizes r⊢(p→q), then r∧p⊢q is realized by: f+(x,y) = (π e+(x))[y], 1 f−((x,y),z) = (e−(x,(y,z)),(π e+(x))[(y,z)]). 2 (cid:3) 4 BENNOVANDENBERG Lemma 3.8. For u:I →J and ϕ:I →Σ universal quantification is given by: st ∀u(ϕ)+j = \[u(i)=j]→ϕ+i + i∈I ∀u(ϕ)−j = [ ϕ−i i∈u−1(j) ∀ (ϕ) (a,b) ⇔ (∀i∈u−1(j)) b∈ϕ− →ϕ (a[0],b) . u j (cid:0) i i (cid:1) Here [i=j]={0: i=j}. Also the Beck-Chevalley condition holds. Proof. Suppose ϕ:I →Σ and ψ:J →Σ . We have to show the equivalence of the following st st two statements: (a) ψ ⊢ ∀ (ϕ), i.e., there exist J u e+ ∈ \ ψj++ →∀u(ϕ)+j+ and e− ∈ \ ψj++×∀u(ϕ)−j →(ψj−)∗ j∈J j∈J such that ∀j ∈J,a∈ψ++,b∈∀ (ϕ)− ∀c∈e−(a,b)ψ (a,c) →∀ (ϕ) (e+(a),b). j u j (cid:0) j (cid:1) u j (b) u∗ψ ⊢ ϕ, i.e., there exist I f+ ∈ \ψu+(+i) →ϕ+i + and f− ∈ \ ψu+(+i)×ϕ−i →(ψu−(i))∗ i∈I i∈I such that ∀i∈I,a∈ψ++,b∈ϕ− ∀c∈f−(a,b)ψ (a,c) →ϕ (f+(a),b). u(i) i (cid:0) u(i) (cid:1) i (a)⇒(b): Takef+(x)=e+(x)[0]andf−(x,y)=e−(x,y). Nowleti∈I,a∈ψ++,b∈ϕ− and u(i) i suppose for all c ∈ f−(a,b) we have ψ (a,c). Then ∀ (ϕ) (e+(a),b) and ϕ (e+(a)[0],b), u(i) u u(i) i hence ϕ (f+(a),b), as desired. i (b) ⇒ (a): Take e+(x)={λy.f+(x)} and e−(x,y)=f−(x,y). Then let j ∈J,a∈ψ++,b∈ j ∀ (ϕ)− andsupposeforeveryc∈e−(a,b)wehaveψ (a,c). We wanttoshow∀ (ϕ) (e+(a),b), u j j u j i.e., (∀i∈u−1(j)) b∈ϕ− →ϕ (f+(a),b) . But this is immediate from (b). (cid:0) i i (cid:1) Validity of the Beck-Chevalley condition is immediate. (cid:3) Lemma 3.9. For u:I →J and ϕ:I →Σ existential quantification is given by: st ∃u(ϕ)+j = [ ϕ+i + i∈u−1(j) ∃u(ϕ)−j = \ ϕ+i + →(ϕ−i )∗ i∈u−1(j) ∃ (ϕ) (a,b) ⇔ (∃i∈u−1(j))(∃s ∈a) s∈ϕ++∧(∀c∈b(s))ϕ (s,c) . u j (cid:0) i i (cid:1) Also the Beck-Chevalley condition holds. Proof. Suppose ϕ:I →Σ and ψ:J →Σ . We have to show the equivalence of the following st st two statements: A TOPOS FOR A NONSTANDARD FUNCTIONAL INTERPRETATION 5 (a) ∃ (ϕ)⊢ ψ, i.e., there exist u J e+ ∈ \ ∃u(ϕ)+j+ →ψj++ and e− ∈ \ ∃u(ϕ)+j+×ψj− →(∃u(ϕ)−j )∗ j∈J j∈J such that ∀j ∈J,a∈∃ (ϕ)++,b∈ψ− ∀c∈e−(a,b)∃ (ϕ) (a,c) →ψ (e+(a),b). u j j (cid:0) u j (cid:1) j (b) ϕ⊢ u∗ψ, i.e., there exist I f+ ∈ \ϕ+i + →ψu+(+i) and f− ∈ \ϕ+i +×ψu−(i) →(ϕ−i )∗ i∈I i∈I such that ∀i∈I,a∈ϕ++,b∈ψ− ∀c∈f−(a,b)ϕ (a,c) →ψ (f+(a),b). i u(i)(cid:0) i (cid:1) u(i) (a) ⇒ (b): Take f+(x) = e+({x}) and f−(x,y) = e−({x},y)[x] = {z(x): z ∈ e−({x},y)}. S Now let i∈I,a∈ϕ++,b∈ψ− and suppose for all c∈f−(a,b) we have ϕ (a,c). Hence i u(i) i (∀d∈e−({a},b))(∀c∈d(a))ϕ (a,c). i Writing j =u(i), we have {a}∈∃ (ϕ)++ and b∈ψ− and u j j (∀d∈e−({a},b))∃ (ϕ) ({a},d). u j Therefore ψ (e+({a}),b), i.e., ψ (f+(a),b). j u(i) (b) ⇒ (a): Take e+(x) = f+(z) and e−(x,y) = {λz.f−(z,y)}. Then let j ∈ J,a ∈ Sz∈x ∃ (ϕ)++,b ∈ ψ− and suppose for every d ∈ e−(a,b) we have ∃ (ϕ) (a,d). Concretely, this u j j u j means that there is an i ∈ u−1(j) and an s ∈ a such that s ∈ ϕ++ and ϕ (s,c) for all i i c∈f−(s,b). This implies ψ (f+(s),b), whence ψ (e+(a),b), because ψ is upwards closedin u(i) j j the first component. Validity of the Beck-Chevalley condition is immediate. (cid:3) Lemma 3.10. The generic predicate is given by the identity on Σ . st Proof. Clear. (cid:3) This completes the proof of Theorem 3.3. 4. Open questions We have defined a new topos, but have not established any of its basic properties. Given the state of the art, we would conjecture the following: (1) Like the modified Diller-Nahm topos DN the topos we have defined is not 2-valued m and its ¬¬-sheaves do not coincide with the category of sets (see [4, 3]). (2) First-orderarithmeticinthe toposwe constructedisgivenbythe D -interpretationof st [2] combined with using HRO as one’s models of G¨odel’s T. (3) As with the Herbrand topos, the functor ∇:Sets → Dst preserves and refllects (at least) first-order logic, but not the natural numbers object. Hence ∇N is a model of nonstandard arithmetic in the D -topos (see [1]). st 6 BENNOVANDENBERG (4) As Jaap van Oosten has shown that the Herbrand topos Her is a subtopos of the modified realizability topos Mod and it is known that there is a connected geometric morphism from the modified Diller-Nahm topos DN to the modified realizability m topos Mod (see [3]), one would expect the D -topos to be a subtopos of DN and st m there to be a connected geometric morphism from it to the Herbrand topos. Indeed, one would expect there to be a commuting square (pullback?) of toposes Dst //DN m (cid:15)(cid:15) (cid:15)(cid:15) Her //Mod in which the horizontal arrows are inclusions of toposes and the vertical ones are con- nected geometric morphisms. References [1] B.vandenBerg.TheHerbrandtopos. arXiv:1112.3837,2012. [2] B. van den Berg, E. Briseid, and P. Safarik. A functional interpretation for nonstandard arithmetic. Ann. Pure Appl. Logic,163(12):1962–1994, 2012. [3] B.Biering.Dialectica Interpretations: A Categorical Analysis.PhDthesis,2008.Availablefromthehome- pageofLarsBirkedal. [4] T.Streicher.AsemanticversionoftheDiller-NahmvariantofG¨odel’sDialecticainterpretation.Unpublished noteavailablefromtheauthor’shomepage, 2006.