Federico Aschieri

Margherita Zorzi

On Natural Deduction in Classical First-Order Logic: Curry-Howard Correspondence, Strong Normalization and Herbrand's Theorem

Keywords: classical first-order logic, natural deduction, Herbrand's theorem, delimited exceptions, Curry-Howard 03F03, 03F30, 03F55

We present a new Curry-Howard correspondence for classical first-order natural deduction. We add to the lambda calculus an operator which represents, from the viewpoint of programming, a mechanism for raising and catching multiple exceptions, and from the viewpoint of logic, the excluded middle over arbitrary prenex formulas. The machinery will allow to extend the idea of learning -originally developed in Arithmetic -to pure logic. We prove that our typed calculus is strongly normalizing and show that proof terms for simply existential statements reduce to a list of individual terms forming an Herbrand disjunction. A by-product of our approach is a natural-deduction proof and a computational interpretation of Herbrand's Theorem.

Introduction

In the midst of an age of baffling paradoxes and contradictions, during the heat of a harsh controversy between opposed approaches to foundations of mathematics -infinitism vs. constructivism -a new and really penetrating insight was required to see a way out. Hilbert's proposed solution, at the beginning of twentieth century, was certainly deep and brilliant. According to him, there was no contradiction between classical and intuitionistic mathematics, because the ideal objects and principles that appear in classical reasoning can always be eliminated from proofs of concrete, incontestably meaningful statements. Hilbert's idea was made precise in his epsilon elimination method (see [START_REF] Moser | The Epsilon Calculus and Herbrand Complexity[END_REF][START_REF] Mints | A Method of Epsilon Substitution for Predicate Logic with Equality[END_REF]), a systematic procedure to eliminate ideal objects from classical proofs and reduce every logical step to a concrete calculation. Hilbert's program was to show the termination of his method, or variants thereof, initially for first-order classical logic, then Peano Arithmetic and finally Analysis. As it turned out, Hilbert was right, and some termination proofs have been provided for example by Ackermann (for a modern proof see [START_REF] Moser | Ackermann's Epsilon Substitution Method (Remixed)[END_REF]) and Mints [START_REF] Mints | Epsilon Substitution Method for Elementary Analysis[END_REF].

Herbrand's and Kreisel's Theorems

After Hilbert, two other seminal results had been obtained stating that it is always possible to eliminate non-constructive reasoning in two important logical systems.

• The first one is Herbrand's Theorem [START_REF] Buss | On Herbrand's Theorem[END_REF], which says that if a simply existential statement ∃α P is derivable in classical first-order logic from a set of purely universal premises, then there is a sequence of terms m 1 , m 2 , . . . , m k such that the Herbrand disjunction P[m 1 /α] ∨ P[m 2 /α] ∨ . . . ∨ P[m k /α] is provable in classical propositional logic from a set of instances of the premises.

• The second one is Kreisel's Theorem [START_REF] Kreisel | On the Interpretation on Non-Finitist Proofs: Part II[END_REF], which says that if a simply existential formula ∃α P is derivable in classical first-order Arithmetic, then it is derivable already in intuitionistic first-order Arithmetic. Using Kreisel's modified realizability [START_REF] Kreisel | On Weak Completeness of Intuitionistic Predicate Logic[END_REF] (or many other techniques), one can compute out of the intuitionistic proof a number n -a witness -such that P[n/α] is true, whenever P[n/α] it is closed.

Both Herbrand's and Kreisel's proof techniques are now obsolete, but the meaning of their results is as valid as ever, because it provides a theoretical justification for an important quest: the search for the constructive content of classical proofs. Herbrand's Theorem tells us what is the immediate computational content of classical first-order logic: the list of witnesses contained in any Herbrand disjunction. Kreisel's Theorem tells us what is the immediate computational content of first-order Arithmetic: the numeric witness for any provable existential statement. What is of great interest, in the light of those results, is to automatically transform proofs into programs in order to compute from any proof of any existential statement a suitable list of witnesses, in first-order logic, a single witness, in Arithmetic. In this paper, we shall address the first-order version of the problem -and propose a new solution.

Natural Deduction and Sequent Calculus

The two most successful and most studied deductive systems for first-order logic are Gentzen's natural deduction [START_REF] Prawitz | Ideas and Results in Proof Theory[END_REF] and Gentzen's sequent calculus [START_REF] Gentzen | Die Widerspruchsfreiheit der reinen Zahlentheorie[END_REF][START_REF] Girard | Proofs and Types[END_REF]. The first elegant constructive proof of Herbrand's Theorem was indeed obtained as a corollary of Gentzen's Cut elimination Theorem. Today, that proof is still the most cited and the most used. On the contrary, we even failed to find in the literature a complete proof of Herbrand's Theorem using classical natural deduction. This is no coincidence, but yet another instance of the legendary duality between the two formalisms: as a matter of fact, some results are much more easily discovered and proved in the sequent calculus, while others are far more easily obtained in natural deduction. Since the time of Gentzen, natural deduction worked seamlessly for intuitionistic logic, and led to the discovery of the Curry-Howard correspondence [START_REF] Sorensen | Lectures on the Curry-Howard isomorphism[END_REF], while sequent calculus was much more technically convenient in classical logic. As pointed out by [START_REF] Plato | Gentzen's Proof of Normalization for Natural Deduction[END_REF], Gentzen's motivation for the creation of sequent calculus was indeed that he was not able to prove a meaningful normalization theorem for classical natural deduction, whilst he was for the intuitionistic case. It indeed took a surprisingly long time to discover suitable reduction rules for classical natural deduction systems with all connectives [START_REF] De Groote | Strong Normalization for Classical Natural Deduction with Disjunction[END_REF] (see also [START_REF] Aschieri | Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1[END_REF][START_REF] Sorensen | Lectures on the Curry-Howard isomorphism[END_REF] for a more detailed history).

The great advantage of using natural deduction instead of sequent calculus is no mystery: it is natural ! In Gentzen's own words, the main aim of natural deduction was to "reproduce as precisely as possible the real logical reasoning in mathematical proofs" [START_REF] Plato | Gentzen's Proof of Normalization for Natural Deduction[END_REF]. Indeed, when logically solving non-trivial problems, humans adopt forward reasoning, which is more adapted to proof-construction: one starts from some observations, draws some consequences and gradually combines them so as to reach the goal. All of that can be elegantly represented in natural deduction. On the other hand, sequent calculus is more suitable for machine-like proof-search: one starts from the final goal and applies mechanically logical rules to reach axioms. As a consequence, when analyzing real mathematical proofs so to investigate their constructive content, one prefers to use natural deduction. Moreover, the reduction of a proof into normal form is nothing but the evaluation of a functional program, and so very easy to understand. The cut-elimination process, instead, is far more involved and difficult to follow. For example, the proof of Herbrand's Theorem by cut-elimination is deceptively simple: while it is rather obvious that the final cut-free proof contains an Herbrand disjunction, it is very painful to gain a step-by-step and clear understanding of how the corresponding list of witnesses has been produced.

Classical Natural Deduction: an Exception-Based Curry-Howard Correspondence

We would like to endow classical first-order natural deduction with a natural set of reduction rules that also allows a natural, seamless proof of Herbrand's Theorem. As a corollary, this system would also have a simple and meaningful computational interpretation. Indeed, we believe that one can say to really understand a theorem when one is able to construct a proof of it that, a posteriori, appears completely natural, almost obvious. Usually, that happens when one has created a framework of concepts and methods that explain the theorem.

EM 1 and Exceptions in Arithmetic

If one wants to understand how is it possible that a classical proof has any computational content in the first place, the concept of learning is essential. It was a discovery by Hilbert that from classical proofs one can extract approximation processes, that learn how to construct non-effective objects by an intelligent process of trial and error. More recently, Interactive realizability [START_REF] Aschieri | Interactive Learning-Based Realizability for Heyting Arithmetic with EM1[END_REF][START_REF] Berardi | Interactive Realizers. A New Approach to Program Extraction from Nonconstructive Proofs[END_REF][START_REF] Aschieri | A New Use of Friedman's Translation: Interactive Realizability[END_REF][START_REF] Aschieri | Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms[END_REF][START_REF] Aschieri | Interactive Realizability for Second-Order Heyting Arithmetic with EM 1 and SK1[END_REF] has been developed, which is a framework that finally combines the learning idea with the formulae-as-types tradition. In [START_REF] Aschieri | Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1[END_REF] a Curry-Howard correspondence for a classical system of Arithmetic is introduced: namely, Heyting Arithmetic HA with the excluded middle schema EM 1 , ∀αP ∨ ∃α¬P, where P is any atomic, and hence decidable, predicate. Treating the excluded middle as primitive, rather than deriving it from the double negation elimination [START_REF] Krivine | Classical Realizability, Interactive models of computation and program behavior[END_REF][START_REF] De Groote | Strong Normalization for Classical Natural Deduction with Disjunction[END_REF], has a key consequence: classical programs can be described as programs that make hypotheses, test and correct them when they are learned to be wrong. In particular, EM 1 is treated as an elimination rule:

Γ, a : ∀α P u : C Γ, a : ∃α ¬P v : C Γ u a v : C
This inference is nothing but a familiar disjunction elimination rule, where the main premise EM 1 has been cut, since, being a classical axiom, it has no computational content in itself. The proof terms u, v are both kept as possible alternatives, since one is not able to decide which branch is going to be executed at the end.

The informal idea expressed by the associated reductions is to assume ∀α P and try to produce some complete proof of C out of u by reducing inside u. Whenever u needs the truth of an instance P[n/α] of the assumption ∀α P, it checks it, and if it is true, it replaces it by its canonical proof which is just a computation. If all instances P[n/α] of ∀α P being checked are true, and no assumption ∀α P is left (this is the non-trivial part), then the normal form u of u is independent from ∀α P and we found some u : C. If instead some assumption of ∀α P is left in u, one may encounter some instance P[n/α] which is false, and thus refute the assumption ∀α P. In this case the attempt of proving C from ∀αP fails, one obtains ¬P[n/α] and u raises the exception n; from the knowledge that ¬P[n/α] holds, a canonical proof term ∃α ¬P is formed and passed to v: a proof term for C has now been obtained and it can be executed.

EM n and Exceptions in Classical Logic

Our goal is to extend the learning methods developed for HA + EM 1 to classical first-order logic. There is a catch: the reductions we have just described do no longer work! The obvious obstacle is that it is not possible to check the truth of formulas, even of atomic ones: there is no such thing as a standard model for classical first-order logic, let alone an absolute notion of truth. Is the whole idea of learning bound to fail and be abandoned or can it be rescued in some way? The problem is that, even though classical first-order logic is proof-theoretically much weaker than first-order Arithmetic, in a sense, it is harder to interpret and gives rise to different issues. The programs extracted from proofs in HA + EM 1 explore many possible computational paths, due to the bifurcations produced by EM 1 . When the proven formula is a simply existential statement, either a path will succeed in finding a correct witness or will fail and throw some information which will activate another path. At the very end, a single computational path will find a witness. Herbrand's Theorem for classical first-order logic, instead, asserts only the existence of a list of possible witnesses for the proven existential formula. This must be due to the fact that it is often impossible to solve the dilemmas that are posed by the use of the exclude middle, and several alternative computational paths are to be kept forever in parallel.

Let us consider again the rule for EM 1 , but now in pure first-order logic:

Γ, a : ∀α P u : C Γ, a : ∃α ¬P v : C Γ u a v : C EM 1
The idea is still to start reducing inside u in order to produce a proof of C. But the first time one needs an instance P[m/α] of the hypothesis ∀α P to hold, where m is now a closed first-order term, an exception is automatically thrown. Since one is not able to decide whether P[m/α] holds, the current universe doubles and a new pair of parallel, mutually exclusive universes is generated. In the first one, P[m/α] is supposed to hold, in the second one, ¬P[m/α] is supposed to. What is the correct universe? One shall never know, and parallel reductions must continue to be made in these two universes. In the first one, inside u, a small progress has been made, because a use of the universal hypothesis ∀α P can be eliminated: P[m/α] holds by the very hypothesis that generated the universe, and it is no longer necessary to justify it as a consequence of ∀α P. Hence u can reduce to the term u -obtained by erasing the premise ∀α P of all eliminations of ∀α P having as conclusion P[m/α]. In the second one, inside v, a considerable progress has been made, since a witness m for ∃α ¬P has been learned, again by the very hypothesis that generated the universe. Hence v can reduce to the term v + obtained by replacing all occurrences of the hypothesis ∃α ¬P with a proof of it by an introduction rule with premise ¬P[m/α]. The generation of the two universes is logically supported by the use of the excluded middle EM 0 over propositional formulas, which has the general form:

Γ, b : ¬Q w 1 : C Γ, b : Q w 2 : C Γ w 1 | w 2 : C EM 0
The conclusion u a v of EM 1 then converts to:

Γ, b : ¬P[m/α] v + : C Γ, a : ∀α P, b : P[m/α] u -: C Γ, a : ∃α ¬P v : C EM 1 Γ, b : P[m/α] u -a v : C EM 0 Γ v + | (u -a v) : C
We see that in the term v + | (u - a v), there is a single bar | separating forever v + and (u - a v): the two terms will give rise to two different and independent computations. In the first, a universal hypothesis has been refuted and a counterexample learned, in the second, the same universal hypothesis has been confirmed : the idea of learning has been saved!

The term u ||| a v decorating the conclusion of the excluded middle EM 2 , for example of the form

Γ, a : ∀α ∃β ¬P u : C Γ, a : ∃α ∀β P v : C Γ u |||a v : C EM 2
will reduce, in a completely equivalent fashion, to

Γ, b : ∀β P[m/α] v + : C Γ, a : ∀α ∃β ¬P, b : ∃β ¬P[m/α] u -: C Γ, a : ∃α ∀β P v : C EM 2 Γ, b : ∃β ¬P[m/α] u -|||a v : C EM 1 Γ v + b (u -|||a v) : C
u -is now obtained from u by erasing the premise ∀α ∃β ¬P of all eliminations of ∀α ∃β ¬P having as conclusion ∃β ¬P[m/α]; v + is obtained by replacing all occurrences of the hypothesis ∃α ∀β P with a proof of it by an introduction rule with premise ∀β P[m/α]. This time the generation of the new pair of universes in the term v + b (u -||| a v) is logically supported by EM 1 , so the number of bars in the last application of EM is two, decreasing by one. Therefore, the two universes are parallel, but can still communicate with each other: an exception may at any moment be raised by v + and a term be passed in particular to u -. This will be very useful, since the hypothesis b : ∃β ¬P[m/α] may block the computation inside u -.

The reduction rules for the excluded middle on prenex formulas with n alternating quantifiers -EM nare the obvious generalization of what we have just explained: for full details see Section §2. The general idea is that the right ∃-branch of the excluded middle always waits for a witness coming from the left ∀-branch.

These two universes are completely separated, but inhabitants of the second can receive "divine gifts" from the first, under the form of possible witnesses. The inhabitants of the second universe cannot see how these godsends are produced, and may accept them as manifestation of divine providence. This should remind the reader of the copycat strategy for EM n in Coquand's game semantics [START_REF] Coquand | A Semantics of Evidence for Classical Arithmetic[END_REF].

In order to implement our reductions we shall use constant terms of the form H ∀αA a , whose task is to automatically raise an exception: the notation raise ∀αA a would also have been just fine. We shall also use a constant W ∃αA ⊥ a denoting some unknown proof term for ∃α A ⊥ (A ⊥ is an involutive negation), whose task is to catch the exception raised by H ∀αA a . Actually, these terms will occur only through typing rules of the form

Γ, a : ∀α A H ∀αA a : ∀α A Γ, a : ∃α A ⊥ W ∃αA ⊥ a : ∃α A ⊥
where a is used just as a name of a communication channel for exceptions: if in u occurs a subterm of the form H ∀αA From the viewpoint of programming, that is a delimited exception mechanism (see de Groote [START_REF] De Groote | A Simple Calculus of Exception Handling[END_REF] and Herbelin [START_REF] Herbelin | An Intuitionistic Logic that Proves Markov's Principle[END_REF] for a comparison). The scope of an exception has the form u a v : C, with u the "ordinary" part of the computation and v the "exceptional" part. Similar mechanism are expressed by the constructs raise and try . . . with . . . in the CAML programming language. There is a substantial difference, however, with the exception handling mechanism used in [START_REF] Aschieri | Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1[END_REF]. In the term H ∀αA a , the formula ∀α A represents an uncomputable guard : the exception should be raised when a term m falsifying the guard has been encountered. Since it is not possible to check when that really happens, the exception is always raised, but creating two parallel cases: in the first, A[m/α] is false and the exceptional part of the computation is executed, in the second, A[m/α] is true and the ordinary part is executed. Thus, the ordinary part of the computation goes on after the first exception, and in fact can raise multiple exceptions, one after another, which are all passed to the exception handler; in [START_REF] Aschieri | Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1[END_REF], instead, the ordinary part of the computation is aborted as soon as the first exception is raised.

Permutation Rules

A problem arises when the conclusion C of the excluded middle is employed as the main premise of an elimination rule to obtain some new conclusion. For example, already with EM 0 , when C = A → B, and Γ w : A, one may form the proof term (w 1 | w 2 )w of type B. In this case, one may not be able to solve the dilemma of choosing between w 1 and w 2 , and the computation may not evolve further: one is stuck.

As in [START_REF] Aschieri | Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1[END_REF], the problem is solved by adding Prawitz's permutation rules [START_REF] Prawitz | Ideas and Results in Proof Theory[END_REF], as usual with disjunction. For example, (u | v)w reduces to uw | vw. In this way, one obtains two important results: first, one may explore both the possibilities, ∀αP holds or ∃α¬P holds, and evaluate uw and vw; second, one duplicates the applicative context [ ]w. If C = A ∧ B, one may form the proof term π 0 (u | v), which reduces to π 0 u | π 0 v, and has the effect of duplicating the context π 0 [ ]. Similar standard considerations hold for the other connectives. Thus permutation rules act similarly to the rules for µ in the λµ-calculus, but are only used to duplicate step-by-step the context and produce implicitly the continuation. Anyway, | behaves like a control-like operator [START_REF] Parigot | Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction[END_REF][START_REF] Krivine | Classical Realizability, Interactive models of computation and program behavior[END_REF].

Herbrand's Disjunction Extraction and Strong Normalization

The computational content of a classical first-order proof of a simply existential statement is the list of witnesses appearing in an Herbrand disjunction. Why in intuitionistic logic is the result of the normalization process a single witness, while in classical logic it is just a list of possibilities? The reduction rules for EM provide an intuitive explanation of why this list is produced and highlight each of the moments when a piece of it is built. During the normalization of a proof term, the computation is first purely intuitionistic and heading towards a single witness. In other terms, only redexes of the standard lambda calculus are at first contracted. However, the computation may be blocked by an instance of a universal hypothesis H ∀αA a m which the program cannot decide. At that time, the universe doubles, but in each of new pair of universes, the computation goes on and stays intuitionistic. In each of the two universes, new universe duplications can occur and so on . . . . At the very end, there will be several different intuitionistic computations: each of them will produce, as expected, a witness, and the collection of all of them will form the Herbrand disjunction. This intuitive description will be formalized in a normal form property that we shall prove.

We shall also prove a strong normalization result stating that every reduction path generated by any proof term will terminate in a normal form. We shall employ a non-deterministic technique introduced in [START_REF] Aschieri | Strong Normalization for HA + EM1 by Non-Deterministic Choice[END_REF], in turn inspired by [START_REF] Aschieri | Non-Determinism, Non-Termination and the Strong Normalization of System T[END_REF]. While the strong normalization result in [START_REF] Aschieri | Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1[END_REF] was obtained by means of a special notion of realizability, we had considerable trouble generalizing that technique. At the end, the non-deterministic approach revealed much more simple to generalize. We thus leave open the interesting problem of defining a realizability or a proof-theoretic semantics for our natural deduction system.

Plan of the Paper

In Section §2 we introduce a type-theoretical version of intuitionistic first-order logic IL extended with EM := n EM n . In Section §3 we prove the strong normalization of a non-deterministic variant IL + EM of IL + EM, which immediately implies the strong normalization of the latter. In Section §4, we prove that from any quasi-closed term having as type a simply existential formula, one can extract a corresponding Herbrand disjunction. We also construct a term with two different normal forms, containing two distinct Herbrand disjunctions, thereby showing that the system IL + EM is non-confluent, as expected.

The System IL + EM

In this section we describe a standard natural deduction system for intuitionistic first-order logic IL, with a term assignment based on the Curry-Howard correspondence (e.g. see [START_REF] Sorensen | Lectures on the Curry-Howard isomorphism[END_REF]), and add on top of it an operator which formalizes the excluded middle principle EM n . First, we shall describe the terms and their computational behavior, proving as main result the Subject Reduction Theorem, stating that the reduction rules preserve the type. Then, we shall analyze the logical meaning of the reductions and present them as pure proof transformations.

We start with the standard first-order language of formulas.

Definition 1 (Language of IL + EM). The language L of IL + EM is defined as follows.

1. The terms of L are inductively defined as either variables α, β, . . . or constants c or expressions of the form f(t 1 , . . . , t n ), with f a function constant of arity n and t 1 , . . . , t n ∈ L. 2. There is a countable set of predicate symbols. The atomic formulas of L are all the expressions of the form P(t 1 , . . . , t n ) such that P is a predicate symbol of arity n and t 1 , . . . , t n are terms of L. We assume to have a 0-ary predicate symbol ⊥ which represents falsity. 3. The formulas of L are built from atomic formulas of L by the logical constants ∨, ∧, →, ∀, ∃, with quantifiers ranging over variables α, β, . . .: if A, B are formulas, then A ∧ B, A ∨ B, A → B, ∀α A, ∃α B are formulas. The logical negation ¬A can be introduced, as usual, as an abbreviation of the formula A → ⊥. 4. Propositional formulas are the formulas whose only logical constants are ∧, ∨, →; we say that a propositional formula is negative whenever ∨ does not occur in it. Propositional formulas will be denoted as P, Q . . . (possibly indexed). Formulas of the form ∀α 1 . . . ∀α n P, with n ≥ 0 and P propositional, will be denoted as ∀ α P and will be called purely universal; if P is also negative, the formula will be called simply universal. 5. A formula is a prenex normal form with alternating quantifiers if it is of the shape

Q 1 α 1 Q 2 α 2 . . . Q n α n P
where, for i = 1 . . . n, Q i ∈ {∀, ∃}, Q i = Q i+1 and P is propositional. 6. An even negation is inductively defined as: i) a formula which is not a negation; ii) a formula of the shape ¬¬A, where A is an even negation. Likewise, an odd negation is inductively defined as: i) a formula ¬A, where A is not a negation; ii) a formula of the shape ¬¬A, where A is an odd negation.

If P is propositional, we define P ⊥ as ¬P, if P is an even negation, as Q, if P is an odd negation and P = ¬Q. For every prenex formula with alternating quantifiers

A, if A = Q 1 α 1 Q 2 α 2 . . . Q n α n P, with Q i ∈ {∀, ∃} for i = 1 . . . n, we define the involutive negation of A as A ⊥ = Q 1 α 1 Q 2 α 2 . . . Q n α n P ⊥ , where Q i ∈ {∀, ∃} \ {Q i }, for i = 1 . . . n.
For deducing the axiom ⊥ → A (ex falso sequitur quodlibet), it is enough to have ⊥ → P, where P is atomic, and also the axioms of equality can be formulated as simply universal. They will not appear explicitly in the logical rules, since at any rate we shall have to treat a more general case: the computational interpretation of proofs having as assumptions an arbitrary set of simply universal statements, as usual in Herbrand's Theorem.

We now define in Figure 1 a set of untyped proof terms, then a type assignment for them.

Grammar of Untyped Proof Terms t, u, v ::= x | tu | tm | λx u | λα u | t, u | u π 0 | u π 1 | ι 0 (u) | ι 1 (u) | t[x.u, y.v] | (m, t) | t[(α, x).u] | (u | v) | (u | | . . . |a v) | H ∀αA a | W ∃αA a | H P
where m ranges over terms of L, x over proof-term variables, α over first-order variables, a over hypothesis variables and A is a prenex formula with alternating quantifiers and negative propositional matrix or is a simply universal formula. We assume that in the term u | | . . . |a v, there is some formula A, such that a occurs free in u only in subterms of the form H ∀αA a and a occurs free in v only in subterms of the form W ∃αA a , and the occurrences of the variables in A different from α are free in both u and v.

Contexts With Γ we denote contexts of the form e 1 : A 1 , . . . , en : An, where each e i is either a proof-term variable x, y, z . . . or an EM hypothesis variable a, b, . . ., and e i = e j for i = j.

Axioms Γ, x : A x : A Γ, a : ∀α A H ∀αA
where α is not free in C nor in any formula B occurring in Γ.

EM 0 Γ, a :

P ⊥ u : C Γ, a : P v : C Γ u | v : C (P negative) EMn Γ, a : ∀α A u : C Γ, a : ∃α A ⊥ v : C Γ u | | . . . |a n+1bars v : C
where A is a formula with alternating quantifiers and: i) when n = 1, A = P with P negative; ii) when n > 1, A = ∃α 1 ∀α 2 ∃α 3 . . . Q n-1 α n-1 P, with P negative and Q n-1 ∈ {∀, ∃}. the free variables are a and those of A minus α. A term of the form H ∀αA a m, with m ∈ L, is said to be active, if its only free variable is a: it represents a raise operator which has been turned on. The hypotheses for propositional formulas P of any form will be represented by terms H P , regardless of their being introduced in the right or left premise of the excluded middle. Hence, the letter H stands for a hypothesis which does not "wait" for a witness, while W for one which does.

We require, for untyped terms of the form

u | | | | | | | | a v
to be meaningful, that whenever H ∀αA a and W ∃αA a occur respectively in u and v, no free variable of A is bound in u or in v. This kind of requirement is standard in Church-style lambda calculi in order to ensure that the subject reduction property holds: the type of a free variable can never occur under the scope of a lambda abstraction, but when the same variable becomes bound this restriction is dropped. Our typing rules guarantee this property as well, but for the underlying untyped calculus one has to explicitly state it as a condition.

In our formulation, the excluded middle is restricted to negative propositional formulas, in the case of EM 0 , and to prenex formulas with alternating quantifiers and negative propositional matrix, in the case of EM n . From the logical viewpoint, however, this is not at all a restriction, since any arbitrary instance A ∨ ¬A of the excluded middle can be proved in our system by standard, but tortuous, logical manipulations (see [1] for a proof in the case of Arithmetic and Appendix A for a simpler proof in our case). The fact that our system captures full classical first-order logic is not surprising, of course, since every formula is classically equivalent to a prenex one. From the computational viewpoint, in fact, we have directly modeled the most difficult instances of EM. It is quite clear that similar reduction rules for the less interesting cases of propositional connectives can be easily given, as for example in von Plato [START_REF] Plato | Natural Deduction: Some Recent Develpments[END_REF], since ∧ is just a finitary counterpart of ∀ and ∨ of ∃. For economy of presentation, we delay the treatment to future work.

Reduction Rules: Computational Description

We are now going to explain the basic reduction rules for the proof terms of IL + EM, which are given in Figure 2. As usual, one has also the reduction scheme: E[t] → E[u], whenever t → u and for any context E. With → * we shall denote the reflexive and transitive closure of the one-step reduction →.

We find among the reductions the ordinary ones of intuitionistic logic for the logical constants. Permutation Rules for EM n are an instance of Prawitz's permutation rules for ∨-elimination [START_REF] Prawitz | Ideas and Results in Proof Theory[END_REF] In the following, with a slight abuse of language, we will sometimes write that b is fresh, intending that, if b is not the empty string , it is a fresh hypothesis variable b.

(λx.u)t → u[t/x] (λα.u)m → u[m/α] u 0 , u 1 π i → u i , for i=0,1 ι i (u)[x 1 .t 1 , x 2 .t 2 ] → t i [u/x i ], for i=0,1 (m, u)[(α, x).v] → v[m/α][u/x], for each term m of L Permutation Rules for EM 0 (u | v)w → uw | vw (u | v)π i → uπ i | vπ i (u | v)[x.w 1 , y.w 2 ] → u[x.w 1 , y.w 2 ] | v[x.w 1 , y.w 2 ] (u | v)[(α, x).w] → u[(α, x).w] | v[(α, x).w] Permutation Rules for EMn (u | | | | | | | |a v)w → uw | | | | | | | |a vw, if a does not occur free in w (u | | | | | | | |a v)π i → uπ i | | | | | | | |a vπ i (u | | | | | | | |a v)[x.w 1 , y.w 2 ] → u[x.w 1 , y.w 2 ] | | | | | | | |a v[x.w 1 , y.w 2 ], if a does not occur free in w 1 , w 2 (u | | | | | | | |a v)[(α, x).w] → u[(α, x).w] | | | | | | | |a v[(α, x).w], if a does not occur free in w 1 , w 2 Reduction Rules for EMn u | | | | | | | |a v → u, if a does not occur free in u u | | | | | | | || |a v → v[a := e] | | | | | | | | b (u[a := e] | | | | | | | || |a v),
Remark 1. In the cases 1 and 2 of Definition 2 of v[a := e], subterms of the form W ∃αP a , with P propositional, are replaced by (m, H P [m/α]), because there is no exception and in particular no witness for P[m/α] to be waited for and caught. Likewise, H ∀αP a m is replaced by H P[m/α] , which does not bear exception variables as subscripts, since it raises no exception. Moreover, we remark that the substitution may replace only prenex hypotheses with alternating quantifiers, thus those introduced by the rule EM n .

In the term u | v, the subterms u and v are forever divided and represent disjoint computational paths: communication between them is not even possible, because there is no associated exception mechanism. Exception variables are not used in terms of the form u | v because there is no useful information that can be raised by u and handed to v: the premises of EM 0 are completely void of positive information, because they are negative formulas. But u | v does not prevent the computation to go on, thanks to the permutation rules and because negative propositional assumptions do not stop the computation, that is, do not prevent normal proofs of existential statements to terminate with an ∃-introduction rule. In Arithmetic it is always possible to eliminate completely the excluded middle from proofs of simply existential statements, because atomic formulas are decidable, and thus one has either the reduction rule u | v → u or u | v → v . In first-order logic the price to pay for undecidability of atomic formulas is that simply existential statements cannot be provided with a unique witness, but only with a list of possibilities: that is why the program extraction theorem in this setting is Herbrand's theorem and not Kreisel's.

The rules for EM n instead translate the informal idea of exception handling we sketched in the introduction: (or H A[m/α] if A is propositional), which confirms, in this "universe", an instance of the stronger ∀αA. Notice that after the substitution u[a := e] some free occurrence of a in u may still be there (the replaced occurrences of a are only the ones of the form H ∀αA • A →-redex is a term u such that u → v for some v and basic reduction of Figure 2. A term t is called an →-normal form (or simply normal form) if t does not contain as subterm any →-redex. We define NF to be the set of normal untyped proof terms.

1. The first EM n -reduction: u | | | | | | | | a v → u (a
• A sequence (finite or infinite) of proof terms u 1 , u 2 , . . . , u n , . . . is said to be a reduction of t, if t = u 1 , and for all i, u i → u i+1 . A proof term u of IL + EM is strongly normalizable if there is no infinite reduction of u. We denote with SN the set of strongly normalizable terms of IL + EM.

In the following, we assume the usual renaming rules and alpha equivalences to avoid capture of variables in the reduction rules that we shall give. We also observe that every typed term which has been obtained by an elimination as a last rule, can be written as r t 1 t 2 . . . t n (n ≥ 0), where r is either a variable x or a term H ∀αA a or H P or a redex and each t i is either a term (when r t 1 . . . t i is obtained by an →-elimination rule or by a ∀-elimination rule) or a constant π i (when r t 1 . . . t i is obtained by an ∧-elimination rule) or an expression [x 0 .u 0 , x 1 .u 1 ] (when r t 1 . . . t i is obtained by an ∨-elimination rule) or an expression [(α, x).u] (when r t 1 . . . t i is obtained by an ∃-elimination rule).

Assume that Γ is a context, t an untyped proof term and A a formula, and Γ t : A: then t is said to be a typed proof term. Typing assignment satisfies Weakening, Exchange and Thinning, as usual. The reductions defined in Figure 2 satisfy the important Subject Reduction Theorem: reduction steps at the level of proof terms preserve the type, which is to say that they correspond to logically sound transformations at the level of proofs. We first give a proof of the Theorem, then analyze in detail its logical meaning in the next subsection. Intuitively, the result holds because the new classical reductions make very minor replacements. In the reduction

u | | | | | | | || | a v → v[a := e] | | | | | | | | b (u[a := e] | | | | | | | || | a v) if v
[m/α] H A[m/α] b : A[m/α] Γ, b : A[m/α] (m, H A[m/α] b ) : ∃α A If v = w 1 w 2 ,
⊥ [m/α] v[a := e] : C Therefore, Γ, b : A ⊥ [m/α] v[a := e] : C Γ, a : ∀α A, b : A[m/α] u[a := e] : C Γ, a : ∃α A ⊥ , b : A[m/α] v : C EM k Γ, b : A[m/α] u[a := e] | | | | | | | || |a v : C EM k-1 Γ v[a := e] | | | | | | | | b (u[a := e] | | | | | | | || |a v) : C Since A[m/α] = A ⊥⊥ [m/α]
, the derivation above is correct and we are done.

We now introduce the concept of quasi-closed term, which intuitively is a term behaving as a closed one, in the sense that it can be executed, but that contains some free simply universal hypotheses on which its correctness depends.

Definition 4 (Quasi-Closed terms). An untyped proof term t is said to be quasi-closed, if it contains as free variables only hypothesis variables a 1 , . . . , a n , such that each occurrence of them is of the form H ∀ αPi ai , where ∀ α P i is simply universal.

The class of quasi-closed terms is meaningful from a computational viewpoint, as explained in Section 4.

Reduction Rules: Logical Interpretation

So far, in studying the system IL + EM, we have given priority to the underlying lambda calculus and characterized it as a functional language endowed with an exception handling mechanism. The explanation of the reductions had little to do with logic and much with computation. However, thanks to the Subject Reduction Theorem, we know we could have proceeded the other way around. Namely, we could have given priority to logic and dealt only with transformation of proofs, in the style of Prawitz natural deduction trees [START_REF] Prawitz | Ideas and Results in Proof Theory[END_REF]. Since it is very instructive to explain directly this point of view, we are finally going to.

First of all, the standard reductions for lambda calculus still correspond to the ordinary conversions for all the logical constants of first-order logic:

[A] . . . B A → B . . . A B converts to: . . . A . . . B A i (i ∈ {1, 2}) A 1 ∨ A 2 [A 1 ] . . . C [A 2 ] . . . C C converts to: . . . A i . . . C . . . A 1 . . . A 2 A 1 ∧ A 2 (i ∈ {1, 2})
A i converts to: . . .

A i . . . A[m/α] ∃α A [A] π C C converts to: . . . A[m/α] π[m/α] C π A ∀α A A[m/α] converts to: π[m/α] A[m/α]
The permutation reductions for the terms of the form

u | | | | | | | || | a v,
are just instances of Prawitz-style permutations for disjunction elimination. From the logical perspective, they are used to systematically reduce, whenever possible, the complexity of the applications of the excluded middle rule, by decreasing the logical complexity of the conclusion. This reduction is essential because the excluded middle is not constructive when employed to prove complex statements; but it becomes such, whenever used to prove simply existential statements. As an example of permutation for EM, we consider the one featuring an implication as conclusion: [∀αA] . . .

B → C [∃αA ⊥ ] . . . B → C B → C . . . B C converts to: [∀αA] . . . B → C . . . B C [∃αA ⊥ ] . . . B → C . . . B C C
Finally, there are two reductions for proofs containing the EM-rule. Their primary goal is to reduce the usage of the universal hypothesis on which the left branch of the excluded middle depends. In the second reduction for EM n , a closed instance A[m/α] of a hypothesis ∀αA is tested, by using EM n-1 . If the test is passed, one can eliminate an occurrence of the hypothesis ∀αA; if the test fails, one has a witness A ⊥ [m/α] for the hypothesis ∃αA ⊥ on which the right branch of the excluded middle depends:

[∀αA] A[m/α] . . . [∀αA] . . . C [∃αA ⊥ ] . . .

C EMn C converts to:

[A ⊥ [m/α]] ∃αA ⊥ . . . C [A[m/α]] . . . [∀αA] . . . C [∃αA ⊥ ] . . . C EMn C EMn-1 C
In the conversion above, it is very important to notice that the original proof is copied almost unchanged and becomes the right branch of a new, but less complex, application of EM; the only difference is that, during the copy, the original proof has lost one or several occurrences of the hypothesis ∀αA, and as a result it appears a little bit simpler.

In the first reduction for EM, one has already arrived at the point where the use of the universal hypothesis ∀αA in the left branch has already been eliminated and thus the proof can be simplified by removing the excluded middle rule altogether: . . . The aim of this section is to prove that each well-typed term of IL + EM is strongly normalizing. To this end, we make a detour into the world of non-determinism. The idea is to map IL + EM to a carefully defined non-deterministic variant IL + EM , for which strong normalization is proven. The Normalization Theorem for IL + EM will plainly follow as a corollary. This proof technique is a generalization of [START_REF] Aschieri | Strong Normalization for HA + EM1 by Non-Deterministic Choice[END_REF], in turn inspired by [START_REF] Aschieri | Non-Determinism, Non-Termination and the Strong Normalization of System T[END_REF].

We now introduce the non-deterministic system IL + EM , which is still a standard natural deduction system for intuitionistic first-order logic with excluded middle. The only syntactical difference with the system IL + EM lies in the shape of proof terms, and is really tiny: the proof terms for EM and EM-hypotheses lose the hypothesis variables used to name them. Thus the grammar of untyped proof terms of IL + EM is defined to be the following:

Grammar of Untyped Terms of IL + EM t, u, v ::= x | tu | tm | λx u | λα u | t, u | u π 0 | u π 1 | ι 0 (u) | ι 1 (u) | t[x.u, y.v] | (m, t) | t[(α, x).u] | (u || . . . | n+1bars v) | H ∀αA | W ∃αA | H P
where m ranges over terms of L, x over proof terms variables and A is either prenex with alternating quantifiers or simply universal.

The term assignment rules of IL + EM are exactly the same of IL + EM, but for the ones for EM-hypotheses and EM, which just replace hypothesis variables a from the former proof terms:

Axioms Γ, a : ∀αA H ∀αA : ∀αA Γ, a : ∃αA W ∃αA : ∃αA Γ, a : ∀αA w 1 : C Γ, a : ∃αA ⊥ w 2 : C EM n Γ w 1 || . . . | n+1bars w 2 : C
The reduction rules for the terms of IL + EM are defined in Figure 3 and are those of the first two groups for IL + EM, plus new non-deterministic rules for EM and closure by context (with * we shall denote the reflexive and transitive closure of the one-step reduction and with + the transitive closure). We explain now the non-deterministic part of the reduction rules. The reduction rule for H ∀αA says that, when the constant is applied to a closed term m ∈ L, it is possible to replace a universal hypothesis ∀αA with a hypothesis A[m/α], denoted by the constant W A[m/α] , when A[m/α] is not propositional and is thus of the shape ∃βB for some universal formula B. The intuition behind the reduction rule for W ∃αA is the following: the term W ∃αA behaves as a "search" operator, which spans non-deterministically all first-order terms as possible witnesses of ∃αA and makes the hypothesis that they are correct (these branches correspond to all the possible pairs (m, H A[m/α] )). The first two rules for the operator | | | | | | | | are standard reductions for the non deterministic choice operator (see [START_REF] De' Liguoro | Non-Deterministic Extensions of Untyped Lambda-Calculus[END_REF][START_REF] Lago | Probabilistic Operational Semantics for the Lambda Calculus[END_REF]). The third rule, together with the reductions for H ∀αA and W ∃αA , is able to "simulate" the reductions of the deterministic

u | | | | | | | | a v
and, in particular, the exception substitution mechanism [a := e].

In the following, we define SN to be the set of strongly normalizing proof terms with respect to the non-deterministic reduction . The reduction tree of a strongly normalizable term with respect to is no more finite, but still well-founded. It is well-known that it is possible to assign to each node of a well-founded tree an ordinal number, in such a way it decreases passing from a node to any of its sons. We will call the ordinal size of a term t ∈ SN the ordinal number assigned to the root of its reduction tree and we denote it by h(t); thus, if t u, then h(t) > h(u). To fix ideas, one may define h(t) := sup{h(u)

+ 1 | t → u}. Reduction Rules for IL (λx.u)t u[t/x] (λα.u)m u[m/α] π i u 0 , u 1 u i , for i = 0, 1 (λx.u)t u[t/x] (λα.u)t u[t/α] u 0 , u 1 π i u i , for i = 0, 1 ι i (u)[x 1 .t 1 , x 2 .t 2 ] t i [u/x i ], for i = 0, 1 (m, u)[(α, x).v] v[m/α][u/x], for each term m of L Permutation Rules for EM (u | | | | | | | | v)w uw | | | | | | | | vw (u | | | | | | | | v)π i uπ i | | | | | | | | vπ i (u | | | | | | | | v)[x.w 1 , y.w 2 ] u[x.w 1 , y.w 2 ] | | | | | | | | v[x.w 1 , y.w 2 ] (u | | | | | | | | v)[(α, x).w] u[(α, x).w] | | | | | | | | v[(α, x).w]
Reduction Rules for EM

(H ∀αA )m W A[m/α] ,
for every closed term m of L and existential A

(H ∀αP )m H P[m/α] , for every closed term m of L W ∃αA (m, H A[m/α] ), for every closed term m of L u | | | | | | | | v u u | | | | | | | | v v u | | | | | | | || | v v | | | | | | | | (u -| | | | | | | || | v)
where u -is the term obtained from u by replacing one or several occurrences of a subterm (H ∀αA )m with W A[m/α] (or with H A[m/α] when A is not existential) We now define the obvious translation mapping untyped proof terms of IL + EM into untyped terms of IL + EM , which just erases every occurrence of every EM-hypothesis variable a.

Definition 5 (Translation of untyped proof terms of IL + EM into IL + EM ). We define a translation * mapping untyped proof terms of IL + EM into untyped proof terms of IL + EM : t * is defined as the term of IL + EM obtained from t by erasing every EM hypothesis variable a.

We now show that the reduction relation for the proof terms of IL + EM can easily simulate the reduction relation → for the terms of IL + EM. This is trivial for the proper reductions of IL and the permutative reductions for EM, and we are going to show that the reduction rules for the terms of the form

u | | | | | | | | a v
can be plainly simulated by with non-deterministic guesses. In particular, each reduction step between terms of IL + EM corresponds to at least a step between their translations: Proposition 1 (Preservation of the Reduction Relation → by ). Let v be any untyped proof term of IL + EM. Then v → w =⇒ v * + w * Proof. It is sufficient to prove the proposition when v is a redex r. We have several possibilities, almost all trivial, and we choose only some representative cases:

1. r = (λx u)t → u[t/x]. We verify indeed that ((λx u)t) * = (λx u * )t * u * [t * /x] = u[t/x] * 2. r = (u | | | | | | | | b v)w → uw | | | | | | | | b vw. We verify indeed that ((u | | | | | | | | b v)w) * = (u * | | | | | | | | v * )w * u * w * | | | | | | | | v * w * = (uw | | | | | | | | b vw) * 3. r = u | | | | | | | || | a v → v[a := e] | | | | | | | | b (u[a := e] | | | | | | | || | a v) (
(H ∀αA )m W A[m/α] (or (H ∀αP )m H P[m/α] ) and W ∃αA (m, H A[m/α] ) -that (u | | | | | | | || | a v) * = u * | | | | | | | || | v * v * | | | | | | | | ((u * ) -| | | | | | | || | v * ) * (v[a := e]) * | | | | | | | | ((u[a := e]) * | | | | | | | || | v * ) = (v[a := e] | | | | | | | | b (u[a := e] | | | | | | | || | a v)) *
(where (u * ) -is the term obtained from u * by replacing some occurrences of a subterm (H ∀αA )m with W A[m/α] or H A[m/α] when A is propositional)

Reducibility

We now want to prove the strong normalization theorem for IL + EM : every term t which is typed in IL + EM is strongly normalizable. We use a simple extension of the reducibility method of Tait-Girard [START_REF] Girard | Proofs and Types[END_REF]. Definition 6 (Reducibility). Assume t is a term in the grammar of untyped terms of IL + EM and C is a formula of L. We define the relation t r C ("t is reducible of type C") by induction and by cases according to the form of C:

m of L, if t * (m, u), then u r A[m/α]

Properties of Reducible Terms

In this section we prove that the set of reducible terms for a given formula C satisfies the usual properties of a Girard reducibility candidate.

Following [START_REF] Girard | Proofs and Types[END_REF], neutral terms are terms that are not "values" and need to be further computed.

Definition 7 (Neutrality).

A proof term is neutral if it is not of the form λx u or λα u or u, t or

ι i (u) or (m, u) or u | | | | | | | | v or H ∀αA . If z = (v | | | | | | | | (u -| | | | | | | || | v))w
, where u -is the term obtained from u by replacing some occurrences of a subterm (H ∀αA )m with W A[m/α] (or H A[m/α] ), then u + u -, therefore by (CR2) and induction hypothesis, for all r r A, we have (u

-| | | | | | | || | v)r r B and thus (u -| | | | | | | || | v) r A → B. We conclude by induction hypothesis that v | | | | | | | | (u -| | | | | | | || | v) r A → B and thus z r B. • C = ∀αA or C = A ∧ B. Similar to the case C = A → B. • C = A 0 ∨ A 1 .
(CR1) is trivial.

(CR2). Suppose t r A 0 ∨ A 1 and t * t . Then t ∈ SN , since t ∈ SN . Moreover, suppose t * ι i (u). Then also t * ι i (u), so u r A i .

(CR3). Assume t is neutral and t t implies t r A 0 ∨ A 1 . Since t t implies t ∈ SN , we have t ∈ SN . Moreover, if t * ι i (u), then, since t is neutral, t t * ι i (u) and thus u r A i . • C = ∃αA. Similar to the case t = A 0 ∨ A 1 .

(CR4). ⇒). Suppose t = u | | | | | | | | v r A 0 ∨ A 1 . Since t u, t v, by (CR2), u r A 0 ∨ A 1 and v r A 0 ∨ A 1 . ⇐). Suppose u r A 0 ∨ A 1 and v r A 0 ∨ A 1 . We have to show that u | | | | | | | || | v r A 0 ∨ A 1 . By definition, u, v ∈ SN ; therefore, as shown in the case C = P , u | | | | | | | || | v ∈ SN . Moreover, suppose u | | | | | | | || | v * ι i (w). It is enough to show that u * ι i (w) or v * ι i (w); this implies w r A i ,
The next task is to prove that all introduction and elimination rules of IL + EM define a reducible term from a list of reducible terms for all premises (Adequacy Theorem 2). In some cases that is true by definition of reducibility; we list below some non-trivial but standard cases we have to prove. Proposition 3. [START_REF] Girard | Proofs and Types[END_REF]. 4. Suppose t r A 0 ∨ A 1 and for every t i r A i it holds u i [t i /x i ] r C. We observe that by (CR3), x i r A i , and so we have u i r C. Thus, in order to prove t[x 0 .u 0 , x 1 .u 1 ] r C, by (CR1), we can reason by triple induction on the ordinal sizes of the reduction trees of t, u 0 , u 1 . By (CR3), it suffices to show that t

As in

[x 0 .u 0 , x 1 .u 1 ] z implies z r C. If z = t [x 0 .u 0 , x 1 .u 1 ] or z = t[x 0 .u 0 , x 1 .u 1 ] or z = t[x 0 .u 0 , x 1 .u 1 ]
, with t t and u i u i , then by (CR2) and by induction hypothesis z r C.

If t = ι i (t i ) and z = u i [t i /x i ], then t i r A i ; therefore, z r C. If t = w 0 | | | | | | | | w 1 and z = (w 0 [x 0 .u 0 , x 1 .u 1 ]) | | | | | | | | (w 1 [x 0 .u 0 , x 1 .u 1 ]) then, since t = w 0 | | | | | | | | w 1 w i , by induction hypothesis w i [x 0 .u 0 , x 1 .u 1 ] r C for i = 0, 1
. By (CR4), we conclude z r C. 5. Similar to 4.

The Adequacy Theorem

Theorem 2 (Adequacy Theorem). Suppose that Γ w : A in the system IL + EM , with Γ = x 1 : A 1 , . . . , x n : A n , ∆ (∆ not containing declarations of proof-term variables), and that the free variables of the formulas occurring in Γ and A are among α 1 , . . . , α k . For all terms r 1 , . . . , r k of L, if there are terms t 1 , . . . , t n such that

for i = 1, . . . , n, t i r A i [r 1 /α 1 • • • r k /α k ] then w[t 1 /x 1 • • • t n /x n r 1 /α 1 • • • r k /α k ] r A[r 1 /α 1 • • • r k /α k ]
Proof.

Notation: for any term v and formula B, we denote

v[t 1 /x 1 • • • t n /x n r 1 /α 1 • • • r k /α k ] with v and B[r 1 /α 1 • • • r k /α k ]
with B. We proceed by induction on w. Consider the last rule R in the derivation of Γ w : A:

1. If R = Γ x i : A i , for some i, then w = x i and A = A i . So w = t i r A i = A.
2. If R = Γ H P : P the thesis is trivial. We prove simultaneously the cases R = Γ W ∃αB : ∃αB and R = Γ H ∀αB : ∀αB i.e. we want to prove that w = W ∃αB = W ∃αB r ∃αB = A and w = H ∀αB = H ∀αB r ∀αB = A respectively. We proceed by induction on B. Let us consider the term w = W ∃αB : we have that, for all terms z such that W ∃αB z, z = (m, H B[m/α] ) for some m ∈ L . It is possible to apply the induction hypothesis to H B[m/α] : thus H B[m/α] r B[m/α] holds and we can conclude W ∃αB r ∃αB by Definition 6. Now, let us apply H ∀αB to an arbitrary term m ∈ L. Since

H ∀αB m W B[m/α] or H ∀αB m H B[m/α] and by induction hypothesis H B[m/α] , W B[m/α] r B[m/α], we can conclude by (CR3)that H ∀αB m r B[m/α].
Therefore, H ∀αB r ∀αB by Definition 6. 10. If R is the ∀I rule, then w = λαu, A = ∀αB and Γ u : B (with α not occurring free in the formulas of Γ). w = λαu, since we may assume α = α 1 , . . . , α k . Let t be a term of L; by proposition 3), it is enough to prove that u[t/α] r B[t/α], which amounts to showing that the induction hypothesis can be applied to u. For this purpose, we observe that, since α = α 1 , . . . , α k , for i = 1, . . . , n we have Proof. Assume Γ = x 1 : A 1 , . . . , x n : A n , ∆ (∆ not containing declarations of proof-term variables). By (CR1), one has x i r A i , for i = 1, . . . , n. From Theorem 2, we derive that t r A. From (CR1), we conclude that t ∈ SN .

t i r A i = A i [t/α]
The strong normalization of IL + EM is readily turned into a strong normalization result for IL + EM, since the reduction → can be simulated by .

Back to IL + EM: Normal Form Property and Herbrand's Disjunction Extraction

In this section, we finally show that our exception-based Curry-Howard correspondence for classical logic is meaningful from the computational perspective. That is, not only does every execution of every program we extract always terminate, but in the case of simply existential formulas ∃α P, any closed program of that type produces a complete finite sequence m 1 , m 2 , . . . , m k of possible witnesses for ∃α P. This means that whatever first-order model we consider, there will be an i such that P[m i /α] is true in it. The result still holds whenever the program t is quasi-closed, which is to say, whenever ∃α P is proven by means of a simply universal theory: a 1 : ∀ α P 1 , . . . , a n : ∀ α P n t : ∃α

In this case, for any first-order model of the formulas a 1 : ∀ α P 1 , . . . , a n : ∀ αP n , there will be an i such that P[m i /α] is true in it. Furthermore, by Subject Reduction, t will contain also a correctness certificate, in the sense that in the normal form of t one finds a proof-term for the formula

P[m 1 /α] ∨ • • • ∨ P[m k /α].
In other terms, we have provided a new proof and a new Curry-Howard computational interpretation of Herbrand's Theorem. The fact that we consider as hypotheses only simply universal ones, i.e. universal formulas without occurrences of ∨, is by no means restrictive: by EM 0 , one can easily prove any propositional formula to be equivalent to a negative one, and thus to derive the former from the latter. In order to prove our results, we first carry out a simple inspection of the normal forms of some terms having propositional or simply existential type. The crucial observation is that every such term contains an exception ready to be raised, as soon as an exception throwing operator occurs in it: more precisely, it has an active subterm of the form H ∀αA a m, for some m ∈ L. From the logical point of view, this means that when one proves a formula of minimal complexity by means of a universal theory, one must use actively one of the universal hypotheses and obtain some concrete consequence of it. Such statements in first-order logic are typically drawn as consequences of the Subformula Property, but a much more primitive argument suffices here. This is indeed providential, since without permutation rules for ∨ and ∃, there will be no Subformula Property. Of course, we do have some permutation rules, namely those for the excluded middle: what is remarkable is that they are going to be enough. Nevertheless, if we think that in intuitionistic Logic or fragments of classical Arithmetic [START_REF] Aschieri | Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1[END_REF] general permutation rules are not needed to compute witnesses, it should not entirely come as a surprise that this is still the case in our framework.

Proposition 4 (Normal Form Property). Let P, P 1 , . . . , P n be negative propositional formulas. Suppose that Γ = x 1 : P 1 , . . . , x n : P n , a 1 : ∀α 1 A 1 , . . . , a m : ∀α m A m , and Γ t : ∃α P or Γ t : P, with t ∈ NF and having all its free variables among x 1 , . . . , x n , a 1 , . . . , a m . Then:

1. Either every occurrence in t of every term H ∀αiAi ai is of the active form H ∀αiAi ai m, where m is a term of L; or t has an active subterm of the form H ∀αiAi ai m, for some non simply universal formula A i and term m of L.

Either

t = (m, u) or t = λx u or t = u, v or t = u | v or t = u | | | | | | | | a v or t = H P or t = x i t 1 t 2 . . . t n or t = H ∀αAi ai m t 2 . . . t n .
Proof. We prove 1. and 2. simultaneously and by induction on t. There are several cases, according to the shape of t:

• t = (m, u), Γ t : ∃α P and Γ u : P[m/α]. We immediately get 1. by induction hypothesis applied to u, while 2. is obviously verified.

• t = λx u, Γ t : P = Q → R and Γ, x : Q u : R. We immediately get 1. by induction hypothesis applied to u, while 2. is obviously verified.

• t = u, v , Γ t : P = Q ∧ R, Γ u : Q and Γ v : R. We immediately get 1. by induction hypothesis applied to u, while 2. is obviously verified.

• t = u | v, Γ, a : Q ⊥ u : ∃α P (resp. u : P) and Γ, a : Q v : ∃α P (resp. v : P). We immediately get the thesis by induction hypothesis applied to u and v, while 2. is obviously verified.

• t = u | | | | | | | | a v,
= u | | | | | | | || | a v → v[a := e] | | | | | | | | b (u[a := e] | | | | | | | || | a v)
, with e = (m, b): but t ∈ NF. Therefore, u has an active subterm of the form H ∀αiAi ai m, for some non simply universal formula A i and m ∈ L. We have thus established 1. for t, while 2. is obviously verified.

• t = H ∀αAi ai . This case is not possible, for Γ t : ∃α P or Γ t : P.

• t = H P . In this case, 1. and 2. are trivially true.

• t is obtained by an elimination rule and we can write it as r t 1 t 2 . . . t n where r is not an application (this notation has been explained in Section 2). Notice that in this case r cannot be a redex neither a term of the form u

| | | | | | | | a v nor u | v
because of the permutation rules and t ∈ NF. We have now two cases:

1. r = x i (resp. r = H P ). Then, since Γ x i : P i (resp. Γ H P : P), we have that for each i, either t i is π j or Γ t i : Q, where Q is a propositional formula. By induction hypothesis, each t i satisfies 1. and thus also t. 2. is obviously verified.

2. r = H ∀αiAi ai . Then, t 1 is m, for some closed term of L. If A i is not simply universal, we obtain that t satisfies 1., for t = H ∀αiAi ai m t 2 . . . t n . If A i = ∀γ 1 . . . γ k Q, with Q propositional, we have that for each i, either t i is a closed term m i of L or t i is π j or Γ t i : R, where R is a propositional formula. By induction hypothesis, each t i satisfies 1. and thus also t. 2. is obviously verified.

If we omit parentheses, every normal proof-term can be written as v 0 | v 1 | . . . | v n , where each v i is not of the form u | v; if for every i, v i is of the form (m i , u i ), then we call the whole term an Herbrand normal form, because it is essentially a list of the witnesses appearing in an Herbrand disjunction. Formally: Definition 9 (Herbrand Normal Forms). We define by induction a set of proof terms, called Herbrand normal forms, as follows:

• Every normal proof-term (m, u) is an Herbrand normal form;

• if u and v are Herbrand normal forms, u | v is an Herbrand normal form.

Our last task is to prove that all quasi-closed proofs of a simply existential statement ∃α P include an exhaustive sequence m 1 , m 2 , . . . , m k of possible witnesses.

Theorem 3 (Herbrand Disjunction Extraction). Let ∃α P be any closed formula where P is negative. Suppose Γ t : ∃α P, t is quasi-closed and t → * t ∈ NF. Then Γ t : ∃α P and t is an Herbrand normal form

(m 0 , u 0 ) | (m 1 , u 1 ) | . . . | (m k , u k ) Moreover, Γ P[m 1 /α] ∨ • • • ∨ P[m k /α].
Proof. We proceed by induction on t . By the Subject Reduction Theorem 1, t : ∃α P. By Proposition 4, t can only have three possible shapes:

1. t = u | | | | | | | | a v.
We show that this cannot happen. First, a must occur free in u, otherwise t / ∈ NF. By Proposition 4, we have two possibilities. i) Every occurrence in u of every term H ∀αiAi ai , with a i free, is of the active form H ∀αiAi ai m, where m ∈ L; in particular this is true when a i = a, which implies t / ∈ NF. ii) u has an active subterm of the form H ∀αiAi ai m, for some non simply universal formula A i and m ∈ L: since t is quasi-closed, a i = a, which again implies t / ∈ NF. In any case, we have a contradiction. 2. t = u | v; then, by induction hypothesis, u, v are Herbrand normal forms, and thus by definition 9, t is an Herbrand normal form as well. 3. t = (m, u); then, we are done.

We have thus shown that t is an Herbrand normal form

(m 0 , u 0 ) | (m 1 , u 1 ) | . . . | (m k , u k )
Finally, we have that for each i, Γ i u i : P[m i /α], for the very same Γ i that types (m i , u i ) of type ∃α P in t . Therefore, for each i,

Γ i u + i : P[m 1 /α] ∨ • • • ∨ P[m k /α], where u + i is of the form ι i1 (. . . ι i k (u i ) . . .). We conclude that Γ u + 0 | u + 1 | . . . | u + k : P[m 1 /α] ∨ • • • ∨ P[m k /α]
We suggest to interpret an Herbrand normal form (m 0 , u 0 ) | (m 1 , u 1 ) | . . . | (m k , u k ) in the following way. Each (m i , u i ) represents the result of an intuitionistic computation of a witness in a possible universe; each time in an intuitionistic computation an exception is raised, a pair of alternative universes is generated. For each particular computation of each of the parallel universes to go through, one needs to replace symbols of the form W ∃αA a with actual terms of L (those are the only symbols that can really block the computation). These witnesses have been obtained by communication coming from other intuitionistic computations in other parallel universes. It is that process of interaction and dialogue between different possible computations that generates the Herbrand normal forms. Define LJ as IL plus an axiom ⊥ → P for every atomic formula P . Then LJ proves the full ex falso quodlibet axiom scheme, that is, ⊥ → A for every formula A.

The goal of this section is to prove that, for every formula A, LJ + EM A ∨ ¬A. We essentially follow the technique of [1], but with several simplifications, since in part we need weaker results. Namely, we show that every formula is equivalent in LJ + EM to a prenex formula with alternating quantifiers. Since LJ + EM proves the excluded middle for such formulas, the result follows.

We start by proving a handful of simple facts. First, we prove that A ⊥ expresses the negation of A, even in an intuitionistically stronger way, since A ⊥ implies ¬A in LJ, and then as a corollary we obtain the provability of A ∨ ¬A for prenex formulas. Then, we prove a result about moving universal quantifiers outwards, which only holds classically; it will be needed for transforming disjunctions in prenex formulas. Finally, we show the classical equivalence between A → B and A ⊥ ∨ B. Proposition 5. For all prenex formulas with alternating quantifiers A, B, the following hold: Proof. We begin with the following observation. Since LJ + EM proves the excluded middle for every atomic formula, LJ + EM proves every classical propositional tautology, in particular (P ∨ Q) ↔ (¬P → Q) and therefore that every propositional formula is equivalent to a negative one. Therefore, LJ + EM F ∨ F ⊥ , for every prenex formula with alternating quantifiers F . 1. By induction on A and by cases according to the shape of A.

• If A is propositional, then either A ⊥ = ¬A = A → ⊥; or A = ¬B and A ⊥ = B. In both cases, the thesis is trivial.

• We are now able to show that every formula can be proved equivalent to a prenex one with alternating quantifiers and thus that the full excluded middle is provable in LJ + EM.

Theorem 4 (Provability of full Excluded Middle).

1. For every formula A, there is a prenex formula with alternating quantifiers A such that LJ + EM A ↔ A . 2. For every formula A, LJ + EM A ∨ ¬A.

Proof.

1. By induction on the number of symbols in A.

• If A is atomic, then A is trivially prenex and the thesis follows.

• If A = ∀αB, then by induction hypothesis LJ + EM B ↔ B, for some prenex formula with alternating quantifiers B. Then LJ + EM A ↔ ∀αB and, provided β does not occur in B, LJ + EM A ↔ ∀α∃βB. Since either ∀αB or ∀α∃βB has alternating quantifiers, we are done.

• If A = ∃αB, the proof is similar to the previous case.

•

am,

  then an exception is raised in u | | | | | | | | a v and passed to v ( | | | | | | | | stands for a sequence of n + 1 bars in the case of EM n ).

Figure 1 :

 1 Figure 1: Term Assignment Rules for IL + EMWe assume that in the proof terms three distinct classes of variables appear: one is made by the variables

  . The reduction rules for EM n model the exception handling mechanism explained in Section §1. Raising an exception e in u | | | | | | | | a v removes some (actually, the active ones) occurrences of hypotheses H ∀αA a in u and all occurrences of hypotheses W ∃αA a in v, introducing simpler hypotheses; we define first an operation removing them, and denoted v[a := e]. Definition 2 (Exception Substitution). Suppose v is any proof term and e = (m, b), where m is a term of L and b an EM-hypothesis variable b or the empty string . Then: 1. If b = and every free occurrence of a in v is of the form W ∃αP a , we define v[a := e] Reduction Rules for IL

  whenever u has some active subterm H ∀αA a m, e = (m, b) and b is either a fresh EM-hypothesis variable b or the empty string in case | | | | | | | | = | .

Figure 2 : 4 .

 24 Figure 2: Reduction Rules for IL + EM

  does not occur free in u). This rule says that no free hypothesis of the shape H ∀αA a : ∀αA occurs in u and thus it is unnecessary in the proof and in the computation; consequently, the proof termu | | | | | | | | a vmay be simplified to u and the computation carries on following only the reduction tree of u. In this case the exceptional partv of u | | | | | | | | a v is never used. 2. The second EM n -reduction: u | | | | | | | || | a v → v[a := e] | | | | | | | | b (u[a := e] | | | | | | | || | a v) (where u has some active subterm H ∀αA a m and e = (m, b)). This rule says that the "active" hypothesis H ∀αA a m : A[m/α], automatically raises in u | | | | | | | || | a v the exception e. The raise of the exception (remember that it is related to the hypothesis variable a) has the following effects: i) we perform the exception substitution [a := e] in v (Definition 2). This means that we replace each occurrence of the term W ∃αA ⊥ a corresponding to a free occurrence of a in v by (m, H A ⊥ [m/α] b ) or (m, H A ⊥ [m/α] ), according as to whether A is propositional or not. This way, we add the exceptional part v[a := e] of u | | | | | | | || | a v to the computation as the left side of the sequence of bars | | | | | | | | b . If b is not the empty string , the new variable b, guaranteed to be "fresh" by definition, corresponds to the newly made hypothesis A ⊥ [m/α] that ensures, in this "universe", that m is a correct witness for ∃αA ⊥ . ii) on the right side of the | | | | | | | | b we have the term (u[a := e] | | | | | | | || | a v) obtained from u | | | | | | | || | a v by performing the substitution [a := e] in u. The substitution removes all the occurrences of H ∀αA a m in u, which are consumed by the raise of the corresponding exception e, and replaces them with a new simpler hypothesis W A[m/α] b

  a m); as a consequence, in the possible further reduction of the subterm u[a := e] | | | | | | | || | a v an exception corresponding to the variable a may be raised again. Notice that u a v reduces to v[a := e] | (u[a := e] a v), with e = (m, ) by definition. Following our notational conventions, in this case | | | | | | | || | a is a and | | | | | | | | b is simply | , that is, |. Moreover, the occurrences of W ∃αA ⊥ a in v are replaced by (m, H A ⊥ [m/α] ) and the occurrences of H ∀αA a m in u are replaced by H A[m/α] . We also point out that | | | | | | | | b is always a strictly shorter sequence of bars with respect to the sequence | | | | | | | || | a and, on the logical side, the formula A[m/α] is of strictly lower complexity with respect to the complexity of the hypothesis ∀αA. Definition 3 (Normal Forms and Strongly Normalizable Terms).

  and u are assigned type B in the first term, then v[a := e] and u[a := e] can still be given type B in the second term, because the only subterms involved in the substitution are of the form H ∀αA a m and W ∃αA a and are always replaced with terms of the same type: respectively, with W A[m/α] b (or H A[m/α] ) and (m, H A[m/α] b ), for some fresh b. Moreover, m is closed and b, which is now free in v[a := e] and u[a := e], is bound in the second term by the operator | | | | | | | | b , which ensures that in the reduction no new free variable is created. Theorem 1 (Subject Reduction). If Γ t : C and t → u, then Γ u : C. Proof. The proof that the reduction rules for IL and the permutation rules for EM preserve the type is completely standard. Thus we are left with the EM n -reductions. We first need to prove that for every closed term m of L and EM-hypothesis variable b not occurring in Γ and v, if we set e = (m, b) with b = b or b = , it holds that i) Γ, a : ∃α A v : B =⇒ Γ, b : A[m/α] v[a := e] : B ii) Γ, a : ∀α A v : B =⇒ Γ, a : ∀α A, b : A[m/α] v[a := e] : B We proceed by induction on the term v. When the last rule in the type derivation of v is an axiom, a rule for EM, conjunction, disjunction, implication, existential quantifier or a rule for universal quantifier introduction, the thesis follows immediately or by simple induction hypothesis: we just deal with the cases of axioms and implication, the others being similar. If v is a variable x or is of the form H ∀αA a or W ∃αA a with a = a, then v[a := e] = v and the thesis is trivial. If v = W ∃αA a , then we are in case i), v[a := e] = (m, H A[m/α] b ) (with A propositional if b = , by Definition 2) and so Γ, b : A

  and we want to show i), then Γ, a : ∃α A w 1 : C → B and Γ, a : ∃α A w 2 : C. Since (w 1 w 2 )[a := e] = w 1 [a := e]w 2 [a := e] and by induction hypothesis Γ, b : A[m/α] w 1 [a := e] : C → B Γ, b : A[m/α] w 2 [a := e] : C we obtain Γ, b : A[m/α] w 1 w 2 [a := e] : C. ii) is analogous. If v = λx w, and we want to show ii) (again, i) is analogous), then B = C → D and Γ, x : C, a : ∀α A w : D. Since (λx w)[a := e] = λx (w[a := e]) and by induction hypothesis Γ, x : C, a : ∀α A, b : A[m/α] w[a := e] : D we obtain Γ, a : ∀α A, b : A[m/α] (λx w)[a := e] : C → D. When the last rule in the type derivation of v is a universal quantifier elimination, then v = w l, with l term of L. If w is not H ∀αA a or l is not m, then v[a := e] = w[a := e]l and one again concludes immediately by induction hypothesis. If w is H ∀αA a and l = m, then v[a := e] = W A[m/α] b (resp. v[a := e] = H A[m/α] ) and we are in case ii). Surely, Γ, a : ∀α A, b : A[m/α] W A[m/α] b (resp. Γ, a : ∀α A, b : A[m/α] H A[m/α] ). This concludes the proof. Now, we are ready to deal with the case of EM n -reductions. The reduction u | | | | | | | | a v → u, with a not occurring free in u, trivially preserves the type. So assume Γ u | | | | | | | || | a v : C and u | | | | | | | || | a v → v[a := e] | | | | | | | | b (u[a := e] | | | | | | | || | a v) where u has some active subterm H ∀αA a m, e = (m, b) and b is fresh. Then, Γ, a : ∀α A u : C and Γ, a : ∃α A ⊥ v : C. By what we have just proved, we obtain Γ, a : ∀α A, b : A[m/α] u[a := e] : C Γ, b : A

C 3 .

 3 The System IL + EM : a Leap into Non-Determinism

Figure 3 :

 3 Figure 3: Reduction Rules for IL + EM

  where u has some active subterm H ∀αA a m and e = (m, b)). We verify indeed -by choosing the appropriate reduction rule for | | | | | | | || | and applying the EM reduction rules

  and we are done. We proceed by triple induction on the number of bars in | | | | | | | || | and the ordinal heights of the reduction trees of u, v. Let us consider the first reduction step: u| | | | | | | || | v z * ι i (w). If z = u or z = v, we are done. If z = u | | | | | | | || | v or z = u | | | | | | | || | v ,with u u and v v , we obtain u * ι i (w) or v * ι i (w) by induction hypothesis applied to z. If z = v | | | | | | | | (u -| | | | | | | || | v), where u -is the term obtained from u by replacing some occurrences of a subterm (H ∀αA )m with W A[m/α] (or H A[m/α] ), then u + u -. Therefore, by induction hypothesis applied to z, either v * ι i (w) or u -| | | | | | | || | v * ι i (w). In the first case, we are done; in the second, by induction hypothesis applied to u -| | | | | | | || | v, we obtain u u - * ι i (w) or v * ι i (w), which completes the proof.

3 . 6 . 7 .

 367 If R is a ∨I rule, say left (the other case is symmetric), then w = ι 0 (u), A = B ∨ C and Γ u : B. So, w = ι 0 (u). By induction hypothesis u r B. Hence, u ∈ SN . Moreover, suppose ι 0 (u) * ι 0 (v). Then u * v and thus by (CR2) v r B. We conclude ι 0 (u) r B ∨ C = A. 4. If R is a ∨E rule, then w = u[x.w 1 , y.w 2 ] and Γ u : B ∨ C, Γ, x : B w 1 : D, Γ, y : C w 2 : D, A = D. By induction hypothesis, we have u r B ∨ C; moreover, for every t r B, we have w 1 [t/x] r D and for every t r C, we have w 2 [t/y] r D. By Proposition 3, we obtain w = u[x.w 1 , y.w 2 ] r D. 5. If R is the → E rule, then w = ut, Γ u : B → A and Γ t : B. So w = ut r A, for u r B → A and t r B by induction hypothesis. If it is the → I rule, then w = λx u, A = B → C and Γ, x : B u : C. So, w = λx u, since we may assume x = x 1 , . . . , x k . For every t r B, by induction hypothesis on u, u[t/x] r C. Therefore, by Proposition 3, λx u r B → C = A. The cases R = ∧E and R = ∧I are straightforward. 8. The cases R = ∃I and R = ∃E are similar respectively to ∨I and ∨E. 9. If R is the ∀E rule, then w = ut, A = B[t/α] and Γ u : ∀αB. So, w = ut. By inductive hypothesis u r ∀αB and so ut r B[t/α].

11 .

 11 If R is the EM rule, then w = u | | | | | | | | v, Γ, a : ∀αB u : C and Γ, a : ∃αB ⊥ v : C and A = C. By induction hypothesis, u, v r C. By (CR4), we conclude w = (u | | | | | | | | v) r C. 3.4. Strong Normalization of IL + EM and IL + EM As corollary, one obtains strong normalization for IL + EM . Corollary 1 (Strong Normalization for IL + EM ). Suppose Γ t : A in IL + EM . Then t ∈ SN .

4. 1 . 1 P

 11 On the Failure of the Church-Rosser Property The system IL + EM does not enjoy the Church-Rosser property. Given three arbitrary constants c, d, e of L, we can exhibit a typed proof term having at least two, distinct normal forms and even giving rise to two distinct Herbrand disjunctions: u := (d, λb.b((λz.H ∀αP a c)(H ∀αP a e))) || a W ∃α¬P a [(α, y).(α, λz.y)] u can be assigned type ∃α. (P(c) → ¬P(d)) → ¬P(α)by decorating the following natural deduction tree:P(c) → ¬P(d) [∀αP(α)] EM c) → ¬P(d)) → ¬P(d) ∃α.(P(c) → ¬P(d)) → ¬P(α) [∃α.¬P(α)] EM 1 ¬P(α) (P(c) → ¬P(d)) → ¬P(α) ∃α.(P(c) → ¬P(d)) → ¬P(α) ∃α.(P(c) → ¬P(d)) → ¬P(α) EM 1 ∃α.(P(c) → ¬P(d)) → ¬P(α)The first computation of the normal form of u we propose gives priority to exceptions: we immediately raise, in sequence, the two exceptions contained in the subterms H ∀αP a c and H ∀αP a e respectively. If we set l := W ∃α¬P a [(α, y).(α, λz.y)], we can reduce u as follows: u → (c, H ¬P(c) )[(α, y).(α, λz.y)] | (d, λb.b((λz.H P(c) )(H ∀αP a e))) || a l → (c, H ¬P(c) )[(α, y).(α, λz.y)] | (e, H ¬P(e) )[(α, y).(α, λz.y)] | (d, λb.b((λz.H P(c) )H P(e) )) || a l → * (c, H ¬P(c) )[(α, y).(α, λz.y)] | (e, H ¬P(e) )[(α, y).(α, λz.y)] | (d, λb.b H P(c) ) → * (c, λz.H ¬P(c) ) | (e, λz.H ¬P(e) ) | (d, λb.b H P(c) ) This last Herbrand normal form yields as witnesses for the Herbrand disjunction c, e, d. The second computation of the normal form of u fires first the only lambda redex contained on the left side of the || a operator before rising the leftmost exception (the one raised by the active subterm H ∀αP a c). The redex erases the active subterm H ∀αP a e, losing forever the possibility of raising the corresponding exception; thus, e will not become one of the witnesses for the Herbrand disjunction. As a consequence, we obtain a different normal form for u: u → (d, λb.b(H ∀αP a c)) || a l → (c, H ¬P(c) )[(α, y)(α, λz.y)] | (d, λb.b H P(c) ) a l → (c, H ¬P(c) )[(α, y)(α, λz.y)] | (d, λb.b H P(c) ) → (c, λz.H ¬P(c) ) | (d, λb.b H P(c) ) This last Herbrand normal form yields as witnesses for the Herbrand disjunction c, d, leaving outside the somewhat redundant e. Appendix A. Provability of Excluded Middle in LJ + EM

1 .

 1 LJ, A, A ⊥ ⊥ 2. LJ + EM A ∨ ¬A 3. LJ + EM (∀α.A ∨ B) ↔ (∀αA ∨ B), whenever α does not occur in B 4. LJ + EM (A → B) ↔ (A ⊥ ∨ B)

2 .

 2 If A = ∀αB, then A ⊥ = ∃αB ⊥ . By induction hypothesis, LJ, B, B ⊥ ⊥ therefore the derivationLJ, A, A ⊥ ∃αB ⊥ LJ, A, A ⊥ , B ⊥ , B ⊥ LJ, A, A ⊥ , B ⊥ B → ⊥ LJ, A, A ⊥ , B ⊥ ∀αB LJ, A, A ⊥ , B ⊥ B LJ, A, A ⊥ , B ⊥ ⊥ LJ, A, A ⊥ ⊥yields the thesis.• If A = ∃αB, then A ⊥ = ∀αB ⊥ . But we have already proved that by induction hypothesis,LJ, B, B ⊥ ⊥ therefore the derivation LJ, A, A ⊥ ∃αB LJ, A, A ⊥ , B ⊥ , B ⊥ LJ, A, A ⊥ , B B ⊥ → ⊥ LJ, A, A ⊥ , B ⊥ ∀αB ⊥ LJ, A, A ⊥ , B ⊥ B ⊥ LJ, A, A ⊥ , B ⊥ LJ, A, A ⊥ ⊥yields the thesis. By the previous point, LJ + EM, A ⊥ ¬A. Since LJ + EM A ∨ A ⊥ , we have that by disjunction elimination, LJ + EM A ∨ ¬A. 3. For sure, LJ (∀αA ∨ B) → (∀α.A ∨ B), so let us show the converse. Indeed, since we can derive LJ + EM, ∀α.A ∨ B, B ⊥ ∀αA byLJ + EM, ∀α.A ∨ B, B ⊥ ∀α.A ∨ B LJ + EM, ∀α.A ∨ B, B ⊥ A ∨ B LJ + EM, ∀α.A ∨ B, B ⊥ , A A LJ + EM, ∀α.A ∨ B, B, B ⊥ ⊥ LJ + EM, ∀α.A ∨ B, B, B ⊥ A LJ + EM, ∀α.A ∨ B, B ⊥ A LJ + EM, ∀α.A ∨ B, B ⊥ ∀αA the following is a derivation of LJ + EM, ∀α.A ∨ B ∀αA ∨ B LJ + EM B ∨ B ⊥ LJ + EM, ∀α.A ∨ B, B B LJ + EM, ∀α.A ∨ B, B ∀αA ∨ B LJ + EM, ∀α.A ∨ B, B ⊥ ∀αA LJ + EM, ∀α.A ∨ B, B ⊥ ∀αA ∨ B LJ + EM, ∀α.A ∨ B ∀αA ∨ B 4. For sure, using 1., LJ (A ⊥ ∨ B) → (A → B). Let us show that LJ + EM (A → B) → (A ⊥ ∨ B). Indeed, LJ + EM A ∨ A ⊥ LJ + EM, A → B, A B LJ + EM, A → B, A A ⊥ ∨ B LJ + EM, A → B, A ⊥ A ⊥ LJ + EM, A → B, A ⊥ A ⊥ ∨ B LJ + EM, A → B A ⊥ ∨ B

  If A = B ∧ C, then by induction hypothesis LJ + EM B ↔ B and LJ + EM C ↔ C , for some prenex formulas with alternating quantifiers B, C . Since LJ + EM (B ∧ C) ↔ (B ∧ C ), it is enough to show the thesis for B ∧ C . We proceed by induction on the number of its symbols. If B = ∀αD, then, assuming without loss of generality that α does not occur in C , it is an elementary fact that LJ (∀αD ∧ C ) ↔ ∀α. D ∧ C and the thesis follows by induction hypothesis applied to D ∧ C . If B = ∃αD, then, assuming without loss of generality that α does not occur in C , it is an elementary fact that LJ (∃αD ∧ C ) ↔ ∃α. D ∧ C and the thesis follows by induction hypothesis applied to D ∧ C . The other cases are symmetric. • If A = B ∨ C, then by induction hypothesis LJ + EM B ↔ B and LJ + EM C ↔ C , for some prenex formulas with alternating quantifiers B, C . Since LJ + EM (B ∨ C) ↔ (B ∨ C ), it is enough to show the thesis for B ∨ C . We proceed by induction on the number of its symbols. If B = ∀αD, then, assuming without loss of generality that α does not occur in C , by proposition 5, point 3, we have LJ + EM (∀αD ∨ C ) ↔ ∀α. D ∨ C and the thesis follows by induction hypothesis applied to D ∨ C . If B = ∃αD, then, assuming without loss of generality that α does not occur in C , it is an elementary fact that LJ (∃αD ∨ C ) ↔ ∃α. D ∨ C and the thesis follows by induction hypothesis applied to D ∧ C . The other cases are symmetric. • If A = B → C, then by induction hypothesis LJ + EM B ↔ B and LJ + EM C ↔ C , for some prenex formulas with alternating quantifiers B, C . We thus have LJ+EM (B → C) ↔ (B → C ); moreover, by proposition 5, LJ + EM (B → C ) ↔ (B ⊥ ∨ C). But we have just proved in the previous case that B ⊥ ∨ C is equivalent in LJ + EM to a prenex formula with alternating quantifiers, which concludes our proof.2. By point 1, for every formula A there is a prenex formula with alternating quantifiers A such that LJ + EM A ↔ A . Since by proposition 5, point 2, LJ + EM A ∨ ¬A , we have LJ + EM A ∨ ¬A.

  1. t r P if and only if t ∈ SN 2. t r A ∧ B if and only if t π 0 r A and t π 1 r B 3. t r A → B if and only if for all u, if u r A, then tu r B 4. t r A ∨ B if and only if t ∈ SN and t * ι 0 (u) implies u r A and t * ι 1 (u) implies u r B 5. t r ∀αA if and only if for every term m of L, tm r A[m/α] 6. t r ∃αA if and only if t ∈ SN and for every term

  Corollary 2 (Strong Normalization for IL + EM). Suppose Γ t : A in IL + EM. Then t ∈ SN. Proof. By Proposition 1, any infinite reduction t = t 1 → t 2 → . . . → t n → . . . in IL + EM gives rise to an infinite reduction t * = t * + . . . in IL + EM . By the strong normalization Corollary 2 for IL + EM and since clearly Γ t * : A, infinite reductions of the latter kind cannot occur; thus neither of the former.

	1	+ t * 2	+ . . . + t * n

  Γ, a : ∀β A u : ∃α P (resp. u : P) and Γ, a : ∃β A ⊥ v : ∃α P (resp. v : P). We first observe that a must occur free in u:otherwise, t = u | | | | | | | | a v u,which would yield a contradiction to t ∈ NF. Now, by induction hypothesis, 1. holds with respect to u. Moreover, it cannot be that every occurrence in u of every hypothesis variable a i or a corresponds to an active term: otherwise, in particular, u would have an active subterm of the form H ∀βA

a m, for some m ∈ L, and thus t

This work was partially supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR)

Partially supported by LINTEL (Linear Techniques For The Analysis of Languages), https://sites.google.com/site/tolintel/

a: ∀α A Γ, a : ∃α A W ∃αA a : ∃α A Γ, a : P H P : PConjunction Γ u : A Γ t : B Γ u, t : A ∧ B Γ u : A ∧ B Γ u π 0 : A Γ u : A ∧ B Γ u π 1 : B Implication Γ t : A → B Γ u : A Γ tu : B Γ, x : A u : B Γ λx u : A → B Disjunction Introduction Γ u : A Γ ι 0 (u) : A ∨ B Γ u : B Γ ι 1 (u) : A ∨ B Disjunction Elimination Γ u : A ∨ B Γ, x : A w 1 : C Γ, y : B w 2 : C Γ u [x.w 1 , y.w 2 ] : C Universal Quantification Γ u : ∀αA Γ um : A[m/α] Γ u : A Γ λα u : ∀αAwhere m is any term of the language L and α does not occur free in any formula B occurring in Γ.ExistentialQuantification Γ u : A[m/α] Γ (m, u) : ∃αA Γ u : ∃αA Γ, x : A t : C Γ u [(α, x).t] : C

Definition 8 (Reducibility Candidates). Extending the approach of [START_REF] Girard | Proofs and Types[END_REF], we define four properties (CR1), (CR2), (CR3), (CR4) of reducible terms t:

(CR1) If t r A, then t ∈ SN .

(CR2) If t r A and t * t , then t r A.

(CR3) If t is neutral and for every t , t t implies t r A, then t r A.

We now prove, as usual, that every term t possesses the reducibility candidate properties. The arguments for establishing (CR1), (CR2), (CR3), are in many cases standard (see [START_REF] Girard | Proofs and Types[END_REF]).

Proposition 2. Let t be a term of IL + EM . Then t has the properties (CR1), (CR2), (CR3), (CR4).

Proof. By induction on C.

• C is atomic. Then t r C means t ∈ SN . Therefore (CR1), (CR2), (CR3) and the left-to-right implication of (CR4) are trivial.

, where u -is the term obtained from u by replacing some occurrences of a subterm

we conclude, again by induction hypothesis, that z ∈ SN .

(CR1). Suppose t r A → B. By induction hypothesis (CR3), for any variable x, we have x r A. Therefore, tx r B, and by (CR1), tx ∈ SN , and thus t ∈ SN .

(CR2). Suppose t r A → B and t t . Let u r A: we have to show t u r B. Since tu r B and tu t u, we have by the induction hypothesis (CR2) that t u r B.

(CR3). Assume t is neutral and t t implies t r A → B. Suppose u r A; we have to show that tu r B. We proceed by induction on the ordinal height of the reduction tree of u (u ∈ SN by induction hypothesis (CR1)). By induction hypothesis, (CR3) holds for the type B. So assume tu z; it is enough to show that z r B. If z = t u, with t t , then by hypothesis t r A → B, so z r B. If z = tu , with u u , by induction hypothesis (CR2) u r A, and therefore z r B by the induction hypothesis relative to the size of the reduction tree of u . There are no other cases since t is neutral.


As a matter of fact, they are made of thousands of stars -at minimum -and, in the contrary of galaxies, they do not contain gas or other dissipative components. Hence, excepting the fact that stars are not punctual, they corresponds exactly to their mathematical modelisation.

The observation of globular clusters reveals that they are characterized by a spherical distribution of their mass.

By consequence, their volumic mass density is a radial function ρ = ρ (r). This density corresponds to the marginal distribution in position space of the total distribution function in the whole phase space : this is a mean field description. In this model the gravitational potential ψ of the cluster is solution of the Poisson equation ∆ψ = 4πGρ, it is then radial too : ψ = ψ (r). The r variable represents the distance between the center of mass of the system and a test star evolving in the mean field potential of the cluster. This test star of mass m experiences a force given by F = -m∇ψ, which is already radial. In this context, it is very well known that its trajectory is contained in a plane. In this plane, the orbit is determined by the total energy E and the squared angular momentum L 2 of the star. These two quantities are conserved during the motion.

The description of the whole dynamics of a globular cluster is then possible when its gravitational potential ψ is given. Three possibilities exists to do this :

-Extract ρ (r) and ψ (r) from observational data. It is a rough and empirical manner, but it is necessary to fix ideas. -Compute ρ (r) and ψ (r) from numerical simulations. But the parameter's space of the result is wide for this kind of experiments. -Propose fundamental physical arguments in order to select a model through all theoretical possibilities. The two first ways are very used and a plenty of references give refined to rough descriptions of globular clusters since their formation until the end of their actual or numerical evolution (see [START_REF] Heggie | The Gravitational Million-Body Problem -A Multidisciplinary Approach to Star Cluster Dynamics[END_REF]). The last way is by far the least used. Michel Hénon's paper [START_REF] Hénon | L'amas isochrone[END_REF] about isochrone cluster, published in french in "Annales d'Astrophysiques" is very representative of this way to do which count no more than a ten of reference in more than two centuries of globular cluster modelisation ! In this paper, we will follow Michel Hénon's paper in a first part to analyze in a second part its influence under gravitational dynamicists community, giving finally a modern reading of the result. I. The isochrone model

As we mention before, the motion of a given star in a spherical globular cluster is contained in a plane. In this plane the two parameters of the orbit are its energy E and its squared angular momentum L 2 . Both these two parameters contribute to the definition of the gravitational potential of the cluster ψ (r) and to the computation of the distance r between the star and the center of mass of the cluster. This contribution is resumed in the definition of the energy of the star

(1) E = m 2 dr dt 2 + L 2 2mr 2 + mψ (r) = cste
Imposing that the total mass of the system 1 is finite, the effective potential

ψ e (r) = L 2 2mr 2 + mψ (r) is such that lim r→0 ψ e (r) = +∞.
At the edge of the system, up to an additive constant, the potential is on the form ψ (r) r→+∞ ∼ -GM/r, where M the total mass of the cluster. Hence, lim r→+∞ ψ e (r) = 0 -. This effective potential is also the place where dr dt = 0, its behavior is represented on figure 1.

When the considered star belongs to the cluster its total energy E is negative. The extreme value E = E c < 0 corresponds to an orbit for which r = r c = cste, it is then circular. For each value of E ∈ ]E c , 0[, the distance is such that r ∈ [r p , r a ]. The extreme values of the radius are the periastron for r p and the apoastron for r a . The time for the transfer from r p to r a is given by

(2) τ 2 = t p t a dt = r p r a dt dr dr = r p r a dr 2 E m -ψ (r) - L 2 m 2 r 2
where we have used the energy to get dr dt . The problem being symmetrical, if this integral is finite, we have r a = r (t a ) = r (t a + τ). The expression (1) of the energy is in fact an ordinary differential equation, fulfilled by both r (t) and r (t + τ). These two functions are then equal when t = t a , the Cauchy criterion -which is supposed valid for this problem -then tell us that they are equal at each time : the distance between the center of mass of the cluster and the star is then a τ-periodic function. The inspection of the relation [START_REF] Hénon | L'amas isochrone[END_REF] shows that, if it exists, the radial period is such that τ = τ E, L 2 . The mass of the star is another parameter of the period which is not under interest in this study. The radial period is computable at least in two fundamental cases :

1. The total mass M of a spherical self-gravitating system is given by the integral of the density over the whole space. In spherical coordinates, using the Poisson equation, this gives -The Kepler potential ψ (r) = -GM/r, where M is the total mass of the cluster. It is the well-known two body problem for which Kepler's third law gives τ = πGM √ 2 (-E) -3/2 . It is also the limit potential viewed by a star of the cluster always evolving in far from center regions.

M = 1 G lim r→∞ r
-The harmonic potential ψ (r) = 2 3 πGρr 2 , where ρ is the constant density of a homogeneous cluster, for which τ = 3π 4Gρ . Using the virial theorem, one can show that ρ depends only of the energy of the considered star and the total mass of this homogeneous system. The central regions of a globular clusters are usually considered as homogenous ones, the gravitational potential is harmonic at the center of such systems. A centrally confined star could then have a radial period depending only of its energy E. Both centrally or far from center confined orbits are then characterized by radial periods which do not depends on the squared angular momentum. In his 1958 paper, Michel Hénon conjectures that this property could propagates to all orbits of all stars of a globular system. This so called "isochrone" property, could be a fundamental physical property allowing to determine the other properties of globular clusters.

Thus, Michel Hénon proposes to find the most general potential ψ i (r) such that

τ = 2 r p r a dr 2 E m -ψ i (r) - L 2 m 2 r 2 = τ (E)
To do this he doesn't use the effective potential but introduces new variables x = 2r 2 and y (x) = xψ i (x) . x y x ( ) Fixing m = 1, the radial period then writes

E x L -0 2 E x L -1 2 x 0 x a
τ = x p x a dx Ex -L 2 -y (x)
x p and x a being the values of x to the periastron and apoastron, roots of the equation y (x) = Ex -L 2 . Due to the finite mass of the y (x) must have infinite branches. In order to identify x p and x a , Michel Hénon then propose a graphical study of the problem. This representation is an alternative of the effective potential theory, it is full of sense and forms a new way for the study of such systems. This graphical study is illustrated in the figure 2.

By an explicit calculus of the radial period in terms of x and y, Michel Hénon shows that τ depends only on the energy E if and only if

P 0 I ∝ (P p,1 P a 1 ) 2
This condition is fulfilled if and only if y (x) is a parabola.

The physical parameters of the problem are

ψ 0 = lim r→0 ψ (r) , ψ ∞ = lim r→+∞ ψ (
r) and the total mass M.

Three cases can be considered :

-If ψ 0 → -∞, it is always possible to choose a reference for the potential such that ψ ∞ = 0. The equation for y (x) is then

y (x) = -GM √ 2x =⇒ ψ i (r) = - GM r
It is the keplerian potential associated to a central mass.

-If ψ 0 → -∞, it is always possible to choose a reference for the potential such that ψ 0 = 0. The equation for y (x) is now It is the harmonic potential. -If both ψ 0 and ψ ∞ are finite, choosing a reference for the potential such that ψ ∞ = 0, the equation for y (x) becomes

y (x) = 1 2 Kx 2 =⇒ ψ i (r) = Kr 2 i i "proc_JP_eng" -
y 2 + G 2 M 2 2ψ 0 y -2G 2 M 2 x = 0 =⇒ ψ i (r) = 0 1 + 1 + r 2 b 2 with b = - GM 2ψ 0 > 0
this is the general form introduced by Michel Hénon for his potential, the isochrone potential. The paper ends by a comparison between this new potential and the globular clusters data observation of this epoch. Michel Hénon finds a good agreement and conjectures a physical explanation : a resonance between orbits during the formation process of globular clusters could vanishes the L 2 dependence of the radial period. The history will forget progressively the isochrone model mainly because more and more observations will reveal that the potential density pair is trickier than a simple stationary model. In 1968 the empirical King model, with 3 free parameter, became the reference. Does the isochrone model, with only the parameter b, could be forgotten ? It should be a big error...

II. A modern lecture of the isochrone model

Isochrone cluster are characterized by a central structure of constant density, namely a core, surrounded by a halo. The size of the core is given by the parameter b of the model. The radial period of the isochrone model can be explicitly computed, it is given by the relation

τ = 2πGM (-2E) 3/2
Using Poisson equation one can give an explicit formula for the mass density

ρ (r) = M 4π 3ab (a + b) -br 2 a 3 (a + b) 3 with a 2 = r 2 -b 2
When r b, i.e. in the halo, the mass density is given by a power law ρ (r) ∝ r -4 . This property correspond to young globular clusters, i.e. characterized by a large two body encounters relaxation time (T c ) in comparison of the Hubble time.

In a numerical way, the equilibrium state with a core and a -4 halo slope structure corresponds to the post collapse state of an initial homogeneous sphere. These kind of systems are generally called "Hénon Spheres" since the pioneering numerical experiments of Michel Hénon in the sixties [START_REF] Hénon | L'évolution initiale d'un amas sphérique[END_REF]. They could correspond to one of the globular clusters formation process. After this formation process which takes a few dynamical times (T d ), such a system evolves under collisional effects under very more longer times, order of them is given by the two body encounters relaxation time (T c N ln N T d , where N is the number of stars in the system). During this slow evolution the extension of the core shrinks progressively and the slope of the halo passes from -4 to -2. At the end of this evolution, the system become unstable and the core collapses under the pressure of the halo. On the century of globular clusters orbiting in our galaxy, 80% have a core-halo structure with slope in the interval [-4, -2] and 20% are said core-collapsed. The fine mechanisms of this evolution begins to be well understood, but, the question of the initial equilibrium state at the beginning of this evolution is always an open problem. In this context, the Michel Hénon's isochrone idea seems to be one of the possible physical explanations.

Very few research are done in order to verify Michel Hénon's conjecture about the resonant mechanism as the origin of the isochrone model. A confirmation of the existence of such a mechanism could be an important and elegant fact in the comprehension of globular clusters, in the direct line of Michel Hénon works.

  Sommaire I The isochrone model ........................................................................ 7 II A modern lecture of the isochrone model ............................................ 10 Bibliographie ........................................................................................ 12Globular clusters are cornerstones in the study of the dynamics of gravitationaly interacting systems of particles.

	i i	i i
	i	"proc_JP_eng" -2014/10/13 -11:20 -page 5 -#1 "proc_JP_eng" -2014/10/13 -11:20 -page 6 -#2	i i
		A marvelous contribution from Michel Hénon to
		globular cluster's study : the isochrone cluster
		Jérôme Perez
		Applied Mathematics Laboratory
		ENSTA ParisTech
	i i		i i
	i i	i i

  FIGURE 2. Illustration from Michel Hénon paper about the characteristic points and y (x) function.

		P a,1
	I
	P p,1
	P 0
	x p,1	,1