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

Realizability algebras : a program to well order R

Introduction

When we want to obtain programs from mathematical proofs, the main problem is, naturally, raised by the axioms : indeed, it has been a long time since we know how to transform a proof in pure (i.e. without axioms) intuitionistic logic, even at second order [START_REF] Curry | Combinatory Logic[END_REF][START_REF] Howard | The formulas-as-types notion of construction. Essays on combinatory logic, λ-calculus, and formalism[END_REF][START_REF] Girard | Une extension de l'interprétation fonctionnelle de Gödel à l'analyse[END_REF]. The very first of these axioms is the excluded middle, and it seemed completely hopeless for decades. The solution, given by T. Griffin [START_REF] Griffin | A formulae-as-type notion of control[END_REF] in 1990, was absolutely surprising. It was an essential discovery in logic because, at this moment, it became clear that all other axioms will follow, as soon as we will work in a suitable framework. The theory of classical realizability is such a framework : it was developed in [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF][START_REF] Krivine | Realizability in classical logic[END_REF], where we treat the axioms of Analysis (second order arithmetic with dependent choice). In [START_REF] Krivine | Structures de réalisabilité, RAM et ultrafiltre sur N[END_REF], we attack a more difficult case of the general axiom of choice, which is the existence of a non trivial ultrafilter on N ; the main tool is the notion of realizability structure, in which the programs are written in λ-calculus. In the present paper, we replace it with the notion of realizability algebra, which has many advantages : it is simpler, first order and much more practical for implementation. It is a three-sorted variant of the usual notion of combinatory algebra. Thus, the programming language is no longer the λ-calculus, but a suitable set of combinators ; remarkably enough, this is almost exactly the original set given by Curry. The λ-terms are now considered only as notations or abbreviations, very useful in fact : a λ-term is infinitely more readable than its translation into a sequence of combinators. The translation used here is new, as far as I know ; its fundamental property is given in theorem 2. The aim of this paper is to show how to transform into programs, the classical proofs which use dependent choice and : i) the existence of a non trivial ultrafilter on N ; ii) the existence of a well ordering on R. Of course, (ii) implies (i) but the method used for (i) is interesting, because it can give simpler programs. This is an important point, because a new problem is appearing now, an important and very difficult problem : to understand the programs we obtain in this way, that is to explain their behavior. A fascinating, but probably long work. The logical frame is given by classical second order logic, in other words the (first order) theory of the comprehension scheme. However, since we use a binary membership relation on individuals, we work, in reality, in at least third order logic. Moreover, this is indispensable since, although the axiom of dependent choice on R can be expressed as a second order scheme, axioms (i) and (ii) cannot be expressed in this way. By using the method expounded in [START_REF] Krivine | Typed lambda-calculus in classical Zermelo-Fraenkel set theory[END_REF], we can obtain the same results in ZF. It seems clear to me that, by developing the technology of classical realizability, we shall be able to treat all "natural" axioms introduced in set theory. It is already done for the continuum hypothesis, which will be the topic of a forthcoming paper. In my opinion, the axiom of choice and the generalized continuum hypothesis in ZF do not pose serious issues, except this : it will be necessary to use the proper class forcing of Easton [START_REF] Easton | Powers of regular cardinals[END_REF] inside the realizability model, and it will probably be very painful.

A very interesting open problem is posed by axioms such as the existence of measurable cardinals or the determination axiom. But the most important open problem is to understand what all these programs do and, in this way, to be able to execute them. I believe that big surprises are waiting for us here. Indeed, when we realize usual axioms of mathematics, we need to introduce, one after the other, the very standard tools in system programming : for the law of Peirce, these are continuations (particularly useful for exceptions) ; for the axiom of dependent choice, these are the clock and the process numbering ; for the ultrafilter axiom and the well ordering of R, these are no less than read and write instructions on a global memory, in other words assignment. It seems reasonable to conjecture that such tools are introduced for some worthwhile purpose, and therefore that the very complex programs we obtain by means of this formalization work, perform interesting and useful tasks. The question is : which ones ?

Remark.

The problem of obtaining a program from a proof which uses a given axiom, must be set correctly from the point of view of computer science. As an example, consider a proof of a theorem of arithmetic, which uses a well ordering of P(N) : if you restrict this proof to the class of constructible sets, you easily get a new proof of the same theorem, which does not use this well ordering any more. Thus, it looks like you simply have to transform this new proof into a program. But this program would be extracted from a proof which is deeply different from (and dramatically more complicated than) the original one. Moreover, with this method, it is impossible to associate a program with the well ordering axiom itself. From the point of view of computer science, this is an unacceptable lack of modularity : since we cannot put the well ordering axiom in a program library, we need to undertake again the programming work with each new proof. With the method which is explained below, we only use the λ-term extracted from the original proof. Therefore, this term contains an unknown instruction for the well ordering axiom on P(N), which is not yet implemented. Then, by means of a suitable compilation, we transform this term into a true program which realizes the initial theorem. As a corollary of this technology, we obtain a program which is associated with the well ordering axiom, which we can put in a library for later use.

Realizability algebras

A realizability algebra is composed of three sets : Λ (the set of terms), Π (the set of stacks), Λ ⋆ Π (the set of processes) with the following operations : (ξ, η) → (ξ)η from Λ 2 into Λ (application) ;

(ξ, π) → ξ . π from Λ×Π into Π (push) ;

(ξ, π) → ξ ⋆ π from Λ×Π into Λ ⋆ Π (process) ; π → k π from Π into Λ (continuation). We have, in Λ, the distinguished elements B, C, E, I, K, W, cc, called elementary combinators or instructions. Notation. The term (. . . (((ξ)η 1 )η 2 ) . . .)η n will be also denoted by (ξ)η 1 η 2 . . . η n or ξη 1 η 2 . . . η n . For example : ξηζ = (ξ)ηζ = (ξη)ζ = ((ξ)η)ζ. We define on Λ ⋆ Π a preorder relation, denoted by ≻. It is the least reflexive and transitive relation such that we have, for any ξ, η, ζ ∈ Λ and π, ̟ ∈ Π :

(ξ)η ⋆ π ≻ ξ ⋆ η . π. I ⋆ ξ . π ≻ ξ ⋆ π. K ⋆ ξ . η . π ≻ ξ ⋆ π. E ⋆ ξ . η . π ≻ (ξ)η ⋆ π. W ⋆ ξ . η . π ≻ ξ ⋆ η . η . π. C ⋆ ξ . η . ζ . π ≻ ξ ⋆ ζ . η . π. B ⋆ ξ . η . ζ . π ≻ (ξ)(η)ζ ⋆ π. cc ⋆ ξ . π ≻ ξ ⋆ k π . π. k π ⋆ ξ . ̟ ≻ ξ ⋆ π.
Finally, we are given a subset ⊥ ⊥ of Λ ⋆ Π which is a terminal segment for this preorder, which means that : p ∈ ⊥ ⊥, p ′ ≻ p ⇒ p ′ ∈ ⊥ ⊥. In other words, we ask that ⊥ ⊥ be such that : (ξ)η ⋆ π / ∈ ⊥ ⊥ ⇒ ξ ⋆ η . π / ∈ ⊥ ⊥.

I ⋆ ξ . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ π / ∈ ⊥ ⊥. K ⋆ ξ . η . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ π / ∈ ⊥ ⊥. E ⋆ ξ . η . π / ∈ ⊥ ⊥ ⇒ (ξ)η ⋆ π / ∈ ⊥ ⊥. W ⋆ ξ . η . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ η . η . π / ∈ ⊥ ⊥. C ⋆ ξ . η . ζ . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ ζ . η . π / ∈ ⊥ ⊥. B ⋆ ξ . η . ζ . π / ∈ ⊥ ⊥ ⇒ (ξ)(η)ζ ⋆ π / ∈ ⊥ ⊥. cc ⋆ ξ . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ k π . π / ∈ ⊥ ⊥. k π ⋆ ξ . ̟ / ∈ ⊥ ⊥ ⇒ ξ ⋆ π / ∈ ⊥ ⊥.

c-terms and λ-terms

We call c-term a term which is built with variables, the elementary combinators B, C, E, I, K, W , cc and the application (binary function We easily see that this rewriting is finite, for any given c-term t : indeed, during the rewriting, no combinator is introduced inside t, but only in front of it. Moreover, the only changes in t are : moving parentheses and erasing occurrences of x. Now, rules 1 to 5 strictly decrease the part of t which remains under λx, and rule 6 can be applied consecutively only finitely many times. The λ-terms are defined as usual. But, in this paper, we consider λ-terms only as a notation for particular c-terms, by means of the above translation. This notation is essential, because almost every c-term we shall use, will be given as a λ-term. Theorem 2 gives the fundamental property of this translation.

Remark. We cannot use the well known KS-translation of λ-calculus, because it does not satisfy Theorem 2.

Lemma 1. If t is a c-term with the only variables x, y 1 , . . . , y n , and if ξ, η 1 , . . . , η n ∈ Λ, then :

(λx t)[η 1 /y 1 , . . . , η n /y n ] ⋆ ξ . π ≻ t[ξ/x, η 1 /y 1 , . . . , η n /y n ] ⋆ π.
To lighten the notation, let us put u * = u[η 1 /y 1 , . . . , η n /y n ] for each c-term u ; thus, we have :

u * [ξ/x] = u[ξ/x, η 1 /y 1 , . . . , η n /y n ].
The proof is done by induction on the number of rules 1 to 6 used to translate the term λx t. Consider the rule used first.

If it is rule 1, then we have

(λx t) * ⋆ ξ . π ≡ (K)t * ⋆ ξ . π ≻ t * ⋆ π ≡ t[ξ/x, η 1 /y 1 , . . . , η n /y n ] ⋆ π since x is not in t.
If it is rule 2, we have t = x and (λx t

) * ⋆ξ . π ≡ I ⋆ξ . π ≻ ξ ⋆π ≡ t[ξ/x, η 1 /y 1 , . . . , η n /y n ]⋆ π.
If it is rule 3, we have t = uv and (λx t)

* ⋆ ξ . π ≡ (Cλx(E)u) * v * ⋆ ξ . π ≻ C ⋆ (λx(E)u) * . v * . ξ . π ≻ (λx(E)u) * ⋆ ξ . v * . π ≻ (E)u * [ξ/x] ⋆ v * . π (by induction hypothesis) ≻ E ⋆ u * [ξ/x] . v * . π ≻ (u * [ξ/x])v * ⋆ π ≡ t[ξ/x, η 1 /y 1 , . . . , η n /y n ] ⋆ π since x is not in v.
If it is rule 4, we have t = ux and (λx t)

* ⋆ ξ . π ≡ (E)u * ⋆ ξ . π ≻ E ⋆ u * . ξ . π ≻ u * ξ ⋆ π ≡ t[ξ/x, η 1 /y 1 , . . . , η n /y n ] ⋆ π since u does not contain x.
If it is rule 5, we have t = ux and (λx t)

* ⋆ ξ . π ≡ (W λx(E)u) * ⋆ ξ . π ≻ W ⋆ (λx(E)u) * . ξ . π ≻ (λx(E)u) * ⋆ ξ . ξ . π ≻ (E)u * [ξ/x] ⋆ ξ . π (by induction hypothesis) ≻ E ⋆ u * [ξ/x] . ξ . π ≻ (u * [ξ/x])ξ ⋆ π ≡ t[ξ/x, η 1 /y 1 , . . . , η n /y n ] ⋆ π. If it is rule 6, we have t = (u)(v)w and (λx t) * ⋆ ξ . π ≡ (λx(B)uvw) * ⋆ ξ . π ≻ (B)u * [ξ/x]v * [ξ/x]w * [ξ/x] ⋆ π (by induction hypothesis) ≻ B ⋆ u * [ξ/x] . v * [ξ/x] . w * [ξ/x] . π ≻ (u * [ξ/x])(v * [ξ/x])w * [ξ/x] ⋆ π ≡ t[ξ/x, η 1 /y 1 , . . . , η n /y n ] ⋆ π. q.e.d.
Theorem 2. If t is a c-term with the only variables x 1 , . . . , x n , and if ξ 1 , . . . , ξ n ∈ Λ,

then λx 1 . . . λx n t ⋆ ξ 1 . . . . . ξ n . π ≻ t[ξ 1 /x 1 , . . . , ξ n /x n ] ⋆ π.
Proof by induction on n ; the case n = 0 is trivial.

We have λx

1 . . . λx n-1 λx n t ⋆ ξ 1 . . . . . ξ n-1 . ξ n . π ≻ (λx n t)[ξ 1 /x 1 , . . . , ξ n-1 /x n-1 ] ⋆ ξ n . π (by induction hypothesis) ≻ t[ξ 1 /x 1 , . . . , ξ n-1 /x n-1 , ξ n /x n ] ⋆ π by lemma 1.
q.e.d.

Natural deduction

Before giving the formal language that we shall use, it is perhaps useful to describe informally the structures (models) we have in mind. They are second order structures, with two types of objects : individuals also called conditions and predicates (of various arity). Since we remain at an intuitive level, we start with a full model which we call the ground model. Such a model consists of :

• an infinite set P (the set of individuals or conditions).

• the set of k-ary predicates is P(P k ) (full model).

• some functions from P k into P .

In particular, there is an individual 0 and a bijective function s : P → (P \ {0}). This enables us to define the set of integers N as the least set which contains 0 and which is closed for s.

There is also a particular condition denoted by 1 and an application denoted by ∧ from P 2 into P .

• some relations (fixed predicates) on P . In particular, we have the equality relation on individuals and the subset C of non trivial conditions. C[p∧q] reads as : "p and q are two compatible conditions". We now come to the formal language, in order to write formulas and proofs about such structures. It consists of :

• individual variables or variables of conditions called x, y, . . . or p, q, . . . • predicate variables or second order variables X, Y, . . . ; each predicate variable has an arity which is in N.

• function symbols on individuals f, g, . . . ; each one has an arity which is in N.

In particular, there is a function symbol of arity k for each recursive function f : N k → N. This symbol will also be written as f . There is also a constant symbol 1 (which represents the greatest condition) and a binary function symbol ∧ (which represents the inf of two conditions).

The terms are built in the usual way with variables and function symbols. The atomic formulas are the expressions X(t 1 , . . . , t n ), where X is an n-ary predicate variable, and t 1 , . . . , t n are terms.

Formulas are built as usual, from atomic formulas, with the only logical symbols →, ∀ :

• each atomic formula is a formula ;

• if A, B are formulas, then A → B is a formula ;

• if A is a formula, then ∀x A and ∀X A are formulas.

Notations.

The formula A 1 → (A 2 → (. . . (A n → B) . . .) will be written

A 1 , A 2 , . . . , A n → B.
The usual logical symbols are defined as follows : (X is a predicate variable of arity 0, also called propositional variable)

⊥ ≡ ∀X X ; ¬A ≡ A → ⊥ ; A ∨ B ≡ (A → ⊥), (B → ⊥) → ⊥ ; A ∧ B ≡ (A, B → ⊥) → ⊥ ; ∃ y F ≡ ∀y(F → ⊥) → ⊥ (
where y is an individual or predicate variable).

More generally, we shall write ∃ y{F 1 , . . . ,

F k } for ∀ y(F 1 , . . . , F k → ⊥) → ⊥.
We shall sometimes write F for a finite sequence of formulas F 1 , . . . , F k . Then, we shall also write ∃ y{ F } and ∀ y( F → ⊥) → ⊥.

x = y is the formula ∀Z(Zx → Zy), where Z is a unary predicate variable.

The rules of natural deduction are the following (the A i 's are formulas, the x i 's are variables of c-terms, t, u are c-terms) :

1.

x 1 : A 1 , . . . , x n : A n ⊢ x i : A i . 2. x 1 : A 1 , . . . , x n : A n ⊢ t : A → B, x 1 : A 1 , . . . , x n : A n ⊢ u : A ⇒ x 1 : A 1 , . . . , x n : A n ⊢ tu : B. 3. x 1 : A 1 , . . . , x n : A n , x : A ⊢ t : B ⇒ x 1 : A 1 , . . . , x n : A n ⊢ λx t : A → B. 4. x 1 : A 1 , . . . , x n : A n ⊢ t : A ⇒ x 1 : A 1 , . . . ,

Realizability

Given a realizability algebra A = (Λ, Π, Λ⋆Π, ⊥ ⊥), a A-model M consists of the following data :

• An infinite set P which is the domain of variation of individual variables.

• The domain of variation of k-ary predicate variables is P(Π) P k .

• We associate with each k-ary function symbol f , a function from P k into P , denoted by f or even f if there is no ambiguity.

In particular, there is a distinguished element 0 in P and a function s : P → P (which is the interpretation of the symbol s). We suppose that s is a bijection from P onto P \ {0}.Then, we can identify s n 0 ∈ P with the integer n, and therefore, we have For each closed formula F I with parameters in M, we define two truth values :

N ⊂ P . Each recursive function f : N k → N is,
F I ⊂ Π and |F I | ⊂ Λ. |F I | is defined as follows : ξ ∈ |F I | ⇔ (∀π ∈ F I ) ξ ⋆ π ∈ ⊥ ⊥.
F I is defined by recurrence on F : • F is atomic : then F I has the form X (t 1 , . . . , t k ) where X : P k → P(Π) and the t i 's are closed terms with parameters in M. We set X (t 1 , . . . , t k ) = X (t 1 , . . . , t k ). Proof by recurrence on the length of the derivation of x 1 : A 1 , . . . , x n : A n ⊢ t : A. We consider the last used rule. 1. We have t = x i , A ≡ A i . Now, we have assumed that ξ i || -A I i ; and it is the desired result. 2. We have t = uv and we already obtained :

• F ≡ A → B : we set F I = {ξ . π ; ξ ∈ |A I |, π ∈ B I }. • F ≡ ∀x A : we set F I = { A I[x←p] ; p ∈ P }. • F ≡ ∀X A : we set F I = { A I[X←X ] ; X ∈ P(Π) P k } if X is a k-
x 1 : A 1 , . . . , x k : A k ⊢ u : B → A and x 1 : A 1 , . . . , x k : A k ⊢ v : B. Given π ∈ A I , we must show (uv)[ξ 1 /x 1 , . . . , ξ k /x k ] ⋆ π ∈ ⊥ ⊥. By hypothesis on ⊥ ⊥, it suffices to show u[ξ 1 /x 1 , . . . , ξ k /x k ] ⋆ v[ξ 1 /x 1 , . . . , ξ k /x k ] . π ∈ ⊥ ⊥.
By the induction hypothesis, we have v[ξ 1 /x 1 , . . . , ξ k /x k ] || -B I and therefore :

v[ξ 1 /x 1 , . . . , ξ k /x k ] . π ∈ B I → A I .
But, by the induction hypothesis, we have also u[ξ 1 /x 1 , . . . , ξ k /x k ] || -B I → A I , hence the result.

We have

A = B → C, t = λx u. We must show λx u[ξ 1 /x 1 , . . . , ξ k /x k ] || -B I → C I ;
thus, we suppose ξ || -B I , π ∈ C I and we have to show λx u[ξ 1 /x 1 , . . . , ξ k /x k ]⋆ξ . π ∈ ⊥ ⊥.

By hypothesis on ⊥ ⊥ and lemma 1, it suffices to show u[ξ/x, ξ 1 /x 1 , . . . , ξ k /x k ] ⋆ π ∈ ⊥ ⊥. This follows from the induction hypothesis applied to x 1 : A 1 , . . . , x n : A n , x : B ⊢ u : C. 4. We have A ≡ ∀X B, and X is not free in A 1 , . . . , A n . We must show :

t[ξ 1 /x 1 , . . . , ξ k /x k ] || -(∀X B) I , i.e. t[ξ 1 /x 1 , . . . , ξ k /x k ] || -B J with J = I[X ← X ]. But, by hypothesis, ξ i || -A I i therefore ξ i || -A J i :
indeed, since X is not free in A i , we have :

A I i = A J i .
Then, the induction hypothesis gives the result. 6. We have A = B[F/Xy 1 . . . y n ] and we must show :

t[ξ 1 /x 1 , . . . , ξ k /x k ] || -B[F/Xy 1 . . . y n ] I assuming that t[ξ 1 /x 1 , . . . , ξ k /x k ] || -(∀X B) I .
This follows from lemma 4 below.

q.e.d.

Lemma 4. B[F/Xy 1 . . . y n ] I = B I[X←X ]
where X : P n → P(Π) is defined by :

X (p 1 , . . . , p n ) = F I[y 1 ←p 1 ,...,yn←pn] .
The proof is by induction on B. That is trivial if X is not free in B. Indeed, the only non trivial case of the induction is B = ∀Y C ; and then, we have Y = X and :

B[F/Xy 1 . . . y n ] I = (∀Y C[F/Xy 1 . . . y n ]) I = Y C[F/Xy 1 . . . y n ] I[Y ←Y] . By induction hypothesis, this gives Y C I[Y ←Y][X←X ] , that is Y C I[X←X ][Y ←Y] i.e. ( ∀Y
C) I[X←X ] .
q.e.d.

Lemma 5. Let X , Y ⊂ Π be truth values. If π ∈ X , then k π || -X → Y. Suppose ξ || -X and ρ ∈ Y ; we must show k π ⋆ ξ . ρ ∈ ⊥ ⊥, that is ξ ⋆ π ∈ ⊥ ⊥, which is clear. q.e.d.
Proposition 6 (Law of Peirce). cc || -∀X∀Y (((X → Y ) → X) → X).

We want to show that cc || -((X → Y) → X ) → X . Thus, we take ξ || -(X → Y) → X and π ∈ X ; we must show that cc ⋆ ξ . π ∈ ⊥ ⊥, that is ξ ⋆ k π . π ∈ ⊥ ⊥. By hypothesis on ξ and π, it is sufficient to show that k π || -X → Y, which results from lemma 5. q.e.d.

Proposition 7. i) If ξ || -A → B, then ∀η(η || -A ⇒ ξη || -B). ii) If ∀η(η || -A ⇒ ξη || -B), then (E)ξ || -A → B. i) From ξη ⋆ π ≻ ξ ⋆ η . π. ii) From (E)ξ ⋆ η . π ≻ ξη ⋆ π.
q.e.d.

Remark. Proposition 7 shows that ξ || -A → B is "almost" equivalent (i.e. up to an ηexpansion of ξ) to ∀η(η || -A ⇒ ξη || -B).

Predicate symbols

In the following, we shall use extended formulas which contain predicate symbols (or predicate constants) R,S, . . . on individuals. Each one has an arity, which is an integer.

In particular, we have a unary predicate symbol C (which represents the set of non trivial conditions).

We have to add some rules of construction of formulas :

• If F is a formula, R is a n-ary predicate constant and t 1 , . . . , t n are terms, then R(t 1 , . . . , t n ) → F and R(t 1 , . . . , t n ) → F are formulas.

• ⊤ is an atomic formula.

In the definition of a A-model M, we add the following clause :

• With each relation symbol R of arity n, we associate an application, denoted by R M or R, from P n into P(Λ). We shall also write

|R(p 1 , . . . , p n )|, instead of R(p 1 , . . . , p n ), for p 1 , . . . , p n ∈ P .
In particular, we have an application C : P → P(Λ), which we denote as

|C[p]|.
We define as follows the truth value in M of an extended formula :

⊤ = ∅. (R(t 1 , . . . , t n ) → F ) I = {t . π; t ∈ |R(t I 1 , . . . , t I n )|, π ∈ F I }. (R(t 1 , . . . , t n ) → F ) I = F I if I ∈ |R(t I 1 , . . . , t I n )| ; (R(t 1 , . . . , t n ) → F ) I = ∅ otherwise. Proposition 8. i) λx(x)I || -∀X∀x 1 . . . ∀x n [(R(x 1 , . . . , x n ) → X) → (R(x 1 , . . . , x n ) → X)]. ii) If we have |R(p 1 , . . . , p n )| = ∅ ⇒ I ∈ |R(p 1 , . . . , p n )| for every p 1 , . . . , p n ∈ P , then : K || -∀X∀x 1 . . . ∀x n [(R(x 1 , . . . , x n ) → X) → (R(x 1 , . . . , x n ) → X)].

Trivial.

q.e.d.

Remark. By means of proposition 8, we see that, if the application R : P n → P(Λ) takes only the values {I} and ∅, we can replace

R(t 1 , . . . , t n ) → F with R(t 1 , . . . , t n ) → F .
We define the binary predicate ≃ by putting |p ≃ q| = {I} if p = q and |p ≃ q| = ∅ if p = q. By the above remark, we can replace p ≃ q → F with p ≃ q → F . Proposition 9 shows that we can also replace p = q → F with p ≃ q → F . Notations. We shall write p = q → F instead of p ≃ q → F . Thus, we have :

p = q → F = F if p = q ; p = q → F = ∅ if p = q.
We shall write p = q for p = q → ⊥. Thus, we have : p = q = Π if p = q and p = q = ∅ if p = q. Using p = q → F instead of p = q → F , and p = q instead of p = q → ⊥, greatly simplifies the computation of the truth value of a formula which contains the symbol =.

Proposition 9. i) λx xI || -∀X∀x∀y((x = y → X) → (x = y → X)) ; ii) λxλy yx || -∀X∀x∀y((x = y → X), x = y → X). i) Let a, b ∈ P , X ⊂ Π, ξ || -a = b → X and π ∈ a = b → X . Then, we have a = b, thus I || -a = b, therefore ξ ⋆ I . π ∈ ⊥ ⊥, thus λx xI ⋆ ξ . π ∈ ⊥ ⊥. ii) Now let η || -(a = b → X ), ζ || -a = b and ρ ∈ X . We show that λxλy yx ⋆ η . ζ . ρ ∈ ⊥ ⊥ in other words ζ ⋆ η . ρ ∈ ⊥ ⊥. If a = b, then η || -X , ζ || -∀Y (Y → Y ). We have η . ρ ∈ X → X , thus ζ ⋆ η . ρ ∈ ⊥ ⊥. If a = b, then ζ || -⊤ → ⊥, thus ζ ⋆ η . ρ ∈ ⊥ ⊥.
In both cases, we get the desired result.

q.e.d.

Remark.

Let R be a subset of P k and 1 R : P k → {0, 1} its characteristic function, defined as follows :

1

R (p 1 , . . . , p n ) = 1 (resp. = 0) if (p 1 , . . . , p n ) ∈ R (resp. (p 1 , . . . , p n ) / ∈ R). Let us define the predicate R in the model M by putting : |R(p 1 , . . . , p n )| = {I} (resp. = ∅) if (p 1 , . . . , p n ) ∈ R (resp. (p 1 , . . . , p n ) / ∈ R).
By propositions 8 and 9, we see that R(x 1 , . . . , x n ) and 1 R (x 1 , . . . , x n ) = 1 are interchangeable. More precisely, we have :

I || -∀X∀x 1 . . . ∀x n ((R(x 1 , . . . , x n ) → X) ↔ (1 R (x 1 , . . . , x n ) = 1 → X)).
For each formula A[x 1 , . . . , x k ], we can define the k-ary predicate symbol N A , by putting

|N A (p 1 , . . . , p k )| = {k π ; π ∈ A[p 1 , . . . , p k ] }.
Proposition 10 below shows that N A and ¬A are interchangeable ; this may simplify truth value computations.

Proposition 10. i) I || -∀x 1 . . . ∀x k (N A (x 1 , . . . , x k ) → ¬A(x 1 , . . . , x k )) ; ii) cc || -∀x 1 . . . ∀x k ((N A (x 1 , . . . , x k ) → ⊥) → A(x 1 , . . . , x k )). i) Let p 1 , . . . , p k ∈ P , π ∈ A(p 1 , . . . , p k ) , ξ || -A(p 1 , . . . , p k ) and ρ ∈ Π. We must show : I ⋆ k π . ξ . ρ ∈ ⊥ ⊥, that is ξ ⋆ π ∈ ⊥ ⊥, which is obvious. ii) Let η || -N A (p 1 , . . . , p k ) → ⊥ and π ∈ A(p 1 , . . . , p k ) . We must show : cc ⋆ η . π ∈ ⊥ ⊥, i.e. η ⋆ k π . π ∈ ⊥ ⊥, which is clear, since k π ∈ |N A (p 1 , . . . , p k )|.
q.e.d.

Fixed point combinator

Theorem 11. Let Y = AA with A = λaλf (f )(a)af . Then, we have Y⋆ξ . π ≻ ξ⋆Yξ . π.

Let f : P 2 → P such that f (x, y) = 1 is a well founded relation on P . Then : i) Y || -∀X{∀x[∀y(f (y, x) = 1 → Xy) → Xx] → ∀x Xx}. ii) Y || -∀X 1 . . . ∀X k {∀x[∀y(X 1 y, . . . , X k y → f (y, x) = 1), X 1 x, . . . , X k x → ⊥] → ∀x(X 1 x, . . . , X k x → ⊥)}. The property Y ⋆ ξ . π ≻ ξ ⋆ Yξ . π is immediate, from theorem 2.
i) We take X :

P → P(Π), p ∈ P and ξ || -∀x[∀y(f (y, x) = 1 → X y) → X x].
We show, by induction on the well founded relation

f (x, y) = 1, that Y ⋆ ξ . π ∈ ⊥ ⊥ for every π ∈ X p. Let π ∈ X p ; from (i), we get Y ⋆ ξ . π ≻ ξ ⋆ Yξ .
π and thus, it is sufficient to prove that ξ ⋆ Yξ . π ∈ ⊥ ⊥. By hypothesis, we have ξ || -∀y(f (y, p) = 1 → X y) → X p ; thus, it suffices to show that Yξ ||f (q, p) = 1 → X q for every q ∈ P . This is clear if f (q, p) = 1, by definition of →.

If f (q, p) = 1, we must show Yξ || -X q, i.e. Y ⋆ ξ . ρ ∈ ⊥ ⊥ for every ρ ∈ X q. But this follows from the induction hypothesis.

ii) The proof is almost the same : take X 1 , . . . , X k : P → P(Π), p ∈ P and ξ || -∀x[∀y(X 1 y, . . . ,

X k y → f (y, x) = 1), X 1 x, . . . , X k x → ⊥].
We show, by induction on the well founded relation f (x, y) = 1, that Y⋆ξ . π ∈ ⊥ ⊥ for every π ∈ X 1 p, . . . , X k p → ⊥ .

As before, we have to show that : Yξ || -X 1 q, . . . , X k q → f (q, p) = 1 for all q ∈ P ; this is obvious if f (q, p) = 1. If f (q, p) = 1, we must show Yξ || -X 1 q, . . . , X k q → ⊥, or else :

Y ⋆ ξ . ρ ∈ ⊥ ⊥ for every ρ ∈ X 1 q, . . . , X k q → ⊥ . But this follows from the induction hypothesis.

q.e.d.

Integers, storage and recursive functions

Recall that we have a constant symbol 0 and a unary function symbol s which is interpreted, in the model M by a bijective function s : P → (P \ {0}).

And also, that we have identified s n 0 with the integer n ; thus, we suppose N ⊂ P . We denote by int(x) the formula ∀X(∀y(Xy → Xsy), X0 → Xx).

Let u = (u n ) n∈N be a sequence of elements of Λ. We define the unary predicate symbol e u by putting :

|e u (s n 0)| = {u n } ; |e u (p)| = ∅ if p / ∈ N. Theorem 12. Let T u , S u ∈ Λ be such that S u || -(⊤ → ⊥), ⊤ → ⊥ and : T u ⋆ φ . ν . π ≻ ν ⋆ S u . φ . u 0 . π ; S u ⋆ ψ . u n . π ≻ ψ ⋆ u n+1 . π
for every ν, φ, ψ ∈ Λ and π ∈ Π. Then :

T u || -∀X∀x[(e u (x) → X), int(x) → X].
T u is called a storage operator.

Let p ∈ P , φ || -e u (p) → X, ν || -int(p) and π ∈ X . We must show T u ⋆ φ . ν . π ∈ ⊥ ⊥ i.e. ν ⋆ S u . φ . u 0 . π ∈ ⊥ ⊥.
• If p / ∈ N, we define the unary predicate Y by putting :

Y (q) ≡ ⊤ if q ∈ N ; Y (q) ≡ ⊤ → ⊥ if q / ∈ N.
Thus, we have obviously φ || -Y (0) and u 0 . π ∈ Y (p) .

But, by hypothesis on ν, we have

ν || -∀y(Y y → Y sy), Y 0 → Y p.
Thus, it is sufficient to show that :

S u || -∀y(Y y → Y sy), i.e. S u || -Y (q) → Y (sq) for every q ∈ P . This is clear if q ∈ N, since we have Y (sq) = ∅. If q / ∈ N, we must show S u || -(⊤ → ⊥), ⊤ → ⊥,
Y s i 0 = {u p-i . π} for 0 ≤ i ≤ p and Y q = ∅ if q / ∈ {s i 0; 0 ≤ i ≤ p}.
By hypothesis on ν, φ, π, we have :

ν || -∀y(Y y → Y sy), Y 0 → Y s p 0 ; φ || -Y 0 ; u 0 . π ∈ Y s p 0 .
Thus, it suffices to show that S u || -∀y(Y y → Y sy), i.e. S u || -Y q → Y sq for every q ∈ P . This is clear if q / ∈ {s i 0; 0 ≤ i < p}, since then Y sq = ∅.

If q = s i 0 with i < p, let ξ || -Y q ; we must show S u ⋆ ξ . u p-i-1 . π ∈ ⊥ ⊥. But we have S u ⋆ ξ . u p-i-1 . π ≻ ξ ⋆ u p-i . π which is in ⊥ ⊥, by hypothesis on ξ.
q.e.d.

Notation. We define the closed c-terms 0 = λxλy y ; σ = λnλf λx(f )(n)f x ; and, for each n ∈ N, we put n = (σ) n 0. We define the unary predicate symbol ent(x) by putting :

|ent(n)| = {n} if n ∈ N ; |ent(p)| = ∅ if p / ∈ N.
In other words, ent(x) is the predicate e u (x) when the sequence u is (n) n∈N .

Theorem 13.

We put T = λf λn(n)Sf 0, with S = λgλx(g)(σ)x. Then, we have :

i) T || -∀X∀x((ent(x) → X), int(x) → X). ii) I || -∀x((ent(x) →int(x)).
Therefore, T is a storage operator (theorem 12). i) We immediately have, by theorem 2 :

T ⋆ φ . ν . π ≻ ν ⋆ S . φ . 0 . π ; S ⋆ ψ . (σ) n 0 . π ≻ ψ ⋆ (σ) n+1 0 . π for every ν, φ, ψ ∈ Λ and π ∈ Π. Now, we check that S || -(⊤ → ⊥), ⊤ → ⊥ : indeed, if ξ || -⊤ → ⊥, then S ⋆ ξ . η . π ≻ ξ ⋆ ση . π ∈ ⊥ ⊥ for every η ∈ Λ and π ∈ Π (by theorem 2).
Then, the result follows immediately, from theorem 12. ii) We must show I ||ent(p) → int(p) for every p ∈ P . We may suppose p ∈ N (otherwise ent(p) = ∅ and the result is trivial). Then, we must show :

I ⋆ σ p 0 . ρ ∈ ⊥ ⊥ knowing that ρ ∈ int(s p 0) .
Therefore, we can find a unary predicate X : P → P(Π), φ || -∀y(Xy → Xsy), ω || -X0 and π ∈ Xs p 0 such that ρ = φ . ω . π. We must show (σ) p 0 ⋆ φ . ω . π ∈ ⊥ ⊥. In fact, we show by recurrence on p, that (σ

) p 0 ⋆ φ . ω . π ∈ ⊥ ⊥ for all π ∈ Xs p 0 . If p = 0, let π ∈ X0 ; we must show 0 ⋆ φ . ω . π ∈ ⊥ ⊥, i.e. ω ⋆ π ∈ ⊥ ⊥, which is clear, since ω || -X0.
To move up from p to p + 1, let π ∈ Xs p+1 0 . We have :

σ p+1 0 ⋆ φ . ω . π ≡ (σ)(σ) p 0 ⋆ φ . ω . π ≻ σ ⋆ σ p 0 . φ . ω . π ≻ φ ⋆ (σ p 0)φω . π.
But, by induction hypothesis, we have σ p 0 ⋆ φ . ω . ρ ∈ ⊥ ⊥ for every ρ ∈ Xs p 0 . It follows that (σ p 0)φω || -Xs p 0. Since φ || -Xs p 0 → Xs p+1 0, we obtain φ ⋆ (σ p 0)φω . π ∈ ⊥ ⊥.

q.e.d. Theorem 13 shows that we can use the predicate ent(x) instead of int(x), which greatly simplifies many computations. In particular, we define the universal quantifier restricted to integers ∀x int by putting ∀x int F ≡ ∀x(int(x) → F ). Thus, we can replace it with the universal quantifier restricted to ent(x) defined as follows :

∀x ent F ≡ ∀x(ent(x) → F ). Then, we have ∀x ent F = {n . π; n ∈ N, π ∈ F [s n 0/x] }.
Therefore, the truth value of the formula ∀x ent F is much simpler than the one of the formula ∀x int F .

Theorem 14. Let φ : N → N be a recursive function. There exists a closed λ-term θ such that, if m ∈ N, n = φ(m) and f is a λ-variable, then θmf reduces into f n by weak head reduction.

This is a variant of the theorem of representation of recursive functions by λ-terms. It is proved in [START_REF] Krivine | Realizability in classical logic[END_REF].

Theorem 15. Let φ : N k → N be a recursive function. We define, in M, a function symbol f , by putting f (s m 1 0, . . . , s m k 0) = s n 0 with n = φ(m 1 , . . . , m k ) ; we extend f on P k \ N k in an arbitrary way. Then, there exists a proof-like term θ such that :

θ || -∀x 1 . . . ∀x k [int(x 1 ), . . . , int(x k ) →int(f (x 1 , . . . , x k ))].
For simplicity, we assume k = 1. By theorem 13, it suffices to find a proof-like term θ such that θ || -∀x[ent(x), (ent(f (x)) → ⊥) → ⊥]. In other words : θ ||ent(p), (ent(f (p)) → ⊥) → ⊥ for every p ∈ P . We can suppose that p = s m 0 (otherwise, -ent(p)| = ∅ and the result is trivial). Thus, we have ent(p) = {m} ; we must show :

θ ⋆ m . ξ . π ∈ ⊥ ⊥ for all π ∈ Π and ξ || -ent(s n 0) → ⊥, with n = φ(m).
Take the λ-term θ given by theorem 14. From this theorem, we get :

θ ⋆ m . ξ . π ≻ ξ ⋆ n . π, which is in ⊥ ⊥, by hypothesis on ξ.
q.e.d.

Remark. We have now found proof-like terms which realize all the axioms of second order arithmetic, with a function symbol for each recursive function.

Standard realizability algebras

A realizability algebra A is called standard if its set of terms Λ and its set of stacks Π are defined as follows :

We have a countable set Π 0 which is the set of stack constants.

The terms and the stacks of A are finite sequences of elements of the set :

Π 0 ∪ {B, C, E, I, K, W, cc, ς, χ, χ ′ , k, (, ), [, ],
. } which are obtained by the following rules :

• B, C, E, I, K, W, cc, ς, χ, χ ′ are terms ;

• each element of Π 0 is a stack ;

• if ξ, η are terms, then (ξ)η is a term ;

• if ξ is a term and π a stack, then ξ . π is a stack ;

• if π is a stack, then k[π] is a term. A term of the form k[π] is called continuation. It will also be denoted as k π .
The set of processes of the algebra A is Λ×Π. If ξ ∈ Λ and π ∈ Π, the ordered pair (ξ, π) is denoted as ξ ⋆ π.

Therefore, every stack has the form π = ξ 1 . . . . . ξ n . π 0 , where ξ 1 , . . . , ξ n ∈ Λ and

π 0 ∈ Π 0 (π 0 is a stack constant).
Given a term τ , we put :

π τ = ξ 1 . . . . . ξ n . τ . π 0 .
We choose a recursive bijection from Π onto N, which is written π → n π . We define a preorder relation ≻, on Λ ⋆ Π. It is the least reflexive and transitive relation such that, for all ξ, η, ζ ∈ Λ and π, ̟ ∈ Π, we have :

C ⋆ ξ . η . ζ . π ≻ ξ ⋆ ζ . η . π. B ⋆ ξ . η . ζ . π ≻ (ξ)(η)ζ ⋆ π. cc ⋆ ξ . π ≻ ξ ⋆ k π . π. k π ⋆ ξ . ̟ ≻ ξ ⋆ π. ς ⋆ ξ . π ≻ ξ ⋆ n π . π. χ ⋆ ξ . π τ ≻ ξ ⋆ τ . π. χ ′ ⋆ ξ . τ . π ≻ ξ ⋆ π τ .
Finally, we have a subset ⊥ ⊥ of Λ ⋆ Π which is a final segment for this preorder, which means that :

p ∈ ⊥ ⊥, p ′ ≻ p ⇒ p ′ ∈ ⊥ ⊥.
In other words, we ask that ⊥ ⊥ has the following properties :

(ξ)η ⋆ π / ∈ ⊥ ⊥ ⇒ ξ ⋆ η . π / ∈ ⊥ ⊥. I ⋆ ξ . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ π / ∈ ⊥ ⊥. K ⋆ ξ . η . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ π / ∈ ⊥ ⊥. E ⋆ ξ . η . π / ∈ ⊥ ⊥ ⇒ (ξ)η ⋆ π / ∈ ⊥ ⊥. W ⋆ ξ . η . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ η . η . π / ∈ ⊥ ⊥. C ⋆ ξ . η . ζ . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ ζ . η . π / ∈ ⊥ ⊥. B ⋆ ξ . η . ζ . π / ∈ ⊥ ⊥ ⇒ (ξ)(η)ζ ⋆ π / ∈ ⊥ ⊥. cc ⋆ ξ . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ k π . π / ∈ ⊥ ⊥. k π ⋆ ξ . ̟ / ∈ ⊥ ⊥ ⇒ ξ ⋆ π / ∈ ⊥ ⊥. ς ⋆ ξ . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ n π . π / ∈ ⊥ ⊥. χ ⋆ ξ . π τ / ∈ ⊥ ⊥ ⇒ ξ ⋆ τ . π / ∈ ⊥ ⊥. χ ′ ⋆ ξ . τ . π / ∈ ⊥ ⊥ ⇒ ξ ⋆ π τ / ∈ ⊥ ⊥.
Remark. Thus, the only arbitrary elements in a standard realizability algebra are the set Π 0 of stack constants and the set ⊥ ⊥ of processes.

The axiom of choice for individuals (ACI)

Let A be a standard realizability algebra and M a A-model, the set of individuals of which is denoted as P . Then, we have :

Theorem 16 (ACI). For each closed formula ∀x 1 . . . ∀x m ∀y F with parameters, there exists a function f :

P m+1 → P such that : i) ς || -∀x 1 . . . ∀x m (∀x(ent(x) → F [f (x 1 , . . . , x m , x)/y]) → ∀y F ). ii) ς || -∀x 1 . . . ∀x m (∀x(int(x) → F [f (x 1 , . . . , x m , x)/y]) → ∀y F ).
For p 1 , . . . , p m , k ∈ P , we define f (p 1 , . . . , p m , k) in an arbitrary way if k / ∈ N. If k ∈ N, we have k = n π k for one and only one stack π k ∈ Π. We define the function f (p 1 , . . . , p m , k) by means of the axiom of choice, in such a way that, if there exists q ∈ P such that :

π k ∈ F [p 1 , . . . , p m , q] , then we have π k ∈ F [p 1 , . . . , p m , f (p 1 , . . . , p m , k)] . i) We must show ς || -∀x(ent(x) → F [p 1 , . . . , p m , f (p 1 , . . . , p m , x)]) → F [p 1 , .
. . , p m , q], for every p 1 , . . . , p m , q ∈ P . Thus, let ξ || -∀x(ent(x) → F [p 1 , . . . , p n , f (p 1 , . . . , p n , x)]) and π ∈ F [p 1 , . . . , p m , q] ; we q.e.d. 3. In the following, there will be individuals which represent sets of integers (proposition 50), but extensionality is not realized. That is why ACI is much weaker than the usual axiom of choice. For instance, it does not imply well-ordering.

must show ς ⋆ ξ . π ∈ ⊥ ⊥, that is ξ ⋆ n π . π ∈ ⊥ ⊥.

Remarks

Generic models

Given a standard realizability algebra A and a A-model M, we now build a new realizability algebra B and a B-model N , which is called generic over M. Then, we shall define the notion of forcing, which is a syntactic transformation on formulas ; it is the essential tool in order to compute truth values in the generic model N . Thus, we consider a standard realizability algebra A and a A-model M, the set of individuals of which is P .

We have a unary predicate C : P → P(Λ), a binary function ∧ : P 2 → P and a distinguished individual 1 ∈ P . We suppose that the data {C, ∧, 1} constitute what we call a forcing structure in M, which means that we have the following property : There exist six proof-like terms α 0 , α 1 , α 2 , β 0 , β 1 , β 2 such that :

τ ∈ |C[(p∧q)∧r]| ⇒ α 0 τ ∈ |C[p∧(q∧r)]| ; τ ∈ |C[p]| ⇒ α 1 τ ∈ |C[p∧1]| ; τ ∈ |C[p∧q]| ⇒ α 2 τ ∈ |C[q]| ; τ ∈ |C[p]| ⇒ β 0 τ ∈ |C[p∧p]| ; τ ∈ |C[p∧q]| ⇒ β 1 τ ∈ |C[q∧p]| ; τ ∈ |C[((p∧q)∧r)∧s]| ⇒ β 2 τ ∈ |C[(p∧(q∧r))∧s]|.
We shall call C-expression any finite sequence of symbols of the form γ = (δ 0 )(δ 1 ) . . . (δ k ) where each δ i is one of the proof-like terms α 0 , α 1 , α 2 , β 0 , β 1 , β 2 . Such an expression is not a c-term, but γτ is, for every c-term τ ; the term γτ = (δ 0 )(δ 1 ) . . . (δ k )τ will also be written (γ)τ . Notation. A ∧-term is, by definition, a term which is written with the variables p 1 , . . . , p k , the constant 1 and the binary function symbol ∧. Let t(p 1 , . . . , p k ), u(p 1 , . . . , p k ) be two ∧-terms. The notation :

γ :: t(p 1 , . . . , p k ) ⇒ u(p 1 , . . . , p k ) means that γ is a C-expression such that τ ∈ |C[t(p 1 , . . . , p k )]| ⇒ (γ)τ ∈ |C[u(p 1 , . . . , p k )]|.
Thus, with this notation, the above hypothesis can be written as follows : α 0 :: (p∧q)∧r ⇒ p∧(q∧r) ; α 1 :: p ⇒ p∧1 ; α 2 :: p∧q ⇒ q ; β 0 :: p ⇒ p∧p ; β 1 :: p∧q ⇒ q∧p ; β 2 :: ((p∧q)∧r)∧s ⇒ (p∧(q∧r))∧s.

Lemma 17. There exist C-expressions β ′ 0 , β ′ 1 , β ′ 2 , β 3 , β ′ 3 such that : β ′ 0 :: p∧q ⇒ (p∧q)∧q ; β ′ 1 :: (p∧q)∧r ⇒ (q∧p)∧r ; β ′ 2 :: p∧(q∧r) ⇒ (p∧q)∧r ; β 3 :: p∧(q∧r) ⇒ p∧(r∧q) ; β ′ 3 :: (p∧(q∧r))∧s ⇒ (p∧(r∧q))∧s. We write the sequence of transformations, with the C-expressions which perform them :

• β ′ 0 = (β 1 )(α 2 )(α 0 )(β 0 )
. p∧q; β 0 ; (p∧q)∧(p∧q) ; α 0 ; p∧(q∧(p∧q)) ; α 2 ; q∧(p∧q) ; β 1 ; (p∧q)∧q.

• β ′ 2 = (β 1 )(α 0 )(β 1 )(α 0 )(β 1
). p∧(q∧r) ; β 1 ; (q∧r)∧p ; α 0 ; q∧(r∧p) ; β 1 ; (r∧p)∧q ; α 0 ; r∧(p∧q) ; β 1 ; (p∧q)∧r.

• β ′ 1 = (α 2 )(α 0 )(β 2 )(β 1 )(α 0 )(α 2 )(β 1 )(β ′ 2 )(β ′ 0 )(β 1
). (p∧q)∧r ; β 1 ; r∧(p∧q) ; β ′ 0 (r∧(p∧q))∧(p∧q) ; β ′ 2 ; ((r∧(p∧q))∧p)∧q ; β 1 ; q∧((r∧(p∧q))∧p) ; α 2 ; (r∧(p∧q))∧p ; α 0 ; r∧((p∧q)∧p) ; β 1 ; ((p∧q)∧p)∧r ; β 2 ; (p∧(q∧p))∧r ; α 0 ; p∧((q∧p)∧r) ; α 2 ; (q∧p)∧r. q.e.d. Lemma 18. Let t be a ∧-term and p a variable of t. Then, there exists a C-expression γ such that γ :: t ⇒ t∧p.

• β 3 = (β 1 )(β ′ 1 )(β 1 ). p∧(q∧r) ; β 1 ; (q∧r)∧p ; β ′ 1 ; (r∧q)∧p ; β 1 ; p∧(r∧q). • β ′ 3 = (β ′ 1 )(β ′ 2 )(β ′ 1 )(α 0 )(β ′ 1 )
Proof by induction on the number of symbols of t which stand after the last occurrence of p. If this number is 0, then t = p or t = u∧p. Then, we have γ = β 0 or β ′ 0 (lemma 17). Otherwise, we have t = u∧v ; if the last occurrence of p is in u, the recurrence hypothesis gives γ ′ :: v∧u ⇒ (v∧u)∧p. Then, we have γ = (β ′ 1 )(γ ′ )(β 1 ). If the last occurrence of p is in v, we have v = v 0 ∧v 1 . If this occurrence is in v 0 , the recurrence hypothesis gives γ ′ ::

u∧(v 1 ∧v 0 ) ⇒ (u∧(v 1 ∧v 0 ))∧p. We put γ = (β ′ 3 )(γ ′ )(β 3 ) (lemma 17). If this occurrence is in v 1 , the recurrence hypothesis gives γ ′ :: (u∧v 0 )∧v 1 ⇒ ((u∧v 0 )∧v 1 )∧p. Then, we put γ = (β 2 )(γ ′ )(β ′
2 ). q.e.d. Lemma 19. Let t, u be two ∧-terms such that each variable of u appears in t. Then, there exists a C-expression γ such that γ :: t ⇒ t∧u.

Proof by recurrence on the length of u. If u = 1, then γ = α 1 ; if u is a variable, we apply lemma 18. If u = v∧w, the recurrence hypothesis gives γ ′ :: t ⇒ t∧v and also γ ′′ :: t∧v ⇒ (t∧v)∧w. Then, we put γ = (α 0 )(γ ′′ )(γ ′ ).

q.e.d.

Theorem 20. Let t, u be two ∧-terms such that each variable of u appears in t. Then, there exists a C-expression γ such that γ :: t ⇒ u.

By lemma 19, we have γ ′ :: t ⇒ t∧u. Thus, we can put γ = (α 2 )(γ ′ ).

q.e.d.

Corollary 21. There exist C-expressions γ I , γ K , γ E , γ W , γ C , γ B , γ cc , γ k such that : γ I :: p∧q ⇒ q ; γ K :: 1∧(p∧(q∧r)) ⇒ p∧r ; γ E :: 1∧(p∧(q∧r)) ⇒ (p∧q)∧r ; γ W :: 1∧(p∧(q∧r)) ⇒ p∧(q∧(q∧r)) ; γ C :: 1∧(p∧(q∧(r∧s))) ⇒ p∧(r∧(q∧s)) ; γ B :: 1∧(p∧(q∧(r∧s))) ⇒ (p∧(q∧r))∧s ; γ cc :: 1∧(p∧q) ⇒ p∧(q∧q) ; γ k :: p∧(q∧r) ⇒ q∧p.

The algebra B

We define now a new realizability algebra B = (Λ, Π, Λ ⋆ Π, ⊥ ⊥ ⊥) : its set of terms is Λ = Λ×P , its set of stacks is Π = Π×P and its set of processes is

Λ ⋆ Π = (Λ ⋆ Π)×P . The distinguished subset ⊥ ⊥ B of Λ ⋆ Π is denoted by ⊥ ⊥ ⊥. It is defined as follows : (ξ ⋆ π, p) ∈ ⊥ ⊥ ⊥ ⇔ (∀τ ∈ C[p]) ξ ⋆ π τ ∈ ⊥ ⊥.
For (ξ, p) ∈ Λ and (π, q) ∈ Π, we put : (ξ, p) ⋆ (π, q) = (ξ ⋆ π, p∧q) ;

(ξ, p) . (π, q) = (ξ . π, p∧q).

For (ξ, p), (η, q) ∈ Λ, we put : (ξ, p)(η, q) = (α 0 ξη, p∧q) with α 0 = λx(χ)λy(χ ′ x)(α 0 )y.

Lemma 22. For each C-expression γ, we put γ = λx(χ)λy(χ ′ x)(γ)y.

Then, we have γ ⋆ ξ . π τ ≻ ξ ⋆ π γτ . This is immediate, by means of theorem 2. We could take also γ = (χ)λxλy(χ ′ y)(γ)x. q.e.d.

γ ⋆ ξ . π τ / ∈ ⊥ ⊥. Therefore, we have ξ ⋆ π γτ / ∈ ⊥ ⊥ et γτ ∈ C[u(p 1 , . . . , p k )]. It follows that : (ξ ⋆ π, u(p 1 , . . . , p k )) / ∈ ⊥ ⊥ ⊥. q.e.d.
Lemma 24. We have (ξ, p)(η, q) ⋆ (π, r) /

∈ ⊥ ⊥ ⊥ ⇒ (ξ, p) ⋆ (η, q) . (π, r) / ∈ ⊥ ⊥ ⊥.
By hypothesis, we have (α 0 ξη ⋆ π, (p∧q)∧r) / ∈ ⊥ ⊥ ⊥ ; thus, there exists τ ∈ C[(p∧q)∧r] such that α 0 ξη ⋆ π τ / ∈ ⊥ ⊥. By lemma 22, we have ξ ⋆ η . π α 0 τ / ∈ ⊥ ⊥ ; since α 0 τ ∈ C[p∧(q∧r)], we have (ξ ⋆ η . π, p∧(q∧r)) / ∈ ⊥ ⊥ and thus (ξ, p) ⋆ (η, q) . (π, r) / ∈ ⊥ ⊥ ⊥. q.e.d. We define the elementary combinators B, C, E, I, K, W, cc of the algebra B by putting :

B = (B * , 1) ; C = (C * , 1) ; E = (E * , 1) ; I = (I * , 1) ; K = (K * , 1) ; W = (W * , 1) ; cc = (cc * , 1) with B * = λxλyλz(γ B )(α 0 x)(α 0 )yz ; C * = γ C C ; E * = λxλy(γ E )(α 0 )xy ; I * = γ I I ; K * = γ K K ; W * = γ W W ; cc * = (χ)λxλy(cc)λk((χ ′ y)(γ cc )x)(χ)λxλy(k)(χ ′ y)(γ k )x. We put k (π,p) = (k * π , p) with k * π = (χ)λxλy(k π )(χ ′ y)(γ k )
x. Theorem 25. For every ξ, η, ζ ∈ Λ and π, ̟ ∈ Π, we have :

I ⋆ ξ . π / ∈ ⊥ ⊥ ⊥ ⇒ ξ ⋆ π / ∈ ⊥ ⊥ ⊥ ; K ⋆ ξ . η . π / ∈ ⊥ ⊥ ⊥ ⇒ ξ ⋆ π / ∈ ⊥ ⊥ ⊥ ; E ⋆ ξ . η . π / ∈ ⊥ ⊥ ⊥ ⇒ ( ξ)η ⋆ π / ∈ ⊥ ⊥ ⊥ ; W ⋆ ξ . η . π / ∈ ⊥ ⊥ ⊥ ⇒ ξ ⋆ η . η . π / ∈ ⊥ ⊥ ⊥. B ⋆ ξ . η . ζ . π / ∈ ⊥ ⊥ ⊥ ⇒ ( ξ)(η) ζ ⋆ π / ∈ ⊥ ⊥ ⊥ ; C ⋆ ξ . η . ζ . π / ∈ ⊥ ⊥ ⊥ ⇒ ξ ⋆ ζ . η . π / ∈ ⊥ ⊥ ⊥. cc ⋆ ξ . π / ∈ ⊥ ⊥ ⊥ ⇒ ξ ⋆ k π . π / ∈ ⊥ ⊥ ⊥. k π ⋆ ξ . ̟ / ∈ ⊥ ⊥ ⊥ ⇒ ξ ⋆ π / ∈ ⊥ ⊥ ⊥.
We shall prove only the cases W, B, k π, cc.

We put ξ = (ξ, p), η = (η, q), ζ = (ζ, r), π = (π, s), ̟ = (̟, q). Suppose W ⋆ ξ . η . π / ∈ ⊥ ⊥ ⊥, and therefore (γ W W ⋆ ξ . η . π, 1∧(p∧(q∧s))) / ∈ ⊥ ⊥ ⊥.

Thus, there exists

τ ∈ C[1∧(p∧(q∧s))] such that γ W W ⋆ ξ . η . π τ / ∈ ⊥ ⊥. Since γ W W ⋆ ξ . η . π τ ≻ ξ ⋆ η . η . π γ W τ , we have ξ ⋆ η . η . π γ W τ / ∈ ⊥ ⊥. But γ W τ ∈ C[p∧(q∧(q∧s))] and it follows that ξ ⋆ η . η . π / ∈ ⊥ ⊥ ⊥. Suppose B ⋆ ξ . η . ζ . π / ∈ ⊥ ⊥ ⊥, that is (B * ⋆ ξ . η . ζ . π, 1∧(p∧(q∧(r∧s)))) / ∈ ⊥ ⊥ ⊥.
Thus, there exists

τ ∈ C[1∧(p∧(q∧(r∧s)))] such that B * ⋆ ξ . η . ζ . π τ / ∈ ⊥ ⊥. But, we have B * ⋆ ξ . η . ζ . π τ ≻ (γ B )(α 0 ξ)(α 0 )ηζ ⋆ π τ (by theorem 2)
≻ (α 0 ξ)(α 0 )ηζ ⋆ π γ B τ (by lemma 22). Therefore, we have (α 0 ξ)(α 0 )ηζ ⋆ π γ B τ / ∈ ⊥ ⊥. But γ B τ ∈ C[(p∧(q∧r))∧s] and thus, we have : ((α 0 ξ)(α 0 )ηζ ⋆ π, (p∧(q∧r))∧s) / ∈ ⊥ ⊥ ⊥, in other words ( ξ

)(η) ζ ⋆ π / ∈ ⊥ ⊥ ⊥. Suppose k π ⋆ ξ . ̟ / ∈ ⊥ ⊥ ⊥, that is (k * π ⋆ ξ . ̟, s∧(p∧q)) / ∈ ⊥ ⊥ ⊥. Thus, there exists τ ∈ C[s∧(p∧q)] such that k * π ⋆ ξ . ̟ τ / ∈ ⊥ ⊥. But we have : k * π ⋆ ξ . ̟ τ ≻ λxλy(k π )(χ ′ y)(γ k )x ⋆ τ . ξ . ̟ ≻ (k π )(χ ′ ξ)(γ k )τ ⋆ ̟ (by theorem 2) ≻ (χ ′ ξ)(γ k )τ ⋆ π ≻ χ ′ ⋆ ξ . γ k τ . π ≻ ξ ⋆ π γ k τ . Thus, we have ξ ⋆ π γ k τ / ∈ ⊥ ⊥ ; but, since γ k τ ∈ C[p∧s], we get ξ ⋆ π / ∈ ⊥ ⊥ ⊥. Suppose cc ⋆ ξ . π / ∈ ⊥ ⊥ ⊥, that is (cc * ⋆ ξ . π, 1∧(p∧s)) / ∈ ⊥ ⊥ ⊥.
Thus, there exists τ ∈ C[1∧(p∧s)] such that cc * ⋆ ξ . π τ / ∈ ⊥ ⊥. But we have :

cc * ⋆ ξ . π τ ≻ λxλy(cc)λk((χ ′ y)(γ cc )x)(χ)λxλy(k)(χ ′ y)(γ k )x ⋆ τ . ξ . π ≻ (cc)λk((χ ′ ξ)(γ cc )τ )(χ)λxλy(k)(χ ′ y)(γ k )x ⋆ π ≻ ((χ ′ ξ)(γ cc )τ )(χ)λxλy(k π )(χ ′ y)(γ k )x ⋆ π ≻ χ ′ ⋆ ξ . γ cc τ . (χ)λxλy(k π )(χ ′ y)(γ k )x . π ≻ ξ ⋆ (χ)λxλy(k π )(χ ′ y)(γ k )x . π γccτ ≡ ξ ⋆ k * π . π γccτ . It follows that ξ ⋆ k * π . π γccτ / ∈ ⊥ ⊥. But we have γ cc τ ∈ C[p∧(s∧s)] and it follows that we have (ξ, p) ⋆ (k * π , s) . (π, s) / ∈ ⊥ ⊥ ⊥, that is ξ⋆ k π . π / ∈ ⊥ ⊥ ⊥. q.e.d.
We have now completely defined the realizability algebra B. For each closed c-term t (proof-like term), let us denote by t B its value in the algebra B (its value in the standard algebra A is t itself). Thus, we have t B = (t * , 1 t ), where t * is a proof-like term and 1 t a condition written with 1, ∧ and parentheses, which are obtained as follows, by recurrence on t : • If t is an elementary combinator B, C, E, I, K, W, cc, then t * is already defined ;

1 t = 1. • (tu) * = α 0 t * u * ; 1 tu = 1 t ∧1 u .

The model N

The B-model N has the same set P of individuals and the same functions as M. By definition, the k-ary predicates of N are the applications from P k into P(Π). But, since Π = Π×P , they are the same as the applications from P k+1 into P(Π), i.e. the k + 1-ary predicates of the model M. Each predicate constant R, of arity k, is interpreted, in the model M, by an application R M from P k into P(Λ). In the model N , this predicate constant is interpreted by the application R N : P k → P(Λ), where R N (p 1 , . . . , p k ) = R M (p 1 , . . . , p k )×{1}. For each closed formula F , with parameters in N , its truth value, which is a subset of Π, will be denoted by |F |. We shall write (ξ, p) | -F to mean that (ξ, p) ∈ Λ realizes F , in other words (∀π ∈ Π)(∀q ∈ P )(((π, q) ∈ |F |) ⇒ (ξ, p) ⋆ (π, q) ∈ ⊥ ⊥ ⊥).

Theorem 26. If we have ⊢ t : A in classical second order logic, where A is a closed formula, then

t B = (t * , 1 t ) | -A.
Immediate application of theorem 3 (adequacy lemma) in the B-model N .

q.e.d. i) We must show that, for each (π, q) ∈ |F |, we have (γξ, p) ⋆ (π, q) ∈ ⊥ ⊥ ⊥, that is :

(γξ ⋆ π, p∧q) ∈ ⊥ ⊥ ⊥. Thus, let τ ∈ C[p∧q], so that γτ ∈ C[1∧q].
Since we have, by hypothesis, (ξ ⋆ π, 1∧q) ∈ ⊥ ⊥ ⊥, it follows that ξ ⋆ π γτ ∈ ⊥ ⊥ and therefore γξ ⋆ π τ ∈ ⊥ ⊥. ii) By hypothesis, there exists

τ ∈ C[p] such that ξ ⋆ π τ / ∈ ⊥ ⊥. Thus, we have η ⋆ π τ / ∈ ⊥ ⊥, so that (η ⋆ π, p) / ∈ ⊥ ⊥ ⊥. Let (π, q) ∈ |F | ; we have (η, p) ⋆ (π, q) ∈ ⊥ ⊥ ⊥, that is (η ⋆ π, p∧q) ∈ ⊥ ⊥.
From what we have just shown, it follows that (ξ ⋆ π, p∧q) ∈ ⊥ ⊥, and therefore (ξ, p) ⋆ (π, q) ∈ ⊥ ⊥ ⊥.

q.e.d.

The integers of the model N

Recall that we have put : σ = λnλf λx(f )(n)f x, 0 = λxλy y and n = (σ) n 0 for every integer n. Thus, we have σ B = (σ * , 1 σ ) and n B = ((σ

) n 0) B = (n * , 1 n ). Therefore 0 B = (KI) B = (K * , 1)(I * , 1) and n + 1 B = σ B n B = (σ * , 1 σ )(n * , 1 n ).
Thus, the recursive definitions of n * , 1 n are the following :

0 * = α 0 K * I * ; (n + 1) * = α 0 σ * n * ; 1 0 = 1∧1 ; 1 n+1 = 1 σ ∧1 n .
We can define the unary predicate ent(x) in the model N in two distinct ways : i) From the predicate ent(x) of the model M, by putting :

|ent(s n 0)| = {(n, 1)} ; |ent(p)| = ∅ if p / ∈ N.
ii) By using directly the definition of ent(x) in the model N ; we denote this predicate by ent N (x). Therefore, we have : [START_REF] Krivine | Realizability in classical logic[END_REF], applied in the model N , we know that the predicates int(x) and ent N (x) are interchangeable. Theorem 28 shows that the predicates int(x) and ent(x) are also interchangeable. Thus, we have three predicates which define the integers in the model N ; it is the predicate ent(x) that we shall mostly use in the sequel. In particular, we shall often replace the quantifier ∀x int with ∀x ent . Theorem 28. There exist two proof-like terms T, J such that :

|ent N (s n 0)| = {n B } ; |ent N (p)| = ∅ if p / ∈ N. From theorem
i) (T, 1) | -∀X∀x((ent(x) → X), int(x) → X). ii) (J, 1) | -∀x(ent(x) →int(x)).
i) We apply theorem 12 to the sequence u : N → Λ defined by u n = (n, 1).

We are looking for two proof-like terms T, S such that :

(S, 1) ⋆ (ψ, p) . (n, 1) . (π, r) ≻ (ψ, p) ⋆ (n + 1, 1) . (π, r) ; (S, 1) | -⊤ → ⊥, ⊤ → ⊥.
(T, 1) ⋆ (φ, p) . (ν, q) . (π, r) ≻ (ν, q) ⋆ (S, 1) . (φ, p) . (0, 1) . (π, r).

Then theorem 12 will give the desired result : (T, 1) | -∀X∀x((ent(x) → X), int(x) → X). We put S = λf λx(γf )(σ)x, with γ :: 1∧(p∧(q∧r)) ⇒ p∧(q∧r).

Then, we have (S, 1) ⋆ (ψ, p) . (ν, q) . (π, r) ≡ (S ⋆ ψ . ν . π, 1∧(p∧(q∧r))) ≻ (γψ ⋆ σν . π, 1∧(p∧(q∧r))) (theorem 2 and proposition 27(ii)) ≻ (ψ ⋆ σν . π, p∧(q∧r)) (proposition 23) ≡ (ψ, p) ⋆ (σν, q) . (π, r).

Suppose first that (ψ, p) | -⊤ → ⊥ ; then, we have (ψ, p) ⋆ (σν, q) . (π, r) ∈ ⊥ ⊥ ⊥ and thus : (S, 1) ⋆ (ψ, p) . (ν, q) . (π, r) ∈ ⊥ ⊥ ⊥. This shows that (S, 1) | -⊤ → ⊥, ⊤ → ⊥. Moreover, if we put ν = n, so that σν = n + 1, and q = 1, we have shown that :

(S, 1) ⋆ (ψ, p) . (n, 1) . (π, r) ≻ (ψ, p) ⋆ (n + 1, 1) . (π, r). Now, we put T = λf λx(γ ′ x)Sf 0, with γ ′ :: 1∧(p∧(q∧r))] ⇒ q∧(1∧(p∧(1∧r))).

Then, we have (T, 1) ⋆ (φ, p) . (ν, q) . (π, r) ≡ (T ⋆ φ . ν . π, 1∧(p∧(q∧r))) ≻ (γ ′ ν ⋆ S . φ . 0 . π, 1∧(p∧(q∧r))) (theorem 2 and proposition 27(ii)) ≻ (ν ⋆ S . φ . 0 . π, q∧(1∧(p∧(1∧r)))) (proposition 23) ≡ (ν, q) ⋆ (S, 1) . (φ, p) . (0, 1) . (π, r) which is the desired result.

ii) We are looking for a proof-like term J such that (J,

1) | -∀x(ent(x) →int(x)). It is sufficient to have (J, 1) | -ent(s n 0) →int(s n 0) for each n ∈ N, since | ent(p)| = ∅ if p / ∈ N.
Let (π, q) ∈ |int(n) | ; we must have (J, 1) ⋆ (n, 1) . (π, q) ∈ ⊥ ⊥ ⊥, that is :

(J ⋆ n . π, 1∧(1∧q)) ∈ ⊥ ⊥ ⊥. But, we have (n * , 1 n ) = ((σ) n 0) B | -int(s n 0) (theorem 3, applied in B) and therefore : (n * , 1 n ) ⋆ (π, q) ∈ ⊥ ⊥ ⊥ or else (n * ⋆ π, 1 n ∧q) ∈ ⊥ ⊥ ⊥. Thus, let τ ∈ C[1∧(1∧q)] ; we have then (γ) n (γ 0 )τ ∈ C[1 n ∧q]
where γ 0 and γ are two C-expressions such that : γ 0 :: 1∧(1∧q) ⇒ (1∧1)∧q ; γ :: p∧q ⇒ (1 σ ∧p)∧q. Indeed, we have seen that 1 0 = 1∧1 and

1 n+1 = 1 σ ∧1 n . It follows that, if τ ∈ C[1∧(1∧q)], then (γ 0 )τ ∈ C[1 0 ∧q], and therefore (γ) n (γ 0 )τ ∈ C[1 n ∧q].
Thus, we have n * ⋆ π (γ) n (γ 0 )τ ∈ ⊥ ⊥. Now, we build below two proof-like terms g, j such that, for each n ∈ N, we have :

a) g ⋆ n . ξ . π τ ≻ ξ ⋆ π (γ) n (γ 0 )τ ; b) j ⋆ n . ξ . π ≻ ξ ⋆ n * . π.
Then, by putting J = λx(gx)(j)x, we have J ⋆ n . π τ ≻ n * ⋆ π (γ) n (γ 0 )τ ∈ ⊥ ⊥, which is the desired result. a) We put g = λkλx(γ 0 )(k)γx ; from theorem 2, we have :

g ⋆ n . ξ . π τ ≻ γ 0 ⋆ (n)γξ . π τ ≻ (n)γξ ⋆ π (γ 0 )τ .
Thus, it suffices to show that (n)γξ ⋆ π τ ≻ ξ ⋆ π (γ) n τ which we do by recurrence on n.

If n = 0, we have immediately 0 ⋆ γ . ξ . π τ ≻ ξ ⋆ π τ since 0 = λxλy y. Going from n to n + 1 : we have (n + 1)γξ

⋆ π τ ≡ (σn)γξ ⋆ π τ ≻ σ ⋆ n . γ . ξ . π τ ≻ γ ⋆ (n)γξ . π τ ≻ (n)γξ ⋆ π (γ)τ ≻ ξ ⋆ π (γ) n+1 τ by induction hypothesis. b) We put β = α 0 σ * , U = λgλy(g)(β)y and j = λkλf (k)Uf 0 * .
Therefore, we have j ⋆ n . ξ . π ≻ nUξ ⋆ 0 * . π. We show, by recurrence on n, that : nUξ ⋆ k * . π ≻ ξ ⋆ (n + k) * . π for each integer k, which gives the desired result with k = 0. For n = 0, we have 0Uξ ⋆ k * . π ≻ ξ ⋆ k * . π since 0 = λxλy y. Going from n to n+1 : we have

(n + 1)⋆U . ξ . k * . π ≡ σn⋆U . ξ . k * . π ≻ U ⋆nUξ . k * . π (since σ = λnλf λx(f )(n)f x) ≻ nUξ ⋆ βk * . π ≡ nUξ ⋆ (k + 1) * . π ≻ ξ ⋆ (n + k + 1) * . π by induction hypothesis.
q.e.d.

Forcing

Forcing is a method to compute truth values of formulas in the generic B-model N .

For each k-ary predicate variable X, we add to the language a new predicate variable, denoted by X + , which has arity k + 1. In the A-model M, we use the variables X and X + ; in the B-model N , only the variables X.

With each k-ary second order parameter X : P k → P(Π) of the model N , we associate a (k + 1)-ary second order parameter X + : P k+1 → P(Π) of the model M. It is defined in an obvious way, since Π = Π×P ; we put :

X + (p, p 1 , . . . , p k ) = {π ∈ Π; (π, p) ∈ X (p 1 , . . . , p k )}.
For each formula F written without the variables X + , with parameters in the model N , we define, by recurrence on F , a formula denoted by p [] -F (read " p forces F "), with parameters in the model A, written with the variables X + and a free condition variable p :

If F is atomic of the form X(t 1 , . . . , t k ), then p [] -F is ∀q(C[p∧q] → X + (q, t 1 , . . . , t k )). If F is atomic of the form X (t 1 , . . . , t k ), then p [] -F is ∀q(C[p∧q] → X + (q, t 1 , . . . , t k )). If F ≡ (A → B) where A, B are formulas, then p [] -F is ∀q(q [] -A → p∧q [] -B). If F ≡ (R(t 1 , . . . , t k ) → B), where R is a predicate constant, then : p [] -F is (R(t 1 , . . . , t k ) → p [] -B). If F ≡ (t 1 = t 2 → B), then p [] -F is (t 1 = t 2 → p [] -B). If F ≡ ∀x A, then p [] -F is ∀x(p [] -A). If F ≡ ∀X A, then p [] -F is ∀X + (p [] -A).
Thus we have, in particular :

If F ≡ ∀x ent A , then p [] -F is ∀x ent (p [] -A).
Lemma 29. Let F be a formula the free variables of which are amongst X 1 , . . . , X k and let X 1 , . . . , X k be second order parameters in the model N , with corresponding arities. Then, we have :

(p [] -F )[X + 1 /X + 1 , . . . , X + k /X + k ] ≡ (p [] -F [X 1 /X 1 , . . . , X k /X k ]).
Immediate, by recurrence on F . q.e.d.

Theorem 30.

For each closed formula F with parameters in the model N , there exist two proof-like terms χ F , χ ′ F , which only depend on the propositional structure of F , such that we have :

ξ || -(p [] -F ) ⇒ (χ F ξ, p) | -F ; (ξ, p) | -F ⇒ χ ′ F ξ || -(p [] -F ) for every ξ ∈ Λ and p ∈ P .
The propositional structure of F is the simple type built with only one atom O and the connective →, which is obtained from F by deleting all quantifiers, all symbols → with their hypothesis, and by identifying all atomic formulas with O. For instance, the propositional structure of the formula :

∀X(∀x(∀y(f (x, y) = 0 → Xy) → Xx) → ∀x Xx) is (O → O) → O.
Proof by recurrence on the length of F .

• If F is atomic, we have F ≡ X (t 1 , . . . , t k ) ; we show that χ F = χ and χ ′ F = χ ′ . Indeed, we have :

p [] -F = ∀q(C[p∧q] → X + (q, t 1 , . . . , t k ) = q {τ . π; τ ∈ C[p∧q], (π, q) ∈ |X (t 1 , . . . , t k ) |},
because, by definition of X + , we have π ∈ X + (q, t 1 , . . . , t k ) ⇔ (π, q) ∈ |X (t 1 , . . . , t k ) |. Therefore, we have :

( * ) ξ || -(p [] -F ) ⇔ (∀q ∈ P )(∀τ ∈ C[p∧q])(∀π ∈ Π)((π, q) ∈ |X (t 1 , . . . , t k ) | ⇒ ξ ⋆ τ . π ∈ ⊥ ⊥). Moreover, we have (ξ, p) | -F ⇔ (∀q ∈ P )(∀π ∈ Π)((π, q) ∈ |F | ⇒ (ξ, p) ⋆ (π, q) ∈ ⊥ ⊥ ⊥) ⇔ (∀q ∈ P )(∀π ∈ Π)((π, q) ∈ |F | ⇒ (ξ ⋆ π, p∧q) ∈ ⊥ ⊥ ⊥) and finally, by definition of ⊥ ⊥ ⊥ : ( * * ) (ξ, p) | -F ⇔ (∀q ∈ P )(∀τ ∈ C[p∧q])(∀π ∈ Π)((π, q) ∈ |F | ⇒ ξ ⋆ π τ ∈ ⊥ ⊥). Suppose that ξ || -(p [] -F ). Since χξ ⋆ π τ ≻ ξ ⋆ τ . π, we have from ( * ) : (∀q ∈ P )(∀τ ∈ C[p∧q])(∀π ∈ Π)((π, q) ∈ |X (t 1 , . . . , t k ) | ⇒ χξ ⋆ τ . π ∈ ⊥ ⊥)
and therefore (χξ, p) | -F from ( * * ). Conversely, suppose that (ξ, p) | -F . By applying ( * * ) and χ ′ ξ ⋆ τ . π ≻ ξ ⋆ π τ , we obtain (∀q

∈ P )(∀τ ∈ C[p∧q])(∀π ∈ Π)((π, q) ∈ |F | ⇒ χ ′ ξ ⋆ τ . π ∈ ⊥ ⊥) and therefore χ ′ ξ || -(p [] -F ) from ( * ). • If F ≡ ∀X A, then p [] -F ≡ ∀X + (p [] -A). Therefore, we have ξ || -(p [] -F ) ≡ ∀X + (ξ || -(p [] -A)). Moreover, we have (ξ, p) | -F ≡ ∀X((ξ, p) | -A).
Let X : P k → P(Π) be a second order parameter in the model N , with the same arity as X, and let X + be the corresponding parameter of the model M.

If ξ || -(p [] -F ), then we have (ξ || -(p [] -A))[X + /X + ], thus ξ || -(p [] -A[X /X]), from lemma 29.
By the recurrence hypothesis, we have

(χ A ξ, p) | -A[X /X]. Since X is arbitrary, it follows that (χ A ξ, p) | -∀X A. Conversely, if we have (ξ, p) | -F , then (ξ, p) | -A[X /X]
for every X . By the recurrence hypothesis, we have

χ ′ A ξ || -(p [] -A[X /X]
), and therefore :

χ ′ A ξ || -(p [] -A)[X + /X + ]
), from lemma 29. Since X + is arbitrary, it follows that :

χ ′ A ξ || -∀X + (p [] -A), that is χ ′ A ξ || -(p [] -∀X A). • If F ≡ ∀x A, then p [] -F ≡ ∀x(p [] -A). Therefore ξ || -p [] -F ≡ ∀x(ξ || -(p [] -A)). Moreover, (ξ, p) | -F ≡ ∀x((ξ, p) | -A).
The result is immediate, from the recurrence hypothesis.

• If F ≡ (t 1 = t 2 → A), then p [] -F ≡ t 1 = t 2 → p [] -A. Therefore : ξ || -(p [] -F ) ≡ (t 1 = t 2 → ξ || -(p [] -A)). Moreover, (ξ, p) | -F ≡ (t 1 = t 2 → (ξ, p) | -A).
The result is immediate, from the recurrence hypothesis.

• If F ≡ A → B, we have p [] -F ≡ ∀q(q [] -A → p∧q [] -B) and therefore : ( * ) ξ || -(p [] -F ) ⇒ ∀η∀q(η || -(q [] -A) → ξη || -(p∧q [] -B)). Suppose that ξ || -(p [] -F ) and put χ F = λxλy(γ 0 )(χ B )(x)(χ ′ A )y. We must show (χ F ξ, p) | -A → B ; thus, let (η, q) | -A and (π, r) ∈ |B |. We must show (χ F ξ, p) ⋆ (η, q) . (π, r) ∈ ⊥ ⊥ ⊥ that is (χ F ξ ⋆ η . π, p∧(q∧r)) ∈ ⊥ ⊥ ⊥. Thus, let τ ∈ C[p∧(q∧r)] ; we must show χ F ξ ⋆ η . π τ ∈ ⊥ ⊥ or else χ F ⋆ ξ . η . π τ ∈ ⊥ ⊥.
From the recurrence hypothesis applied to (η, q) | -A, we have

χ ′ A η || -(q [] -A). From ( * ), we have therefore (ξ)(χ ′ A )η || -(p∧q [] -B).
Applying again the recurrence hypothesis, we get :

((χ B )(ξ)(χ ′ A )η, p∧q) | -B. But since (π, r) ∈ |B |, we have : ((χ B )(ξ)(χ ′ A )η, p∧q) ⋆ (π, r) ∈ ⊥ ⊥ ⊥, that is ((χ B )(ξ)(χ ′ A )η ⋆ π, (p∧q)∧r) ∈ ⊥ ⊥ ⊥. Since τ ∈ C[p∧(q∧r)], we have γ 0 τ ∈ C[(p∧q)∧r] and therefore (χ B )(ξ)(χ ′ A )η ⋆ π γ 0 τ ∈ ⊥ ⊥.
But, by definition of χ F , we have, from theorem 2 :

χ F ⋆ ξ . η . π τ ≻ (χ B )(ξ)(χ ′ A )η ⋆ π γ 0 τ which gives the desired result : χ F ⋆ ξ . η . π τ ∈ ⊥ ⊥. Suppose now that (ξ, p) | -A → B ; we put χ ′ F = λxλy(χ ′ B )(α 0 x)(χ A )y. We must show χ ′ F ξ || -(p [] -A → B) that is ∀q(χ ′ F ξ || -(q [] -A → p∧q [] -B)). Thus, let η || -q [] -A and π ∈ p∧q [] -B ; we must show χ ′ F ξ ⋆ η . π ∈ ⊥ ⊥.

By the recurrence hypothesis, we have (χ

A η, q) | -A, therefore (ξ, p)(χ A η, q) | -B or else, by definition of the algebra B : ((α 0 ξ)(χ A )η, p∧q) | -B. Applying again the recurrence hypothesis, we have (χ ′ B )(α 0 ξ)(χ A )η || -(p∧q [] -B) and therefore : (χ ′ B )(α 0 ξ)(χ A )η ⋆ π ∈ ⊥ ⊥. But we have : χ ′ F ξ ⋆ η . π ≻ χ ′ F ⋆ ξ . η . π ≻ (χ ′ B )(α 0 ξ)(χ A )η ⋆ π
from theorem 2 ; the desired result follows.

q.e.d. A formula F is said to be first order if it is obtained by the following rules : • ⊥ is first order.

• If A, B are first order, then A → B is first order.

• If B is first order, R is a predicate symbol and t 1 , . . . , t k are terms with parameters, then R(t 1 , . . . , t k ) → B, t 1 = t 2 → B are first order.

• If A is first order, then ∀x A is first order (x is an individual variable).

Remarks. i) If

A is a first order formula, it is the same for ∀x ent A. ii) This notion will be extended below (see proposition 37).

Theorem 31. Let F be a closed first order formula. There exist two proof-like terms δ F , δ ′ F , which depend only on the propositional structure of F , such that we have :

ξ || -(C[p] → F ) ⇒ (δ F ξ, p) | -F ; (ξ, p) | -F ⇒ δ ′ F ξ || -(C[p] → F ) for every ξ ∈ Λ and p ∈ P .
The proof is by recurrence on the construction of F following the above rules.

• If F is ⊥, we put : δ ⊥ = λx(χ)λy(x)(α)y with α :: p∧q ⇒ p . δ ′ ⊥ = λxλy(χ ′ x)(α ′ )y with α ′ :: p ⇒ p∧1 . Indeed, suppose that ξ || -C[p] → ⊥ and let us show that (δ ⊥ ξ, p)(π, q) ∈ ⊥ ⊥ ⊥, that is : (δ ⊥ ξ ⋆ π, p∧q) ∈ ⊥ ⊥ ⊥. Thus, let τ ∈ C[p∧q], so that ατ ∈ C[p], so that ξ ⋆ ατ . π ∈ ⊥ ⊥, by hypothesis on ξ, which gives δ ⊥ ξ ⋆ π τ ∈ ⊥ ⊥. Conversely, if (ξ, p) | -⊥, we have (ξ, p) ⋆ (π, 1) ≡ (ξ ⋆ π, p∧1) ∈ ⊥ ⊥ ⊥ for every π ∈ Π. But, if τ ∈ C[p], we have α ′ τ ∈ C[p∧1], therefore ξ ⋆ π α ′ τ ∈ ⊥ ⊥, thus δ ′ ⊥ ξ ⋆ τ . π ∈ ⊥ ⊥. Therefore δ ′ ⊥ ξ || -C[p] → ⊥. • If F is A → B, we put : δ A→B = λxλy(χ)λz((χ ′ )(δ B )λd((x)(α)z)(δ ′
A y)(β)z)(γ)z with α :: p∧(q∧r) ⇒ p; β :: p∧(q∧r) ⇒ q ; γ :: p∧(q∧r) ⇒ 1∧r. Indeed, suppose that ξ || -C[p], A → B, (η, q) | -A and (π, r) ∈ |B |.

We must show (δ A→B ξ, p) ⋆ (η, q) . (π, r) ∈ ⊥ ⊥ ⊥, that is (δ A→B ξ ⋆ η . π, p∧(q∧r)) ∈ ⊥ ⊥ ⊥. Thus, let τ ∈ C[p∧(q∧r)] ; we must show δ A→B ξ ⋆ η . π τ ∈ ⊥ ⊥.

We have ατ ∈ C[p], βτ ∈ C[q] ; but, by the recurrence hypothesis, we have :

δ ′ A η || -C[q] → A, therefore (δ ′ A η)(β)τ || -A and ((ξ)(α)τ )(δ ′ A η)(β)τ || -B ; thus λd((ξ)(α)τ )(δ ′ A η)(β)τ || -C[1] → B. From the recurrence hypothesis, we have ((δ B )λd((ξ)(α)τ )(δ ′ A η)(β)τ, 1) | -B, thus : ((δ B )λd((ξ)(α)τ )(δ ′ A η)(β)τ, 1) ⋆ (π, r) ∈ ⊥ ⊥ ⊥, that is : ((δ B )λd((ξ)(α)τ )(δ ′ A η)(β)τ ⋆ π, 1∧r) ∈ ⊥ ⊥ ⊥. But, we have γτ ∈ C[1∧r], therefore (δ B )λd((ξ)(α)τ )(δ ′ A η)(β)τ ⋆ π γτ ∈ ⊥ ⊥, and thus : ((χ ′ )(δ B )λd((ξ)(α)τ )(δ ′ A η)(β)τ )(γ)τ ⋆ π ∈ ⊥ ⊥. It follows that : (χ)λz((χ ′ )(δ B )λd((ξ)(α)z)(δ ′ A η)(β)z)(γ)z ⋆ π τ ∈ ⊥ ⊥ so that δ A→B ξ ⋆ η . π τ ∈ ⊥ ⊥.
We now put :

δ ′ A→B = λxλyλz((δ ′ B )(α 0 x)(δ A )λd z)(α)y with α :: p ⇒ p∧1. Suppose that (ξ, p) | -A → B ; let τ ∈ C[p], η || -A and π ∈ B . We must show : δ ′ A→B ξ ⋆ τ . η . π ∈ ⊥ ⊥. We have λd η || -C[1] → A ; applying the recurrence hypothesis, we have ((δ A )λd η, 1) | -A, thus (ξ, p)((δ A )λd η, 1) | -B that is ((α 0 ξ)(δ A )λd η, p∧1) | -B.
p ⊑ q ∧ q ⊑ p, that is ∀r(¬C[q∧r] ↔ ¬C[p∧r]).

In the sequel, we shall often write F → C[p] instead of ¬C[p] → ¬F ; Then p ⊑ q is written ∀r(C[p∧r] → C[q∧r]) and p ∼ q is written ∀r(C[p∧r] ↔ C[q∧r]).

Remark. We recall that C[p] is not a formula, but a subset of Λ ; in fact, in some realizability models which will be considered below, there will exist a formula C[p] such that :

|C[p]| = {τ ∈ Λ c ; τ || -C[p]}.
In such cases, we can identify C[p] with the formula C[p].

• If F is a closed formula, we shall write | -F to mean that there exists a proof-like term θ such that (θ, 1) | -F . From proposition 27(i), this is equivalent to say that there exists a proof-like term θ such that (θ, p) | -F for every p ∈ P .

Proposition 32. i) ξ || -¬C[p∧q] ⇒ (χξ, p) | -J (q) ; (ξ, p) | -J (q) ⇒ χ ′ ξ || -¬C[p∧q]. ii) ξ || -∀r(C[p∧(1∧r)], C[q] → ⊥) ⇒ (χξ, p) | -¬C[q] ; (ξ, p) | -¬C[q] ⇒ χ ′ ξ || -∀r(C[p∧(1∧r)], C[q] → ⊥). iii) If ξ || -¬R(a 1 , . . . , a k ) then (ξ, p) |
-¬R(a 1 , . . . , a k ) for all p (R is a predicate symbol of arity k).

i) If ξ || -¬C[p∧q], then ξ ⋆ τ . π ∈ ⊥ ⊥ and therefore χξ ⋆ π τ ∈ ⊥ ⊥ for all τ ∈ C[p∧q]. Thus, we have : (χξ ⋆π, p∧q) ∈ ⊥ ⊥ ⊥, that is (χξ, p)⋆(π, q) ∈ ⊥ ⊥ ⊥ for every π ∈ Π, i.e. (χξ, p) | -J (q). If (ξ, p) | -J [q], we have (ξ, p)⋆(π, q) ∈ ⊥ ⊥ ⊥, thus (ξ ⋆π, p∧q) ∈ ⊥ ⊥ ⊥ for all π ∈ Π. Therefore, iii) Let τ ∈ |R(a 1 , . . . , a k )| ; we have ξ ⋆ τ . π ∈ ⊥ ⊥ for all π ∈ Π, thus (ξ ⋆ τ . π, a) ∈ ⊥ ⊥ ⊥ for all a ∈ P , and therefore (ξ, p) ⋆ (τ, 1) . (π, q) ∈ ⊥ ⊥ ⊥.

we have ξ ⋆π τ ∈ ⊥ ⊥, that is χ ′ ξ ⋆τ . π ∈ ⊥ ⊥ for each τ ∈ C[p∧q]. Therefore χ ′ ξ || -¬C[p∧q]. ii) If ξ || -∀r(C[p∧(1∧r)], C[q] → ⊥), we have ξ ⋆ υ . τ . π ∈ ⊥ ⊥ if υ ∈ C[p∧(1∧r)] and τ ∈ C[q]. Therefore χξ ⋆ τ . π υ ∈ ⊥ ⊥, thus (χξ ⋆ τ . π, p∧(1∧r)) ∈ ⊥ ⊥ ⊥ that is : (χξ, p) ⋆ (τ, 1) . (π, r) ∈ ⊥ ⊥. But (τ, 1) is arbitrary in C N [q],
q.e.d.

Theorem 33 (Elementary properties of the generic ideal). i) (α, 1) | -¬J (1) with α ::

1∧(p∧q) ⇒ p∧1. ii) (θ, 1) | -∀x(¬C[x] → J (x))
where θ = λx(χ)λy((χ ′ x)(β)y)(α)y with α :: 1∧(p∧q) ⇒ q and β :: 1∧(p∧q) ⇒ p∧(1∧1). iii) (θ, 1) | -∀x∀y(J (x∧y), ¬J (x) → J (y)) where θ = λxλy(α)(y)(β)x with α :: 1∧(p ′ ∧(q ′ ∧q)) ⇒ q ′ ∧((q∧p ′ )∧1) and β :: (q∧p ′ )∧p ⇒ p ′ ∧(p∧q). iv) (θ, 1) | -∀x(∀y(¬C[x∧y] → J (y)) → ¬J (x)) where θ = λxλy(γ)(x)λz(χ ′ y)(β)z, with β :: p∧q ⇒ q∧p and γ :: 1∧(r∧(q∧r ′ )) ⇒ r∧(1∧p). v) (θ, 1) | -∀x∀y(J (x), y ⊑ x → J (y)) where θ = λxλy((χ)λz(((χ ′ )(α 0 y)λz ′ (χ ′ x)(β)z ′ )(α)z)(γ)z, with α :: 1∧(p ′ ∧(r∧q)) ⇒ (r∧1)∧(1∧1) ; α ′ :: 1∧(p ′ ∧(q ′ ∧q)) ⇒ q∧p ′ ; β :: p∧q ⇒ q∧p. i) Let (ξ, p) | -J (1) ; we must show that (α, 1) ⋆ (ξ, p) . (π, q) ∈ ⊥ ⊥ ⊥, that is to say : (α ⋆ ξ . π, 1∧(p∧q)) ∈ ⊥ ⊥ ⊥. But, from proposition 23, we have : (α ⋆ ξ . π, 1∧(p∧q)) ≻ (ξ ⋆ π, p∧1) ≡ (ξ, p) ⋆ (π, 1). Now, we have (ξ, p) ⋆ (π, 1) ∈ ⊥ ⊥ ⊥ by hypothesis on (ξ, p). ii)Let (η, p) | -¬C[q] and (π, q) ∈ |J (q) |. We must show that (θ, 1) ⋆ (η, p) . (π, q) ∈ ⊥ ⊥ ⊥, i.e. (θ ⋆η . π, 1∧(p∧q)) ∈ ⊥ ⊥ ⊥. Thus, let τ ∈ C[1∧(p∧q)] ; we must show that θ ⋆η . π τ ∈ ⊥ ⊥.

From proposition 32, we have χ ′ η || -C[p∧(1∧1)], C[q] → ⊥. Now, we have βτ ∈ C[p∧(1∧1)] and ατ ∈ C[q], therefore χ ′ η ⋆ βτ . ατ . π ∈ ⊥ ⊥ thus (χ)λy((χ ′ η)(β)y)(α)y ⋆ π τ ∈ ⊥ ⊥ thus θ ⋆ η . π τ ∈ ⊥ ⊥.

iii) Let (ξ, p ′ ) | -J (p∧q), (η, q ′ ) | -¬J (p) and (π, q) ∈ |J (q) |. We must show that :

(θ, 1) ⋆ (ξ, p ′ ) . (η, q ′ ) . (π, q) ∈ ⊥ ⊥ ⊥, i.e. (θ ⋆ ξ . η . π, 1∧(p ′ ∧(q ′ ∧q))) ∈ ⊥ ⊥ ⊥.

From propositions 27(ii) and 23, it suffices to show :

((α)(η)(β)ξ ⋆ π, 1∧(p ′ ∧(q ′ ∧q))) ∈ ⊥ ⊥ ⊥ then (η ⋆ βξ . π, q ′ ∧((q∧p ′ )∧1)) ∈ ⊥ ⊥ ⊥, that is : (η, q ′ ) ⋆ (βξ, q∧p ′ ) . (π, 1) ∈ ⊥ ⊥ ⊥.
By hypothesis on (η, q ′ ), we have now to show that (βξ, q∧p ′ ) | -J (p), i.e. : (βξ, q∧p ′ ) ⋆ (̟, p) ∈ ⊥ ⊥ ⊥, or else (βξ ⋆ ̟, (q∧p ′ )∧p) ∈ ⊥ ⊥ ⊥ for all ̟ ∈ Π. But, by proposition 23, we have : (βξ ⋆ ̟, (q∧p ′ )∧p) ≻ (ξ ⋆ ̟, p ′ ∧(p∧q)) ≡ (ξ, p ′ ) ⋆ (̟, p∧q) ∈ ⊥ ⊥ ⊥ by hypothesis on (ξ, p ′ ). iv) Let (ξ, q) | -J (p) and (η, r) | -∀q(¬C[p∧q] → J (q)) ; we must show that :

(θ, 1) ⋆ (η, r) . (ξ, q) . (π, r ′ ) ∈ ⊥ ⊥ ⊥, that is (θ ⋆ η . ξ . π, 1∧(r∧(q∧r ′ ))) ∈ ⊥ ⊥ ⊥.
From proposition 32(i), we have

χ ′ ξ || -¬C[q∧p]. Let τ ∈ C[p∧q], thus βτ ∈ C[q∧p] there- fore χ ′ ξ ⋆ βτ . ρ ∈ ⊥ ⊥ for every ρ ∈ Π. Therefore, we have λx(χ ′ ξ)(β)x ⋆ τ . ρ ∈ ⊥ ⊥, thus λz(χ ′ ξ)(β)z || -¬C[p∧q]. From proposition 32(iii), we have (λz(χ ′ ξ)(β)z, 1) | -¬C[p∧q].
By hypothesis on (η, r), we thus have (η, r) ⋆ (λz(χ ′ ξ)(β)z, 1) . (π, q) ∈ ⊥ ⊥ ⊥, i.e. : (η ⋆ λz(χ ′ ξ)(β)z . π, r∧(1∧q)) ∈ ⊥ ⊥ ⊥, thus ((γ)(η)λz(χ ′ ξ)(β)z ⋆ π, 1∧(r∧(q∧r ′ ))) ∈ ⊥ ⊥ ⊥ (proposition 23) and therefore (θ ⋆ η . ξ . π, 1∧(r∧(q∧r ′ ))) ∈ ⊥ ⊥ ⊥.

v) Let (ξ, p ′ ) | -J (p) and (η, r) | q ⊑ p ; we must show that :

(θ, 1) ⋆ (ξ, p ′ ) . (η, r) . (π, q) ∈ ⊥ ⊥ ⊥ for all π ∈ Π, that is (θ ⋆ ξ . η . π, 1∧(p ′ ∧(r∧q))) ∈ ⊥ ⊥ ⊥.

From proposition 32(i), we have

χ ′ ξ || -¬C[p ′ ∧p], thus λz ′ (χ ′ ξ)(β)z ′ || -¬C[p∧p ′ ] : indeed, if τ ∈ C[p∧p ′ ] and ρ ∈ Π, we have λz ′ (χ ′ ξ)(β)z ′ ⋆τ . ρ ≻ (χ ′ ξ)(β)τ ⋆ρ ∈ ⊥ ⊥ since βτ ∈ C[p ′ ∧p].
Then, from proposition 32(iii), we have (λz

′ (χ ′ ξ)(β)z ′ , 1) | -¬C[p∧p ′ ]. But, by hypothesis on (η, r), we have (η, r) | -(¬C[p∧p ′ ] → ¬C[q∧p ′ ]). It follows that : (η, r)(λz ′ (χ ′ ξ)(β)z ′ , 1) | -¬C[q∧p ′ ], i.e. ((α 0 η)λz ′ (χ ′ ξ)(β)z ′ , r∧1) | -¬C[q∧p ′ ]. From proposition 32(ii), we have (χ ′ )(α 0 η)λz ′ (χ ′ ξ)(β)z ′ || -C[(r∧1)∧(1∧1)], C[q∧p ′ ] → ⊥. Let τ ∈ C[1∧(p ′ ∧(r∧q))], therefore ατ ∈ C[(r∧1)∧(1∧1)] and α ′ τ ∈ C[q∧p ′ ]. Thus, we have : (((χ ′ )(α 0 η)λz ′ (χ ′ ξ)(β)z ′ )(α)τ )(γ)τ ⋆ π ∈ ⊥ ⊥, therefore : (χ)λz(((χ ′ )(α 0 η)λz ′ (χ ′ ξ)(β)z ′ )(α)z)(α ′ )z ⋆ π τ ∈ ⊥ ⊥. In other words : ((χ)λz(((χ ′ )(α 0 η)λz ′ (χ ′ ξ)(β)z ′ )(α)z)(α ′ )z ⋆ π, 1∧(p ′ ∧(r∧q))) ∈ ⊥ ⊥ ⊥ or else, from proposition 27(ii) : (θ ⋆ ξ . η . π, 1∧(p ′ ∧(r∧q))) ∈ ⊥ ⊥ ⊥.
q.e.d.

Theorem 34 (Density).

For each function φ : P → P , we have : (θ, 1) | -∀x(¬C[x∧φ(x)] → J (x)), ∀x J (x∧φ(x)) → ⊥ where θ = (β)λxλy(x)(ϑ)y, ϑ = (χ)λdλxλy(χ ′ x)(α)y ; with α :: q∧r ⇒ q∧(q∧r) ; β :: 1∧(p∧(q∧r)) ⇒ p∧(1∧q).

Let (ξ, p) |

-∀x(¬C[x∧φ(x)] → J (x)), (η, q) | -∀x J (x∧φ(x)) and (π, r) ∈ Π.

we must show that (θ ⋆ ξ . η . π, 1∧(p∧(q∧r))) ∈ ⊥ ⊥ ⊥ ; thus, let τ 0 ∈ C[1∧(p∧(q∧r))]. We must show θ ⋆ ξ . η . π τ 0 ∈ ⊥ ⊥.

We first show that (ϑη, 1) | -¬C[q∧φ(q)].

Thus, let (̟, r ′ ) ∈ Π and τ ∈ C[q∧φ(q)] ; we must show (ϑη, 1) ⋆ (τ, 1) . (̟, r ′ ) ∈ ⊥ ⊥ ⊥ i.e. (ϑη ⋆ τ . ̟, 1∧(1∧r ′ )) ∈ ⊥ ⊥ ⊥ or else ϑη ⋆ τ . ̟ τ ′ ∈ ⊥ ⊥ for each τ ′ ∈ C[1∧(1∧r ′ )]). Now, ϑη ⋆ τ . ̟ τ ′ ≻ η ⋆ ̟ ατ and ατ ∈ C[q∧(q∧φ(q))]. Thus, it suffices to show :

(η ⋆ ̟, q∧(q∧φ(q))) ∈ ⊥ ⊥ ⊥ or else (η, q) ⋆ (̟, q∧φ(q)) ∈ ⊥ ⊥ ⊥. But this follows from the hypothesis on (η, q), which implies (η, q) | -J (q∧φ(q)). By hypothesis on ξ, we have (ξ, p) | -¬C[q∧φ(q)] → J (q). It follows that :

(ξ, p) ⋆ (ϑη, 1) . (π, q) ∈ ⊥ ⊥ ⊥, that is (ξ ⋆ ϑη . π, p∧(1∧q)) ∈ ⊥ ⊥ ⊥. But we have τ 0 ∈ C[1∧(p∧(q∧r))]), thus βτ 0 ∈ C[p∧(1∧q)]. It follows that ξ⋆ϑη . π βτ 0 ∈ ⊥ ⊥.
This gives the desired result, since θ ⋆ ξ . η . π τ 0 ≻ ξ ⋆ ϑη . π βτ 0 .

q.e.d.

Countable downward chain condition

In this section, we consider a standard realizability algebra A and a A-model M. We suppose that the set P (domain of variation of individual variables) has a power ≥ 2 ℵ 0 . We choose a surjection ε : P → P(Π) N and we define a binary predicate in the model M, which we denote also by ε, by putting :

n ε p = ε(p)(n) if n ∈ N ; n ε p = ∅ if n /
∈ N (we use, for the predicate ε, the notation n ε p instead of ε(n, p)). Therefore, the predicate ε enables us to associate, with each individual, a set of integers which are its elements. Proposition 35 shows that the following axiom is realized : For every set, there exists an individual which has the same integer elements. This axiom will be called axiom of representation of predicates on N and denoted by RPN.

Proposition 35 (RPN). λx(x)0 0 || -∀X∃x∀n ent (Xn ↔ n ε x). This formula is ∀X(∀x[∀n(ent(n), Xn → n ε x), ∀n(ent(n), n ε x → Xn) → ⊥] → ⊥). Thus, we consider a unary parameter X : P → P(Π) and a term ξ ∈ Λ such that :

ξ || -∀x[∀n(ent(n), X n → n ε x), ∀n(ent(n), n ε x → X n) → ⊥].
We must show that λx(x)0 0 ⋆ ξ . π ∈ ⊥ ⊥, or else ξ ⋆ 0 . 0 . π ∈ ⊥ ⊥ for every stack π ∈ Π.

By definition of ε, there exists p 0 ∈ P such that X n = n ε p 0 for every integer n. But, we have :

ξ || -∀n(ent(n), X n → n ε p 0 ), ∀n(ent(n), n ε p 0 → X n) → ⊥. Thus, it suffices to show that 0 || -∀n(ent(n), X n → n ε p 0 ) and 0 || -∀n(ent(n), n ε p 0 → X n).
Recall that the predicate ent(x) is defined as follows :

| ent(n)| = {n} if n ∈ N and | ent(n)| = ∅ if n / ∈ N. Therefore, we have to show : 0 ⋆ n . η . ρ ∈ ⊥ ⊥ for all n ∈ N, η || -X (n) and ρ ∈ n ε p 0 ; 0 ⋆ n . η ′ . ρ ′ ∈ ⊥ ⊥ for all n ∈ N, η ′ || -n ε p 0 and ρ ′ ∈ X (n).
But this follows from η⋆ρ ∈ ⊥ ⊥ and η ′ ⋆ρ ′ ∈ ⊥ ⊥, which is trivially true, since X n = n ε p 0 .

q.e.d. We suppose now that {C, ∧, 1} is a forcing structure in M. Then we define also the symbol ε in the B-model N by putting : |n ε p | = n ε p ×{1} for n, p ∈ P . In other words

|n ε p | = {(π, 1); π ∈ ε (p)(n)} if n ∈ N ; |n ε p | = ∅ if n / ∈ N. Proposition 36. The predicate ε + (q, n, p) is q = 1 → n ε p. The formula q [] -n ε p is C[q∧1] → n ε p.
Immediate, by definition of |n ε p |. q.e.d.

Proposition 37. i) ξ || -(C[p] → n ε q) ⇒ (δξ, p) |
n ε q where δ = λx(χ)λy(x)(α)y and α ::

p∧1 ⇒ p. ii) (ξ, p) | -n ε q ⇒ δ ′ ξ || -(C[p] → n ε q) where δ ′ = λxλy(χ ′ x)(α ′ )y and α ′ :: p ⇒ p∧1. We have (ξ, p) | -n ε p ⇔ (ξ, p) ⋆ (π, 1) ∈ ⊥ ⊥ ⊥ for all π ∈ n ε p , or else : (ξ, p) | -n ε p ⇔ ξ π τ ∈ ⊥ ⊥ for each τ ∈ C[p∧1] and π ∈ n ε p . i) Suppose that ξ || -(C[p] → n ε q), τ ∈ C[p∧1] and π ∈ n ε p . Then,we have : δξ ⋆ π τ ≻ ξ ⋆ ατ . π ∈ ⊥ ⊥, since ατ ∈ C[p].
ii) Suppose that (ξ, p) ||n ε q, τ ∈ C[p] and π ∈ n ε p . Then,we have :

δ ′ ξ ⋆ τ . π ≻ ξ ⋆ π α ′ τ ∈ ⊥ ⊥, since α ′ τ ∈ C[p∧1].
q.e.d. The notion of first order formula has been defined previously (see theorem 31). We extend this definition with the following clause :

• t ε u is first order, for all terms t, u. Proposition 37 shows that theorem 31 remains true for this extended notion. We say that the forcing structure {C, ∧, 1} satisfies the countable downward chain condition (in abridged form c.d.c.) if there exists a proof-like term cdc such that : cdc || -∀X[∀n ent ∃p X(n, p), ∀n ent ∀p∀q(X(n, p), X(n, q) → p = q), ∀n ent ∀p∀q(X(n, p), X(sn, q) → q ⊑ p) → ∃p ′ {∀n ent ∀p(X(n, p) → p ′ ⊑ p), (∀n ent ∀p(X(n, p)

→ C[p]) → C[p ′ ])}].
The intuitive meaning of this formula is : If X(n, p) is a decreasing sequence of conditions, then there exists a condition p ′ which is less than all of them ; moreover, if all these conditions are non trivial, then p ′ is non trivial.

We intend, in this section to prove the :

Theorem 38 (Conservation of reals).

If the c.d.c. is verified, then there exists a proof-like term crl such that : (crl, 1) | -∀X∃x∀n ent (Xn ↔ n ε x).

Thus, we have :

(

2) λdλxλy((x)(α ′ )y)(β ′ )y || -(p ′ [] -∀n ent (n ε q 0 → X n))
with α ′ :: (p∧r)∧q ⇒ r∧1 and β ′ :: (p∧r)∧q ⇒ p∧q.

• The formula p ′ [] -∀n ent (X n → n ε q 0 ) is written as ∀n ent ∀r(r [] -X n → p ′ ∧r []n ε q 0 ), or else : ∀n ent ∀r(r [] -X n, C[(p ′ ∧r)∧1] → n ε q 0 ), that is, by definition of q 0 :

∀n ent ∀r(r [] -X n, C[(p ′ ∧r)∧1] → p ′ [] -X n). But, we have : ζ || -∀n ent (p ′ [] -±X n), in other words ζ || -∀n ent ∀r(r [] -X n, C[p ′ ∧r] → p ′ [] -X n). Therefore : (3) λnλxλy(ζnx)(α ′′ )y || -p ′ [] -∀n ent (X n → n ε q 0 ) with α ′′ :: (p∧r)∧1 ⇒ p∧r. It follows from (1,2,3) that : ((λyλz((η)λx(ξyz)(β)x)(α)τ ) λdλxλy((x)(α ′ )y)(β ′ )y) λnλxλy(ζnx)(α ′′ )y || -⊥.
Therefore, we can put crl2 = λx 0 λy 0 λz 0 λu((λyλz((y 0 )λx(x 0 yz)(β)x)(α)u)λdλxλy((x)(α ′ )y)(β ′ )y)λnλxλy(z 0 nx)(α ′′ )y.

q.e.d. The remaining of this section is devoted to the proof of theorem 39.

Definition of a sequence by dependent choices

In this section, we are given a fixed element p 0 ∈ P and a finite sequence of formulas with parameters F (n, p, p ′ ). We are also given a proof-like term dse such that : dse || -∀n∀p∃p ′ F (n, p, p ′ ).

From theorem 16(i) (axiom of choice for individuals), there exists a function f : P 3 → P such that : ς || -∀n∀p(∀k ent ( F (n, p, f (n, p, k)) → ⊥) → ∀p ′ ( F (n, p, p ′ ) → ⊥)).

It follows that λx(dse)(ς)x || -∀n∀p(∀k ent ( F (n, p, f (n, p, k)) → ⊥) → ⊥). We define a function denoted by (m¡n), from P 2 into P , by putting, for m, n ∈ P : (m¡n) = 1 if m, n ∈ N and m < n ; (m¡n) = 0 otherwise. Obviously, the relation (m¡n) = 1 is well founded on P . Thus, from theorem 11(ii), we have :

Y || -∀k(∀l(ent(l), F (n, p, f (n, p, l)) → (l¡k) = 1),ent(k), F (n, p, f (n, p, k)) → ⊥) → ∀k(ent(k), F (n, p, f (n, p, k)) → ⊥). Therefore, if we set Y ′ = λx(Y)λyλz(x)zy, we have : Y ′ || -∀k ent {∀l ent ( F [n, p, f (n, p, l)] → (l¡k) = 1), F [n, p, f (n, p, k)] → ⊥} → ∀k ent ( F [n, p, f (n, p, k)] → ⊥). Thus, we have : λx(dse)(ς)(Y ′ )x || -∀k ent {∀l ent ( F [n, p, f (n, p, l)] → (l¡k) = 1), F [n, p, f (n, p, k)] → ⊥} → ⊥.
We define the formula G(n, p, k) ≡ ∀l ent ( F (n, p, f (n, p, l)) → (l¡k) = 1) and the finite sequence of formulas H(n, p, k) ≡ {G(n, p, k), F (n, p, f (n, p, k))}. Then, we have shown :

Lemma 40. dse0 || -∀n∀p∃k ent { H(n, p, k)}, with dse0 = λx(dse)(ς)(Y ′ )x.
Lemma 47. There exist two proof-like terms cdc3 and for such that : i) cdc3 || -∀n ent ∀p∀q(Φ(n, p), Φ(sn, q) → q ⊑ p). ii) for || -∀n ent ∀q(Φ(sn, q) → q [] -±X n).

By lemma 42(iii), we have : rec || -∀k ent ( H(n, p, k), Φ(n, p) → Φ(sn, f (n, p, k))). Using cdc2 (lemma 44), we get : || -∀k ent ( H(n, p, k), Φ(n, p), Φ(sn, q) → q = f (n, p, k)). Now, H(n, p, k) is a sequence of four formulas, the last two of which are : f (n, p, k) ⊑ p and f (n, p, k) [] -±X n.

i) It follows first that || -∀k ent ( H(n, p, k), Φ(n, p), Φ(sn, q) → q ⊑ p).

Hence the result, since we have dse0 || -∃k ent { H(n, p, k)} (lemma 40).

ii) It follows also that || -∀k ent ( H(n, p, k), Φ(n, p), Φ(sn, q) → q [] -±X n). Thus, we obtain || -∀n ent ∀q(Φ(sn, q) → q [] -±X n) since we have cdc1 || -∀n ent ∃p Φ(n, p) (lemma 43) and dse0 || -∀n∀p∃k ent { H(n, p, k)} (lemma 40).

q.e.d. We can now apply the c.d.c. to the predicate Φ(x, y), which gives a proof-like term cdc0 such that cdc0 || -∃p ′ { Ω(n, p, p ′ )} with : Ω(n, p, p ′ ) ≡ {∀n ent ∀p(Φ(n, p) → p ′ ⊑ p), ∀n ent ∀p(Φ(n, p), ¬C[p] → ⊥), ¬C[p ′ ] → ⊥}. Therefore, in order to complete the proof of theorem 39, it is sufficient to find proof-like terms dec0,dec1,dec2 such that : dec0 || -∀p ′ ( Ω(n, p, p ′ ), ¬C[p 0 ], C[p ′ ] → ⊥) ; dec1 || -∀p ′ ( Ω(n, p, p ′ ) → p ′ ⊑ p 0 ) ; dec2 || -∀p ′ ( Ω(n, p, p ′ ) → ∀n ent (p ′ [] -±X n)). Thus, let ω 0 , ω 1 ∈ Λ be such that : ω 0 || -∀n ent ∀p(Φ(n, p) → p ′ ⊑ p) and ω 1 || -∀n ent ∀p(Φ(n, p), ¬C[p] → ⊥), ¬C[p ′ ] → ⊥ Applying lemma 42(i) with n = 0, p = p 0 , we obtain (ω 0 )λxλy y ||p ′ ⊑ p 0 . Therefore, we can take dec1 = λaλb(a)λxλy y. q.e.d. By means of lemmas 47(ii) and 49 and also ω 0 || -∀n ent ∀p(Φ(n, p) → p ′ ⊑ p), we obtain : λnλx((lef1)(for)nx)(ω 0 )nx || -∀n ent ∀q(Φ(sn, q) → p ′ [] -±X n). But, we have cdc1 || -∀n ent ∃p Φ(n, p) (lemma 43) ; it follows that : λn(cc)λk((cdc1)(s)n)λx(k)((lef1)(for)nx)(ω 0 )nx || -∀n ent (p X [] -±X n). Thus, we can put dec2 = λaλbλn(cc)λk((cdc1)(s)n)λx(k)((lef1)(for)nx)(a)nx. This completes the proof of theorem 39.

q.e.d.

The ultrafilter axiom on N

Let us consider a standard realizability algebra A and a A-model M in which the individual set (which is also the set of conditions) is P = P(Π) N . The binary relation ε is defined by n ε p = p(n) if n ∈ N ; otherwise n ε p = ∅.

1 is defined by 1(n) = ∅ for every n ∈ N ; ∧ is defined by n ε (p∧q) = n ε p ∧ n ε q for every n ∈ N.

The axiom of representation of predicates on N (RPN)

We define the following recursive function of arity k, denoted by (n 1 , . . . , n k ) (coding of k-uples) : (n 1 , n 2 ) = n 1 + (n 1 + n 2 )(n 1 + n 2 + 1)/2 ; (n 1 , . . . , n k+1 ) = ((n 1 , . . . , n k ), n k+1 ).

Proposition 50. || -∀X∃x∀y int 1 . . . ∀y int k ((y 1 , . . . , y k ) ε x ↔ X(y 1 , . . . , y k )) where X is a predicate variable of arity k.

Let X : P k → P(Π) be a predicate of arity k. We define a ∈ P by putting : a(n) = X (n 1 , . . . , n k ) for n ∈ N, n = (n 1 , . . . , n k ). Then, we have immediately : I || -∀y ent

• If F is ∀x A, F † is ∀x int A † . • If F is ∀X A, F † is ∀X -A † .
We note that, if F is a formula of first order arithmetic, then F † is simply the restriction F int of F to the predicate int(x). Let F be a closed formula of second order arithmetic and let us consider a proof of F , which uses the axiom of dependent choice DC and the axiom UA of ultrafilter on N, written in the following form, with a constant J of predicate : "J is a maximal non trivial ideal on P(N) ". We can transform it immediately into a proof of F † if we add the axiom RPN of representation of predicates on N : ∀X∃x∀y(y ε x ↔ Xy). Thus, we obtain : x : UA, y : RPN, z : DC † ⊢ t[x, y, z] : F † . Therefore, we have ⊢ u : UA, RPN → G with u = λxλyλz t[x, y, z] and G ≡ DC † → F † . Thus, G is a first order formula. In the previous section, we obtained proof-like terms θ, θ ′ such that (θ, G vξ 0 η 0 all the results obtained in the framework of usual classical realizability. The case when F is an arithmetical (resp. Π 1 1 ) formula is considered in [START_REF] Krivine | Realizability in classical logic[END_REF] (resp. [START_REF] Krivine | Realizability : a machine for Analysis and set theory[END_REF]). T is the proof-like term for integer storage, given in theorem 13(i). π, κ are arbitrary ; therefore, by taking a constant for κ, we obtain a program which computes n from m.

Well ordering on R

The A-model M is the same as in the previous section : the set of individuals is P = P(Π) N . Recall that an element of P is called sometimes an individual, sometimes a condition, depending on the context. We put (m, n) = m + (m + n)(m + n + 1)/2 (bijection of N 2 onto N). We define a binary function γ : P 2 → P by putting : γ(n, p)(i) = p(i, n) if n ∈ N ; γ(n, p) is arbitrary (for instance 0) if n / ∈ N.

  which follows from the hypothesis.• If p ∈ N, we have p = s p 0 ; we define the unary predicate Y by putting :

  But we have : ξ ||ent(n π ) → F [p 1 , . . . , p m , f (p 1 , . . . , p m , n π )] by hypothesis on ξ ; n π ∈ |ent(n π )| by definition of ent ; π ∈ F [p 1 , . . . , p m , f (p 1 , . . . , p m , n π )] by hypothesis on π and by definition of f . ii) The proof is the same ; in fact, (ii) is weaker than (i) since | ent(x)| ⊂ | int(x)|.

  Proposition 27. i) If (ξ, 1) | -F , then (γξ, p) | -F for each p ∈ P , with γ :: p∧q ⇒ 1∧q. ii) Let ξ, η ∈ Λ be such that ξ ⋆ π ≻ η ⋆ π for each π ∈ Π. Then, we have : (ξ ⋆ π, p) / ∈ ⊥ ⊥ ⊥ ⇒ (η ⋆ π, p) / ∈ ⊥ ⊥ ⊥ for every π ∈ Π and p ∈ P ; (η, p) | -F ⇒ (ξ, p) | -F for every closed formula F .

  and therefore : (χξ, p) | -C[q] → ⊥. If (ξ, p) | -¬C[q], we have (ξ, p) ⋆ (τ, 1) . (π, r) ∈ ⊥ ⊥ ⊥, and therefore (ξ ⋆ τ . π, p∧(1∧r)) ∈ ⊥ ⊥ ⊥ for each τ ∈ C[q]. Thus, we have ξ ⋆ τ . π υ ∈ ⊥ ⊥ therefore χ ′ ξ ⋆ υ . τ . π ∈ ⊥ ⊥ for each υ ∈ C[p∧(1∧r)]. It follows that χ ′ ξ || -∀r(C[p∧(1∧r)], C[q] → ⊥).

  Lemma 48. cdc4 || -(C[p 0 ] → ∀n ent ∀p(Φ(n, p), ¬C[p] → ⊥)) where cdc4 = λaλbλc((bλx 0 λx 1 λx 2 λx 3 λxλy(x)(x 1 )y)λx xa)c.Let τ ∈ C[p 0 ], ξ || -Φ(n, p) and η || -¬C[p]. Making X(x, y) ≡ ¬¬C[y] in the definition de Φ, we get : ξ || -∀n ′ ∀p ′ ∀k ent (G[n ′ , p ′ , k], F [n ′ , p ′ , f (n ′ , p ′ , k)], ¬¬C[p ′ ] → ¬¬C[f (n ′ , p ′ , k)]), ¬¬C[p 0 ], ¬C[p] → ⊥. We have λx(x)τ || -¬¬C[p 0 ]. Moreover, since F [n ′ , p ′ , q] ≡ {(¬C[q] → ¬C[p ′ ]), (q ⊑ p ′ ), q [] -±X n}, we easily get : λx 0 λx 1 λx 2 λx 3 λxλy(x)(x 1 )y || -∀n ′ ∀p ′ ∀k ent (G[n ′ , p ′ , k], F [n ′ , p ′ , f (n ′ , p ′ , k)], ¬¬C[p ′ ] → ¬¬C[f (n ′ , p ′ , k)]). It follows that ((ξλx 0 λx 1 λx 2 λx 3 λxλy(x)(x 1 )y)λx(x)τ )η || -⊥, i.e. (cdc4)τ ξη || -⊥.q.e.d. From lemma 48, we immediately deduce λx(ω 1 )(cdc4)x || -C[p 0 ], ¬C[p ′ ] → ⊥. Therefore, we can put dec0 = λaλbλx(b)(cdc4)x. Lemma 49. i) lef0 || -∀p∀q(p [] -X n, q ⊑ p → q [] -X n) with lef0 = λxλyλz(cc)λk((y)λu(k)(x)u)z. ii) lef1 || -∀p∀q(p [] -±X n, q ⊑ p → q [] -±X n) with lef1 = λxλyλzλu((lef0)(cc)λh((y)λv(h)(x)vu)z.i) This is immediate, if we write explicitly the formulas :p [] -X n ≡ ∀r(C[p∧r] → X + (r, n)) ; q ⊑ p ≡ ∀r(¬C[p∧r] → ¬C[q∧r]) ; q [] -X n ≡ ∀r(C[q∧r] → X + (r, n)).We declare x : p [] -X n, y : q ⊑ p, z : C[q∧r], k : ¬X + n. ii) We write down the formulas :p [] -±X n ≡ ∀r(C[p∧r], r [] -X n → p [] -X n) ; q ⊑ p ≡ ∀r(¬C[p∧r] → ¬C[q∧r]) ; q [] -±X n ≡ ∀r(C[q∧r], r [] -X n → q [] -X n).We declare x : p [] -±X n, y : q ⊑ p, z : C[q∧r], u : r [] -X n, v : C[p∧r], h : ¬(p || -X n).

1 .

 1 . . ∀y ent k ((y 1 , . . . , y k ) ε a → X (y 1 , . . . , y k )) and I || -∀y ent 1 . . . ∀y ent k (X (y 1 , . . . , y k ) → (y 1 , . . . , y k ) ε a). It follows that :

  1) | -UA and (θ ′ , 1) | -RPN (theorems 38 and 52). Therefore, theorem 26 (adequacy lemma) gives (u * , 1 u)(θ, 1)(θ ′ , 1) | -G, that is to say : (v, (1 u ∧1)∧1) | -G with v = ((α 0 )(α 0 )u * θ)θ ′ . By theorem 31, we thus have δ ′ G v || -C[(1 u ∧1)∧1] → G, that is : δ ′ G v || -C[(1 u ∧1)∧1], DC † → F .The axiom DC † is consequence of ACI (axiom of choice for individuals). Therefore, by theorem 16, we have a proof-like term η 0 || -DC † . Moreover, we have obviously a proof-like termξ 0 || -C[(1 u ∧1)∧1].Thus, finally, we have δ ′ G vξ 0 η 0 || -F . Then, we can apply to the program ζ = δ ′

  Let us take two very simple examples : If F ≡ ∀X(X1, X0 → X1), we have ζ ⋆ κ . κ ′ . π ≻ κ ⋆ π for all terms κ, κ ′ ∈ Λ and every stack π ∈ Π. If F ≡ ∀m int ∃n int (φ(m, n) = 0), where φ is a function symbol, then for every m ∈ N, there exists n ∈ N such that φ(m, n) = 0 and ζ ⋆ m . T κ . π ≻ κ ⋆ n . π ′ .

  x n : A n ⊢ t : ∀x A for every variable x (individual or predicate) which does not appear in A 1 , . . . , A n . 5.x 1 : A 1 , . . . , x n : A n ⊢ t : ∀x A ⇒ x 1 : A 1 , . . . , x n : A n ⊢ t : A[τ /x]where x is an individual variable and τ is a term. 6. x 1 : A 1 , . . . , x n : A n ⊢ t : ∀X A ⇒ x 1 : A 1 , . . . , x n : A n ⊢ t : A[F/Xy 1 . . . y k ] where X is a predicate variable of arity k and F an arbitrary formula. Xy 1 . . . y k ], the variables y 1 , . . . , y k are bound. A more usual notation is : A[λy 1 . . . λy k F/X]. I prefer this one, to avoid confusion with the λ defined for c-terms.

	Remark.
	In the notation A[F/

  by hypothesis, a function symbol. Of course, we assume that its interpretation f : P k → P takes the same values as f on N k . Finally, we have also a condition 1 ∈ P and a binary function ∧ from P 2 into P . A closed term (resp. a closed formula) with parameters in the model M is, by definition, a term (resp. a formula) in which all free occurrences of each variable have been replaced with a parameter, i.e. an object of the same type in the model M : a condition for an individual variable, an application from P k into P(Π) for a k-ary predicate variable.

	Each closed term t, with parameters in M has a value t ∈ P .
	An interpretation I is an application which associates an individual (condition) with each
	individual variable and a parameter of arity k with each second order k-ary variable.
	I[x ← p] (resp. I[X ← X ]) is, by definition, the interpretation obtained by changing,
	in I, the value of the variable x (resp. X) and giving to it the value p ∈ P (resp.
	X ∈ P(Π) P k ).
	For each formula F (resp. term t), we denote by F I (resp. t I ) the closed formula (resp.
	term) with parameters obtained by replacing each free variable with the value given by I.

  ary predicate variable. Notation. We shall write ξ || -F for ξ ∈ |F |. If x 1 : A 1 , . . . , x k : A k ⊢ t : A and if ξ 1 || -A I 1 , . . . , ξ k || -A I k , where I is an interpretation, then t[ξ 1 /x 1 , . . . , ξ k /x k ] || -A I . In particular, if A is closed and if ⊢ t : A, then t || -A.

	Theorem 3 (Adequacy lemma).

  . 1. A seemingly simpler formulation of this axiom of choice is the existence of a function φ : P m → P such that ∀x 1 . . . ∀x m (F [φ(x 1 , . . . , x m )/y] → ∀y F ). It clearly follows from theorem 16 : simply define φ(x 1 , . . . , x m ) as f (x 1 , . . . , x m , x) for the first integer x such that ¬F [f (x 1 , . . . , x m , x)/y] if there is such an integer ; otherwise, φ(x 1 , . . . , x m ) is arbitrary. But this function φ is not a function symbol, i.e. it cannot be defined in the ground model. For this reason, we prefer to use this axiom in the form stated in theorem 16, which is, after all, much simpler. 2 .The axiom of dependent choice DC is a trivial consequence of ACI ; therefore theorem 16 shows that DC is realized by a proof-like term. Theorem 16 is also crucial to prove theorem 38 (see lemma 40).

(ξ)η ⋆ π ≻ ξ ⋆ η . π. I ⋆ ξ . π ≻ ξ ⋆ π. K ⋆ ξ . η . π ≻ ξ ⋆ π. E ⋆ ξ . η . π ≻ (ξ)η ⋆ π. W ⋆ ξ . η . π ≻ ξ ⋆ η . η . π.

This means that the axiom RPN, which is realized in the A-model M (see proposition 35) is also realized in the generic B-model N .

Remark. The aim of this section is to write down a formula Φ(x, y) which represents the graph of a function φ : N → P such that the formulas φ(0) = p 0 and ∀n ent F (n, φ(n), φ(n + 1)) are realized by proof-like terms. We shall only apply the results of this section to a particular sequence F of length 3.

Applying again the recurrence hypothesis, we find : (δ ′ B )(α 0 ξ)(δ A )λd η || -C[p∧1] → B. Since we have ατ ∈ C[p∧1], we get : (δ ′ B )(α 0 ξ)(δ A )λd η ⋆ ατ . π ∈ ⊥ ⊥ and finally δ ′ A→B ξ ⋆ τ . η . π ∈ ⊥ ⊥.

• If F ≡ R( q) → B, where R is a k-ary predicate symbol and p ∈ P k , we put : δ R→B = λxλy(α)(δ B )λz(x)zy with α :: p∧(1∧r) ⇒ p∧r. δ ′ R→B = λxλyλz((δ ′ B )(α 0 )xz)(α ′ )y with α ′ :: p ⇒ p∧1. Suppose that ξ || -C[p], R[ q] → B and let η ∈ |R[ q]|, (π, r) ∈ |B |. We must show :

(δ R→B ξ, p) ⋆ (η, 1) . (π, r) ∈ ⊥ ⊥ ⊥, that is (δ R→B ξ ⋆ η . π, p∧(1∧r)) ∈ ⊥ ⊥ ⊥. Thus, let τ ∈ C[p∧(1∧r)] ; we must show δ R→B ξ ⋆ η . π τ ∈ ⊥ ⊥. But, we have : (δ B )λz(ξ)zη ⋆ π ατ ∈ ⊥ ⊥, thus (α)(δ B )λz(ξ)zη ⋆ π τ ∈ ⊥ ⊥, therefore δ R→B ξ ⋆ η . π τ ∈ ⊥ ⊥.

The generic ideal

We define a unary predicate J : P → P(Π) in the model N (second order parameter of arity 1), by putting J (p) = Π×{p} ; we call it the generic ideal. Thus, the binary predicate J + : P 2 → P(Π) which corresponds to it in the model M, is such that J + (p, q) = ∅ (resp. Π) if p = q (resp. p = q). In other words : J + (p, q) is the predicate p = q. The formula p || -J (q) is ∀r(C[p∧r] → J + (r, q)). Therefore, we have : p || -J (q) = ¬C [p∧q] ; in other words : p || -J (q) is exactly ¬C[p∧q]. Notations.

• We denote by p ⊑ q the formula ∀r(¬C[q∧r] → ¬C [p∧r]) and by p ∼ q the formula Notation. The formula ∀q(C[p∧q], q [] -Xn → p [] -Xn) reads as " p decides Xn ", and is denoted by p [] -±Xn. It can also be written as ∀q∀r(C[p∧q], q [] -Xn, C[p∧r] → X + (r, n)). If X : P → P(Π×P ) is a unary predicate in the B-model N , and X + : P 2 → P(Π) is the corresponding binary predicate in the standard A-model M, the formula ∀q(C[p∧q], q [] -X n → p [] -X n) is thus also denoted by p [] -±X n.

Theorem 39. If the c.d.c. is verified, there exists a proof-like term dec such that : dec || -∀X∀p 0 ∃p ′ {(C[p 0 ] → C[p ′ ]), p ′ ⊑ p 0 , ∀n ent (p ′ [] -±Xn)}.

Remark. This formula means that, for any predicate X, the set of conditions which decide Xn for all integers n is dense.

We first show how theorem 38 can be deduced from this theorem 39.

From theorem 30, it is sufficient to find a proof-like term crl0 such that :

From theorem 39, it is sufficient to find a proof-like term crl1 such that :

We must have (crl2)ξηζτ || -⊥. We choose q 0 ∈ P such that we have n ε q 0 = p ′ [] -X n for all n ∈ N, which is possible, by definition of ε. We trivially have ξ || -

Replacing r and r ′ with p ′ , we obtain :

where α, β are C-expressions such that α : p ⇒ p∧p ; β :: p∧q ⇒ (p∧q)∧q. Thus, we have :

Remark. The meaning of H(n, p, k) is "k is the least integer such that F (n, p, f (n, p, k))".

Lemma 41. Let cp be a proof-like term such that, for every m, n ∈ N, we have :

where y, y ′ are two sequences of distinct variables of the same length as the sequence F .

q.e.d. We now define the binary predicate : Φ(x, y) ≡ ∀X(∀n∀p∀k ent ( H(n, p, k), X(n, p) → X(sn, f (n, p, k))), X(0, p 0 ) → X(x, y)) and we show that Φ(x, y) is a sequence of conditions (functional relation on N) and also some other properties of Φ.

Remark. Intuitively, the predicate Φ is the graph of the function φ of domain N, recursively defined by the conditions :

where f ′ (n, p) is f (n, p, k) for the least k such that F (n, p, f (n, p, k)). Unfortunately, we cannot introduce f ′ as a function symbol because, unlike f , it is not defined in the ground model.

Lemma 42. i) λxλy y || -Φ(0, p 0 ). ii) λx(x)II || -∀y(Φ(0, y) → y = p 0 ). iii) rec || -∀x∀y∀k ent ( H(x, y, k), Φ(x, y) → Φ(sx, f (x, y, k))) where rec = λkλxλ yλx ′ λzλu(zkx y)(x ′ )zu and y is a sequence of distinct variables of the same length as F . i) Trivial. ii) We define the binary predicate X : P 2 → P(Π) by putting : X (0, q) = q = p 0 and X (p, q) = ∅ for p = 0. We replace X with X in the definition of Φ(0, y). Since we have sn = 0 for all n ∈ P , we obtain Φ(0, y) ⊃ ⊤, p 0 = p 0 → y = p 0 ; hence the result.

iii

q.e.d.

Lemma 43. cdc1 || -∀n ent ∃p Φ(n, p) where : cdc1 = λn((n)λxλy(x)λz(cd1)zy)λx(x)λxλy y with cd1 = λxλy(dse0)λlλ z(y)(rec)l zx ; z is a sequence of distinct variables of the same length as H.

Proof by recurrence on n ; we have λxλy y || -Φ(0, p 0 ), therefore λx(x)λxλy y || -∃y Φ(0, y). We now show that cd1 || -Φ(x, y) → ∃yΦ(sx, y). Thus, we consider ξ || -Φ(x, y), η || -∀y(Φ(sx, y) → ⊥). We have rec || -∀l ent ( H(x, y, l), Φ(x, y) → Φ(sx, f (x, y, l))) (lemma 42iii), η || -(Φ(sx, f (x, y, l)) → ⊥), and therefore : λlλ z(η)(rec)l zξ || -∀l ent ( H(x, y, l) → ⊥), where z has the same length as H. Now, we have dse0 || -∃k ent { H(x, y, k)} (lemma 40) ; therefore : (dse0)λlλ z(η)(rec)l zξ || -⊥, that is (cd1)ξη || -⊥. Thus, we have shown that cd1 || -∀y(Φ(x, y) → ∃yΦ(sx, y)), and it follows that : λxλy(x)λz(cd1)zy || -∃yΦ(x, y) → ∃yΦ(sx, y).

q.e.d.

Lemma 44. There exists a proof-like term cdc2 such that : cdc2 || -∀n ent ∀p∀q(Φ(n, p), Φ(n, q) → p = q).

We give a detailed proof, by recurrence on n. It enables us to write explicitly the proof-like term cdc2.

For n = 0, the lemma 42(ii) gives the result : Φ(0, p), Φ(0, q) → p = q.

Let us fix m and suppose that ∀p∀q(Φ(m, p), Φ(m, q) → p = q). We define the binary predicate : Ψ(n, q) ≡ ∀p∀k ent (n = sm, H(m, p, k), Φ(m, p) → q = f (m, p, k)).

We show that || -∀p∀k ent ( H(n, p, k), Φ(n, p) → Ψ(sn, f (n, p, k))), that is to say : || -∀p∀q∀k ent ∀l ent { H(n, p, k), Φ(n, p), sn = sm, H(m, q, l), Φ(m, q) → f (n, p, k) = f (m, q, l)}. But we have sn = sm = n = m , Φ(m, p), Φ(m, q) → p = q by hypothesis of recurrence ; H(m, p, k), H(m, p, l) → k = l (lemma 41(ii)), and it follows that f (n, p, k) = f (m, q, l). If we put Ψ ′ (x, y) ≡ Φ(x, y) ∧ Ψ(x, y), we have :

|| -∀p∀k ent ( H(n, p, k), Ψ ′ (n, p) → Ψ ′ (sn, f (n, p, k))) ; we have also || -Ψ ′ (0, p 0 ). This shows that || -(Φ(x, y) → Ψ ′ (x, y)) by making X ≡ Ψ ′ in the definition of Φ. Thus, we have || -Φ(sm, q) → ∀p∀k ent ( H(m, p, k), Φ(m, p) → q = f (m, p, k)).

It follows that :

) and therefore || -Φ(sm, q), Φ(sm, q ′ ) → ∀p∀k ent ( H(m, p, k), Φ(m, p) → q = q ′ ). Thus, we obtain || -Φ(sm, q), Φ(sm, q ′ ) → q = q ′ , since we have cdc1 || -∃p Φ(m, p) by lemma 43 and dse0 || -∀p∃k ent { H(m, p, k)} by lemma 40.

q.e.d.

End of the proof of theorem 39

In order to show theorem 39, we fix p 0 ∈ P and a binary predicate X : P 2 → P(Π).

We have to find a proof-like term dec such that :

We apply the above results, taking for F (n, p, p ′ ) the sequence of three formulas :

Lemma 45 below gives a proof-like term dse such that dse || -∀n∀p∃p ′ { F (n, p, p ′ )}.

Lemma 45. dse || -∀p∃p ′ { F (n, p, p ′ )} where dse = λa(λh(aII)λxλy h)λz(cc)λk((aλx xz)β ′ )λxλy(k)(y)(α)x with β ′ = λxλy(x)(β)y, α :: (p∧q)∧r ⇒ r∧q and β :: (p∧q)∧r ⇒ p∧r.

The formula we consider is written as

In fact, we show :

q.e.d.

This formula is written ∀p∀q∀r

Thus, we obtain λxλy(x)(β)y ⋆ ξ . τ . π ∈ ⊥ ⊥ for every π ∈ Π.

q.e.d. We propose now to apply the countable downward chain condition to the binary predicate Φ(x, y). Lemmas 43 and 44 show that the first two hypothesis of the c.d.c. are realized by cdc1 and cdc2. The third one is given by lemma 47 below.

λx(x)I || -∀X∃x∀y

Then, it suffices to apply theorem 13.

q.e.d.

The comprehension scheme for N (CSN)

Let F [y, x 1 , . . . , x k ] be a formula the free variables of which are taken among y, x 1 , . . . , x k . We define a k-ary function g F : P k → P , in other words g F :

Indeed, we have trivially :

Then, it suffices to apply theorem 13. q.e.d.

Remark.

The binary function symbol ∧ is obtained by applying CSN to the formula y ε x 1 ∧ y ε x 2 .

The generic model

We denote by C[x] the formula ∀m int ∃n int (m+ n) ε x, which says that the set x of integers is infinite.

Therefore, in order to complete the definition of the algebra B (and of the B-model N ), it remains to find proof-like terms α 0 , α 1 , α 2 , β 0 , β 1 , β 2 such that :

). Now, we easily have, in natural deduction :

Therefore, by theorem 3 (adequacy lemma), we can put α i = θα * i and

The countable downward chain condition

In this section, we show the :

Theorem 52.

The forcing structure {C, ∧, 1} satisfies the countable downward chain condition in M.

Remark. The proof of this theorem is a formalization of the following simple result :

The set of infinite subsets of N with the preorder "p ⊑ q ⇔ p \ q is finite", satisfies the countable downward chain condition. The proof is as follows : let p n be a decreasing sequence for this preorder ; put h n = i≤n p i , k n = the first element of h n which is ≥ n, and consider {k n ; n ∈ N} which is an infinite subset of N.

We have to find a proof-like term cdc such that : cdc || -∀X∃x{∀n ent ∃p X(n, p), ∀n ent ∀p∀q(X(n, p), X(n, q) → p = q), ∀n ent ∀p∀q(X(n, p), X(sn, q

By theorem 13, this amounts to find a proof-like term cdc' such that : cdc' || -∀X∃x{∀n int ∃p X(n, p), ∀n int ∀p∀q(X(n, p), X(n, q) → p = q), ∀n int ∀p∀q(X(n, p), X(sn, q

)}. By theorem 3 (adequacy lemma), given a formula F , we can use the following method to show || -F : First, show || -A 1 , . . . , || -A k , then show A 1 , . . . , A k ⊢ F by means of the rules of classical second order natural deduction (which contains the comprehension scheme), and of the following axioms which are realized by proof-like terms in the A-model M : • t = u for all closed terms t, u which take distinct values in M. • ∀x int 1 . . . ∀x int k (t(x 1 , . . . , x k ) = u(x 1 , . . . , x k )) for all the equations between terms which are true in N.

• The foundation scheme (SCF, see theorem 11ii) which consists of the formulas :

→ ∀x int (X 1 x, . . . , X k x → ⊥)} where f : P 2 → P is such that the relation f (y, x) = 1 is well founded on N.

• The axiom of choice scheme for individuals (ACI, see theorem 16) which consists of the formulas ∀ x(∀y int F ( x, f F ( x, y)) → ∀y F ( x, y)) ; x = (x 1 , . . . , x k ) is a finite sequence of variables, ∀ x∀y int F is an arbitrary closed formula, and f F is a function symbol of arity k + 1.

• The axiom of representation of predicates on N (RPN, see proposition 50) which consists of the formulas ∀X∃x∀ y int ((y 1 , . . . , y k ) ε x ↔ X y) ; y = (y 1 , . . . , y k ) is a sequence of k variables and X is a predicate variable of arity k.

• The comprehension scheme for integers (CSN, see proposition 51), which consists of the formulas ∀ x∀y int (y ε g F ( x) ↔ F [y, x]) ; x = (x 1 , . . . , x k ) is a sequence of k variables, ∀ x∀y int F is an arbitrary closed formula, and g F is a function symbol of arity k.

Lemma 53. ⊢ ∀p∀q(p ⊑ q ↔ ∃m int ∀n int (n + m ε p → n + m ε q)).

We apply the CSN to the formula F [y, x] ≡ y ε / x ; thus, we obtain :

⊢ ∀x∀y int (y ε ¬x ↔ y ε / x) using the notation ¬x for g F (x). We have p ⊑ q ≡ ∀r(C[p∧r] → C[q∧r]) and therefore p ⊑ q ⊢ C[p∧¬q] → C[q∧¬q]. But, we have C[q∧¬q] ⊢ ∀m int ∃n int (m + n ε q ∧ m + n ε / q) ⊢ ⊥, and thus :

Conversely, from the hypothesis :

q.e.d. Applying RPN and the comprehension scheme, we obtain || -∀X∃h D(h, X) with :

Remark. The intuitive meaning of D(h, X) is : h is the individual associated with the decreasing sequence of conditions X ′ , the n-th term of which is the intersection of the n first terms of the sequence X.

We apply CSN to the formula F (k, n, h) ≡ (k, n) ε h. Thus, we obtain :

We shall use the notation h n for g F (n, h). Therefore, we have :

Remark. The intuitive meaning of Φ(k, h, n) is : " k is the first element of h n which is ≥ n ".

We apply CSN to the formula F (k, h) ≡ ∃n int Φ(k, h, n). Thus, we obtain :

We shall use the notation inf(h) for g F (h). Therefore, we have :

. The hypothesis of the c.d.c. are :

This formula is written ∀m int ∀n int ∀k int (k ε h n+m → k ε h n ). Now, we have :

q.e.d.

We have D(h, X), int(k), int(n) ⊢ ∀p∀i int (i ≤ sn, X(i, p) → k ε p) → k ε h sn . But, we have int(n), int(i), i ≤ sn ⊢ i ≤ n ∨ i = sn, and therefore :

q.e.d.

Proof by recurrence on n. We must show :

For n = 0, we have D(h, X) ⊢ ∀k int (∀q(X(0, q) → k ε q) → k ε h 0 ). Thus, it suffices to show : D(h, X), H * [X] ⊢ ∀p∃m int ∀l int ∀q(X(0, p), l + m ε p, X(0, q) → l + m ε q), which follows, in fact, from H 1 [X], that is X(0, p), X(0, q) → p = q. The recurrence hypothesis is ∀p(X(n, p) → p ⊑ h n ) ; H 2 [X] is ∀p∀q(X(n, p), X(sn, q) → q ⊑ p) ; H 0 [X] is ∃p X(n, p). Moreover, we have easily q ⊑ p, p ⊑ r ⊢ q ⊑ r. Thus, it follows that : ∀p(X(sn, p) → p ⊑ h n ), i.e. ∀p∃m int ∀l int (X(sn, p), l + m ε p → l + m ε h n ). Now, we have, by lemma 55 :

Therefore, we have ∀p∃m int ∀l int (X(sn, p), l + m ε p → l + m ε h sn ) that is : ∀p(X(sn, p) → p ⊑ h sn ), which is the desired result. q.e.d.

We have ∀n int ∀p(X(n, p) → C[p]) from H 3 . Moreover, we have easily :

). Thus, applying lemma 56, we obtain :

q.e.d.

By the foundation scheme (SCF), we have :

q.e.d.

We have C[inf(h)] ≡ ∀m int ∃i int (i + m ε inf(h)). Now, by definition of the function symbol inf, we have :

By definition de Φ, we have trivially

q.e.d.

Thus, we have to show :

From k ′ > k, we deduce i ′ + n ′ > k, and thus j ′ < i ′ . Therefore, we have

By definition of Φ, we have trivially

By lemmas 54 and 60, we get :

We have eventually obtained the desired proof-like term cdc', which completes the proof of theorem 52.

q.e.d.

The ultrafilter

In the model N , we have defined the generic ideal J , which is a unary predicate, by putting : J (p) = Π×{p} for every p ∈ P . By theorem 33, we have :

-∀x∀y(J (x), y ⊑ x → J (y)) By theorem 31, we have || -F ⇔ | -F for every closed first order formula F .

Remark. A "first order" formula contains quantifiers on the individuals which, by means of the symbol ε , represent the subsets of N. Therefore, it is a second order formula from the point of view of Arithmetic. But it contains no quantifier on sets of individuals.

By theorems 13 and 28, we can use, in F , the quantifier ∀x int , since the quantifier ∀x ent is first order. Therefore, we have :

since all these formulas are first order. Properties (i) to (viii) show that, in the B-model N , the following formula is realized : J is a maximal non trivial ideal on the Boolean algebra of the subsets of N which are represented by individuals. Now, by theorems 38 and 52, the following formula is realized in N : Every subset of N is represented by an individual. Thus the following formula is realized in N : J is a maximal non trivial ideal on the Boolean algebra of the subsets of N.

Programs obtained from proofs

Let F be a formula of second order arithmetic, that is to say a second order formula every individual quantifier of which is restricted to N and every second order quantifier of which is restricted to P(N). We associate with F , a first order formula F † , defined by recurrence on F :

where X -is an individual variable associated with the unary predicate variable X.

Notation. In the sequel, we shall write p n instead of γ(n, p). Thus, it is the same to give an individual p or a sequence of individuals p n (n ∈ N). If i, n ∈ N, we have (i, n) ε p = i ε p n . We fix a well ordering ⊳ on P = P(Π) N , which is strict (i.e. ∀x¬(x ⊳ x)) and isomorphic to the cardinal 2 ℵ 0 : every proper initial segment of ⊳ is therefore of power < 2 ℵ 0 . We define a binary function, denoted by (p ⊳ q) by putting (p ⊳ q) = 1 if p ⊳ q ; (p ⊳ q) = 0 otherwise. Since the relation (p ⊳ q) = 1 is well founded on P , we have (theorem 11) :

in the A-model M, but also in every B-model N . We shall write, in abridged form, y ⊳ x for (y ⊳ x) = 1. Thus, in M and N , the relation ⊳ is well founded but, in general, not total. It is a strict order relation, in both models ; indeed we have immediately, in the model M :

Since all these formulas are first order, by theorem 31, we have also, in the model N :

). A condition p ∈ P is also a sequence of individuals p k . Intuitively, we shall consider it, as " the set of individuals p k+1 for k ε p 0 " ; we define accordingly the condition 1, the formula C[p] which says that p is a non trivial condition, and the binary operation ∧. 1 is the empty set, in other words i ε 1 0 (i.e. (i, 0) ε 1) must be false. Therefore, we put :

A condition is non trivial if the set of individuals, which is associated with it, is totally ordered by ⊳. Therefore, we put :

The set associated with p∧q is the union of the sets associated with p and with q ; therefore, we put : p∧q = r where r 0 is defined by : 2i ε r 0 = i ε p 0 ; 2i + 1 ε r 0 = i ε q 0 ; r j+1 is defined by : r 2i+1 = p i+1 ; r 2i+2 = q i+1 . The notation p ⊂ q means that the set associated with q contains the one associated with p. Therefore, we put : p ⊂ q ≡ ∀i ent (i ε p 0 → ∃j ent {j ε q 0 , p i+1 = q j+1 }).

e are proof-like terms representing respectively the recursive functions :

It follows that f ix || -∀j(ent(j), j ε q 0 → p i+1 = q j+1 ) → ⊥. Suppose that y ||j ε q 0 and let j ∈ |ent(j)|. If p i+1 = q j+1 , then gjyh || -⊥ ; therefore gjyh ||p i+1 = q j+1 . We have shown : λjλy(g)jyh || -∀j(ent(j), j ε q 0 → p i+1 = q j+1 ). Therefore (f ix)λjλy(g)jyh || -⊥. ii) We suppose :

If we replace j ′ with 2j ′′ , and then with 2j ′′ + 1, we obtain, by definition of ∧ :

Then, there are two cases :

we have y ||i ′′ ε p 0 and, by ( 1), (u)(d 0 )j ′′ ||j ′′ ε q 0 → p i ′′ +1 = q j ′′ +1 . Therefore : λj(u)(d 0 )j || -∀j(ent(j), j ε q 0 → p i ′′ +1 = q j+1 ) and it follows that :

. By making j ′′ = i ′′ , we obtain (u)(d 1 )i ′′ ||i ′′ ε r 0 → ⊥ and therefore :

(u)i ′ y || -⊥. Thus, in both cases, we get :

q.e.d.

) in other words || -∀p∀q(p ⊂ q → q ⊑ p).

i) Let f ||p ⊂ q, g || -C[q], that is : f || -∀i(ent(i), i ε p 0 , ∀j(ent(j), j ε q 0 → p i+1 = q j+1 ) → ⊥) ; g || -∀j∀j ′ (ent(j), ent(j ′ ), j ε q 0 , j ′ ε q 0 → E[q j+1 , q j ′ +1 ]) with :

Let y ||j ε q 0 , y ′ ||j ′ ε q 0 . We have gj j ′ yy ′ || -E[q j+1 , q j ′ +1 ] ; if p i+1 = q j+1 and p i ′ +1 = q j ′ +1 , then : gj j ′ yy ′ || -E[p i+1 , p i ′ +1 ], and therefore gj j ′ yy ′ uvw || -⊥. Thus, we have λjλy(g)jj ′ yy ′ uvw ||ent(j), j ε q 0 → ⊥ if p i+1 = q j+1 and p i ′ +1 = q j ′ +1 . Therefore, λjλy(g)jj ′ yy ′ uvw || -∀j(ent(j), j ε q 0 → p i+1 = q j+1 ) if p i ′ +1 = q j ′ +1 , thus :

ii) Follows immediately from (i) and || -∀p∀q∀r(p ⊂ q → p∧r ⊂ q∧r) (lemma 61). q.e.d. The following lemma shows that we can build the algebra B and the B-model N .

Lemma 63. There exist six proof-like terms α 0 , α 1 , α 2 , β 0 , β 1 , β 2 such that :

∀p∀q∀r∀s(C[((p∧q)∧r)∧s] → C[(p∧(q∧r))∧s]).

We only show the first case. By lemma 62(i), it suffices to find a proof-like term : θ || -∀p∀q∀r(p∧(q∧r) ⊂ (p∧q)∧r). Thus, we suppose : y ||i ε (p∧(q∧r)) 0 ; u || -∀j(ent(j), j ε ((p∧q)∧r) 0 → (p∧(q∧r)) i+1 = ((p∧q)∧r) j+1 ). There are three cases : • i = 2i ′ ; then, we have y ||i ′ ε p 0 . We make j = 2i = 4i ′ , therefore : u ||ent(2i), i ′ ε p 0 → p i ′ +1 = p i ′ +1 . Thus, we have : (u)(d 0 )iy || -⊥.

• i = 4i ′ + 1 ; then, we have y ||i ′ ε q 0 . We make j = i + 2 = 4i ′ + 3, thus : u ||ent(i + 2), i ′ ε q 0 → q i ′ +1 = q i ′ +1 . Thus, we have : ((u)(σ) 2 i)y || -⊥.

• i = 4i ′ + 3 ; then, we have y ||i ′ ε r 0 . We make j = i -3 = 4i ′ , thus :

. Therefore, we have : ((u)(p) 3 i)y || -⊥ (p is the program for the predecessor). Thus, we put θ = λiλyλu(((e 4 i)(u)(d 0 )iy)((u)(σ) 2 i)y)((u)(p) 3 i)y, where e 4 is defined by its execution rule :

q.e.d. We now show the : Theorem 64. The forcing structure {C, ∧, 1} satisfies the countable downward chain condition in M.

The hypothesis of the c.d.c. are : H 0 ≡ ∀n∃p X (n, p) ; H 1 ≡ ∀n ent ∀p∀q{X (n, p), X (n, q) → p = q} ; H 2 ≡ ∀n ent ∀p∀q(X (n, p), X (sn, q) → q ⊑ p) ; H 3 ≡ ∀n ent ∀p(X (n, p) → C[p]). Moreover, by theorem 16, we have a binary function f : P 2 → P such that : ς || -∀n ent (∃p X (n, p) → ∃k ent X (n, f (n, k))). Therefore, by H 0 , we can also use the hypothesis :

Lemma 65. H ⊢ ∀p∀q∀m ent ∀n ent (X (m, p), X (n, q) → C[p∧q]).

We show ∀m int ∀n int (X (m, p), X (m + n, q) → q ⊑ p) by recurrence on n.

For n = 0, this follows from H 1 , H 3 . For the recurrence step, we use H 2 . Thus, we have ∀p∀q∀m ent ∀n ent (X (m, p), X (n, q) → p ⊑ q ∨ q ⊑ p). q.e.d. We define the wanted limit h by defining h 0 and h m+1 for each m ∈ N.

Intuitively, X defines a sequence of countable sets, and h is the union of these sets.

• Proof of H * ⊢ X (n, p) → h ⊑ p. By lemma 62(ii), it suffices to show X (n, p) → p ⊂ h, that is : X (n, p), i ε p 0 , ∀m ent (m ε h 0 , → h m+1 = p i+1 ) → ⊥, for n, i ∈ N. We fix k ∈ N and we put m = (i, n, k). By definition of h, it suffices to show :

, we deduce f (n, k) = p and therefore : (f (n, k)) 0 = p 0 and (f (n, k)) i+1 = p i+1 . Thus, it remains to show :

This completes the proof of theorem 64. q.e.d.

The well ordering on P(N)

In the model N , we define the unary predicate G(x) ≡ ∃p∃i ent {¬J (p), i ε p 0 , x = p i+1 }.

We must show | -¬J (p), ¬J (q), i ε p 0 , x = p i+1 , j ε q 0 , y = q j+1 → E[x, y], that is : | -¬J (p), ¬J (q), i ε p 0 , j ε q 0 → E[p i+1 , q j+1 ]. By theorem 33(ii) and (iii), we have | -¬J (p), ¬J (q) → C[p∧q]. Therefore, it is sufficient to show that | -C[p∧q], i ε p 0 , j ε q 0 → E[p i+1 , q j+1 ]. We show below that we have I || -C[p∧q], i ε p 0 , j ε q 0 → E[p i+1 , q j+1 ]. Since this is a first order formula, this gives the desired result, by theorem 31. Indeed, we have : p i+1 = (p∧q) 2i+1 ; q j+1 = (p∧q) 2j+2 ; i ε p 0 = 2i ε (p∧q) 0 ; j ε q 0 = 2j + 1 ε (p∧q) 0 . Therefore, it remains to show :

q.e.d. Lemma 66 shows that ⊳ is a total relation on G. But, moreover, ⊳ is a well founded relation in N . Therefore, we have : | -G is well ordered by ⊳. We define now two functions on P : • a unary function δ : P → P by putting i ε δ(p) 0 = i + 1 ε p 0 ; δ(p) i+1 = p i+2 .

• a binary function φ : P 2 → P by putting : 47 0 ε φ(p, q) 0 = ∅ ; i + 1 ε φ(p, q) 0 = i ε p 0 ; φ(p, q) 1 = q ; φ(p, q) i+2 = p i+1 for every i ∈ N. Therefore, we have δ(φ(p, q)) = p and φ(p, q) 1 = q for all p, q ∈ P and thus : I || -∀p∀q(δ(φ(p, q)) = p) ; I | -∀p∀q(δ(φ(p, q)) = p) ; I || -∀p∀q(φ(p, q) 1 = q) ; I | -∀p∀q(φ(p, q) 1 = q). Intuitively, δ(p) defines the set we obtain by removing p 1 from the set associated with p ; φ(p, q) defines the set we obtain by adding q to the set associated with p.

Lemma 67. If p, q ∈ P , there exists q ′ ∈ P such that δ(q ′ ) = q and p i ⊳ q ′ for every i ∈ N.

For each a ∈ P , we have δ(φ(q, a)) = q. But the application a → φ(q, a) is obviously injective, since φ(q, a) 1 = a. Thus, the set {φ(q, a); a ∈ P } is of cardinal 2 ℵ 0 . Now, by hypothesis on ⊳, every proper initial segment of P , for the well ordering ⊳, is of cardinal < 2 ℵ 0 . Thus, there exists some a 0 ∈ P such that p i ⊳ φ(q, a 0 ) for every i ∈ N. Then, it suffices to put q ′ = φ(q, a 0 ).

q.e.d. Therefore, we can define a binary function ψ : P 2 → P such that we have : δ(ψ(p, q)) = q and (p i ⊳ ψ(p, q)) = 1 for all p, q ∈ P and i ∈ N. Thus, we have : I || -∀p∀q(δ(ψ(p, q)) = q) ; I | -∀p∀q(δ(ψ(p, q)) = q). KI || -∀p∀q∀i ent (p i ⊳ ψ(p, q)) ; KI | -∀p∀q∀i ent (p i ⊳ ψ(p, q)).

Lemma 68. We have | -∀q∃x{G(x), δ(x) = q}.

This is written as | -∀q[∀x∀p∀i ent (δ(x) = q, i ε p 0 , x = p i+1 → J (p)) → ⊥] or else : | -∀q[∀p∀i ent (i ε p 0 , δ(p i+1 ) = q → J (p)) → ⊥]. By making i = 0, it is sufficient to show : [START_REF] Berardi | On the computational content of the axiom of choice[END_REF] | -∀q[∀p(0 ε p 0 , δ(p 1 ) = q → J (p)) → ⊥]. By replacing p with φ(p, ψ(p, q)) in (1), we see that it remains to show : | -∀q¬∀p J (φ(p, ψ(p, q))).

Lemma 69. || -∀p∀q(C[p] → C[φ(p, ψ(p, q))]).

We have C[r] ≡ ∀i ent ∀j ent (i ε r 0 , j ε r 0 → E[r i+1 , r j+1 ]). Therefore, in order to show that || -C[p] → C[r], it suffices to show :

(1) || -C[p] → ∀i ent ∀j ent (i + 1 ε r 0 , j + 1 ε r 0 → E[r i+2 , r j+2 ]) and

(2) || -C[p] → ∀j ent (0 ε r 0 , j + 1 ε r 0 → E[r 1 , r j+2 ]). We apply this remark by putting r = φ(p, ψ(p, q)). Then ( 1) is written as || -C[p] → C[p] since i + 1 ε r 0 = i ε p 0 and r i+2 = p i+1 and the same for j. Thus, it suffices to show [START_REF] Curry | Combinatory Logic[END_REF], that is : || -C[p] → ∀j ent (0 ε φ(p, ψ(p, q)) 0 , j + 1 ε φ(p, ψ(p, q)) 0 → E[φ(p, ψ(p, q)) 1 , φ(p, ψ(p, q)) j+2 ]). But, we have I || -∀p∀q(0 ε φ(p, q) 0 ) ; I || -∀p∀q(j ε p 0 → j + 1 ε φ(p, ψ(p, q)) 0 ) ; I || -∀p∀q(φ(p, ψ(p, q)) 1 = ψ(p, q)) ; I || -∀p∀q(φ(p, ψ(p, q)) j+2 = p j+1 ). Therefore, it remains to show :

|| -C[p] → ∀j ent (j ε p 0 → E[ψ(p, q), p j+1 ]) which is trivial, since we have KI || -∀p∀q∀j ent (p j+1 ⊳ ψ(p, q)).

q.e.d.

Lemma 70. λiλxλy((y)(σ)i)x || -∀p∀q(p ⊂ φ(p, q)).

This is written as : λiλxλy((y)(σ)i)x || -∀i(ent(i), i ε p 0 , ∀j(ent(j), j ε φ(p, q) 0 → φ(p, q) j+1 = p i+1 ) → ⊥) which is immediate, by making j = i + 1.

q.e.d. We have ||p ⊂ φ(p, ψ(p, q)) (lemma 70), and it follows that :

||φ(p, ψ(p, q)) ⊑ p (lemma 62ii), and thus || -C[φ(p, ψ(p, q))] → C[p∧φ(p, ψ(p, q))]. Therefore, by lemma 69, we have : || -∀p∀q(C[p] → C[p∧φ(p, ψ(p, q))]). Since this is a first order formula, we have, by theorem 31 : | -∀p∀q(C[p] → C[p∧φ(p, ψ(p, q))]) and therefore, by theorem 33(ii) : | -∀p∀q(¬C[p∧φ(p, ψ(p, q))] → J (p)). Then, we apply theorem 34, which gives : | -∀q¬∀p J (φ(p, ψ(p, q))) which is the desired result.

q.e.d.

Theorem 71. The following formulas are realized in N : i) There exists a well ordering on the set of individuals.

ii) There exists a well ordering on the power set of N.

i) Lemma 68 shows that, in N , the function δ is a surjection from G onto the set P of individuals. But, we have seen that the formula : " G is well ordered by ⊳ " is realized in N . ii) By theorems 38 and 64, the following formula is realized in N : " Every subset of N is represented by an individual ". Hence the result, by (i).

q.e.d. Theorem 71(ii) enables us to transform into a program any proof of a formula of second order arithmetic, which uses the existence of a well ordering on R. The method is the same as the one explained above for the ultrafilter axiom.