Valentin Blot

A direct computational interpretation of second-order arithmetic via update recursion

Second-order arithmetic has two kinds of computational interpretations: via Spector's bar recursion of via Girard's polymorphic lambda-calculus. Bar recursion interprets the negative translation of the axiom of choice which, combined with an interpretation of the negative translation of the excluded middle, gives a computational interpretation of the negative translation of the axiom scheme of comprehension. It is then possible to instantiate universally quantified sets with arbitrary formulas (second-order elimination). On the other hand, polymorphic lambda-calculus interprets directly second-order elimination by means of polymorphic types. The present work aims at bridging the gap between these two interpretations by interpreting directly second-order elimination through update recursion, which is a variant of bar recursion.

INTRODUCTION

In this introduction we recall the existing interpretations of secondorder arithmetic, we present the outline of our contribution, and we mention some related work.

Bar recursive interpretations

The usual route, summarized in figure 1, for interpreting secondorder arithmetic via bar recursion consists of a derivation of the axiom scheme of comprehension through a combination of the excluded middle with the axiom of countable choice, followed by a negative translation into first-order intuitionistic arithmetic extended with the negative translation of the axiom of choice. Finally, this system is interpreted with the help of bar recursion that gives computational content to the negative translation of the axiom of countable choice (or to the double-negation shift which, together with the axiom of countable choice, implies intuitionistically the negative translation of the axiom of countable choice).

We review in this section the various existing bar recursive interpretations of second-order arithmetic.

Spector's original bar recursion. Gödel's dialectica interpretation [START_REF] Gödel | Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes[END_REF] provides a computational interpretation of arithmetic into System T -simply-typed lambda-calculus with natural numbers and a recursor. Spector extends this interpretation to an interpretation of second-order arithmetic [START_REF] Spector | Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics[END_REF] by extending Gödel's System T with a bar recursion operator. Spector uses this bar recursion operator to interpret what he calls the F axiom scheme, but which is nowadays known as double-negation shift (DNS). Composing his interpretation with a negative translation from classical arithmetic with countable choice into intuitionistic arithmetic with countable choice and DNS, he obtains an interpretation of classical arithmetic with countable choice and therefore of second-order arithmetic.

Berardi-Bezem-Coquand's demand-driven operator. Berardi, Bezem and Coquand define an operator [START_REF] Berardi | On the Computational Content of the Axiom of Choice[END_REF] (usually called BBC) inspired by Spector's bar recursion but that has a more direct and intuitive behavior. Also, contrary to Spector's interpretation that extends Gödel's Dialectica, their interpretation extends Kreisel's modified realizability [START_REF] Kreisel | Interpretation of analysis by means of constructive functionals of finite types[END_REF]. The BBC operator is demand-driven in the sense that it computes step by step finite approximations of an ideal infinite object, the order of these steps being dictated by the environment in which the operator executes. They use this operator to provide a computational interpretation of (a principle equivalent to) the negative translation of the axiom of countable choice. Their interpretation is therefore slightly more direct than Spector's in the sense that it interprets the negative translation of the axiom of countable choice rather than DNS.

Berger-Oliva's modified bar recursion. Berger and Oliva define an operator [START_REF] Berger | Modified bar recursion and classical dependent choice[END_REF] that more closely resembles Spector's bar recursion, but their interpretation extends Kreisel's modified realizability, as Berardi-Bezem-Coquand's. Moreover, they follow more closely the lead of Spector by interpreting DNS, from which the negative translation of the axiom of countable choice can be derived.

Streicher and Krivine's bar recursion in classical realizability. Streicher gives a presentation of Krivine's classical realizability in the setting of categorical realizability, as a subtopos K of the relative realizability topos E induced by the model of coherence spaces and stable maps and a well-chosen set of proof-like elements [START_REF] Streicher | A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus[END_REF]. Using bar induction and the interpretation of bar recursion as a stable map between appropriate coherence spaces, he shows that E validates the double-negation shift principle, and because E also validates countable choice, he obtains that the classical realizability topos K validates countable choice.

Krivine uses the BBC operator to realize the negative translation of the axiom of countable choice [START_REF] Krivine | Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis[END_REF].

Interpretation of second-order arithmetic via system F

The second kind of interpretation of second-order arithmetic is via Girard's representation theorem [START_REF] Girard | Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur[END_REF] that relies on a translation of second-order arithmetic into Girard-Reynolds polymorphic lambdacalculus [START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types[END_REF][START_REF] Reynolds | Towards a theory of type structure[END_REF] (system F). This interpretation uses a version of second-order arithmetic that is obtained from first-order arithmetic by adding a quantifier on predicates, rather than the axiom schema

Contributions

As explained above, the bar recursive interpretations of secondorder arithmetic involve several logical transformations prior to the concrete interpretation by programs. Conversely, the polymorphic interpretation exploits a strong correspondence between quantification on predicates and polymorphic types. In the present paper we make a crucial step towards the unravelling of a similar strong correspondence in the case of bar recursion. Indeed, we interpret directly the same system of second-order arithmetic as the one used in Girard's representation theorem, via a bar recursive interpretation of the elimination of quantification on predicates. We define a very generic notion of realizability value and prove a general result about the behavior of the variant of bar recursion we use. This general result proves to be flexible enough so that it can be used for proving both termination of the programming language and correctness of the realizability interpretation.

Related work

Berger defines a variant of the bar recursion operator that he calls "update recursion" [START_REF] Berger | A Computational Interpretation of Open Induction[END_REF]. This variant is closely related to the BBC operator, in the sense that it builds finite approximations of an ideal infinite object step-by-step and on demand. Berger proves that this operator realizes a principle called "update induction" and shows that the BBC operator can indeed be implemented via update recursion. Berger's operator is the variant of bar recursion that most closely fits our needs, so we use (a slight variant of) it in the present work. However, we show directly that our version of update recursion realizes second-order elimination, without going through update induction.

Aschieri, Berardi and Birolo extend lambda-calculus with a variant of delimited exceptions and use interactive realizability to interpret intuitionistic first-order arithmetic extended with a restricted form of excluded middle EM1 on Σ 0 1 formulas [START_REF] Aschieri | Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1[END_REF]. Powell uses a similar idea in the context of Gödel's Dialectica interpretation to define the concept of learning algorithms [START_REF] Powell | Gödel's functional interpretation and the concept of learning[END_REF], that build approximations to witnesses of decidable formulas. He then transforms a countable sequence of learning algorithms into a single algorithm and proves that it can be used to interpret arithmetical comprehension on Σ 0 1 formulas. Our work can be seen as an extension of these works, where we relax the decidability requirement and provide computational content to the full comprehension axiom instead of its restriction to Σ 0 1 formulas.

Outline of the paper

In the first section, we present the system of second-order arithmetic used in Girard's representation theorem, where the usual comprehension axiom is replaced with the equivalent notion of quantification over predicates.

In the next section we define our programming language together with its operational and denotational semantics.

In the final section, we define our general notion of realizability value and prove a very generic result about update recursion, then we prove normalization of our programming language using "propositional" realizability values a.k.a. reducibility candidates. Then we prove adequacy of our interpretation via realizability values that depend on natural numbers and sets of natural numbers. Finally, we validate this interpretation by proving an extraction result from proofs of Π 0 2 formulas of second-order arithmetic.

SECOND-ORDER ARITHMETIC

We define in this section the theory of second-order arithmetic for which we provide a computational interpretation in the following sections.

This theory is the one used in Girard's representation theorem with quantifications over predicates, as witnessed by the ∀2𝑒 rule, where 𝐴 [𝑥 .𝐵/𝑋 ] is the formula 𝐴 where every instance of an atom of the form 𝑋 (𝑡) for some term 𝑡 is replaced with the formula 𝐵 [𝑡/𝑥].

Second-order logic has two kinds of variables: 𝑥, 𝑦, . . . denote first-order (number) variables and 𝑋, 𝑌, . . . denote second-order (set) variables. The terms of second-order arithmetic are built from number variables, 0, successor, addition and multiplication:

𝑡, 𝑢 ::= 𝑥 | 0 | 𝑆 𝑡 | 𝑡 + 𝑢 | 𝑡 × 𝑢
Formulas are built from atomic formulas (set variables applied to some term), implication and first-and second-order universal quantification:

𝐴, 𝐵 ::= 𝑋 (𝑡) | 𝐴 ⇒ 𝐵 | ∀𝑥 𝐴 | ∀𝑋 𝐴
The formal system of second-order arithmetic (rules and axioms) is defined in figure 2. Our proof trees are annotated with proof terms for convenience, but we do not consider any kind of reduction on these proof terms.

As usual, other logical connectors such as equality, conjunction, disjunction and first-and second-order quantification can be encoded in second-order logic. In the present paper we only use the following encodings:

𝑋 ≡ 𝑋 (0) 𝑡 = 𝑢 ≡ ∀𝑋 (𝑋 (𝑡) ⇒ 𝑋 (𝑢)) ⊥ ≡ ∀𝑋 𝑋 ¬𝐴 ≡ 𝐴 ⇒ ⊥ 𝑡 ≠ 𝑢 ≡ ¬ (𝑡 = 𝑢)
In particular, while formally all our predicate variables are unary, we encode the nullary ones via an arbitrary instantiation at 0. This technical choice allows for a more uniform treatment in the realizability interpretation. Note also that since we have terms for addition and multiplication, we could also encode predicate variables of arbitrary arity, but we do not need them in the present work.

THE PROGRAMMING LANGUAGE

In this section we describe the programming language in which we interpret proofs made in second-order arithmetic. We first define its syntax, typing rules and operational semantics, and then we define its denotational semantics in complete partial orders.

Syntax, typing and operational semantics

This programming language is an extension of simply-typed lambdacalculus with primitive natural numbers, sum types, a unit type and an update recursion operator ur.

The types are as follows, where 𝜄 denotes the type of natural numbers:

𝜎, 𝜏 ::

= 𝜄 | 1 | 𝜎 → 𝜏 | 𝜎 + 𝜏
The typing rules and operational semantics are given in figure 3, where the notation 𝜆_.𝑀 is a shorthand for 𝜆𝑥 .𝑀 when 𝑥 is not free in 𝑀, and the construct _ ⟨_ ↦ →⟩ in the reduction rule for update recursion is syntactic sugar for the update of a notion of partial function that we define now. These partial functions on natural numbers, that the update recursion operator relies on, are encoded as functions from natural numbers to a sum type 𝜎 + 1, that we use as an option type. We consider that such a partial function

𝑀 : 𝜄 → 𝜎 + 1 is defined at 𝑛 ∈ N if 𝑀 𝑛 ⇝ * {𝑁 | } for some 𝑁 : 𝜎, and is undefined at 𝑛 ∈ N if 𝑀 𝑛 ⇝ * { | ★}.
Consequently, the function with empty domain is defined as:

𝜖 ≡ 𝜆_. { | ★}
and if 𝑀 is some partial function, then 𝑀 ⟨𝑁 1 ↦ → 𝑁 2 ⟩ denotes its update with value 𝑁 2 at 𝑁 1 , which is defined as:

𝑀 ⟨𝑁 1 ↦ → 𝑁 2 ⟩ ≡ 𝜆𝑥 .if 𝑥 = 𝑁 1 then {𝑁 2 | } else (𝑀 𝑥)
where:

if 𝑀 = 𝑁 then 𝑃 1 else 𝑃 2 ≡ (𝑀 ? 𝜄 (𝜆𝑢.𝑢 ? 𝜄 𝑃 1 (𝜆𝑦_.𝑃 2 )) (𝜆𝑥𝑧𝑢.𝑢 ? 𝜄 𝑃 2 (𝜆𝑦_.𝑧 𝑦))) 𝑁
is an operation deciding equality on natural numbers. We now comment on the update recursion operator. By looking at the type of the recursor, one can understand update recursion as an operator turning a program of type:

(𝜄 → 𝜎 + (𝜎 → 𝜄)) → 𝜄 into a program of type: (𝜄 → 𝜎 + 1) → 𝜄
That is, if some 𝑀 takes as input a sequence of elements which are either of type 𝜎 or of type 𝜎 → 𝜄, then ur 𝑀 takes simply as input a partial function to 𝜎. The reduction rule of ur shows how this happens: if 𝑀 needs the value of its argument at some point 𝑛, then:

• either the partial function given as argument to ur 𝑀 is defined at 𝑛, in which case ur 𝑀 provides that value to 𝑀, as a value of type 𝜎, • or the argument to ur 𝑀 is undefined at 𝑛, in which case ur 𝑀 provides indirectly to 𝑀 a value of type 𝜎 → 𝜄 by reading the input 𝑁 of type 𝜎 from 𝑀, and triggering a recursive call with an updated partial function having value 𝑁 at 𝑛.

Our version of update recursion is a bit different from Berger's [START_REF] Berger | A Computational Interpretation of Open Induction[END_REF]. The first difference is that we use sum types, while Berger encodes them with booleans and products. The second difference is that while the first argument in our version is of type:

(𝜄 → 𝜎 + (𝜎 → 𝜄)) → 𝜄
the first argument in Berger's version is (with our notations) of type:

(𝜄 → 𝜎 + 1) → (𝜄 → 𝜎 → 𝜄) → 𝜄
Finaly, Berger's update recursion satisfies (with our notations) the following equation:

Γ ⊢ 𝑀 : 𝜎 + 𝜏 Γ ⊢ 𝑀 ? + : (𝜎 → 𝜈) → (𝜏 → 𝜈) → 𝜈 Γ ⊢ ★ : 1 Γ ⊢ ur : ((𝜄 → 𝜎 + (𝜎 → 𝜄)) → 𝜄) → (𝜄 → 𝜎 + 1) → 𝜄 typing derivations (𝜆𝑥 .𝑀) 𝑁 ⇝ 𝑀 [𝑁 /𝑥] ur 𝑀 𝑁 ⇝ 𝑀 (𝜆𝑥 .𝑁 𝑥 ? + (𝜆𝑦. {𝑦 | }) (𝜆_. { | 𝜆𝑦.ur 𝑀 (𝑁 ⟨𝑥 ↦ → 𝑦⟩))}) S 𝑛 ⇝ 𝑛 + 1 0 ? 𝜄 𝑁 1 𝑁 2 ⇝ 𝑁 1 𝑛 + 1 ? 𝜄 𝑁 1 𝑁 2 ⇝ 𝑁 2 𝑛 (𝑛 ? 𝜄 𝑁 1 𝑁 2 ) {𝑀 | }? + 𝑁 1 𝑁 2 ⇝ 𝑁 1 𝑀 { | 𝑀 }? + 𝑁 1 𝑁 2 ⇝ 𝑁 2 𝑀 𝐸 [𝑀] ⇝ 𝐸 [𝑁 ] if 𝑀 ⇝ 𝑁 where 𝐸 [_] ::= 𝐸 [_] 𝑀 | S 𝐸 [_] | 𝐸 [_] ? 𝜄 | 𝐸 [_] ? +
operational semantics Figure 3: The programming language

Denotational semantics: complete partial orders

The termination of the update recursion operator depends crucially on the continuity of programs: if a program turns an infinite sequence into a value of type 𝜄, then it can only depend on a finite part of its input sequence. The intuition is that such a program converges in a finite number of steps to a final value, and therefore during this computation it can only evaluate its input at a finite number of positions. The denotational model of complete partial orders does provide a general framework to talk about continuity of programs in this sense.

Moreover, it will be convenient, for proving correctness of update recursion, to talk about ideal sequences which are limits of finite sequences, but may not be expressible as programs. Such ideal sequences may even be non-computable. If (𝑎 𝑛 ) 𝑛∈N is a sequence of elements of some complete partial order 𝐷, then the function that turns 𝑛 ∈ N into 𝑎 𝑛 is itself an element of the complete partial order of functions from natural numbers to 𝐷, so the model of complete partial orders is very suited for handling such ideal sequences.

We now turn to the basic definitions about complete partial orders: Definition 3.1. A partially ordered set 𝐷 is directed if it is nonempty and:

∀𝑥, 𝑦 ∈ 𝐷, ∃𝑧 ∈ 𝐷, 𝑥 ≤ 𝑧 and 𝑦 ≤ 𝑧 A complete partial order (cpo) is a partial order 𝐷:

• which has a least element ⊥,

• such that every directed subset 𝑋 ⊆ 𝐷 has a least upper bound 𝑋 ∈ 𝐷.

A continuous function between cpos is a function that preserves directed sets and their suprema: Definition 3.2. If 𝐷 and 𝐸 are cpos, a map 𝑓 : 𝐷 → 𝐸 is continuous if for all directed 𝑋 ⊆ 𝐷, 𝑓 (𝑋 ) ⊆ 𝐸 is directed and:

𝑓 𝑋 = 𝑓 (𝑋 )
The following proposition is a fundamental result about cpos that permits the interpretation of functional programming languages in the model of cpos. Its proof can be found, e.g. in [START_REF] Amadio | Domains and Lambda-Calculi[END_REF]. Proposition 3.3. The set of pointwise ordered continuous maps from cpo 𝐷 to cpo 𝐸 is a cpo that we denote with 𝐷 → 𝐸.

Moreover, the componentwise ordering on products of cpos turns the model of cpos into a cartesian closed category, and therefore into a model of 𝜆-calculus (see [START_REF] Amadio | Domains and Lambda-Calculi[END_REF] for details).

After these general definitions about the model of cpos, we move to its use for our programming language.

We start with the operation of lifting of a cpo, which adds a least element to an existing cpo: if 𝐴 is a partially ordered set we let 𝐴 ⊥ be the set 𝐴 ∪ {⊥} equipped with the order on 𝐴 extended with ⊥ ≤ 𝑎 for all 𝑎 ∈ 𝐴 ⊥ . If 𝐴 is a set then it is implicitly equipped with the discrete ordering. Liftings of such sets are used to interpret base types. We associate to each type 𝜎 a cpo [𝜎] as follows:

[𝜄] = N ⊥ [𝜎 → 𝜏] = [𝜎] → [𝜏] [1] = {★} ⊥ [𝜎 + 𝜏] = ([𝜎] ⊎ [𝜏]) ⊥
where we choose the same symbol ★ to denote the program on the unit type and its interpretation. We now prove that the operation deciding equality between natural numbers, the empty function and the update of a partial function do have the intended semantics. Proposition 3.4. We have:

if 𝑀 = 𝑁 then 𝑃 1 else 𝑃 2 =          ⊥ if [𝑀] = ⊥ or [𝑁 ] = ⊥ [𝑃 1 ] if [𝑀] = [𝑁 ] ≠ ⊥ [𝑃 2 ] if ⊥ ≠ [𝑀] ≠ [𝑁 ] ≠ ⊥ [𝜖] (𝑎) = { | ★} [𝑀 ⟨𝑁 1 ↦ → 𝑁 2 ⟩] (𝑎) =          ⊥ if 𝑎 = ⊥ [{𝑁 2 | }] if 𝑎 = [𝑁 1 ] [𝑀] (𝑎) if 𝑎 ≠ [𝑁 1 ] and 𝑎 ≠ ⊥ Proof. For the first item: if [𝑀] = ⊥ then: [if 𝑀 = 𝑁 then 𝑃 1 else 𝑃 2 ] = ⊥
otherwise define:

𝑑 0 = [𝜆𝑢.𝑢 ? 𝜄 𝑃 1 (𝜆𝑦_.𝑃 2 )] 𝑑 𝑛+1 = [𝜆𝑥𝑧𝑢.𝑢 ? 𝜄 𝑃 2 (𝜆𝑦_.𝑧 𝑦)] (𝑛) (𝑑 𝑛 )
so that:

[if𝑀 = 𝑁 then 𝑃 1 else 𝑃 2 ] = 𝑑 [𝑀 ] ([𝑁 ])
We then prove by induction on

𝑛 ∈ N that 𝑑 𝑛 (⊥) = ⊥, 𝑑 𝑛 (𝑛) = [𝑃 1 ] and 𝑑 𝑛 (𝑚) = [𝑃 2 ]
if 𝑚 ≠ 𝑛, from which the result follows. The second item is immediate and the third follows easily from the first by case analysis. □

We now prove that the interpretation of update recursion satisfies the recursive equation implied by its reduction rule: Lemma 3.5. For all ì 𝑎, 𝑏:

𝔉 ([ur] ( ì 𝑎) (𝑏)) = [ur] ( ì 𝑎) (𝑏)
Proof. Indeed, 𝔉 is continuous so:

𝔉 ([ur] ( ì 𝑎) (𝑏)) = 𝔉 𝑛∈N 𝔉 𝑛 (⊥) = 𝑛∈N 𝔉 𝔉 𝑛 (⊥) = 𝑛∈N 𝔉 𝑛+1 (⊥) = ⊥ ∨ 𝑛∈N 𝔉 𝑛+1 (⊥) = 𝑛∈N 𝔉 𝑛 (⊥) = [ur] ( ì 𝑎) (𝑏) □
The following proposition asserts that the denotational semantics of our programming language is correct with respect to its operational semantics. Proof. By case on the reduction 𝑀 ⇝ 𝑁 , using the previous lemma for the case of update recursion. □

The following result, computational adequacy, allows to "go back" from the denotational model to the syntactic language on base types. It asserts that if some program on a base type is interpreted as a value, then it must reduce to that value. It will be particularly useful for proving that extracted programs do compute the intended values. The result is standard, usually proved via logical relations, the interested reader can refer to [START_REF] Amadio | Domains and Lambda-Calculi[END_REF]. In the following we will often drop the interpretation brackets and use programs with parameters, that is, we will write 𝑀 [ ì 𝑎/ì 𝑥] instead of [𝑀] ( ì 𝑎).

REALIZABILITY

In this section we define a general notion of realizability value. We first use it to prove normalization of our programming language.

We then define the interpretation of proofs in our programming language and we prove the correctness of this interpretation with respect to realizability values associated to formulas. Finally, we prove an extraction theorem from proofs of Π 0 2 theorems.

[𝑥 𝑖 ] ( ì 𝑎) = 𝑎 𝑖 [𝜆𝑥 .𝑀] ( ì 𝑎) (𝑏) = [𝑀] ( ì 𝑎, 𝑏) [𝑀 𝑁 ] ( ì 𝑎) = [𝑀] ( ì 𝑎) ([𝑁 ] ( ì 𝑎)) [★] ( ì 𝑎) = ★ [𝑛] ( ì 𝑎) = 𝑛 [S 𝑀] ( ì 𝑎) = [𝑀] ( ì 𝑎) + 1 [𝑀 ? 𝜄 ] ( ì 𝑎) (𝑏) (𝑐) = 𝑑 [𝑀 ] ( ì 𝑎)
where

         𝑑 ⊥ = ⊥ 𝑑 0 = 𝑏 𝑑 𝑛+1 = 𝑐 (𝑛) (𝑑 𝑛 ) [{𝑀 | }] ( ì 𝑎) = {[𝑀] ( ì 𝑎) | } [{ | 𝑀 }] ( ì 𝑎) = { | [𝑀] ( ì 𝑎)} [𝑀 ? + ] ( ì 𝑎) (𝑏) (𝑐) =          ⊥ if [𝑀] ( ì 𝑎) = ⊥ 𝑏 (𝑑) if [𝑀] ( ì 𝑎) is some {𝑑 | } 𝑐 (𝑑) if [𝑀] ( ì 𝑎) is some { | 𝑑 } [ur] ( ì 𝑎) (𝑏) = 𝑛∈N 𝔉 𝑛 (⊥) where 𝔉 = [𝜆𝑧𝑟 𝑓 .𝑧 (𝜆𝑥 .𝑓 𝑥 ? + (𝜆𝑦. {𝑦 | }) (𝜆_. { | 𝜆𝑦.𝑟 (𝑓 ⟨𝑥 ↦ → 𝑦⟩))})] ( ì 𝑎) (𝑏)
Figure 4: Denotational semantics in complete partial orders

Realizability values

In this section we define a general notion of realizability value that is just a subset of the cpo interpretation of a type. We then prove some properties on these realizability values and we prove a general result on the behavior of update recursion with respect to arbitrary realizability values.

A → B = {𝑓 ∈ [𝜎 → 𝜏] | ∀𝑎 ∈ A, 𝑓 (𝑎) ∈ B} A + B = {A | } ∪ { | B}
As for subtyping, → is contravariant on the left and covariant on the right with respect to inclusion. We also have some commutation rules with respect to unions and intersections. Lemma 4.2. For every realizability values A 1 , A 2 on 𝜎 and B 1 ,

B 2 on 𝜏, if A 2 ⊆ A 1 and B 1 ⊆ B 2 then: A 1 → B 1 ⊆ A 2 → B 2
Il (A 𝑒 ) 𝑒 ∈𝐸 is a family of realizability values and B is a realizability value, then:

𝑒 ∈𝐸 (A 𝑒 → B) = 𝑒 ∈𝐸 A 𝑒 → B 𝑒 ∈𝐸 (B → A 𝑒 ) = B 𝑒 → 𝑒 ∈𝐸 A 𝑒 𝑒 ∈𝐸 (A 𝑒 → B) ⊆ 𝑒 ∈𝐸 A 𝑒 → B 𝑒 ∈𝐸 (B → A 𝑒 ) ⊆ B → 𝑒 ∈𝐸 A 𝑒 Proof. For the first item, let 𝑓 ∈ A 1 → B 1 and let 𝑎 ∈ A 2 . Then 𝑎 ∈ A 1 so 𝑓 (𝑎) ∈ B 1 ⊆ B 2 .
The second item follows from the basic rules of quantifiers. □

The following proposition describes very precisely the behavior of update recursion on arbitrary realizability values. We will use it both for proving normalization of our programming language, and for proving correctness of our interpretation of the ∀2𝑒 rule of second-order arithmetic. Our proof is largely inspired by [START_REF] Berger | The Berardi-Bezem-Coquand-functional in a domaintheoretic setting[END_REF].

ur ∈ 𝑛∈N ({𝑛} → A 𝑛 + (A 𝑛 → B)) → B → 𝑛∈N ({𝑛} → A 𝑛 + {★}) → B
Proof. Remark that 𝑛∈N ({𝑛} → A 𝑛 + {★}) is a realizability value on the type 𝜄 → 𝜎 + 1 of partial functions on 𝜎 that we presented earlier. We define a preorder ≼ on this realizability value, which corresponds to the usual order between partial functions, as follows:

𝑓 ≼ 𝑔 iff ∀𝑛 ∈ N, 𝑓 (𝑛) ∈ {A 𝑛 | } ⇒ 𝑔 (𝑛) = 𝑓 (𝑛)
Be careful that this preorder ≼ is not the cpo order ≤. It is a different preorder that we only use in the proof of the current proposition.

Let 𝑎 ∈ 𝑛∈N ({𝑛} → A 𝑛 + (A 𝑛 → B)) → B and let:

𝐸 = 𝑓 ∈ 𝑛∈N ({𝑛} → A 𝑛 + {★}) ur 𝑎 𝑓 ∉ B
We prove that every non-empty chain of (𝐸, ≼) has an upper bound but (𝐸, ≼) has no maximal element. Therefore by Zorn's lemma 𝐸 must be empty, which proves the result. Every non-empty chain of (𝐸, ≼) has an upper bound. Let 𝐹 ⊆ 𝐸 be a non-empty chain. Define ⋎𝐹 by ⋎𝐹 (⊥) = ⊥ and:

if ∀𝑓 ∈ 𝐹, 𝑓 (𝑛) = { | ★} then ⋎𝐹 (𝑛) = { | ★} if ∃𝑓 ∈ 𝐹, 𝑓 (𝑛) ∈ {A 𝑛 | } then ⋎𝐹 (𝑛) = 𝑓 (𝑛)
Note that since 𝐹 is a chain, the value in the second case is unique so ⋎𝐹 is well defined. By construction, ⋎𝐹 is an upper bound of 𝐹 in 𝑛∈N ({𝑛} → A 𝑛 + {★}), so we are left to prove ⋎𝐹 ∈ 𝐸. Suppose for the sake of contradiction that ⋎𝐹 ∉ 𝐸, that is, ur 𝑎 ⋎𝐹 ∈ B. Define 𝑓 𝐼 for finite 𝐼 ⊆ N by:

𝑓 𝐼 (⊥) = ⊥ 𝑓 𝐼 (𝑛) = ⋎𝐹 (𝑛) if 𝑛 ∈ 𝐼 ⊥ otherwise
Then for the cpo order ≤ on [𝜄 → 𝜎 + 1]:

• {𝑓 𝐼 | 𝐼 ⊆ N finite} is directed • ⋎𝑓 = {𝑓 𝐼 | 𝐼 ⊆ N finite}
By monotonicity of ur 𝑎 we have for all 𝐼 :

ur 𝑎 𝑓 𝐼 ≤ ur 𝑎 ⋎𝐹 so ur 𝑎 𝑓 𝐼 ∈ {⊥, ur 𝑎 ⋎𝐹 } and then by continuity of ur 𝑎 there must exist 𝐼 0 such that:

ur 𝑎 𝑓 𝐼 0 = ur 𝑎 ⋎𝐹 By definition of ⋎𝐹 and non-emptiness of 𝐹 , for each 𝑖 ∈ 𝐼 0 there exists 𝑓 𝑖 ∈ 𝐹 such that:

𝑓 𝑖 (𝑖) = ⋎𝐹 (𝑖) = 𝑓 𝐼 0 (𝑖)
Then since 𝐹 is a chain and 𝐼 0 is finite, there exists 𝑓 ∈ 𝐹 such that 𝑓 𝑖 ≼ 𝑓 for every 𝑖 ∈ 𝐼 0 . Finally, for each 𝑛 ∈ N:

• if 𝑛 ∉ 𝐼 0 then 𝑓 𝐼 0 (𝑛) = ⊥ ≤ 𝑓 (𝑛) • if 𝑛 ∈ 𝐼 0 then 𝑓 𝑛 (𝑛) = ⋎𝐹 (𝑛) = 𝑓 𝐼 0 (𝑛) and: -if 𝑓 𝑛 (𝑛) ∈ {A 𝑛 | } then 𝑓 (𝑛) = 𝑓 𝑛 (𝑛) since 𝑓 𝑛 ≼ 𝑓 ,

Normalization

We now use the general notion of realizability value to prove the normalization of our programming language. For that, we define for each type 𝜎 the realizability value |𝜎 | on 𝜎 as follows:

|𝜄| = N |𝜎 → 𝜏 | = |𝜎 | → |𝜏 | |1| = {★} |𝜎 + 𝜏 | = |𝜎 | + |𝜏 |
These realizability values are the semantic counterparts of the usual reducibility candidates, so they satisfy the following property: □

We are now ready to prove that each program belongs to the realizability value associated to its type:

𝑛∈N ({𝑛} → |𝜎 | + (|𝜎 | → |𝜄|)) = 𝑛∈N {𝑛} → |𝜎 | + (|𝜎 | → |𝜄|) = |𝜄| → |𝜎 | + (|𝜎 | → |𝜄|) 𝑛∈N ({𝑛} → |𝜎 | + {★}) = 𝑛∈N {𝑛} → |𝜎 | + |1| = |𝜄| → |𝜎 | + |1| □
From this theorem and the previous lemma we get normalization of our programming language: Corollary 4.6. If 𝑀 is a closed program, then 𝑀 is normalizing.

Realizability interpretation

We now define the interpretation of second-order arithmetic proofs as programs of our programming language. Our interpretation follows the line of modified realizability and associates to each proof of a formula 𝐴 in second-order arithmetic a program which type 𝐴 † is derived from the formula. The mapping is defined as follows:

𝑋 (𝑡) † ≡ 𝜄 (𝐴 ⇒ 𝐵) † ≡ 𝐴 † → 𝐵 † (∀𝑥 𝐴) † ≡ 𝜄 → 𝐴 † (∀𝑋 𝐴) † ≡ 𝐴 †
We interpret 𝑋 (𝑡) with type 𝜄 in order to be able to extract natural numbers from proofs in theorem 4.14. In case we aren't interested in extraction then we can interpret 𝑋 (𝑡) with an arbitrary discrete non-empty type. Before interpreting proofs as programs, we have to interpret terms 𝑡 of the logic as programs 𝑡 † of type 𝜄. The free variables of 𝑡 † are the first-order variables of 𝑡 and they are of type 𝜄. This interpretation is straightforward, since addition and multiplication are easily implemented with the following programs:

𝑀 + 𝑁 ≡ 𝑁 ? 𝑀 (𝜆𝑥𝑧.S 𝑧) 𝑀 × 𝑁 ≡ 𝑁 ? 0 (𝜆𝑥𝑧.𝑀 + 𝑧)
Finally, the proof of a sequent: 𝑥 are the free first-order variables of 𝐴 1 , . . . , 𝐴 𝑛 , 𝐴. The interpretation of logical rules and arithmetical axioms is given in figure 5. Most of these interpretations are standard and the novelty here lies in the interpretation of the ∀2𝑒 rule. The interpretation of this rule consists in an instance of update recursion applied to a program inductively defined over the formula under the second-order quantification.

𝑝 1 : 𝐴 1 , . . . ,

Realizability semantics

We now have to prove that this interpretation is correct with respect to the logic. In order to define what we mean by correct, we associate to each formula a realizability value that represents (the interpretations of) the programs which are correct with respect to the formula.

A valuation for a term 𝑡 (resp. a formula 𝐴) is a mapping of firstorder variables of 𝑡 (resp. 𝐴) to elements of N and second-order variables of 𝐴 to elements of P (N). As we did for programs, instead of pairs (𝑡, 𝑣) (resp. (𝐴, 𝑣)) of a term (resp. formula) and a valuation for it, we rather use terms (resp. formulas) with parameters, that is, terms (resp. formulas) where free variables are replaced with their assignment through 𝑣. The value |𝑡 | in N of a closed term with parameters 𝑡 is defined using the standard interpretations of 𝑆, + and × in N. Proof. The proof is by induction on 𝑡, using that 0 † = 0, 𝑆 𝑡 † = 𝑡 † + 1 and the following facts:

𝑡 † + 𝑢 † = 𝑡 † + 𝑢 † 𝑡 † × 𝑢 † = 𝑡 † × 𝑢 † □
We are now ready to define the realizability value associated to each formula with parameters. The whole realizability semantics is parameterized by a set ⊥ ⊥ ⊆ N that will be the set of realizers of the formula ⊥. Allowing for a non-empty set of realizers of ⊥ is a well-known technique for keeping computational content from classical proofs. Indeed, if ⊥ has no realizers then for any formula 𝐴, either 𝐴 has realizers, in which case ¬𝐴 has no realizer, or 𝐴 has no realizer, in which case everything is a realizer of ¬𝐴. Therefore ¬¬𝐴 has no computational content and we cannot hope to get anything interesting when eliminating double negation on it.

For each closed formula with parameters 𝐴 we define the realizability value |𝐴| ⊆ 𝐴 † of 𝐴 on 𝐴 † as follows:

|𝑋 (𝑡)| = N if |𝑡 | ∈ 𝑋 ⊥ ⊥ if |𝑡 | ∉ 𝑋 |𝐴 ⇒ 𝐵| = |𝐴| → |𝐵| |∀𝑥 𝐴| = 𝑥 ∈N ({𝑥 } → |𝐴|) |∀𝑋 𝐴| = 𝑋 ⊆N |𝐴|

Adequacy

We now prove the main result of our realizability interpretation.

The adequacy theorem asserts that the program interpreting a given proof belongs to the realizability value of the formula proven.

Theorem 4.8. For each proof in second-order arithmetic:

𝑝 1 : 𝐴 1 , . . . , 𝑝 𝑛 : 𝐴 𝑛 ⊢ 𝜋 : 𝐴 such that 𝐹𝑉 (𝐴 1 , . . . , 𝐴 𝑛 , 𝐴) ⊆ {𝑥 1 , . . . , 𝑥 𝑚 , 𝑋 1 , . . . , 𝑋 𝑘 }, if: (𝑥 1 , . . . , 𝑥 𝑚 ) ∈ N 𝑚 (𝑋 1 , . . . , 𝑋 𝑘 ) ∈ (P (N)) 𝑘 (𝑎 1 , . . . , 𝑎 𝑛 ) ∈ |𝐴 1 | × . . . × |𝐴 𝑛 | then: 𝜋 † [𝑎 1 , . . . , 𝑎 𝑛 /𝑝 1 , . . . , 𝑝 𝑛 ] ∈ |𝐴|
The proof of this theorem proceeds by induction on 𝜋. We split it into three parts: adequacy for the axioms, adequacy for the firstorder intuitionistic part, and adequacy for the 𝐷𝑛𝑒 and ∀2𝑒 rules.

Adequacy for the axioms. In the case of axioms, the correctness of our interpretation is mostly straightforward. As usual, we use recursion on natural numbers to interpret induction. Lemma 4.9. If 𝜋 : 𝐴 is an axiom of second-order arithmetic then:

𝜋 † ∈ |𝐴|
Proof. By cases. For axioms add0, addS, mul0 and mulS, this is a consequence of the fact that if 𝑡 and 𝑢 are terms with parameters such that

|𝑡 | = |𝑢 |, then 𝜆𝑝.𝑝 ∈ |𝑡 = 𝑢 |. Indeed, if |𝑡 | = |𝑢 | then for all 𝑋 ⊆ N, |𝑋 (𝑡)| = |𝑋 (𝑢)|, so |𝑡 = 𝑢 | = |∀𝑋 (𝑋 ⇒ 𝑋 )| = ⊥ ⊥ → ⊥ ⊥.
For sinj, let 𝑥, 𝑦 ∈ N. Adequacy for the first-order intuitionistic part. We now prove adequacy for the system without the 𝐷𝑛𝑒 and ∀2𝑒 rules. As for the axioms, this result is straightforward. Lemma 4.10. For each proof in second-order arithmetic without the 𝐷𝑛𝑒 and ∀2𝑒 rules:

If 𝑥 = 𝑦 then |𝑆 𝑥 = 𝑆 𝑦| = ⊥ ⊥ → ⊥ ⊥ = |𝑥 = 𝑦|, so 𝜆𝑝.𝑝 ∈ |𝑆 𝑥 = 𝑆 𝑦 ⇒ 𝑥 = 𝑦|. If 𝑥 ≠ 𝑦 then there exists 𝑋 ⊆ N such that 𝑥 ∈ 𝑋 but 𝑦 ∉ 𝑋 , so |𝑥 = 𝑦| = N → ⊥ ⊥.
exf 𝐵 † ∈ ⊥ ⊥ → |𝐵 [𝑡/𝑥]| = |𝑋 (𝑡) ⇒ 𝐵 [𝑡/𝑥]| 𝑏 ∈ |𝐵 [𝑡/𝑥]| → ⊥ ⊥ = |𝐵 [𝑡/𝑥] ⇒ 𝑋 (𝑡)|
The cases 𝑌 (𝑡) for 𝑌 ≠ 𝑋 , 𝐴 □

We now give an intuition about the computational behavior of our interpretation of the ∀2𝑒 rule.

The first argument that we give to update recursion for realizing the ∀2𝑒 rule is some:

𝑎 ∈ 𝑥 ∈N ({𝑥 } → |𝐵| + |¬𝐵|) → |⊥|
This realizer is built from the inductively defined 𝜑 can be understood as a "current knowledge" about the 𝑛s at which we have a realizer of 𝐵 (𝑛). For a given 𝑓 , if 𝑓 𝑛 is some {𝑏 | } then the "current knowledge" is that 𝑏 is a realizer for 𝐵 (𝑛). Otherwise if 𝑓 𝑛 is { | ★} then we know nothing about 𝐵 (𝑛) yet. At the beginning of the computation we have no information at all so the second argument is the "empty knowledge" 𝜖.

Update recursion then has to provide 𝑎 with some realizer of 𝑥 ∈N ({𝑥 } → |𝐵| + |¬𝐵|), that is, a "perfect knowledge" that provides for each 𝑛 either a realizer of 𝐵 (𝑛), or a realizer of ¬𝐵 (𝑛). The way it approximates such a perfect knowledge is as follows: if 𝑛 is such that 𝑓 𝑛 = {𝑏 | } for some 𝑏 ∈ |𝐵 (𝑛)|, then the "current knowledge" already contains a realizer for 𝐵 (𝑛), so update recursion can simply return it. Otherwise, update recursion has to provide either a realizer of 𝐵 (𝑛), or a realizer of ¬𝐵 (𝑛). At that point update recursion chooses to build a realizer of ¬𝐵 (𝑛) by reading from 𝑎 a realizer 𝑏 of 𝐵 (𝑛) and making a recursive call with an extended knowledge that contains 𝑏 as a realizer of 𝐵 (𝑛). Inside the recursive call, if 𝑎 reads again its input at point 𝑛 then update recursion will use the new current knowledge and answer with this same 𝑏 that 𝑎 provided before the recursive call.

This recursive process will eventually stop at some point because 𝑎 being continuous, it can only look at the "current knowledge" at a finite number of points.

Extraction

The adequacy theorem gives us the possibility of extracting programs from proofs in second-order arithmetic, as witnessed by the following extraction theorem:

CONCLUSION AND FUTURE WORKS

We have defined a bar recursive interpretation of second-order arithmetic presented as arithmetic with quantification on predicates rather than the equivalent axiom scheme of comprehension. This presentation of second-order arithmetic is the one that most closely reflects the typing rules of polymorphic 𝜆-calculus, and as such we made a step towards a comparison of the two families of interpretations of second-order arithmetic: bar recursion and system F. As a future work we would like to deepen the understanding of the connection between these two principles by comparing the computational behavior of programs extracted from a single proof via the two techniques.

Another aspect that we would like to study is wether it is possible to use control operators in the interpretation of the ∀2𝑒 rule. Indeed, there is a strong connection between the negative translation of proofs and the continuation-passing style (cps) translation of programs, the latter being the Curry-Howard equivalent of the former. Calculi with control features have been designed to interpret classical proofs directly. Most of these calculi contain a notion of duality that corresponds on the logical side to the duality between a formula and its negation, and on the computational side to a call-by-name or a call-by-value evaluation strategy. During the computation of an approximation to the "perfect knowledge" mentioned in the previous section, update recursion has an asymmetric behavior that consists in building a realizer of ¬𝐵 by reading a realizer of 𝐵 and making a recursive call with a new knowledge extended with this new realizer. This behavior corresponds to the call-by-name interpretation of the excluded middle under a cps translation. We would therefore like to have a version of update recursion that uses control operators and can be translated either to the current version through a call-by-name cps translation, or to a dual version through a call-by-value cps translation. Moreover, control operators can capture context and restore it at a later point. We would like to explore the possibility of using this property to define more intuitive versions of our 𝜑 1 and 𝜑 2 that could act on all instances of 𝑋 (𝑡) in a formula through context capture.

  If 𝑎 ∈ 𝐴 and 𝑏 ∈ 𝐵 we write {𝑎 | } ∈ 𝐴 ⊎ 𝐵 and { | 𝑏} ∈ 𝐴 ⊎ 𝐵. Similarly we write {𝐴 | } = {{𝑎 | } | 𝑎 ∈ 𝐴} and { | 𝐵} = {{ | 𝑏} | 𝑏 ∈ 𝐵}. Each program 𝑥 1 : 𝜎 1 , . . . , 𝑥 𝑛 : 𝜎 𝑛 ⊢ 𝑀 : 𝜎 is interpreted as a continuous function [𝑀] from [𝜎 1 ] × . . . [𝜎 𝑛 ] (equipped with the componentwise ordering) to [𝜎] as described in figure 4.

Proposition 3 . 6 .

 36 If 𝑀 ⇝ 𝑁 then [𝑀] = [𝑁 ].

Proposition 3 . 7 .

 37 If 𝑀 : 𝜄 and 𝑁 : 1 are closed programs such that [𝑀] = 𝑛 for some 𝑛 ∈ N and [𝑁 ] = ★, then 𝑀 ⇝ * 𝑛 and 𝑁 ⇝ * ★.

Definition 4 . 1 .

 41 A realizability value A on a type 𝜎 is a subset of its interpretation [𝜎]. We define for each realizability values A on 𝜎 and B on 𝜏 the following realizability values on 𝜎 → 𝜏 and 𝜎 + 𝜏:

Proposition 4 . 3 .

 43 Let (A 𝑛 ) 𝑛∈N be a family of realizability values on 𝜎 and let B ⊆ N. Then:

  and therefore 𝑓 𝐼 0 (𝑛) = 𝑓 (𝑛) if ⋎𝐹 (𝑛) = { | ★} then 𝑓 (𝑛) = { | ★} by definition of ⋎𝐹 since 𝑓 ∈ 𝐹 , and therefore 𝑓 𝐼 0 (𝑛) = 𝑓 (𝑛) therefore 𝑓 𝐼 0 ≤ 𝑓 and ur 𝑎 ⋎𝐹 = ur 𝑎 𝑓 𝐼 0 ≤ ur 𝑎 𝑓 by monotonicity of ur 𝑎. But ur 𝑎 ⋎𝐹 ∈ B so ur 𝑎 ⋎𝐹 ≠ ⊥, which means that ur 𝑎 𝑓 = ur 𝑎 ⋎𝐹 ∈ B, contradicting 𝐹 ⊆ 𝐸. (𝐸, ≼) has no maximal element. Suppose for the sake of contradiction that 𝑓 is a maximal element of 𝐸. Then ur 𝑎 𝑓 ∉ B, so by lemma 3.5: 𝑎(𝜆𝑥 .𝑓 𝑥 ? + (𝜆𝑦. {𝑦 | }) (𝜆_. { | 𝜆𝑦.ur 𝑎 (𝑓 ⟨𝑥 ↦ → 𝑦⟩))}) = ur 𝑎 𝑓 ∉ B but then by hypothesis on 𝑎 we have: 𝜆𝑥 .𝑓 𝑥 ? + (𝜆𝑦. {𝑦 | }) (𝜆_. { | 𝜆𝑦.ur 𝑎 (𝑓 ⟨𝑥 ↦ → 𝑦⟩))} ∉ 𝑛∈N ({𝑛} → A 𝑛 + (A 𝑛 → B)) so there exists 𝑛 ∈ N such that: 𝑓 𝑛 ? + (𝜆𝑦. {𝑦 | }) (𝜆_. { | 𝜆𝑦.ur 𝑎 (𝑓 ⟨𝑛 ↦ → 𝑦⟩))} ∉ A 𝑛 + (A 𝑛 → B) Since 𝑓 𝑛 ∈ A 𝑛 + {★}, either there exists 𝑏 ∈ A 𝑛 such that 𝑓 𝑛 = {𝑏 | }, or 𝑓 𝑛 = { | ★}. In the first case, we obtain {𝑏 | } ∉ A 𝑛 + (A 𝑛 → B), which is a contradiction. Therefore 𝑓 𝑛 = { | ★} and we have: { | 𝜆𝑦.ur 𝑎 (𝑓 ⟨𝑛 ↦ → 𝑦⟩)} ∉ A 𝑛 + (A 𝑛 → B) so there exists 𝑏 ∈ A 𝑛 such that ur 𝑎 (𝑓 ⟨𝑛 ↦ → 𝑏⟩) ∉ B and then 𝑓 ⟨𝑛 ↦ → 𝑏⟩ ∈ 𝐸. But 𝑓 ≼ 𝑓 ⟨𝑛 ↦ → 𝑏⟩ and 𝑓 ⟨𝑛 ↦ → 𝑏⟩ 𝑛 = {𝑏 | } by 3.4, so since 𝑓 𝑛 = { | ★} we also have 𝑓 ⟨𝑛 ↦ → 𝑏⟩ 𝑓 , contradicting the maximality of 𝑓 in 𝐸. □

Lemma 4 . 4 .

 44 For every type 𝜎, there exists 𝑀 such that [𝑀] ∈ |𝜎 | and every such 𝑀 reduces to a normal form. Proof. We prove the results by induction on 𝜎. We have [0] ∈ |𝜄| and [★] ∈ |1|. If we have [𝑀] ∈ |𝜏 | then [𝜆_.𝑀] ∈ |𝜎 → 𝜏 | and [{ | 𝑀 }] ∈ |𝜎 + 𝜏 |. Normalization on |𝜄| and |1| is a consequence of computational adequacy (proposition 3.7). If we have [𝑀] ∈ |𝜎 → 𝜏 | but 𝑀 diverges, then for 𝑁 such that [𝑁 ] ∈ |𝜎 | ≠ ∅, 𝑀 𝑁 diverges as well, contradicting the induction hypothesis on 𝜏. If we have [𝑀] ∈ |𝜎 + 𝜏 | but 𝑀 diverges, then 𝑀 ? + (𝜆_.★) (𝜆_.★) diverges as well, but since |𝜎 + 𝜏 | = {|𝜎 | | } ∪ { | |𝜏 |}, we have [𝑀 ? + (𝜆_.★) (𝜆_.★)] = ★ ∈ |1|, contradicting computational adequacy.

Theorem 4 . 5 .

 45 For each typing derivation: 𝑥 1 : 𝜎 1 , . . . , 𝑥 𝑛 : 𝜎 𝑛 ⊢ 𝑀 : 𝜏 if: (𝑎 1 , . . . , 𝑎 𝑛 ) ∈ |𝜎 1 | × . . . × |𝜎 𝑛 | then: 𝑀 [𝑎 1 , . . . , 𝑎 𝑛 /𝑥 1 , . . . , 𝑥 𝑛 ] ∈ |𝜏 | Proof. The proof proceeds by induction on the structure of 𝑀. The cases 𝑥, 𝜆𝑥 .𝑀, 𝑀 𝑁 , 𝑛, S 𝑀, {𝑀 | }, { | 𝑀 }, and ★ are straightforward. For recursion, let 𝑀 : 𝜄 be such that [𝑀] ∈ |𝜄| = N, and let 𝑎 ∈ |𝜎 | and 𝑏 ∈ |𝜄 → 𝜎 → 𝜎 |. We define 𝑑 0 = 𝑎 and 𝑑 𝑛+1 = 𝑏 (𝑛) (𝑑 𝑛 ) and prove by induction on 𝑛 ∈ N that 𝑑 𝑛 ∈ |𝜎 |. Indeed, 𝑑 0 = 𝑎 ∈ |𝜎 | and 𝑑 𝑛+1 = 𝑏 (𝑛) (𝑑 𝑛 ) ∈ |𝜎 | since 𝑛 ∈ |𝜄| and 𝑑 𝑛 ∈ |𝜎 | by induction hypothesis. For case analysis, let 𝑀 : 𝜎 + 𝜏 be such that [𝑀] ∈ |𝜎 + 𝜏 | = |𝜎 | + |𝜏 | and let 𝑏 1 ∈ |𝜎 → 𝜈 | and 𝑏 2 ∈ |𝜏 → 𝜈 |. If [𝑀] ∈ {|𝜎 | | } then there exists 𝑐 ∈ |𝜎 | such that [𝑀] = {𝑐 | } and therefore we get [𝑀 ? + ] (𝑏 1 ) (𝑏 2 ) = 𝑏 1 (𝑐) ∈ |𝜈 |, and if [𝑀] ∈ { | |𝜏 |} then there exists 𝑐 ∈ |𝜏 | such that [𝑀] = { | 𝑐} and therefore we get [𝑀 ? + ] (𝑏 1 ) (𝑏 2 ) = 𝑏 2 (𝑐) ∈ |𝜈 |. Finally, for update recursion, this is a consequence of 4.3 with A 𝑛 = |𝜎 | and B = |𝜄| = N, since by lemma 4.2:

Lemma 4 . 7 .

 47 If 𝑡 is a closed term with parameters, then 𝑡 † = |𝑡 |.

  Similarly, |𝑆 𝑥 = 𝑆 𝑦| = N → ⊥ ⊥, and therefore 𝜆𝑝.𝑝 ∈ |𝑆 𝑥 = 𝑆 𝑦 ⇒ 𝑥 = 𝑦|. For sn0, let 𝑥 ∈ N. Since |𝑆 𝑥 | = 𝑥 + 1 ≠ 0, we have as before |𝑆 𝑥 = 0| = N → ⊥ ⊥ and so |𝑆 𝑥 ≠ 0| = (N → ⊥ ⊥) → ⊥ ⊥. We then obtain 𝜆𝑝.𝑝 0 ∈ |𝑆 𝑥 ≠ 0|. For ind, let 𝑋 ⊆ N, 𝑎 ∈ |𝑋 (0)| and 𝑏 ∈ |∀𝑥 (𝑋 (𝑥) ⇒ 𝑋 (𝑆 𝑥))|. We prove by induction that for all 𝑥 ∈ N, 𝑥 ? 𝜄 𝑎 𝑏 ∈ |𝑋 (𝑥)|. Indeed, 0 ? 𝜄 𝑎 𝑏 = 𝑎 ∈ |𝑋 (0)| and if 𝑥 ? 𝜄 𝑎 𝑏 ∈ |𝑋 (𝑥)| then 𝑥 + 1 ? 𝜄 𝑎 𝑏 = 𝑏 𝑥 (𝑥 ? 𝜄 𝑎 𝑏) ∈ |𝑋 (𝑥 + 1)| since 𝑥 ? 𝜄 𝑎 𝑏 ∈ |𝑋 (𝑥)| by induction hypothesis.□

Figure 5 :

 5 Figure 5: Realizability interpretation of second-order arithmetic

𝑝 1 :

 1 𝐴 1 , . . . , 𝑝 𝑛 : 𝐴 𝑛 ⊢ 𝜋 : 𝐴 such that 𝐹𝑉 (𝐴 1 , . . . , 𝐴 𝑛 , 𝐴) ⊆ {𝑥 1 , . . . , 𝑥 𝑚 , 𝑋 1 , . . . , 𝑋 𝑘 }, if:(𝑥 1 , . . . , 𝑥 𝑚 ) ∈ N 𝑚 (𝑋 1 , . . . , 𝑋 𝑘 ) ∈ (P (N)) 𝑘 (𝑎 1 , . . . , 𝑎 𝑛 ) ∈ |𝐴 1 | × . . . × |𝐴 𝑛 | then: 𝜋 † [𝑎 1 , . . . , 𝑎 𝑛 /𝑝 1 , . . . , 𝑝 𝑛 ] ∈ |𝐴|Proof. The proof is by induction on 𝜋. Most of the cases are straightforward. For the ∀𝑒 rule we use lemma 4.7.□Adequacy for the 𝐷𝑛𝑒 and ∀2𝑒 rules. This section contains the main result: correctness of our interpretation of second-order elimination. First, we prove adequacy for double-negation elimination: Lemma 4.11. For each formula 𝐴 with parameters:dne 𝐴 † ∈ |¬¬𝐴 ⇒ 𝐴| exf 𝐴 † ∈ |⊥ ⇒ 𝐴|Proof. We proceed by induction on the structure of 𝐴 for dne 𝐴 † . For 𝑋 (𝑡), let 𝑎 ∈ |¬¬𝑋 (𝑡)|. If |𝑡 | ∈ 𝑋 then |𝑋 (𝑡)| = N, so we have dne 𝑋 (𝑡 ) † (𝑎) ∈ |𝑋 (𝑡)|. If |𝑡 | ∉ 𝑋 , then |𝑋 (𝑡)| = ⊥ ⊥ so we have 𝑎 ∈ (⊥ ⊥ → ⊥ ⊥) → ⊥ ⊥ and therefore: dne 𝑋 (𝑡 ) † (𝑎) = 𝑎 (𝜆𝑝.𝑝) ∈ ⊥ ⊥ = |𝑋 (𝑡)| 𝐴 ⇒ 𝐵 and ∀𝑥 𝐴 are consequences of lemma 4.10. For ∀𝑋 𝐴, let 𝑎 ∈ |¬¬∀𝑋 𝐴| and let 𝑋 ⊆ N. Then we have that |∀𝑋 𝐴| = 𝑋 ⊆N |𝐴| ⊆ |𝐴|, so by property of → with respect to inclusion, |¬¬∀𝑋 𝐴| ⊆ |¬¬𝐴|, so 𝑎 ∈ |¬¬𝐴| and therefore: dne (∀𝑋 𝐴) † 𝑎 = dne 𝐴 † 𝑎 ∈ |𝐴| For exf 𝐴 † , if 𝑎 ∈ |⊥| then 𝜆_.𝑎 ∈ |¬¬𝐴| by lemma 4.10 and therefore exf 𝐴 † (𝑎) = dne 𝐴 † (𝜆_.𝑎) ∈ |𝐴|. □ Before proving adequacy for the ∀2𝑒 rule, we prove the following lemma about our inductively defined 𝜑 1 and 𝜑 2 : Lemma 4.12. If: 𝑎 ∈ 𝑥 ∈N ({𝑥 } → |𝐵| + |¬𝐵|) 𝑋 = {𝑥 ∈ N | 𝑎 𝑥 ∈ {|𝐵| | }} then: 𝜑 1 𝐴,𝐵,𝑋 [𝑎/𝑟 ] ∈ |𝐴 ⇒ 𝐴 [𝑥 .𝐵/𝑋 ]| 𝜑 2 𝐴,𝐵,𝑋 [𝑎/𝑟 ] ∈ |𝐴 [𝑥 .𝐵/𝑋 ] ⇒ 𝐴| Proof. We proceed by induction on 𝐴. In the 𝑋 (𝑡) case we need to prove: 𝑎 𝑡 † ? + (𝜆𝑞𝑝.𝑞) 𝜆𝑞.exf 𝐵 † ∈ |𝑋 (𝑡) ⇒ 𝐵 [𝑡/𝑥]| 𝑎 𝑡 † ? + (𝜆𝑞𝑝.0) (𝜆𝑞.𝑞) ∈ |𝐵 [𝑡/𝑥] ⇒ 𝑋 (𝑡)| If 𝑎 𝑡 † = {𝑏 | } for some 𝑏 ∈ |𝐵 [𝑡/𝑥]| then |𝑋 (𝑡)| = N by definition of 𝑋 and lemma 4.7, so: 𝜆𝑝.𝑏 ∈ N → |𝐵 [𝑡/𝑥]| = |𝑋 (𝑡) ⇒ 𝐵 [𝑡/𝑥]| 𝜆𝑝.0 ∈ |𝐵 [𝑡/𝑥]| → N = |𝐵 [𝑡/𝑥] ⇒ 𝑋 (𝑡)| If 𝑎 𝑡 † = { | 𝑏} for some 𝑏 ∈ |¬𝐵 [𝑡/𝑥]| then |𝑋 (𝑡)| = ⊥ ⊥ by definition of 𝑋 and lemma 4.7, so:

Theorem 4 . 14 .

 414 Each proof in second-order arithmetic of a closed formula of the form ∀𝑥∀𝑋 (∀𝑦 (𝑡 = 0 ⇒ 𝑋 ) ⇒ 𝑋 ) (which is the usual second-order encoding of ∀𝑥∃𝑦 𝑡 = 0) can be extracted to a program 𝑀 : 𝜄 → 𝜄 such that for all 𝑥 ∈ N there exists 𝑦 ∈ N such that 𝑀 𝑥 ⇝ * 𝑦 with |𝑡 | = 0. Proof. Let 𝜋 be a proof of ∀𝑥∃𝑦 𝑡 = 0. The adequacy lemma gives us for each 𝑥 ∈ N, 𝜋 † 𝑥 ∈ |∀𝑦 (𝑡 = 0 ⇒ ∅) ⇒ ∅|. Fix now: ⊥ ⊥ = {𝑦 ∈ N | |𝑡 | = 0} We now prove that 𝜆𝑦𝑝.𝑝 𝑦 ∈ |∀𝑦 (𝑡 = 0 ⇒ ∅)|. Let 𝑦 ∈ N and let 𝑎 ∈ |𝑡 = 0| = |∀𝑌 (𝑌 (𝑡) ⇒ 𝑌 (0))|. In particular for 𝑌 = N\ {0}, 𝑎 ∈ |𝑌 (𝑡)| → ⊥ ⊥. There are two cases: • If |𝑡 | = 0, then 𝑦 ∈ ⊥ ⊥ = |𝑌 (𝑡)| by definition of ⊥ ⊥, • if |𝑡 | ≠ 0 then |𝑌 (𝑡)| = N so 𝑦 ∈ |𝑌 (𝑡)|. In both cases 𝑎 𝑦 ∈ ⊥ ⊥. Therefore we get: 𝜆𝑦𝑝.𝑝 𝑦 ∈ |∀𝑦 (𝑡 = 0 ⇒ ∅)| so: 𝜋 † 𝑥 (𝜆𝑦𝑝.𝑝 𝑦) ∈ ⊥ ⊥ = {𝑦 ∈ N | |𝑡 | = 0} We can therefore define: 𝑀 = 𝜆𝑥 .𝜋 † 𝑥 (𝜆𝑦𝑝.𝑝 𝑦) and we have by proposition 3.7 that for all 𝑥 ∈ N there exists 𝑦 ∈ N such that 𝑀 𝑥 ⇝ * 𝑦 and |𝑡 | = 0. □

  𝑝 𝑛 : 𝐴 𝑛 ⊢ 𝜋 : 𝐴 is interpreted as a program 𝜋 † which typing derivation's conclusion is of the form:

ì 𝑥 : 𝜄, 𝑝 1 : 𝐴 † 1 , . . . , 𝑝 𝑛 : 𝐴 † 𝑛 ⊢ 𝜋 † : 𝐴 † where ì

  𝑝 † ≡ 𝑝 (𝜆𝑝.𝜋) † ≡ 𝜆𝑝.𝜋 † (𝜋 1 𝜋 2 ) † ≡ 𝜋 † 1 𝜋 † 2 (𝜆𝑥 .𝜋) † ≡ 𝜆𝑥 .𝜋 † (𝜋 𝑡) † ≡ 𝜋 † 𝑡 † (𝜆𝑋 .𝜋) † ≡ 𝜋 † (dne 𝐴 ) † ≡ dne 𝐴 † where ⊢ dne 𝜎 : ((𝜎 → 𝜄) → 𝜄) → 𝜎 is defined by: dne 𝜄 ≡ 𝜆𝑝.𝑝 (𝜆𝑞.𝑞) dne 𝜎→𝜏 ≡ 𝜆𝑝𝑞.dne 𝜏 (𝜆𝑟 .𝑝 (𝜆𝑠.𝑟 (𝑠 𝑞))) (𝜋 (𝑥 .𝐵)) † ≡ dne (𝐴[𝑥 .𝐵/𝑋 ] ) † 𝜆𝑝.ur 𝜆𝑟 .𝑝 𝜑 1 𝐴,𝐵,𝑋 𝜋 † 𝜖 where for ì 𝑥 = 𝐹𝑉 (𝐴), ì 𝑥 : ì 𝜄, 𝑟 : 𝜄 → 𝐵 † + 𝐵 † → 𝜄 ⊢ 𝜑 1 𝐴,𝑥 .𝐵,𝑋 : 𝐴 † → (𝐴 [𝑥 .𝐵/𝑋 ]) † ì 𝑥 : ì 𝜄, 𝑟 : 𝜄 → 𝐵 † + 𝐵 † → 𝜄 ⊢ 𝜑 2 𝐴,𝑥 .𝐵,𝑋 : (𝐴 [𝑥 .𝐵/𝑋 ]) † → 𝐴 † 𝑋 (𝑡 ),𝑥 .𝐵,𝑋 ≡ 𝑟 𝑡 † ? + (𝜆𝑞𝑝.𝑞) 𝜆𝑞.exf 𝐵 † 𝜑 2 𝑋 (𝑡 ),𝑥 .𝐵,𝑋 ≡ 𝑟 𝑡 † ? + (𝜆𝑞𝑝.0) (𝜆𝑞.𝑞) ⇒𝐴 2 ,𝑥 .𝐵,𝑋 ≡ 𝜆𝑝𝑞.𝜑 1 𝐴 2 ,𝑥 .𝐵,𝑋 𝑝 𝜑 2 𝐴 2 ,𝑥 .𝐵,𝑋 𝑞 𝜑 2 𝐴 1 ⇒𝐴 2 ,𝑥 .𝐵,𝑋 ≡ 𝜆𝑝𝑞.𝜑 2 𝐴 2 ,𝑥 .𝐵,𝑋 𝑝 𝜑 1 𝐴 2 ,𝑥 .𝐵,𝑋 𝑞 ⊢ exf 𝜎 : 𝜄 → 𝜎 exf 𝜎 ≡ 𝜆𝑝.dne 𝜎 (𝜆_.𝑝) add0 † ≡ 𝜆𝑥𝑝.𝑝 addS † ≡ 𝜆𝑥𝑦𝑝.𝑝 mul0 † ≡ 𝜆𝑥𝑝.𝑝 mulS † ≡ 𝜆𝑥𝑦𝑝.𝑝 sn0 † ≡ 𝜆𝑥𝑝.𝑝 0 sinj † ≡ 𝜆𝑥𝑦𝑝.𝑝 ind † ≡ 𝜆𝑝𝑞𝑥 .𝑥 ? 𝜄 𝑝 𝑞

				are defined by:
	𝜑 1	𝜑 1 𝑌 (𝑡 ),𝑥 .𝐵,𝑋 ≡ 𝜆𝑝.𝑝	𝜑 1 ∀𝑦 𝐴,𝑥 .𝐵,𝑋 ≡ 𝜆𝑝𝑦.𝜑 1 𝐴,𝐵,𝑋 (𝑝 𝑦)	𝜑 1 ∀𝑌 𝐴,𝑥 .𝐵,𝑋 ≡ 𝜑 1 𝐴,𝐵,𝑋
		𝜑 2 𝑌 (𝑡 ),𝑥 .𝐵,𝑋 ≡ 𝜆𝑝.𝑝	𝜑 2 ∀𝑦 𝐴,𝑥 .𝐵,𝑋 ≡ 𝜆𝑝𝑦.𝜑 2 𝐴,𝐵,𝑋 (𝑝 𝑦)	𝜑 2 ∀𝑌 𝐴,𝑥 .𝐵,𝑋 ≡ 𝜑 2 𝐴,𝐵,𝑋
		if 𝑌 ≠ 𝑋
	𝜑 1 𝐴 1

  1 ⇒ 𝐵 2 and ∀𝑦 𝐴 are consequences of 4.10, and the case ∀𝑌 𝐴 is a consequence of:|∀𝑌 (𝐶 ⇒ 𝐷)| ⊆ |∀𝑌 𝐶 ⇒ ∀𝑌 𝐷 | □Finally, we prove adequacy for the ∀2𝑒 rule: Proposition 4.13. For each proof in second-order arithmetic without the ∀2𝑒 rule:𝑝 1 : 𝐴 1 , . . . , 𝑝 𝑛 : 𝐴 𝑛 ⊢ 𝜋 : ∀𝑋 𝐴 such that 𝐹𝑉 (𝐴 1 , . . . , 𝐴 𝑛 , ∀𝑋 𝐴) ⊆ {𝑥 1 , . . . , 𝑥 𝑚 , 𝑋 1 , . . . , 𝑋 𝑘 }, if: (𝑥 1 , . . . , 𝑥 𝑚 ) ∈ N 𝑚(𝑋 1 , . . . , 𝑋 𝑘 ) ∈ (P (N)) 𝑘 (𝑎 1 , . . . , 𝑎 𝑛 ) ∈ |𝐴 1 | × . . . × |𝐴 𝑛 | † [𝑎 1 , . . . , 𝑎 𝑛 /𝑝 1 , . . . , 𝑝 𝑛 ] ∈ |𝐴 [𝑥 .𝐵/𝑋 ]| Proof. Let 𝑀 = 𝜋 † [𝑎 1 , . . . , 𝑎 𝑛 /𝑝 1 , . . . , 𝑝 𝑛 ] ∈ |∀𝑋 𝐴| and let 𝑎 ∈ |¬𝐴 [𝑥 .𝐵/𝑋 ] |. We have to prove: ur 𝜆𝑟 .𝑎 𝜑 1 𝐴,𝐵,𝑋 𝑀 𝜖 ∈ |⊥| We apply proposition 4.3 with A 𝑛 = |𝐵 [𝑛/𝑥]| and B = |⊥| so we have to prove: This second property is immediate since for all 𝑛 ∈ N, 𝜖 𝑛 = { | ★} by proposition 3.4. For the first property, let: and 𝑀 ∈ |∀𝑋 𝐴| ⊆ |𝐴 [{𝑥 ∈ N | 𝑏 𝑥 ∈ {𝐵 | }} /𝑋 ]|.

	then:
	(𝜋 (𝑥 .𝐵)) 𝜆𝑟 .𝑎 𝜑 1 𝐴,𝐵,𝑋 𝑀 ∈	({𝑥 } → |𝐵| + |¬𝐵|) → |⊥|
	𝑥 ∈N
	𝜖 ∈	({𝑥 } → |𝐵| + {★})
	𝑥 ∈N
	𝑏 ∈	({𝑥 } → |𝐵| + |¬𝐵|)
	𝑥 ∈N
	so we are left to prove 𝑎 𝜑 1 𝐴,𝐵,𝑋 [𝑏/𝑟 ] 𝑀 ∈ |⊥|, and since we have
	𝑎 ∈ |¬𝐴 [𝑥 .𝐵/𝑋 ] | it suffices to prove:
		({𝑥 } → |𝐵| + |¬𝐵|)
	𝑥 ∈N

𝜑 1 𝐴,𝐵,𝑋 [𝑏/𝑟 ] 𝑀 ∈ |𝐴 [𝑥 .𝐵/𝑋 ]| which is a consequence of lemma 4.12 since: 𝑏 ∈

  1 𝐴,𝑥 .𝐵,𝑋 and 𝜑 2 𝐴,𝑥 .𝐵,𝑋 and goes down in the structure of 𝐴 to find every occurence of 𝑋 (𝑡) for some term 𝑡. For each such occurence, 𝑎 replaces 𝑋 (𝑡) with 𝐵 [𝑡/𝑥] depending on its input at point 𝑡 † , and on whether 𝑋 (𝑡) occurs positively (𝜑 1 ) or negatively (𝜑 2 ) in 𝐴: • if the input of 𝑎 at point 𝑡 † is some {𝑏 | } then: if 𝑋 (𝑡) occurs positively then 𝑎 uses 𝜆_.𝑏 as a realizer of ⊤ ⇒ 𝐵 [𝑡/𝑥] if 𝑋 (𝑡) occurs negatively then 𝑎 uses a trivial realizer of 𝐵 [𝑡/𝑥] ⇒ ⊤ • if the input of 𝑎 at point 𝑡 † is some { | 𝑏} then: if 𝑋 (𝑡) occurs positively then 𝑎 uses exf 𝐵 † as a realizer of ⊥ ⇒ 𝐵 [𝑡/𝑥] if 𝑋 (𝑡) occurs negatively then 𝑎 uses 𝑏 as a realizer of 𝐵 [𝑡/𝑥] ⇒ ⊥ We now explain the meaning of the second argument of update recursion, on which recursion happens. Each partial function:

	𝑓 ∈	({𝑥 } → |𝐵| + {★})
	𝑥 ∈N

𝜓 𝑀 𝑁 = 𝑀 𝑁 (𝜆𝑥𝑦.𝑁 𝑥 ? + (𝜆_.0) (𝜆_.𝜓 𝑀 (𝑁 ⟨𝑥 ↦ → 𝑦⟩))) Berger's version and ours are however interdefinable: ur 𝑀 = 𝜓 (𝜆𝑢𝑣.𝑀 (𝜆𝑥 .𝑢 𝑥 ? + (𝜆𝑦. {𝑦 | }) (𝜆_. { | 𝑣 𝑥 }))) 𝜓 𝑀 = ur(𝜆𝑢.𝑀 (𝜆𝑥 .𝑢 𝑥 ? + (𝜆𝑦. {𝑦 | }) (𝜆_. { | ★})) (𝜆𝑥 .𝑢 𝑥 ? + (𝜆__.0) (𝜆𝑣.𝑣))) LICS '22, August 2-5, 2022, Haifa, Israel Valentin BlotΓ ⊢ sn0 : ∀𝑥 (𝑆 𝑥 ≠ 0) Γ ⊢ add0 : ∀𝑥 (𝑥 + 0 = 𝑥) Γ ⊢ mul0 : ∀𝑥 (𝑥 × 0 = 0) Γ ⊢ sinj : ∀𝑥∀𝑦 (𝑆 𝑥 = 𝑆 𝑦 ⇒ 𝑥 = 𝑦) Γ ⊢ addS : ∀𝑥∀𝑦 (𝑥 + 𝑆 𝑦 = 𝑆 (𝑥 + 𝑦)) Γ ⊢ mulS : ∀𝑥∀𝑦 (𝑥 × 𝑆 𝑦 = 𝑥 + 𝑥 × 𝑦) Γ ⊢ ind : ∀𝑋 (𝑋 (0) ⇒ ∀𝑥 (𝑋 (𝑥) ⇒ 𝑋 (𝑆 𝑥)) ⇒ ∀𝑥 𝑋 (𝑥))axioms of second-order arithmetic𝐴𝑥 (𝑝:𝐴) ∈Γ Γ ⊢ 𝑝 : 𝐴 𝐷𝑛𝑒 Γ ⊢ dne 𝐴 : ¬¬𝐴 ⇒ 𝐴 Γ, 𝑝 : 𝐴 ⊢ 𝜋 : 𝐵 ⇒𝑖 Γ ⊢ 𝜆𝑝.𝜋 : 𝐴 ⇒ 𝐵 Γ ⊢ 𝜋 1 : 𝐴 ⇒ 𝐵 Γ ⊢ 𝜋 2 : 𝐴 ⇒𝑒 Γ ⊢ 𝜋 1 𝜋 2 : 𝐵 Γ ⊢ 𝜋 : 𝐴 ∀𝑖 𝑥∉𝐹𝑉 (Γ) Γ ⊢ 𝜆𝑥 .𝜋 : ∀𝑥 𝐴 Γ ⊢ 𝜋 : ∀𝑥 𝐴 ∀𝑒 Γ ⊢ 𝜋 𝑡 : 𝐴 [𝑡/𝑥] Γ ⊢ 𝜋 : 𝐴 ∀2𝑖 𝑋 ∉𝐹𝑉 (Γ) Γ ⊢ 𝜆𝑋 .𝜋 : ∀𝑋 𝐴 Γ ⊢ 𝜋 : ∀𝑋 𝐴 ∀2𝑒 Γ ⊢ 𝜋 (𝑥 .𝐵) : 𝐴 [𝑥 .𝐵/𝑋 ]rules of second-order logic Figure 2: Second-order arithmetic (𝑥:𝜎 ) ∈Γ Γ ⊢ 𝑥 : 𝜎 Γ, 𝑥 : 𝜎 ⊢ 𝑀 : 𝜏 Γ ⊢ 𝜆𝑥 .𝑀 : 𝜎 → 𝜏 Γ ⊢ 𝑀 : 𝜎 → 𝜏 Γ ⊢ 𝑁 : 𝜎 Γ ⊢ 𝑀 𝑁 : 𝜏 𝑛∈N Γ ⊢ 𝑛 : 𝜄 Γ ⊢ 𝑀 : 𝜄 Γ ⊢ S 𝑀 : 𝜄 Γ ⊢ 𝑀 : 𝜄 Γ ⊢ 𝑀 ? 𝜄 : 𝜎 → (𝜄 → 𝜎 → 𝜎) → 𝜎 Γ ⊢ 𝑀 : 𝜎 Γ ⊢ {𝑀 | } : 𝜎 + 𝜏 Γ ⊢ 𝑀 : 𝜏 Γ ⊢ { | 𝑀 } : 𝜎 + 𝜏