Jean-Louis Krivine
email: krivine@pps.jussieu.fr

R S P P S Team

Realizability in classical logic

Remarks

Indeed, the implication ⇐ is obvious. Conversely, if ⊥ ⊥ 6 = ∅, let t ? π ∈ ⊥ ⊥ ; then k π t ? ρ Â t ? π ∈ ⊥ ⊥ for every stack ρ, and therefore k π t ∈ |⊥|.

Introduction

The essential aim is to explore the Curry-Howard correspondence : we want to associate a program with each mathematical proof and to consider each theorem as a specification, i.e. to find the common behavior of the programs associated with every proof of this theorem. It is a very difficult and very interesting problem, which I call the '' specification problem '' in what follows.

In the first place, we must give the programming language in which we write these programs, and also explain in which way they are executed. This is done in the first section, it is the '' program side '' of the correspondence. As we shall see, this programming frame is very similar to usual imperative programming. As the theory develops, many usual and important notions of imperative and system programming will naturally appear, such as : storage and call-by-value for datas, pointers, signature of files, system clock, boot, . . . Then we must give a computational content to each logical rule and each axiom. We do this by means of elementary instructions. The instructions for the rules of intuitionistic propositional logic have been found long time ago, at the very discovery of the Curry-Howard correspondence ; the programming language was Church's lambda-calculus. Then the instructions for intuitionistic second order logic were obtained and the programming language was still the same. But mathematical proofs are not done in intuitionistic logic, not even in pure classical logic. We need axioms and the usual axiom systems are :

1. Second order classical Peano arithmetic with the axiom of dependent choice ; this system is also called '' Analysis ''.

2. Zermelo-Fraenkel set theory with the axiom of choice.

In this paper, we consider the first case. We shall give new elementary instructions for the lacking axioms, which are : the excluded middle, the axiom of recurrence and the axiom of dependent choice. It is necessary, for that, to define an extension of lambda-calculus. We notice that some of these instructions are incompatible with β-reduction. Therefore the execution strategy is deterministic and is given in the form of a weak head reduction machine. The same machine is used for Zermelo-Fraenkel set theory. The instructions associated with 1 the axioms of ZF are given in [START_REF] Krivine | Typed lambda-calculus in classical Zermelo-Fraenkel set theory[END_REF]. The full axiom of choice remained an open problem until recently (may 2005). The new instructions necessary for this axiom and also for the continuum hypothesis will be given in a forthcoming paper.

Terms, stacks, processes, execution

We denote by PL the set of closed λ-terms built with some set of constants which are called instructions ; one of these instructions is denoted by cc. We shall denote the application of t to u by (t)u or tu ; the application of t to n arguments u 1 ,. . . ,u n is denoted by (t)u 1 . . . u n or tu 1 . . . u n . Therefore, we have tuv = (t)uv = (tu)v with this notation. Elements of PL are called proof-like terms.

Let L ⊃ PL be the set of closed λ-terms built with a new constant k and a set Π 0 6 = ∅ of new constants called stack constants.

A closed λ-term of L of the form kt 1 . . . t n π 0 with n ∈ N, t 1 , . . . , t n ∈ L and π 0 ∈ Π 0 is called a continuation.

A λ c -term is, by definition, a closed λ-term τ ∈ L with the following properties :

-each occurrence of k in τ appears at the beginning of a subterm of τ which is a continuation ; -each occurrence of a stack constant in τ appears at the end of a subterm of τ which is a continuation.

Remark. Proof-like terms are therefore λ c -terms which do not contain the symbol k or, which amounts to the same thing, which do not contain any stack constant.

The set of λ c -terms is denoted by Λ c . In what follows, we almost always consider only λ c -terms ; so, they will be called simply '' terms '' or '' closed terms ''.

Lemma 1. i) PL ⊂ Λ c ; ii) If tu ∈ Λ c and u / ∈ Π 0 , then t ∈ Λ c and u ∈ Λ c ; iii) If tu ∈ Λ c and u ∈ Π 0 , then tu is a continuation ; iv) If λx t, u ∈ Λ c , then t[u/x] ∈ Λ c ; v) If t 1 , . . . , t n ∈ Λ c (n ∈ N) and π 0 ∈ Π 0 , then (k t 1 . . . t n )π 0 ∈ Λ c . i) Trivial.

ii) Consider an occurrence of k (resp. of a stack constant π 0 ) in t or u ; it is therefore in tu. Since tu ∈ Λ c , this occurrence is at the beginning (resp. at the end) of a continuation kt 1 . . . t n π 0 = (kt 1 . . . t n )π 0 which is a subterm of tu. Now u 6 = π 0 , so that this subterm is not tu itself ; thus, kt 1 . . . t n π 0 is a subterm of t or u. iii) We have u = π 0 ∈ Π 0 and this occurrence of π 0 is at the end of a subterm of tπ 0 which is a continuation (kt 1 . . . t n )π 0 . Therefore, this subterm is tπ 0 itself. iv) Consider an occurrence of k (resp. π 0 ) in t[u/x] ; thus, it is in λx t or u. But λx t, u ∈ Λ c , so that this occurrence is at the beginning (resp. at the end) of a continuation kt 1 . . . t n π 0 which is a subterm of λx t or u. If this continuation is a subterm of u, it is also a subterm of t[u/x]. If it is a subterm of λx t, then this occurrence of k (resp. π 0 ) in t[u/x] is at the beginning (resp. at the end) of the subterm kt 1 [u/x] . . . t n [u/x]π 0 , which is a continuation. v) Trivial.

Q.E.D.

If t 1 , . . . , t n ∈ Λ c (n ∈ N) and π 0 ∈ Π 0 , the sequence π = (t 1 , . . . , t n , π 0 ) is called a stack and is denoted by t 1 .t 2 . . . t n .π 0 ; the set of stacks is denoted by Π. The continuation kt 1 . . . t n π 0 is denoted by k π . If t ∈ Λ c and π = t 1 .t 2 . . . t n .π 0 ∈ Π, then the stack t.t 1 .t 2 . . . t n .π 0 is denoted by t.π. Thus, the dot is an application of Λ c ×Π in Π. Every term τ ∈ Λ c is either an application, or an abstraction, or a constant which is an instruction (indeed, this term can be neither k, nor a stack constant, by definition of λ c -terms). From lemma 1, it follows that, for every τ ∈ Λ c , we are in one and only one of the following cases : i) τ is an application tu with u / ∈ Π 0 (and therefore t, u ∈ Λ c ) ; ii) τ is an abstraction λx t ; iii) τ is an instruction (particular case : τ = cc) ; iv) τ is an application tu with u ∈ Π 0 , i.e. τ = k π for some stack π.

A process is an ordered pair (τ, π) with τ ∈ Λ c , π ∈ Π. It is denoted by τ ? π ; τ is called the head or the active part of the process. The set of all processes will be denoted by Λ c ? Π.

We describe now the execution of processes, which is denoted by Â. We give the rule to perform one execution step of the process τ ? π. It depends on the form (i), . . . , (iv) of τ given above. In the four rules that follow, t, u, λx v denote elements of Λ c ; π, ρ denote stacks. i) tu ? π Â t ? u.π (push) ; ii) λx v ? u.π Â v[u/x] ? π (pop) ; iii) cc ? t.π Â t ? k π .π (store the stack) ; the rule for other instructions will be given in due time ; iv) k π ? t.ρ Â t ? π (restore the stack). We say that the process t ? π reduce to t 0 ? π 0 (notation t ? π Â t 0 ? π 0 ) if we get t 0 ? π 0 from t ? π by means of a finite (possibly null) number of execution steps.

Remark.

By lemma 1, we can check that the four execution rules give processes when applied to processes.

Truth values and types

Consider an arbitrary set of processes, which is denoted by ⊥ ⊥ and which we suppose ccsaturated ; it means that :

t ? π ∈ ⊥ ⊥, t 0 ? π 0 Â t ? π ⇒ t 0 ? π 0 ∈ ⊥ ⊥. P(Π) is called the set of truth values. If U ⊂ Π is a truth value and t ∈ Λ c , we say that t realizes U (notation t k-U ) if (∀π ∈ U ) t ? π ∈ ⊥ ⊥. The set {t ∈ Λ c ; t k-U} will be denoted by |U |. Thus, we have | S i∈I U i | = T i∈I |U i |.
The truth value ∅ (resp. Π) is called true (resp. false) and denoted by > (resp. ⊥). Thus, we have |>| = Λ c ; t ∈ |⊥| ⇔ t ? π ∈ ⊥ ⊥ for every stack π ∈ Π. Whenever U, V are truth values, we define the truth value :

(U → V ) = {t.π; t k-U, π ∈ V } ; we put ¬U = (U → ⊥).
We shall sometimes use the following notation, when V is a truth value and A ⊂ Λ c :

(A → V ) = {t.π; t ∈ A, π ∈ V }. For example, {t} → V is the truth value {t.π; π ∈ V } if t ∈ Λ c and V ⊂ Π. With this notation, U → V is the same as |U | → V , for U, V ⊂ Π.
Types are usual formulas of second order logic, written in the following language : the only logical symbols are → and ∀ ; we have function symbols of arity k which are functions from N k into N and predicate symbols of arity k which are applications from N k into P(Π) (k is any integer ≥ 0). First order variables (also called individual variables) are denoted by x, y, . . . ; second order variables (also called predicate variables) are denoted by X, Y, . . . Each second order variable has an arity which is an integer. Predicate variables of arity 0 are also called propositional variables.

Notations.

The formula

F 0 → (F 1 → . . . → (F n → G) . . .) is denoted by F 0 , F 1 , . . . , F n → G. ⊥ is defined by ∀X X ; ¬F by F → ⊥ ; F ∨ G by ∀X[(F → X), (G → X) → X] ; F ∧ G by ∀X[(F, G → X) → X] ; ∃Y F [Y ] by ∀X{∀Y (F [Y ] → X) → X} ; ∃y F [y] by ∀X{∀y(F [y] → X) → X} ; We use the notation ∃Y {F 1 [Y ], . . . , F k [Y ]} for the formula : ∀X{∀Y (F 1 [Y ], . . . , F k [Y ] → X) → X} ;
we have the same notation for the first order existential quantifier.

(In all these formulas, X is a propositional variable and Y has an arbitrary arity). x = y is defined by ∀X(Xx → Xy) (where X has arity 1). Let x 1 , . . . , x k be individual variables, X a predicate variable of arity k, A and F arbitrary formulas. Then, we define A[F/Xx 1 . . . x k ] by induction on (the length of) A :

If X is not free in A, then A[F/Xx 1 . . . x k ] is A. If A is X(t 1 , . . . , t k ), then A[F/Xx 1 . . . x k ] is F [t 1 /x 1 , . . . , t k /x k ]. (A → B)[F/Xx 1 . . . x k ] is A[F/Xx 1 . . . x k ] → B[F/Xx 1 . . . x k ]. (∀y A)[F/Xx 1 . . . x k ] is ∀y A[F/Xx 1 . . . x k ]. (∀Y A)[F/Xx 1 . . . x k ] is ∀Y A[F/Xx 1 . . . x k ] if Y is
a predicate variable which is 6 = X (as usual, we assume that y et Y are not free in F ). When F is an atomic formula of the form R(x 1 , . . . , x k ), where R is either a second order variable of arity k, or a parameter (R ∈ P(Π) N k ), we write also A

[R/X] instead of A[F/Xx 1 . . . x k ].
We now give the deduction rules for classical second order logic and, at the same time, the typing rules for λcc-terms, which are the usual λ-terms (possibly not closed) written with the constant cc ; in such an expresssion as '' t : A '', t is a λcc-term and A is a type, i.e. a second order formula.

Let Γ be a context, i.e. an expression of the form x

1 : A 1 , . . . , x n : A n . 1. Γ `xi : A i (1 ≤ i ≤ n) 2. Γ `t : A → B, Γ `u : A ⇒ Γ `tu : B. 3. Γ, x : A `t : B ⇒ Γ `λx t : A → B. 4. Γ `t : (A → B) → A ⇒ Γ `cc t : A. 5. Γ `t : A ⇒ Γ `t : ∀x A (resp. ∀X A) if x (resp. X) is not free in Γ. 6. Γ `t : ∀x A ⇒ Γ `t : A[τ /x] for every term τ of L. 7. Γ `t : ∀X A ⇒ Γ `t : A[F/Xx 1 . . . x k ] for every formula F .
Rule 4 uses the interpretation of Griffin [START_REF] Griffin | A formulae-as-type notion of control[END_REF] for the law of Peirce. Rule 7 uses Takeuti's interpretation for the comprehension scheme.

Let A be a closed second order formula with first order parameters in N and second order parameters of arity k in P(Π) N k for each integer k. We define below its truth value, which is denoted by kAk. We denote by |A| the set of terms in Λ c which realize A, i.e. |A| = {t ∈ Λ c ; (∀π ∈ kAk) t ? π ∈ ⊥ ⊥}. We write t k-A (read '' t realizes A '') if t ∈ |A|. The definition of kAk is given by induction on A : If A is atomic, i.e. A ≡ R(t 1 , . . . , t k ), then t 1 , . . . , t k are closed terms and R ∈ P(Π) N k is a second order parameter. Let a i ∈ N be the value of t i ; then, we put : kR(t 1 , . . . , t k )k = R(a 1 , . . . , a k ) ⊂ Π.

The other steps of induction are as follows :

kA → Bk = {t.π ; t ∈ |A|, π ∈ kBk} ; k∀x Ak = [ a∈N kA[a/x]k ; (and therefore |∀x A| = \ a∈N |A[a/x]|) ; k∀X Ak = [ {kA[R/X]k; R ∈ P(Π) N k } if X is a predicate variable of arity k (and therefore |∀X A| = \ {|A[R/X]|; R ∈ P(Π) N k }).
We get k⊥k = Π and |⊥| is the least truth value. There is a greatest truth value, denoted by >, which is ∅ ; thus, |>| = Λ c .

The following theorem shows that realizability is compatible with deduction in classical second order logic. It is an essential tool in this theory.

Theorem 2 (Adequation lemma).

Let A 1 , . . . , A k , A be closed formulas such that x 1 : A 1 , . . . , x k : A k `t : A is provable with the rules above.

If t i k-A i for 1 ≤ i ≤ k, then t[t 1 /x 1 , . . . , t k /x k ] k-A.
In particular, if A is a closed formula and `t : A is provable, then t k-A.

The following lemma is a stronger, but more complicated, form of this theorem ; it is suitable for a proof by induction.

Lemma 3.

Let A 1 , . If it is rule 2, we have t = uv and Γ `u : A → B, v : A. We must show that t 0 ∈ |B 0 |, that is u 0 v 0 ? π ∈ ⊥ ⊥ for every stack π ∈ kB 0 k. But u 0 v 0 ? π Â u 0 ? v 0 .π, hence the result since, by induction hypothesis, we have

u 0 ∈ |A 0 → B 0 |, v 0 ∈ |A 0 | and thus v 0 .π ∈ kA 0 → B 0 k. If it is rule 3, we have t = λx u, A = (B → C) and Γ, x : B `u : C. We must show that λx u 0 ∈ |B 0 → C 0 |, that is λx u 0 ? π ∈ ⊥ ⊥ for every π ∈ kB 0 → C 0 k. Now, we have π = v.$ with v ∈ |B 0 | and $ ∈ kC 0 k. By induction hypothesis, we have u 0 [v/x] k-C 0 and therefore u 0 [v/x] ? $ ∈ ⊥ ⊥. Thus λx u 0 ? v.$ ∈ ⊥ ⊥, because ⊥ ⊥ is cc-saturated.
If it is rule 4, we have t = cc u and Γ `u

: (A → B) → A. We must show that t 0 ∈ |A 0 |, that is cc u 0 ? π ∈ ⊥ ⊥ for every π ∈ kA 0 k. Since ⊥ ⊥ is cc-saturated, it is sufficient to show that u 0 ? k π .π ∈ ⊥ ⊥. We first show that k π ∈ |A 0 → B 0 | : indeed, if v ∈ |A 0 | et ρ ∈ kB 0 k, then k π ? v.ρ Â v ? π ∈ ⊥ ⊥. Now,
∈ |B 0 [R/X]| for every R ∈ P(Π) N k . Thus t 0 ∈ |∀X B 0 | = |A 0 |. If it is rule 6, we have A = B[τ /x] and Γ `t : ∀x B. By induction hypothesis, we get t 0 ∈ |∀x B 0 |. But, if a ∈ N is the value of τ , we have |B 0 [τ /x]| = |B 0 [a/x]| ⊃ |∀x B 0 | and therefore t ∈ |B 0 [τ /x]| = |A 0 |.
If it is rule 7, we have A = B[Φ(z 1 , . . . , z p )/Xz 1 . . . z p ] and therefore : A 0 = B 0 [Φ 0 (z 1 , . . . , z p )/Xz 1 . . . z p ]. We have Γ `t : ∀X B and we must show that t 0 ∈ |A 0 |. By induction hypothesis, we know that t 0 ∈ |∀X B 0 | and the result follows from lemma 4.

Q.E.D. Lemma 4. Let Φ (resp. A) be a formula with parameters, with the only free variables z 1 , . . . , z p (resp. X of arity p). Define R ∈ P(Π) N p by : R(a 1 , . . . , a p ) = kΦ[a 1 /z 1 , . . . , a p /z p ]k for a 1 , . . . , a p ∈ N.

Then kA[Φ/Xz 1 . . . z p ]k = kA[R/X]k and therefore : kA[Φ/Xz 1 . . . z p ]k ⊂ k∀X Ak and |∀X A| ⊂ |A[Φ/Xz 1 . . . z p ]|. We show kA[Φ/Xz 1 . . . z p ]k = kA[R/X]k by induction on the length of A. The result is trivial if X is not free in A, if A is atomic, or if A = (B → C). If A = ∀x B, then kA[Φ/Xz 1 . . . z p ]k = S a∈N kB[Φ/Xz 1 . . . z p ][a/x]k = S a∈N kB[a/x][Φ/Xz 1 . . . z p ]k = S a∈N kB[a/x][R/X]k by induction hypothesis = S a∈N kB[R/X][a/x]k = k∀x B[R/X]k = kA[R/X]k. If A = ∀Y B, with Y of arity q and Y 6 = X, then : kA[Φ/Xz 1 . . . z p ]k = S {kB[Φ/Xz 1 . . . z p ][S/Y ]k; S ∈ P(Π) N q } = S {kB[S/Y ][Φ/Xz 1 . . . z p ]k; S ∈ P(Π) N q } = S {kB[S/Y ][R/X]k; S ∈ P(Π) N q } by induction hypothesis = S {kB[R/X][S/Y ]k; S ∈ P(Π) N q } = k∀Y B[R/X]k = kA[R/X]k. Q.E.D.
Remark. The terms we obtain by means of proofs in classical second order logic are λcc-terms, that is λ-terms with the constant cc, not necessarily closed. On the other hand, the terms which appear in processes are in Λ c (i.e. closed terms with instructions and continuations). The common elements are proof-like terms with the only instruction cc (hence the name '' proof-like '').

Theorem 5. For U, V ∈ P(Π),

we put U ≤ V ⇔ (∃θ ∈ PL) θ k-U → V . Suppose that ⊥ ⊥ is coherent, which means that (∀θ ∈ PL) θ 6k-⊥.
Then ≤ is a preorder (i.e. reflexive and transitive) and (P(Π), ≤) is a Boolean algebra.

Proof that ≤ is a preorder : if U ≤ V and V ≤ W , then there are ξ, η ∈ PL such that ξ k-U → V , η k-V → W . Therefore η•ξ k-U → W , hence U ≤ W . Proof that (P(Π), ≤) is a Boolean algebra : we have U ∧ V ≤ U and U ∧ V ≤ V (the proofs of U ∧ V → U and U ∧ V → V give the requested terms). Moreover, if Z ≤ U, V , then ξ k-Z → U, η k-Z → V thus λzλf ((f )(ξ)z)(η)z k-Z → U ∧ V . Therefore we have Z ≤ U ∧ V and U ∧ V = inf(U, V ).
In the same way, we get U ∨ V = sup(U, V ).

We have I k-⊥ → U and I k-U → >. Therefore ⊥ is the least element and > is the greatest. We have ¬U ∧ U ≤ ⊥ and > ≤ ¬U ∨ U since ¬U ∧ U → ⊥ and > → ¬U ∨ U are provable.

Thus ¬U is the complement of U.

It remains to show that > 6 ≤ ⊥. This clearly follows from the hypothesis that ⊥ ⊥ is coherent.

Q.E.D.
As soon as we choose a coherent set ⊥ ⊥, each closed formula with parameters is given a value in this Boolean algebra. The set T ⊥ ⊥ of formulas with value 1, i.e. formulas which are realized by a proof-like term, is a consistent theory which contains second order logic. We are interested in the models of this theory ; we call them generic models.

The case when ⊥ ⊥ = ∅ is trivial : the Boolean algebra is {0, 1} and we get back the standard model we started with.

We say that a closed formula F , with parameters, is realized if there exists a proof-like term θ such that θ k-F for any choice of the cc-saturated set ⊥ ⊥.

All axioms of second order logic are realized. Thus, generic models satisfy second order logic.

The tools we have built up to now are sufficient in order to solve the specification problem for some very simple valid formulas.

Theorem 6. If `θ : ∀X(X → X), then θ ? t.π Â t ? π for every t ∈ Λ c and π ∈ Π.

Given t and π, we put ⊥ ⊥ = {p ∈ Λ c ? Π; p  t ? π} and kXk = {π}. Thus, we have t k-X. But, by theorem 2, we have θ k-X → X, hence θ ? t.π ∈ ⊥ ⊥. It is exactly what we wanted to show.

Q.E.D.

We denote by Bool(x) the formula ∀X(X1, X0 → Xx), which is equivalent to x = 0 ∨ x = 1 in classical secod order logic.

Theorem 7. If `θ : Bool(1) (resp. Bool(0)), then θ ? t.u.π Â t ? π (resp. u ? π) for every t, u ∈ Λ c and π ∈ Π.

Given t and π, we put ⊥ ⊥ = {p ∈ Λ c ? Π; p  t ? π} and we define a unary parameter X by putting kX1k = {π}, kXnk = ∅ for n 6 = 1. Thus, we have t k-X1 and u k-X0.

If `θ : Bool(1), by theorem 2, we have θ k-X1, X0 → X1, hence θ ? t.u.π ∈ ⊥ ⊥, which is the result.

Q.E.D.
Remark. The meaning of these theorems is that the terms of type ∀X(X → X) (resp. Bool(1), Bool(0)) behave essentially like I = λx x (resp. λxλy x, λxλy y).

Axiom of recurrence and call by value

We should now realize the axiom of recurrence, which is : ∀x Int(x) where Int(x) is the formula ∀X[∀y(Xy → Xsy), X0 → Xx] that says that the individual x is an integer. Unfortunately, this axiom is not realized. It means that, in a generic model, there may be individuals which are not integers. Moreover, we shall see later that, in general, there may be also non standard integers in generic models.

In order to solve this problem, we introduce now some simple tools, which will appear essential in what follows.

We define a binary predicate constant, denoted by 6 =, by putting km 6

= nk = ∅ if m 6 = n and km 6 = nk = Π if m = n.
The following theorem shows that we can profitably use the formula x 6 = y instead of x = y → ⊥.

Theorem 8. The formula ∀x∀y[x 6 = y ↔ (x = y → ⊥)] is realized. Indeed :

λx xI k-∀x∀y[(x = y → ⊥) → x 6 = y] and λxλy yx k-∀x∀y[x 6 = y → (x = y → ⊥)]. We first check that |m = n| = |∀X(X → X)| if m = n and |m = n| = |> → ⊥| if m 6 = n. It is immediate, since m = n is the formula ∀X(Xm → Xn). We have to show that λx xI k-(m = n → ⊥) → m 6 = n and λxλy yx k-m 6 = n, m = n → ⊥ for every m, n ∈ N.
In the first case, we only need to check that :

λx xI k-(m = m → ⊥) → ⊥, which is obvious since I k-m = m.
In the second case, we must check that :

λxλy yx k->, m = n → ⊥ if m 6 = n and λxλy yx k-⊥, m = n → ⊥ if m = n
which is immediate, using the above computation of |m = n|.

Q.E.D.

Theorem 9. Suppose that θ ? k π .ρ ∈ ⊥ ⊥ for any stack π ∈ kXk and ρ ∈ kY k. Then :

V θ k-¬X → Y with V = λxλy(cc)λh(y)(cc)λk(h)(x)k. Let t k-¬X et ρ ∈ kY k. We must show that V θ ? t.ρ ∈ ⊥ ⊥ ; but V θ ? t.ρ Â V ? θ.t.ρ Â (cc)λh(t)(cc)λk(h)(θ)k ? ρ Â t ? (cc)λk(k ρ )(θ)k.ρ. Since t k-X → ⊥, it is therefore sufficient to prove that (cc)λk(k ρ )(θ)k k-X, in other words (cc)λk(k ρ )(θ)k ?π ∈ ⊥ ⊥ for every π ∈ kXk.
This is true because this process reduces into θ ? k π .ρ.

Q.E.D.

Remark.

With the notation introduced page 3, the hypothesis of theorem 9 is : θ k-{k π ; π ∈ kXk} → Y . Theorem 9 says that the set |¬X| behaves, in some sense, like its subset {k π ; π ∈ kXk} ; and it gives a simple way to check that X ∨ Y is realized.

Theorem 10 (Storage of integers). We put T = λf λn(nλg g•s)f 0, where s is a λ-term for the successor (for instance s = λnλf λx(f

)(n)fx). If φ ∈ Λ c is such that φ ? s n 0.π ∈ ⊥ ⊥ for every π ∈ kXk, then T φ k-Int[s n 0] → X.
Remarks.

1. With the notation introduced page 3, the hypothesis of theorem 10 is : φ k-{s n 0} → X.

Theorem 10 says that the set |Int[s n 0]| behaves, in some sense, like its subset {s n 0}.

2.
T is called a storage operator [START_REF] Krivine | A general storage theorem for integers in call-by-name λ-calculus[END_REF]. We understand intuitively its behavior by comparing the weak head reductions of φν and T φν, where φ and ν are λ-terms, ν ' β λf λx(f ) n x (Church integer). We get T φν Â (φ)(s) n 0, which means that the integer argument ν of φ is computed first. In other words, T simulate call by value in a weak head reduction, that is a call by name execution.

Note that we use the same symbol s for a λ-term and a function symbol of L.

Proof. Let ν k-Int[s n 0] and π ∈ kXk ; we must show that T φ ? ν.π ∈ ⊥ ⊥.

We define a unary predicate P by putting : kP (j)k = {s n-j 0.π} for 0 ≤ j ≤ n and kP (j)k = ∅ for j > n.

We have φ k-P 0 by hypothesis on φ.

Let us show that λg g•s k-∀x(P x → P sx), which means that λg g•s ∈ |P (j) → P (j + 1)| for every j ∈ N. It is trivial for j ≥ n.

If j < n, let ξ ∈ |P (j)| ; we must show that λg g•s ? ξ.s n-j-1 0.π ∈ ⊥ ⊥. But we have : λg g•s ? ξ.s n-j-1 0.π Â ξ •s ? s n-j-1 0.π Â ξ ? s n-j 0.π ∈ ⊥ ⊥ by hypothesis on ξ.

Now, we have T φ ? ν.π Â ν ? λg g•s.φ.0.π which is in ⊥ ⊥ because : ν k-∀x(P x → P sx), P 0 → P s n 0 by hypothesis, φ k-P 0 and 0.π ∈ kP s n 0k.

Q.E.D.

We are interested in the theory called Analysis or Second order Peano arithmetic, which is classical second order logic with the following supplementary axioms :

1. A set of equational formulas, i.e. formulas of the form :

∀x 1 . . . ∀x k [t(x 1 , . . . , x k ) = u(x 1 , . . . , x k )],
where t, u are terms which represent functions from N k into N. Of course, all these formulas are supposed to be true in N. For instance, we can take the following equational formulas, where 0, s, p, +, . are function symbols that represent respectively the integer 0, the successor function, the predecessor, the addition and multiplication on integers :

p0 = 0 ; ∀x(psx = x) ; ∀x(x + 0 = x) ; ∀x[x + sy = s(x + y)] ; ∀x(x.0 = 0) ; ∀x∀y[x.sy = x.y + x].
2. ∀x(0 6 = sx).

3. The recurrence axiom ∀x Int(x).

4. The axiom of dependent choice.

All equational axioms 1 are realized by I = λx x. Axiom 2 is realized by any proof-like term.

But there is a problem with axiom 3, as is shown by the following theorem :

Theorem 11. There is no proof-like term and even no instruction which realizes ∀x Int(x).

Let ξ be such an instruction ; thus, we have ξ k-Int(0) and ξ k-Int(1) for every choice of the set ⊥ ⊥. Let δ = λx xx, α 0 = δδ0, α 1 = δδ1 ; let π be some stack. We first take ⊥ ⊥ = {p ∈ Λ c ? Π; p  α 0 ? π} (recall that Λ c ? Π is the set of processes). We define a unary predicate X by putting kX0k = {π}, kX(i + 1)k = ∅ for every i ∈ N. Thus, we have α 0 k-X0 and t k-∀y(Xy → Xsy) for every t ∈ Λ c . But ξ k-Int(0), thus ξ k-∀y(Xy → Xsy), X0 → X0. It follows that ξ ? λx α 1 .α 0 .π ∈ ⊥ ⊥. In other words, ξ ? λx α 1 .α 0 .π  α 0 ? π.

We now take ⊥ ⊥ = {p ∈ Λ c ? Π; p  α 1 ? π} and we define the unary predicate X by putting kX0k = ∅, kX(i + 1)k = {π} for every i ∈ N. Therefore, we have t k-X0 for every t ∈ Λ c and λx α 1 k-∀y(Xy → Xsy). But ξ k-Int(1), thus ξ k-∀y(Xy → Xsy), X0 → X1. It follows that ξ ? λx α 1 .α 0 .π ∈ ⊥ ⊥. In other words, ξ ? λx α 1 .α 0 .π  α 1 ? π. This is obviously a contradiction with the preceding result, because no process can reduce both to α 0 ? π and α 1 ? π.

Q.E.D.

A solution for axiom 3 (we shall give another method later) is simply to remove it by means of the following well known property :

Every proof of a formula Θ in second order classical logic, using axioms 1, 2 and 3, can be converted into a proof of Θ Int using axioms 1, 2 and the following axioms :

3'. ∀x 1 . . . ∀x k {Int[x 1 ], . . . , Int[x k ] → Int[f (x 1 , . . . , x k )]} for each function symbol f of L.
Θ Int is the formula that we obtain by restricting to Int all first order quantifiers in Θ. It is inductively defined as follows :

If A is atomic, then A Int ≡ A ; (A → B) Int ≡ A Int → B Int ; (∀X A) Int ≡ ∀X A Int ; (∀x A) Int ≡ ∀x(Int[x] → A Int ).
It remains to find for which functions from N k into N the formulas 3' are realised. The solution is given by the following theorem :

Theorem 12. Let f be a function symbol of arity k, which represents a (total) recursive function.

Then the formula ∀x 1 . . .

∀x k {Int[x 1 ], . . . , Int[x k ] → Int[f (x 1 , . . . , x k )]} is realised.
We first need a result about usual λ-calculus.

Notations.

Λ is the set of usual λ-terms.

If t, u ∈ Λ, then t ' β t 0 means that t is β-equivalent to t 0 ; t  t 0 means that t reduce to t 0 by weak head reduction : a step of weak head reduction is

(λx u)vv 1 . . . v n  (u[v/x])v 1 . . . v n .
The following lemma explains why we use the same symbol  for weak head reduction of usual λ-terms and for the execution des processes.

Lemma 13. Let ξ, η, t 1 , . . . , t k ∈ Λ some usual closed λ-terms and let π ∈ Π. If η is not an application (in other words, η is a λ-constant or η = λx η 0 ) and if ξ Â (η)t 1 . . . t k , then ξ ? π Â η ? t 1 . . . . .t k .π.
The proof is by induction on the length of the weak head reduction ξ Â (η)t (u[v/y])v 1 . . . v n ? π Â η ? t 1 . . . . .t k .π. Now, during the first n -1 reduction steps of the left hand side, the head of the process is an application ; since η is not, we did not reach yet the right hand process after these steps. Thus, we have :

(u[v/y]) ? v 1 . . . v n .π Â η ? t 1 . . . . .t k .π. It follows that : ξ ? π = (λy u)vv 1 . . . v n ? π Â (u[v/y]) ? v 1 . . . v n .π Â η ? t 1 . . . . .t k .π. Q.E.D.

Notations.

For t, u ∈ Λ c , we define : (t) n u pour n ∈ N by : (t)

0 u = u, (t) n+1 u = (t)(t) n u. t•u by λx(t)(u)
x, where x does appear in t, u.

Lemma 14. Let f, a be λ-constants and ξ ∈ Λ such that ξ ' β (f ) n a.

Suppose that φ k-∀y(Xy → Xsy) and α k-X0. Then ξ[φ/f, α/a] k-Xs n 0.

Proof by induction on n. If n = 0, then ξ ' β a and therefore ξ Â a. If π ∈ kX0k, then ξ ? π Â a ? π, by lemma 13. Thus ξ[φ/f, α/a] ? π Â α ? π ∈ ⊥ ⊥. We can now prove theorem 12. For simplicity, we suppose k = 1 ; thus, we have a recursive function f : N → N. Let φ ∈ Λ be a λ-term which represents f : for each n ∈ N, we have φs n 0 ' β λf λx(f ) p x with p = f (n).

If n > 0, then ξ Â (f )η with η ' β (f ) n-1 a. Let π ∈
T φ k-Int[s n 0] → Int[s p 0], that is T φ k-Int[n] → Int[f (n)]. Since this is true for every n ∈ N, it follows that T φ k-∀x(Int[x] → Int[f (x)]).
Q.E.D.

Arithmetical formulas

We can now consider the specification problem for arithmetical theorems. We begin by two simple forms : ∀x∃y[f (x, y) = 0] and ∃x∀y[f (x, y) = 0] where f is a recursive function. We suppose that these formulas are proved in classical second order arithmetic, using equational axioms written with total recursive function symbols (so that theorem 12 applies). In order to remove the recurrence axiom, we write these theorems in this form :

∀x[Int(x) → ∃y{Int(y), f(x, y) = 0}] and ∃x{Int(x), ∀y[Int(y) → f (x, y) = 0]}.

Theorem 16. If `θ : ∀x[Int(x), ∀y{Int(y) → f (x, y) 6 = 0} → ⊥], then for every n ∈ N, κ ∈ Λ c and π ∈ Π, we have θ ? n.T κ.π Â κ ? s p 0.π 0 with f (n, p) = 0 (T is defined in theorem 10).

Remark. If we take for κ a '' stop '' instruction, we see that the program θ can compute, for each integer n, an integer p such that f (n, p) = 0. A '' stop '' instruction has no reduction rule when it comes in head position ; therefore, execution stops at this moment.

Of course, the theorem remains true if we use other axioms in the proof of the formula ∀x∃y[f (x, y) = 0],

provided that these axioms are realized by suitable instructions. For instance, as we shall see later, we can use the axiom of dependent choice for this proof ; then, the program θ will contain a clock instruction the reduction rule of which is :

? t.π Â t ? n.π, where n is an integer which is the current time.

Proof. We choose n ∈ N and we put ⊥ ⊥ = {p ∈ Λ c ? Π; p  κ ? s p 0.ρ with ρ ∈ Π and f (n, p) = 0}. By theorem 2 (adequation lemma), we have :

( * ) θ k-Int(n), ∀y{Int(y) → f (n, y) 6 = 0} → ⊥.
We have n k-Int(n) by theorem 15. We show that T κ k-∀y{Int(y) → f (n, y) 6 = 0}, in other words that T κ k-Int(p) → f (n, p) 6 = 0 for every integer p. By theorem 10, it is sufficient to prove that κ ? s p 0.ρ ∈ ⊥ ⊥ for every ρ ∈ kf (n, p) 6 = 0k. It is trivial if f (n, p) 6 = 0 since kf (n, p) 6 = 0k = ∅. If f (n, p) = 0, it is again true by definition of ⊥ ⊥.

It follows from ( * ) that θ ? T κ.π ∈ ⊥ ⊥ for every π ∈ Π, which is the desired result.

Q.E.D.

We consider now an arithmetical theorem Φ of the form : ∃x{Int(x), ∀y[Int(y) → f (x, y) = 0]}.

We define a game between two players called ∃ and ∀ : ∃ plays an integer m, ∀ answers by an integer n ; the play stops as soon as f (m, n) = 0 and then ∃ won ; therefore ∀ wins if and only if the play does not stop.

Intuitively, ∃ is the '' defender '' of the theorem and ∀ '' attacks '' this theorem, searching to exhibit a counter-example. It is clear that ∃ has a winning strategy if and only if N |= Φ ; moreover, in this case, there is an obvious strategy for ∃ : simply play successively 0, 1, 2, . . . We shall show (theorem 17) that the program associated with a proof of Φ behaves exactly as a winning strategy for ∃ in this game. For this, we need to add an instruction κ to our programming language, in order to allow an interactive execution. The execution rule of κ is the following :

κ ? s n 0.ξ.π Â ξ ? s p 0.κ np .π 0 for n, p ∈ N, ξ ∈ Λ c , π, π 0 ∈ Π ; s is a fixed λ-term for the successor in Church integers ; κ np is a double sequence of '' stop '' instructions.

Observe that this execution rule is non deterministic, since the integer p and the stack π 0 are arbitrary. The intuitive meaning of this rule is as follows : in the left hand side, the program, which is also the player ∃, plays the integer n ; in the right hand side, the attacker ∀ answers by playing p and the execution goes on ; κ np keeps the trace of the ordered pair (n, p) of integers.

Theorem 17. If `θ : [∃x∀y(f (x, y) = 0)] Int , then every reduction of θ ? T κ.π ends up into κ np ? π 0 with f (n, p) = 0. T is the storage operator defined in theorem 10.

We take for ⊥ ⊥ the set of processes every reduction of which ends up into κ np ?π 0 with f (n, p) = 0 and π 0 ∈ Π. We must show that θ ? T κ.π ∈ ⊥ ⊥ for every π ∈ Π. By theorem 2, we have θ k-∀x[Int(x), ∀y(Int(y) → f (x, y) = 0) → ⊥] → ⊥. Therefore, by definition of k-, it is sufficient to show that :

T κ k-∀x[Int(x), ∀y(Int(y) → f (x, y) = 0) → ⊥]. Let n ∈ N ; we must show that T κ k-Int[s n 0] → [∀y(Int(y) → f (n, y) = 0) → ⊥].
By theorem 10, we only need to show that, if π ∈ Π and ξ k-∀y(Int(y) → f (n, y) = 0) then κ ? s n 0.ξ.π ∈ ⊥ ⊥. By definition of ⊥ ⊥, it is sufficient to show that ξ ? s p 0.κ np .π ∈ ⊥ ⊥ for every p ∈ N and π ∈ Π. But, by hypothesis on ξ, for every p ∈ N and $ ∈ kf (n, p) = 0k, we have ξ ? s p 0.$ ∈ ⊥ ⊥. Therefore, it suffices to show that κ np .π ∈ kf (n, p) = 0k for every p ∈ N and π ∈ Π. If f (n, p) = 0, then kf (n, p) = 0k is k∀X(X → X)k that is to say : {t.ρ; t ∈ Λ c , ρ ∈ Π, t?ρ ∈ ⊥ ⊥}. But, by definition of ⊥ ⊥, we have also κ np ? π ∈ ⊥ ⊥ and therefore κ np .π ∈ kf (n, p) = 0k. If f (n, p) 6 = 0, then kf (n, p) = 0k = k> → ⊥k that is to say {t.ρ; t ∈ Λ c , ρ ∈ Π} ; thus, we have again κ np .π ∈ kf (n, p) = 0k.

Q.E.D.

It follows that every proof of Φ in classical analysis gives rise to an interactive program which wins against any attacker. Indeed, at each answer of the attacker ∀, the program, which is nobody else than the player ∃, provides an object (s n 0, ξ) constituted with an integer n (the '' provisional solution '') and an exception handler ξ, which will be used in case of a pertinent answer of the opponent. They are the two arguments of κ which can therefore be considered as a pointer towards this object.

We can, without any supplementary effort, add a universal quantifier, which gives the Theorem 18. If `θ : [∀x∃y∀z(f (x, y, z) = 0)] Int , then every reduction of θ ? m.T κ.π ends up into κ np ? π 0 with f (m, n, p) = 0.

The generalization to the case of an arithmetical formula with an arbitrary number of alternating quantifiers is given in [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF].

We shall now prove that every arithmetical formula which is true in N is realized. We use for this the trivial winning strategy of the player ∃, which we express by a program.

Theorem 19.

Let θ be a closed λ-term such that θti  (ti)(θt)(s)i. If N |= ∀x∃y∀z[f (x, y, z) 6 = g(x, y, z)], then λx θx0 k-∀x∃y{Int(y), ∀z(f (x, y, z) 6 = g(x, y, z))}.

Remark. This formula is obviously stronger than [∀x∃y∀z(f (x, y, z) 6 = g(x, yz))] Int which is therefore also realized.

Suppose that there exists an integer m such that : λx θx0 6k-∀y[Int(y), ∀z(f (m, y, z) 6 = g(m, y, z)) → ⊥] → ⊥. Thus, there exists t ∈ Λ c and π 0 ∈ Π such that t k-∀y[Int(y), ∀z(f (m, y, z) 6 = g(m, y, z)) → ⊥] and θt0 ? π 0 / ∈ ⊥ ⊥. Thus, we have t ? 0.θt1.π 0 / ∈ ⊥ ⊥ and therefore θt1 6k-∀z(f (m, 0, z) 6 = g(m, 0, z)). This means that there exists p 0 ∈ N and π 1 ∈ Π such that f (m, 0, p 0 ) = g(m, 0, p 0 ) and θt1 ? π 1 / ∈ ⊥ ⊥. Therefore, we have t ? 1.θt2.π 1 / ∈ ⊥ ⊥ and so on. Therefore we build, in this way, a sequence of integers p i (i ∈ N) such that f (m, i, p i ) = g(m, i, p i ). This is a contradiction with the hypothesis that N |= ∀x∃y∀z[f (x, y, z) 6 = g(x, y, z)].

Q.E.D.

This theorem generalizes to an arbitrary number of alternating quantifiers (see below the subsection '' Arbitrary arithmetical formulas '').

Axiom of foundation in generic models

We obviously have N |= ∀x∃y∀z(x 6 = y + z) (take y = sx). Thus, by theorem 19, we have λx θx0 k-∀x∃y{Int(y), ∀z(x 6 = y + z)}. We shall deduce that generic models are '' well founded '' : Theorem 20. The formula ∀x∃!n∃!y{Int(n), y ' 0, x = n + y} is realized, where y ' 0 is the formula ∀z(y 6 = sz).

It is sufficient to show that this formula is a logical consequence of the above formula and of identities ∀x∀y∀z(f (x, y, z) = g(x, y, z)) which are true in N. Existence : let p be the least integer such that ∀z(x 6 = z +p). Then p 6 = 0 because ∀z(x 6 = z +0) is false, by z +0 = z. Threfore p = sn and, by definition of p, there exists y such that x = y +n. We cannot have y = sz, otherwise x = sz + n = z + sn = z + p.

Unicity : suppose that x = y + n = y 0 + n 0 , with Int(n), Int(n 0 ) y, y 0 ' 0. Suppose n ≤ n 0 , thus n 0 = n + k with Int(k). Therefore, we have y + n = y 0 + n + k, thus y = y 0 + k ; since y is not a successor, we have k = 0, thus n = n 0 and y = y 0 .

Q.E.D.

With each individual of the model, we can therefore associate an integer (of the model) and only one. In this way, we can consider integers as equivalence classes. It is another interpretation of the recurrence scheme : instead of restricting individuals to integers, we keep individuals and we restrict to predicates which are saturated for this equivalence relation. The two models of second order arithmetic obtained in this way are obviously isomorphic.

The following theorem is also an expression of well foundedness. It will be used later. We define the predicate x 6 = X y (predicate of order 3, where X is a propositional variable) by putting, for m, n ∈ N : km 6

= X nk = ∅ if m 6 = n and km 6 = X nk = kXk if m = n.
Lemma 22 tells us that this predicate is equivalent to x = y → X.

Lemma 22. The formula ∀X∀x∀y{x 6 = X y ↔ (x = y → X)} is realized. Indeed, we have :

λx xI k-∀X∀x∀y[(x = y → X) → x 6 = X y] and λxλy yx k-∀X∀x∀y[x 6 = X y → (x = y → X)].
Same proof as for theorem 8, which is the particular case X = ⊥.

Q.E.D.

The following theorem gives the specification associated with a formula of the form :

∀x∃y{Int(y), ∀z[f (x, y, z) 6 = g(x, y, z)]} when N |= ∀x∃y∀z[f (x, y, z) 6 = g(x,
i such that N |= ∀z[f (m, n i , z) 6 = g(m, n i , z)].
By lemma 22, the formula ∀X∀x{∀y[Int(y), ∀z(f (x, y, z) 6 = X g(x, y, z)) → X] → X} is equivalent to ∀X∀x{∀y[Int(y) → ∃z(f (x, y, z) = g(x, y, z)) ∨ X] → X}, and therefore to : ∀x∃y{Int(y), ∀z[f (x, y, z) 6 = g(x, y, z)]}. We can thus suppose : θ k-∀X∀x{∀y[Int(y), ∀z(f (x, y, z) 6 = X g(x, y, z)) → X] → X}.

(∃i ∈ N)(∀z ∈ N) f (m, n i , z) 6 = g(m, n i , z)}.
It is therefore sufficient to prove that T κ k-∀y[Int(y), ∀z(f (m, y, z) 6 = X g(m, y, z)) → X for every m ∈ N. By theorem 10, we have to show that κ ? n.t.π ∈ ⊥ ⊥ for every n ∈ N and every t such that t k-∀z(f (m, n, z) 6 = X g(m, n, z)). In other words, we must check :

i) (∀z ∈ N)(f (m, n, z) 6 = X g(m, n, z)) ⇒ κ ? n.t.π ∈ ⊥ ⊥ ; it is clear, by definition of ⊥ ⊥. ii) t k-X ⇒ κ ? n.t.π ∈ ⊥ ⊥, or else t ? π ∈ ⊥ ⊥ ⇒ κ ? n.t.π ∈ ⊥ ⊥ ; it is clear again by definition of ⊥ ⊥. Q.E.D.
For instance, the formula ∀x∃y{Int(y), ∀z(x 6 = y + z)} is a specification for the '' streams of integers '' which take arbitrarily high values. If we define e : N 2 → {0, 1} by e(m, n) = 1 ⇔ m = n, the formula ∀x∃y{Int(y), e(x, y) 6 = 0} is a specification for the '' streams of integers '' which take every possible value. It is the same for the formula (which is equivalent to the former one) : ∀x∃y{Int(y), ∀z(x 2 + y 2 6 = 2xy + sz)}.

Arbitrary arithmetical formulas

Remark. This subsection may be skipped at first reading.

Let us now consider a formula Φ of the form : ∃x 1 ∀y 1 . . . ∃x k ∀y k (f (x 1 , y 1 , . . . , x k , y k ) 6 = 0) where f : N 2k → N is an arbitrary function.

We define a game associated with Φ (players ∃ and ∀ are respectively the '' defender '' and the '' attacker '' of the formula Φ) ; we also define the notion of reached position at a given moment : A position of the game is a finite sequence of integers n 1 p 1 . . .

n i p i (0 ≤ i ≤ k).
N |= ∀x 1 . . . ∀x k {f [x 1 , φ 1 (x 1 ), x 2 , φ 2 (x 1 , x 2 ), . . . , x k , φ k (x 1 , . . . , x k )] = 0} which is the Skolem form of ¬Φ ; thus N |= ¬Φ.
Conversely, if N |= ¬Φ, there exist k functions φ i (x 1 , . . . , x i ) such that the Skolem form of ¬Φ is satisfied. They obviously provide a winning strategy for the opponent ∀.

Theorem 24. Suppose que N |= ∃x 1 ∀y 1 . . . ∃x k ∀y k (f (x 1 , y 1 , . . . , x k , y k ) 6 = 0) where f : N 2k → N is an arbitrary function. Then the formula : ∃x 1 {Int(x 1 ), ∀y 1 ∃x 2 {Int(x 2 ), . . . ∃x k {Int(x k ), ∀y k (f (x 1 , y 1 , . . . , x k , y k ) 6 = 0)} . . .} is realized by a proof-like term which is independent of f (it is, in fact, a usual closed λ-term).

• if we put φ(m) = n j for the first j such that m = m j , then f (m i , φ(m i ), p i ) = 0 for every i ∈ N.

It follows that N |= ∀m∀p[f (m, φ(m), p) = 0] and therefore N 6 |= ∃m∀n∃p[f (m, n, p) = 1]. Q.E.D.
Without any supplementary effort, we can add two universal quantifiers : in head position, a quantifier ∀l is justified because the λ-term which we got does not depend on f . The last quantifier ∀q is justified, because the equation f (m, n, p) = 0 can be written f (m, n, p) 6 = 0 → ⊥, which only takes the truth values > → ⊥ and ⊥ → ⊥. We replace it with : ∀q(f (l, m, n, p, q) 6 = 0) → ⊥ which has the same property. Therefore, we get : Theorem 27. Let f : N 5 → N be an arbitrary function such that N |= ∀l∃m∀n∃p∀q(f (l, m, n, p, q) 6 = 0) and let θ be the closed λ-term defined in theorem 25. Then we have : λx θx000 k-∀l∃m{Int(m), ∀n∃p{Int(p), ∀q[f (l, m, n, p, q) 6 = 0]}} which is the formula :

∀l[∀m{Int(m), ∀n[∀p(Int(p), ∀q(f (l, m, n, p, q) 6 = 0) → ⊥) → ⊥] → ⊥} → ⊥].

The axiom of choice in analysis

In order to get programs from proofs in classical analysis, it remains to realize the axiom of dependent choice or a slightly weaker form : the axiom of countable choice. This axiom is, indeed, used very often in analysis. We consider first the axiom of countable choice which is technically simpler to realize. It consists of the following axiom scheme :

∀ Ỹ ∃Z∀x(∃X F [x, X, Ỹ ] → F [x, Z(x, y)/Xy, Ỹ ]).
F is a second order formula in which the binary predicate variable Z does not appear ; X is of arity 1 ; Ỹ = (Y 1 , . . . , Y n ) is a finite sequence of second order variables (which are, in fact, parameters).

We shall rather write this axiom in contrapositive form :

(CAC) ∀ Ỹ ∃Z∀x(F [x, Z(x, y)/Xy, Ỹ ] → ∀X F [x, X, Ỹ ]).
This means that Z(x, y) is a counter-example to ∀X F [x, X], if there is one. In order to realize this axiom scheme, we add a new instruction, which is denoted by χ ; its reduction rule is given as follows : consider a fixed bijection n 7 → π n from N onto Π (which we do not even need to suppose recursive) ; let π 7 → n π be the inverse function. For each n ∈ N, we denote by n a fixed λ-term which is ' β λf λx(f ) n x, for instance λf λx(f ) n x itself, or s n 0, where s is a λ-term for the successor. The reduction rule for χ is then the following : χ ? t.π Â t ? n π .π for every t ∈ Λ c and π ∈ Π.

Remark. We shall examine later the intuitive meaning of this reduction rule.

Of course, from now on, the set ⊥ ⊥ of processes is supposed to be cc-saturated for this new notion of reduction.

Theorem 28.

Let F [x, X] be a formula with parameters, X being a unary predicate variable. There exists a function U :

N 3 → P(Π) such that : χ k-∀x{∀n(Int[n] → F [x, U (x, n, y)/Xy]) → ∀X F [x, X]}.
For each individual x and each stack π, we have :

π ∈ k∀X F [x, X]k ⇔ (∃R ∈ P(Π) N ) π ∈ kF [x, R/X]k.
By the axiom of countable choice, there exists a function U :

N 3 → P(Π) such that : π ∈ k∀X F [x, X]k ⇔ π ∈ kF [x, U (x, n π , y)/Xy]k. Let us show that U has the desired property : we consider an individual x ∈ N, t ∈ |∀n(Int[n] → F [x, U (x, n, y)/Xy])| and π ∈ k∀X F [x, X]k.
We have to show that χ ? t.π ∈ ⊥ ⊥. By the reduction rule of χ, it is sufficient to prove that t ? n π .π ∈ ⊥ ⊥. But this follows immediately from :

• t k-Int(s nπ 0) → F [x, U (x, n π , y)/Xy] which is true by hypothesis on t ;

• n π k-Int(s n π 0) by theorem 15 ;

• π ∈ kF [x, U (x, n π , y)/Xy]k by hypothesis on π and by definition of U.

Q.E.D. The formula ∃U ∀x{∀n(Int[n] → F [x, U (x, n, y)/Xy]) → ∀X F [x, X]} is therefore realized by λx xχ. But this formula implies, in classical second order logic, the countable axiom of choice (CAC), that is ∃Z∀x{F [x, Z(x, y)/Xy]) → ∀X F [x, X]}.
The proof is easy : it is sufficient, by means of the comprehension scheme, to define Z(x, y) by the following formula : '' U (x, n, y) for the first integer n such that ¬F [x, U (x, n, y)/Xy] if there is one ''. Notice that this proof uses the excluded middle ; therefore, the λ c -term we get to realize CAC contains the instructions χ and cc.

However, a careless formalization of this proof will give a complicated and not very comprehensible term. It is therefore interesting to give an explicit and more refined method, in order to obtain a simple term. This is done below in the section '' A program for the countable choice axiom ''.

The axiom of dependent choice

It is the following axiom scheme :

∀X∃Y H[X, Y ] → ∃Z∀k(Int[k] → H[Z(k, y)/Xy, Z(k + 1, y)/Y y])
for every formula H which does not contain the variable Z.

We write this scheme in the following form :

(DC) ∃Z∀k(Int(k), F [Z(k, y)/Xy, Z(k + 1, y)/Y y] → ∀Y F [Z(k, y)/Xy, Y ])
for every formula F which does not contain the variable Z. The first form follows immediately from this one, by setting F ≡ ¬H. Conversely, we get the second form if we set H(X, Y )

≡ [F (X, Y ) → ∀Y F (X, Y )] in the first one : indeed, ∀X∃Y H[X, Y ] is then provable.
Let <x, y> be a symbol of binary function, which represents a bijection of N 2 onto N. We suppose it to be recursive so that theorem 12 applies. Lemma 29. For every U : N 2 → P(Π), there exists V :

N 2 → P(Π) such that : χ k-∀n{Int[n] → F [U (x, y)/Xy, V (<n, x>, y)/Y y]} → ∀Y F [U(x, y)/Xy, Y ].
Same proof as for theorem 28. For each individual x and each stack π, we have :

π ∈ k∀Y F [U (x, y)/Xy, Y ]k ⇔ (∃R ∈ P(Π) N ) π ∈ kF [U(x, y)/Xy, R/Y ]k.
It follows, by the countable choice axiom, that there exists a function V :

N 2 → P(Π) such that π ∈ k∀Y F [U (x, y)/Xy, Y ]k ⇔ π ∈ kF [U(x, y)/Xy, V (<n π , x>, y)/Y y]k.
We now show that V has the desired property : consider π ∈ k∀Y F [U (x, y)/Xy, Y ]k and t ∈ |∀n{Int[n] → F [U (x, y)/Xy, V (<n, x>, y)/Y y]}|. We have to show that χ ? t.π ∈ ⊥ ⊥, that is t ? n π .π ∈ ⊥ ⊥. But this follows immediately from : • t k-Int(s nπ 0) → F [U (x, y)/Xy, V (<n π , x>, y)/Y y] by hypothesis on t ;

• n π k-Int(s nπ 0) by theorem 15 ;

• π ∈ kF [U (x, y)/Xy, V (<n π , x>, y)/Y y]k by hypothesis on π and by definition of V .

Q.E.D.
Theorem 30. Let F [X, Y ] be a formula with parameters, X, Y being unary predicate variables. Then, there exists A :

N 3 → P(Π) such that : χ k-∀x∀k(∀n{Int[n] → F [A(k, x, y)/Xy, A(k + 1, <n, x>, y)/Y y]} → ∀Y F [A(k, x, y)/Xy, Y ]).
By lemma 29, we have (∀U

∈ P(Π) N 2 )(∃V ∈ P(Π) N 2 )Φ(U, V ) where Φ(U, V ) is the formula χ k-∀n{Int[n] → F [U (x, y)/Xy, V (<n, x>, y)/Y y]} → ∀Y F [U(x, y)/Xy, Y ].
Therefore, we get the result by application of the axiom of dependent choice (in the usual form, i.e. the first one) to the formula Φ(U, V ).

Q.E.D.

By theorem 30, in order to realize the axiom scheme (DC), it is sufficient to derive it, in classical second order logic, from the formula :

b

F [A] ≡ ∀x∀k(∀n{Int[n] → F [A(k, x, y)/Xy, A(k + 1, <n, x>, y)/Y y]} → ∀Y F [A(k, x, y)/Xy, Y ]). But the formula b F [A] is trivially equivalent to ∀x∀k∃n{Int[n], G[x, k, n, A]} with : G[x, k, n, A] ≡ F [A(k, x,

Variants and interpretations

We get the same results using, instead of χ, a dual instruction χ * , which operates on terms instead of stacks. Consider a bijection n 7 → τ n from N onto Λ c and let t 7 → n t be the inverse function. Then the reduction rule for χ * is the following :

χ * ? t.π Â t ? n t .π for every t ∈ Λ c and π ∈ Π.

We have the analogue of theorem 28, the proof being a little more complicated.

Theorem 31.

Let F [x, X] be a formula with parameters, X being a unary predicate variable. There exists U :

N 3 → P(Π) such that : χ * k-∀x{∀n(Int[n] → F [x, U (x, n, y)/Xy]) → ∀X F [x, X]}.
For each n ∈ N we put P n (⊥ ⊥) = {π ∈ Π; τ n ? n.π / ∈ ⊥ ⊥}. For each individual x, we have k∀X F [x, X]k = S {kF [x, R/X]k; R ∈ P(Π) N }. It follows that, given x, n ∈ N such that P n (⊥ ⊥) ∩ k∀X F [x, X]k 6 = ∅, there exists a function R : N → P(Π) such that : P n (⊥ ⊥) ∩ kF [x, Ry/Xy]k 6 = ∅. By the axiom of countable choice, there exists a function U : N 3 → P(Π) which has the following property :

if P n (⊥ ⊥) ∩ k∀X F [x, X]k 6 = ∅ then P n (⊥ ⊥) ∩ kF [x, U (x, n, y)/Xy]k 6 = ∅. Now, let x ∈ N, π ∈ k∀X F [x, X]k and t ∈ |∀n(Int[n] → F [x, U (x,
n, y)/Xy])|. We have to show that χ * ? t.π ∈ ⊥ ⊥ and, by the reduction rule of χ * , it is sufficient to show that : t ? n t .π ∈ ⊥ ⊥. If it is not true, we put n = n t , and therefore τ n = t ; we have then :

π ∈ P n (⊥ ⊥) ∩ k∀X F [x, X]k.
By definition of U, there exists π 0 ∈ P n (⊥ ⊥) ∩ kF [x, U (x, n, y)/Xy]k. From π 0 ∈ P n (⊥ ⊥), we deduce τ n ? n.π 0 / ∈ ⊥ ⊥. But, since π 0 ∈ kF [x, U (x, n, y)/Xy]k, it follows, by hypothesis on t, that t ? n.π 0 ∈ ⊥ ⊥, because n k-Int[s n 0] (theorem 15). It is a contradiction, because t = τ n .

Q.E.D.

We show, in the same way, the analogue of lemma 29. We can then realize the axioms of denumerable and dependent choice, by a pure repetition of the above arguments, using χ * instead of χ. We now remark that instructions analogous to χ and χ * are very common in programmation :

The 'quote' instruction

The reduction rule of instruction χ * , which is :

( * )
χ * ? t.π Â t ? n t .π shows that χ is very similar to the instruction quote of LISP. Indeed, n t can be used in the same way that (quote t), if we assume that t 7 → n t is a recursive bijection from Λ c onto N. For instance, since n u is, in this case, a recursive function of n tu , we can define, by means of χ * , an instruction χ 0 such that χ 0 ? φ.ψ.π Â φ ? n ψ .π : let a be a closed λ-term such that (a)n tu ' β n u and let χ 0 = λxλy(χ * )(λd x•a)y. As this example shows, the instruction χ * is not compatible with β-reduction : in fact, we cannot replace (λd x•a)y with x•a.

The signature

An objection to the interpretation above is that quote is a reversible instruction, which is almost always used with its reverse unquote or eval. On the contrary, even if we suppose that χ (resp. χ * ) is one-to-one from Π (resp. Λ c ) onto N, we do not make use of the inverse function. It is therefore more relevant (and much easier to implement) to interpret n t , in the reduction rule ( * ) above, as the signature of t : it is an integer which is computed from the text of t and which is supposed to characterize it. Examples of well known usual programs for signature are MD-5 (for '' Message Digest '') or SHA-1 (for '' Secure Hash Algorithm ''). Since these programs give integers of fixed length (128 bits for MD-5 and 160 bits for SHA-1), they clearly do not provide an injective function from Λ c into N. But, during the execution of a given process, it is extremely improbable that two different terms with the same signature occur ; therefore, we consider such an event as impossible. And it is all we need in order to realize the axiom of dependent choice.

The clock

Here is another possible interpretation for the instructions χ and χ * . We observe that the application n 7 → τ n may be any surjective function from N onto Λ c . Then the reduction rule of χ * is :

χ * ? t.π Â t ? n.π.

where n is any integer such that τ n = t. This suggests the following interpretation : χ * is an input instruction ; when it comes in head position, the process χ * ? t.π waits for an integer n which is provided by a human operator or some external process. Then the reduction χ * ? t.π Â t ? n.π takes place and the execution goes on. The only condition is that we must be able to retrieve t from n ; in other words, the integers which are provided to the processes χ * ? t.π and χ * ? t 0 .π 0 with t 6 = t 0 must be different.

A very simple and natural way to obtain this behavior is by providing the integer n by means of a clock, since two different λ c -terms cannot appear at the same time. In other words, let us be given a second process, which is executed in parallel with the principal process, and which only increments an integer at each reduction step. It is this process which provides the integer n when necessary, that is when χ * arrives in head position in the principal process.

For an example of a model with a clock, look at the section below : '' The standard generic model ''.

A program for the countable choice axiom

We give here an explicit λ c -term, containing the instruction χ, which realizes the axiom of countable choice and we explain its behaviour.

In the proof of theorem 28, we defined a function U : N 3 → P(Π) (ternary predicate).

We define now the binary predicate V (x, y) by putting : V (x, y) ≡ ∀n{

\ m<n |{m} → F U (x, m)|, {n}, ¬F U (x, n) → U(x, n, y)}.
We use the notations

F U (x, n) for F [x, U (x, n, y)/Xy] and F V (x) for F [x, V (x, y)/Xy] ; the notation {m} → F V (x, m) is defined page 3.
We propose to realize the formula F V (x) → ∀X F [x, X], which is the axiom of denumerable choice. Now, we have :

Theorem 32 (Extensionality scheme).

i) For every formula G[X], the formula :

Ext[G] ≡ ∀X{G[X] → G * [X]} is provable in intuitionistic second order logic, with : G * [X] ≡ ∀U {∀y(Xy → Uy), ∀y(Uy → Xy) → G[Uy/Xy]}. ii) `λgλuλu 0 λvλv 0 ((g)v•u)u 0 •v 0 : Ext[G * ].
i) This is immediate, by recurrence on G.

ii) We have g : G * [X], u : ∀y(Xy → Uy), u 0 : ∀y(Uy → Xy), v : ∀y(Uy → V y), v 0 : ∀y(V y → Uy) `v•u : ∀y(Xy → V y), u 0 •v 0 : ∀y(V y → Xy), and therefore ((g

)v•u)u 0 •v 0 : G[V y/Xy]. Q.E.D.

Remark. Ext[G]

tells us that the formulas G and G * are equivalent. The λ-term which is associated to the proof of this equivalence depends, in general, on G. It does not depend on it for formulas of the form G * .

Therefore we shall, in fact, realize the denumerable axiom of choice in the form :

F * V (x) → ∀X F [x, X] where F * V (x) is the formula F * [x, V (x, y)/Xy] that is to say : ∀X{∀y(V (x, y) → Xy), ∀y(Xy → V (x, y)) → F [x, X]}.
A trivial variant of theorem 28 gives :

χ k-∀x{∀n|{n} → F U (x, n)| → ∀X F [x,
Y k-∀n( \ m<n |{m} → F U (x, m)|, {n} → F U (x, n)) → ∀n|{n} → F U (x, n)|. So, we must now realize : F * V (x), \ m<n |{m} → F U (x, m)|, {n} → F U (x, n).
By the law of Peirce, it is sufficient to realize :

F * V (x), \ m<n |{m} → F U (x, m)|, {n}, ¬F U (x, n) → F U (x, n) which is : ∀X{∀y(V (x, y) → Xy), ∀y(Xy → V (x, y)) → F [x, X]}, \ m<n |{m} → F U (x, m)|, {n}, ¬F U (x, n) → F U (x, n).
But n is now a fixed integer, so that we can put Xy ≡ U(x, n, y) ; our goal is now :

{∀y(V (x, y) → U (x, n, y)), ∀y(U (x, n, y) → V (x, y)) → F U (x, n)}, \ m<n |{m} → F U (x, m)|, {n}, ¬F U (x, n) → F U (x, n).
It is clearly a consequence of the two following formulas, that we have therefore to realize :

\ m<n |{m} → F U (x, m)|, {n}, ¬F U (x, n) → (V (x, y) → U(x, n, y)) \ m<n |{m} → F U (x, m)|, {n}, ¬F U (x, n) → (U(x, n, y) → V (x, y)).
By definition of V , it is immediate that the first formula is realized by λxλnλkλv vxnk.

Lemma 33. There exists a closed usual λ-term, denoted by Comp, such that, for every n, n 0 ∈ N

: Comp n n 0 xyz  x if n < n 0 ; Comp n n 0 xyz  y if n 0 < n ; Comp n n 0 xyz  z if n = n 0 . Trivial. Q.E.D.
It follows that, if we put α = (k)(x 0 )n and α 0 = (k 0 )(x)n 0 , we have :

λxλnλkλx 0 λn 0 λk 0 Comp nn 0 αα 0 k- \ m<n |{m} → Xm|, {n}, ¬Xn, \ m 0 <n 0 |{m 0 } → Xm 0 |, {n 0 }, ¬Xn 0 → (Y n → Y n 0 ).
By replacing Xn with F U (x, n) and Y n with U(x, n, y), we see that we have realized :

\ m<n |{m} → F U (x, m)|, {n}, ¬F U (x, n), \ m 0 <n 0 |{m 0 } → F U (x, m 0 )|, {n 0 }, ¬F U (x, n 0 ) → (U(x, n ,
y) → U(x, n 0 , y)) which, by the definition of V , can also be written as :

λxλnλkλuλx 0 λn 0 λk 0 Comp nn 0 αα 0 u k- \ m<n |{m} → F U (x, m)|, {n}, ¬F U (x, n) → (U(x, n, y) → V (x, y)).
This is exactly the desired result and we obtain finally the following term which realizes the axiom of denumerable choice :

Theorem 34. There exists a binary predicate V :

N 2 → P(Π) such that : λf (χ)(Y)λxλn(cc)λk fτ 0 τ 1 k-∀X{∀y(V (x, y) ↔ Xy) → F [x, X]} → ∀X F [x, X] with τ 0 = λv vxnk, τ 1 = λuλx 0 λn 0 λk 0 Comp nn 0 αα 0 u, α = (k)(x 0 )n and α 0 = (k 0 )(x)n 0 .
Let us look at the behaviour of the term γ = λf (χ)(Y)λxλn(cc)λk fτ 0 τ 1 . Consider a process γ ? f.π in which γ is in head position. We have : γ ? f.π Â χ ? Yξ.π (where ξ = λxλn(cc)λk fτ 0 τ 1 depends only on f )

 Yξ ? n π .π  ξ ? η.n π .π (with η = Yξ). Therefore γ ? f.π  f ? τ f π 0 .τ f π 1 .π with τ f π i = τ i [η/x, n π /n, k π /k]. Now τ f π
0 is simply the triple <η, n π , k π >. In other words τ f π 0 stores the current state f.π at the present execution of γ. τ f π 1 performs the real job : it looks at two such states f.π and f 0 .π 0 and compare their indexes n and n 0 . If n = n 0 it does nothing.

If n < n 0 (resp. n 0 < n) it restarts with γ ? f 0 .π (resp. γ ? f.π 0 ) :

the second file with the first stack.

Thus, the main function of this program is to update files (if χ is a clock) or to choose a good version of a file (if χ is a signature).

Non standard integers

We give here sufficient conditions in order that every generic model contains non standard individuals. Let us define a unary predicate G by putting kGnk = {π n } (n 7 → π n is here a one-to-one recursive function from N onto Π).

Theorem 35. i) We suppose that :

(H ⊥ ⊥ ) For each stack constant $, there exists a proof-like term ξ such that ξ ? $ ∈ ⊥ ⊥.

Then I k-∀x Gx → ⊥ and (∀n ∈ N)(∃ξ ∈ PL) ξ k-Gn.

ii) χ k-∀x[Int(x) → Gx] → ⊥.

i) We have immediately k∀x Gxk = {π n ; n ∈ N} = Π and therefore I k-∀x Gx → ⊥.

We are looking at some ξ ∈ PL such that ξ ? π n ∈ ⊥ ⊥. Now, we have π n = t 0 . . . t k .$, $ being a stack constant. By (H ⊥ ⊥ ), we have some η ∈ PL such that η ? $ ∈ ⊥ ⊥. Il is sufficient to set ξ = λx 0 . . . λx k η.

ii) Let t k-∀x[Int(x) → Gx] and π ∈ Π, π = π n . We must show that χ ? t.π ∈ ⊥ ⊥ that is t ? n.π ∈ ⊥ ⊥, by the reduction rule of χ. It is immediate, by hypothesis on t, since n k-Int(n) and π ∈ kGnk.

Q.E.D.

Thus, with hypothesis (H ⊥ ⊥ ), a generic model satisfies Gn for each standard integer n and also ∃x ¬Gx. It contains therefore necessarily a non standard individual. If, moreover, the instruction χ is present, it satisfies ∃x{Int(x), ¬Gx}. Then, it contains necessarily non standard integers.

Theorem 38. Let Θ = λxλyccλk((x)(k)y0)((x)(k)y1)(k)y2. Then we have : Θ k-∀x[∀y(xy 6 = 0, xy 6 = x → y 2 6 = y), x 6 = 0 → x 2 6 = x] (This formula says that the Boolean algebra B is atomless).

By a simple computation, we see that we must show the following two properties :

i) Θ k-(⊥, ⊥ → ⊥), ⊥ → ⊥.

ii) Θ k-|>, ⊥ → ⊥| ∩ |⊥, > → ⊥|, > → ⊥.

Proof of (i) : let t ∈ |⊥, ⊥ → ⊥| and u ∈ |⊥|. We have to show that Θ ? t.u.π ∈ ⊥ ⊥ that is, by reduction, t ? k π u0.((t)(k π )u1)(k π )u2.π ∈ ⊥ ⊥. But, from u k-⊥, we easily deduce that k π uξ k-⊥ for every ξ ∈ Λ c . Since t k-⊥, ⊥ → ⊥, it follows that ((t)(k π )u1)(k π )u2 k-⊥ and therefore t ? k π u0.((t)(k π )u1)(k π )u2.π ∈ ⊥ ⊥.

Proof of (ii) : let t ∈ |>, ⊥ → ⊥| ∩ |⊥, > → ⊥| and u ∈ Λ c . Again, we have to show that t ? k π u0.((t)(k π )u1)(k π )u2.π ∈ ⊥ ⊥. If it is not true, we have : k π u0 6k-⊥ (because t k-⊥, > → ⊥) and ((t)(k π )u1)(k π )u2 6k-⊥ (because t k->, ⊥ → ⊥).

But, since t k-⊥, > → ⊥ (resp. >, ⊥ → ⊥), we deduce k π u1 6k-⊥ (resp. k π u2 6k-⊥).

It follows that k π u0, k π u1, k π u2 appear all in head position in some thread. Since they contain k π , these threads are the same (their stack constant is the one of π). Suppose, for example, that k π u0 appears first in head position, then k π u1, and then k π u2. We have thus :

k π u0 ? π 0 Â u ? π Â • • • Â k π u1 ? π 1 Â u ? π Â • • • Â k π u2 ? π 2 Â u ? π Â • • •
But such an execution is clearly impossible because, at the second appearance of the process u ? π, we enter in a loop and can never arrive at k π u2 ? π 2 .

Q.E.D.

The generic thread

Consider a fixed one-to-one recursive function n 7 → ξ n from N onto PL. We define a unary predicate P by taking for kP nk the set of stacks the bottom constant of which is π ξn .

Theorem 39. In the generic model, ¬P contains exactly one individual and it is not a standard integer. In other words, the following formulas are realized : i) P n for each n ∈ N ; ii) ∀x P x → ⊥ ; iii) ∀x∀y[¬P x, x 6 = y → P y].

i) Let n ∈ N be such that δδ0 6k-P n and δδ1 6k-P n. Thus, there exist ρ 0 , ρ 1 ∈ Π which have the same stack constant π ξ n , such that δδ0 ? ρ 0 / ∈ ⊥ ⊥ and δδ1 ? ρ 1 / ∈ ⊥ ⊥. We have therefore ξ n ? π ξ n  δδ0 ? ρ 0 and ξ n ? π ξ n  δδ1 ? ρ 1 , which is clearly impossible. ii) We have k∀xP xk = S n∈N kP nk = Π. Therefore I k-∀x P x → ⊥. iii) We show, by means of theorem 9, that V λxλy y k-∀x∀y[¬P x, x 6 = y → P y] that is to say V λxλy y k-¬P m, m 6 = n → P n for m, n ∈ N. So, let π ∈ kP mk, t km 6 = n and π 0 ∈ kP nk ; we must show that λxλy y ? k π .t.π 0 ∈ ⊥ ⊥. It is obvious if m 6 = n, since then the stacks π and π 0 , which have different stack constants, cannot appear both in the same thread. If m = n, we have t k-⊥, which give the desired result, because λxλy y ? k π .t.π 0  t ? π 0 .

Q.E.D.

We now add to λ c -calculus an instruction σ with the following reduction rule : σ ? t.π Â t ? n.π where n is the number of the stack constant of π (this constant is therefore π ξ n ).

π ∈ kp 6 = gk. Then, we have to show that ? t.u.π ∈ ⊥ ⊥ ; suppose, on the contrary, that ? t.u.π appears in a thread, at the n-th step. By hypothesis on π, this thread is ξ p ? π ξ p ; we have therefore u = v(n, p), by definition of v, hence v(n, p) k-F [x, X]. By definition of Φ, we have then u = v(n, p) k-F [x, Φ(n, p, x, y)/Xy]. But, since n k-Int[n], it follows that t ? n.u.π ∈ ⊥ ⊥, by hypothesis on t. It is a contradiction, because this process appears at the (n + 1)-th step in the thread ξ p ? π ξ p .

Q.E.D.

It follows that the generic model satisfies the formula : ∀x∀X(F [x, X] → ∃n{Int[n], F [x, Φ(n, g, x, y)/Xy]}). We can then define the binary predicate Ψ(x, y) by the formula : '' Φ(n, g, x, y) for the first integer n such that F [x, Φ(n, g, x, y)/Xy], or ⊥ if there is no such integer ''. Then, we have, in the generic model : ∀x∀X(F [x, X] → F [x, Ψ(x, y)/Xy]), which gives the denumerable axiom of choice.

By the same methods as above, we can also easily get the axiom of dependent choice.

Theorem 21 .

 21 Let Y be the Turing combinator : Y = AA with A = λaλf (f )(a)af . Then Y k-∀X{∀n( \ m<n |Xm| → Xn) → ∀n Xn}. Let X : N → P(Π), k ∈ N and t k-∀n( \ m<n |Xm| → Xn).

  y)/Xy, A(k + 1, <n, x>, y)/Y y] → ∀Y F [A(k, x, y)/Xy, Y ]. Thus, we can define inductively a sequence of integers n k , by the conditions n 0 = 0 and n k+1 = <n, n k > for the first integer n such that G[n k , k, n, A]. Now, if we define Z(k, y) by A(k, n k , y), we get F [Z(k, y)/Xy, Z(k + 1, y)/Y y] → ∀Y F [Z(k, y)/Xy, Y ] for each integer k, that is (DC).

  . . , A k , A be formulas, free variables of which are amongst y 1 , . . . , y m , Y 1 , . . . , Y n . Let b i ∈ N (1 ≤ i ≤ m) and P j ∈ P(Π) N k j (1 ≤ j ≤ n), where k j is the arity of Y j . Suppose thatx 1 : A 1 , . . . , x k : A k `t : A is provable with the above rules. If t i k-A i [b 1 /y 1 , . . . , b m /y m , P 1 /Y 1 , . . . , P n /Y n ] for 1 ≤ i ≤ k, then t[t 1 /x 1 , . . . , t k /x k ] k-A[b 1 /y 1 , . . . , b m /y m , P 1 /Y 1 , . . . , P n /Y n ]. make an induction on the length of the proof of Γ `t : A where Γ is the context x 1 : A 1 , . . . , x k : A k . We shall use the notation t 0 for t[t 1 /x 1 , . . . , t k /x k ] and A 0 for A[b 1 /y 1 , . . . , b m /y m , P 1 /Y 1 , . . . , P n /Y n ]. Consider the rule used in the last step of

	We the proof :
	If it is rule 1 the result is trivial ;

  by induction hypothesis, we know that u 0 ∈ |(A 0 → B 0 ) → A 0 |, hence the result. If it is rule 5 for a first order x, we have A = ∀x B and Γ `t : B. By induction hypothesis, weget t 0 ∈ |B 0 [a/x]| for each a ∈ N. Thus t 0 ∈ T a∈N |B 0 [a/x]| = |∀x B 0 | = |A 0 |. If itis rule 5 for a second order variable X of arity k, we have A = ∀X B and Γ `t : B. By induction hypothesis, we have t 0

  kXs n 0k ; then ξ ? π Â f ? η.π, by lemma 13 and therefore ξ[φ/f, α/a] ? π Â φ ? η[φ/f, α/a].π. Now, φ ∈ |Xs n-1 0 → Xs n 0| Let n ∈ N and ν ∈ Λ such that ν ' β λf λx(f ) n x. Then ν k-Int[s n 0].Xsy), α k-X0 and π ∈ kXs n 0k ; we must show that ν ? φ.α.π ∈ ⊥ ⊥. Since ν ' β λf λx(f ) n x, we have ν Â λf η, η Â λa ξ and ξ ' β (f ) n a. By lemma 13, we have ν ? φ.α.π Â λf η ? φ.α.π Â η[φ/f ] ? α.π. Again by lemma 13, we have : η ? α.π Â λa ξ ? α.π Â ξ[α/a] ? π and thus η[φ/f ] ? α.π Â ξ[φ/f, α/a] ? π. Finally, we have ν ? φ.α.π Â ξ[φ/f, α/a] ? π. But, by lemma 14, we have ξ[φ/f, α/a] k-Xs n 0 and therefore ν ? φ.α.π Â ξ[φ/f, α/a] ? π ∈ ⊥ ⊥.

and, by induction hypothesis, η[φ/f, α/a] ∈ |Xs n-1 0|. Thus φ ? η[φ/f, α/a].π ∈ ⊥ ⊥. Q.E.D. Theorem 15. Let φ k-∀y(Xy → Q.E.D.

  Thus φs n 0 Â λf ξ and, by theorem 15, we have λf ξ k-Int[s p 0]. Let π ∈ kInt[s p 0]k ; we have λf ξ ? π ∈ ⊥ ⊥. Now, by lemma 13, we have φs n 0 ? π Â λf ξ ? π ; but this reduction has necessarily at least one step, because φs n 0 6 = λf ξ (φs n 0 does not begin by λ). Therefore φ ? s n 0.π Â λf ξ ? π ∈ ⊥ ⊥. Since this holds for each π ∈ kInt[s p 0]k, theorem 10 shows that

  We show, by induction on k, that Y ? t.π ∈ ⊥ ⊥ for every π ∈ Xk. By induction hypothesis, we have Y ? t.ρ ∈ ⊥ ⊥ for every ρ ∈ S

m<k Xm and therefore Yt k-\ m<n |Xm|. Thus, by hypothesis on t, we have t ? Yt.π ∈ ⊥ ⊥ for every π ∈ Xk. But we have Y ? t.π Â t ? Yt.π hence the result. Q.E.D.

  The player ∃ chooses first an already reached position n 1 p 1 . . . n i p i with 0 ≤ i < k and an integer n i+1 ; then, the player ∀ chooses an integer p i+1 . The position n 1 p 1 . . . n i+1 p i+1 is then reached. Then, he continues with the next k-uple of integers. If the play is infinite, we obtain k functions φ i (x 1 , . . . , x i ) such that :

If

i + 1 = k and f (n 1 , p 1 , . . . , n k , p k ) 6 = 0, then the play stops and ∃ won. In every other case, the play goes on. Therefore ∀ wins if and only if the play does not stop. It is easy to see that N |= Φ if and only if the player ∃ has a winning strategy for this game.

Moreover, we can effectively (and very simply) describe such a strategy. It does not even depend on the function f , but only on the number k of quantifiers : The player ∃ uses an effective enumeration of N k . When he reaches the k-uple n 1 . . . n k , he chooses the longest already reached position of the form n 1 p 1 . . . n i p i . We have i < k because this position was reached for a k-uple of integers which is different from n 1 . . . n k . Then, he plays successively n i+1 , . . . , n k without taking any account of the choices of player ∀.

  X]} (we replacedInt[n] with {n}, which has the advantage to avoid the introduction of a storage operator).Therefore, we have now to realize : F * V (x) → ∀n|{n} → F U (x, n)|. We have seen (theorem 21) that, if Y is the fixed point combinator of Turing, then : Y k-∀X{∀n( It follows that, by replacing Xn with |{n} → F U (x, n)|, we have :

	\ m<n	|Xm| → Xn) → ∀n Xn}.

Remarks.

This formula is obviously stronger than Φ Int , which is therefore also realized. Theorem 24 is a generalization of theorem 19.

The integers of a generic model give therefore a first order model which is elementarily equivalent to N. The term which realizes Φ is obtain by means of a program for the winning strategy given above.

We shall only consider the case where N |= Φ ≡ ∃m∀n∃p(f (m, n, p) 6 = 0). We then write, in the following way, a proof-like term independent of f which realizes the formula ∃m{Int(m), ∀n∃p{Int(p), f(m, n, p) 6 = 0)}} : m, p are λ-variables, which represent Church integers ; s 0 and s 1 are closed usual λ-terms such that the ordered pair (s 0 mp, s 1 mp) is the successor of the pair (m, p) in a fixed recursive enumeration of N 2 which begins with (0, 0). σ is a variable which represents a finite sequence of ordered pairs (m 0 , η 0 ), . . . , (m k , η k ) where m i is a Church integer and η i a λ c -term. In other words, σ represents a λ c -term of the form λhλx(hm

H and Σ are closed usual λ-terms, defined as follows : Hσηm  η i for the first i such that m = m i , if m is equal to one of the integers m i of the sequence σ ; otherwise Hσηm  η. Σσηm  σ if m is equal to one of the integers m i of the sequence σ ; otherwise Σσηm  τ , where τ is the sequence obtained by adding the pair (m, η) at the end of the sequence σ.

we have to show that θξ000 k-⊥.

Lemma 26. Let η 0 , . . . , η k ∈ Λ c and m, p, m 0 , n 0 , . . . , m k , n k ∈ N, m 0 , . . . , m k being distinct integers ; suppose that

By definition of θ, we have ξmt σmp 6k-⊥ with t σmp = λη(η 0 p)(θ)ξσ 0 m 0 p 0 . By hypothesis on ξ, it follows that t σmp 6k-

We have η 0 = Hσηm and therefore η 0 k-∀p{Int(p) → f (m, n 0 , p) = 0}, by definition of H. Now, we have : t σmp η Â η 0 p.θξσ 0 m 0 p 0 . If f (m, n 0 , p) 6 = 0, then η 0 p k-> → ⊥ ; therefore t σmp η k-⊥ which is a contradiction. Therefore, we have f (m, n 0 , p) = 0 and it follows that η 0 p k-0 = 0, that is η 0 p k-⊥ → ⊥ ; if θξσ 0 m 0 p 0 k-⊥, we get once more the contradiction t σmp η k-⊥.

Q.E.D. Now suppose that θξ000 6k-⊥ ; applying iteratively lemma 26, we obtain a sequence (m i , n i , p i , η i ) i∈N such that : • (m i , p i ) i∈N is the fixed enumeration of N 2 which begins with (0, 0) ;

The standard generic model

Consider a fixed one-to-one recursive function ξ 7 → π ξ from PL (the set of proof-like terms) onto the set of stack constants. Every set ⊥ ⊥ such that (∀ξ ∈ PL) ξ ? π ξ / ∈ ⊥ ⊥ is clearly coherent, which means that (∀ξ ∈ PL) ξ 6k-⊥. In this section, we take for ⊥ ⊥ the greatest saturated set of processes which has this property. In fact, it is simpler to consider the complement ⊥ ⊥ c of ⊥ ⊥ in the set Λ c ? Π of processes. Therefore, we set :

For each ξ ∈ PL, the set of processes which are obtained by reduction of ξ ? π ξ will be called the thread generated by ξ ; ⊥ ⊥ c is thus the union of all threads. We have : Lemma 36. A process is in ⊥ ⊥ if and only if it does not appear in any thread. A term t ∈ Λ c realizes ⊥ if and only if it does not come in head position in any thread.

Trivial.

Q.E.D.

Remember that T ⊥ ⊥ is the set of closed formulas with parameters which are realized by some proof-like term. The models of this theory (which is coherent if and only if ⊥ ⊥ is) are called generic models . With this particular choice of ⊥ ⊥, we shall call them standard generic models.

We now show some properties of these models, with the following assumptions : 1. There is no instruction which changes the current stack constant. In other words, in the thread generated by ξ ∈ PL, the only stack constant which appears is π ξ .

2. Every instruction is deterministic, that is to say that each process has at most one successor. We then say that execution is sequential.

Theorem 37. Let a 0 = δδ0 and a 1 = δδ1, with δ = λx xx. Then :

There are three possible values for kn 6 = 1,

If it is not true, by hypothesis on t, we have k π a 0 , k π a 1 6k-⊥. Therefore, both terms appear in head position in some thread ; since they both contain the stack constant at the bottom of π, these thread are the same one (by hypothesis 1 above). But then a 0 and a 1 appear in head position in the same thread. Now, by hypothesis 2, one of them appears in head position before the other, for instance a 0 . But it is clear that a 1 can never come in head position after that.

The formula ∃x∃y{x 2 = x, x 6 = 0, x 6 = 1} is therefore satisfied in the generic model. Thus, there are individuals which are not integers and the axiom of recurrence is not satisfied. We shall see later that there are also non standard integers.

Let B be the set of individuals x such that x 2 = x. Since all equational formulas which are true in N are also true in generic models, it is clear that B is a Boolean algebra, which is therefore 6 = {0, 1}. We now show that B is, indeed, infinite and even atomless.

In the generic model, the unique individual which satisfies ¬P x is therefore an integer. By theorem 39, it is a non standard integer.

Proof. Let t k-∀x[Int(x) → P x] and π ∈ Π. We must show that σ ? t.π ∈ ⊥ ⊥ ; it is sufficient to prove that t ? n.π ∈ ⊥ ⊥, n being the number of the stack constant of π. Therefore, we have π ∈ kP nk and t k-Int(n) → P n. Hence the result, since n k-Int(n).

Q.E.D.

We can therefore add to our second order language a symbol of constant g (for generic), with the following axioms : Int(g), ∀x[x 6 = g ↔ P x], g 6 = n for each integer n. The predicate P x will be denoted by x 6 = g ; thus kn 6 = gk is, for each integer n, the set of stacks which have π ξ n as their stack constant. It is interesting to study the properties of the (non standard) proof-like λ c -term ξ g and of the thread ξ g ? π ξ g , which will be, rather naturally, called the generic thread.

Remark. With the help of the instruction σ, we can therefore prove the existence of a non standard integer. By means of the second fixed point theorem of λ-calculus, we can do without this instruction, but we have a somewhat weaker result :

Let ∆ : N → N be the recursive function defined by ∆m = n ⇔ ξ n = ξ m m and let δ be a closed λ-term which represents this function. We define the integers p, q by setting ξ p = λx(θ)(δ)x and q = ∆p. We have therefore ξ q ? π ξq = ξ p p ? π ξq  θ ? δp.π ξq , which shows that θ ? δp.π ξq / ∈ ⊥ ⊥. Now, we have π ξq ∈ kP qk and, by theorem 15, δp k-Int(q). It follows that θ 6k-Int(q) → P q.

Q.E.D.

The clock

With the present definition of ⊥ ⊥, in order to add a new instruction ι, it is sufficient to give its reduction rule only when it comes in head position in a thread. Indeed, ⊥ ⊥ is the complement of the union of all threads and the only condition it has to satisfy is to be cc-saturated (see the section '' Truth values and types ''). It is therefore sufficient to define each thread, i.e. the sequence of processes obtained by the execution of ξ ? π ξ , for each proof-like term ξ (possibly containing the instruction ι).

It is in this way that we define the clock instruction . Its reduction rule is ? t.π Â t ? n.π where n ∈ N is obtained in the following way : let ξ ? π ξ be the (unique) thread in which the process ? t.π appears. Then n is the number of reduction steps from ξ ? π ξ ('' the boot '') to ? t.π (if ? t.π appears more than once in the thread ξ ? π ξ , we consider its first appearance ; notice that, in this case, the execution ends in a loop).

Definition. A proof-like term θ will be called strongly solvable iff θ k-⊥ → ⊥. In other words : for every t ∈ Λ c \ PL, if θ ? t comes in head position in a thread, then t also comes in head position in this thread.

When θ is a closed usual λ-term, this means that it has a head normal form which is λx xt 1 . . . t n (hence the terminology '' strongly solvable '').

The following theorem shows that every standard strongly solvable proof-like term comes in head position in the generic thread.

Theorem 42. Let θ be a strongly solvable proof-like term and φ θ : N 2 → {0, 1} the recursive function such that : φ θ (n, p) = 1 ⇔ θ comes in head position in the thread ξ p ? π ξ p at the (n + 4)-th step. Then λxλy(θ)(y)x k-∀p{∀n[Int(n) → φ θ (n, p) 6 = 1] → p 6 = g} (in other words, ∃n{Int(n), φ θ (n, g) = 1}).

Let p ∈ N, π ∈ kp 6 = gk and t k-∀n[Int(n) → φ θ (n, p) 6 = 1]. We prove the result by contradiction : suppose that λxλy(θ)(y)x ? t.π / ∈ ⊥ ⊥. Therefore, this process appears in a thread, which is certainly ξ p ? π ξp since π ∈ kp 6 = gk. We have thus : ξ p ? π ξ p  λxλy(θ)(y)x ? t.π  θ ? tn.π, where the integer n, which is provided by , is the number of steps in the reduction of ξ p ? π ξ p until λxλy(θ)(y)x ? t.π. Thus, we obtain θ ? tn.π at the (n + 4)-th step of reduction. Since θ is in head position at this moment, we have φ θ (n, p) = 1. By hypothesis on t, it follows that tn k-⊥. Now, by hypothesis, θ k-⊥ → ⊥ and therefore θ ? tn.π ∈ ⊥ ⊥. It is a contradiction, because θ ? tn.π appears in the thread ξ p ? π ξ p .

Q.E.D.

Corollary 43. Let θ be a proof-like term such that θ m is strongly solvable for each integer m (with m = s m 0) and let ψ θ : N 3 → {0, 1} be the recursive function defined by ψ θ (m, n, p) = 1 iff θ m comes in head position at the (n + 4)-th step in the thread ξ p ? π ξ p . Then we have :

It means that the following formula is realized : '' for every integer m, θ m comes in head position in the generic thread ξ g ? π ξ g ''. Therefore also the formula : '' the generic thread neither stops nor loops '' (take, for instance, θ = λxλy y). Proof. By theorem 10, it is sufficient to prove that, for every integers m, p and every stack ρ ∈ k∀n[Int(n) → ψ θ (m, n, p) 6 = 1] → p 6 = gk, we have : λm λxλy(θm)(y)x ? m.ρ ∈ ⊥ ⊥, that is λxλy(θ m)(y)x ? ρ ∈ ⊥ ⊥. But this results from theorem 42 and from the fact that ψ θ (m, n, p) = φ θ m(n, p).

Q.E.D.

The denumerable axiom of choice

Here we check that, by means of the clock instruction , we can realize the axiom of denumerable choice.

Theorem 44. Let F [x, X] be a formula with parameters, X being a unary predicate variable. There exists Φ : N 4 → P(Π) such that :

k-∀x∀p∀X{∀n(Int[n], F [x, Φ(n, p, x, y)/Xy] → ⊥), F [x, X] → p 6 = g}.

We define v : N 2 → Λ c by putting : v(n, p) = the λ c -term u which is in second position in the stack, at the n-th execution step in the thread ξ p ? π ξ p . At the n-th step of this execution, we have therefore a process of the form τ ? t.u.π.

We define now Φ(n, p, x, y), by means of the denumerable axiom of choice, in such a way that : If there exists X : N → P(Π) such that v(n, p) k-F [x, X] then v(n, p) k-F [x, Φ(n, p, x, y)/Xy]. We show that Φ has the desired property : consider x, p ∈ N, an application X : N → P(Π), λ c -terms t, u such that t k-∀n(Int[n], F [x, Φ(n, p, x, y)/Xy] → ⊥), u k-F [x, X] and a stack