1 Introduction↩︎

The conceptual connection between Herbrand’s theorem and functional interpretation is well known. It was made explicit by Gerhardy and Kohlenbach in [1], in which Herbrand’s theorem is proved using a functional interpretation of the classical first-order predicate calculus. The approach to Herbrand extraction via functional interpretation was further explored by Ferreira and Ferreira [2], who developed a so-called “Herbrandized” functional interpretation for classical first-order logic (see also [3]). In both these works, we obtain the result that the realizer extracted from a proof of an existential formula, when reduced to normal form, describes the witnessing set of terms for a Herbrand disjunction. Thus, Herbrand’s theorem is elegantly located as a special case of functional interpretation.

These works form part of a quite large literature on various approaches to Herbrand’s theorem, using a variety of tools including proof nets [4], [5], expansion trees [6], [7] and game semantics [8]. The present work builds on an approach developed by Afshari, Hetzl and Leigh [9], and further in [10], [11], in which Herbrand disjunctions are extracted directly from sequent calculus proofs without relying on cut elimination. Functional interpretations, by contrast, are usually carried out for Hilbert-style axiomatic systems.

The idea of Herbrand schemes is to view a sequent calculus proof as a type of grammar, known as a higher-order recursion scheme. These grammars associate certain non-terminal symbols with formula occurrences in the end sequents of proofs, and these are supplied with rewrite rules depending on the last inference rule of the proof. For a proof of an existential formula, the language generated by the grammar is a set of witnessing terms for a Herbrand disjunction. Again, there is a connection with functional interpretation here, noted already in [9], in the use of higher-order types.

In this note we aim to further complete the emerging picture by showing how, using ideas from Herbrand schemes, we can derive realizing terms in a typed lambda-calculus similar to that used by Gerhardy and Kohlenbach directly from proofs in classical sequent calculus. These realizers allow us to construct Herbrand disjunctions for valid existential formulas. We thus obtain again a method to extract Herbrand disjunctions directly from sequent calculus proofs without relying on cut elimination, but this time using functional interpretation instead of a higher-order grammar.

A full presentation of Herbrand schemes would take up too much space here; the interested reader is advised to consult [9]–[11] for comparison. The results presented here are self-contained and do not require a previous understanding of Herbrand schemes. However, the procedure to extract realizing terms from proofs presented here was found by a close examination of the type structure and rewrite rules given in [9]. Indeed the way that term extraction works here remains very closely related to Herbrand schemes. In particular, we retain the following two features:

1. Each formula \(A\) is associated with two distinct types: an evidence type \([A]\) and a counter-evidence type \(\langle A \rangle\) (called “output” and “input” types in [9]).

2. For each proof, and each formula occurrence in the end sequent, we essentially construct a program that extracts evidence for that formula from potential counter-evidence for each formula occurence of the end sequent.

This program extraction is modular and pieces together programs extracted from immediate subproofs uniformly from the last inference rule used. In Herbrand schemes, these programs are represented by non-terminal symbols of the grammar with associated rewrite rules. If a sequent calculus proof \(p\) has end sequent \(A_1,\ldots,A_k\), then a Herbrand scheme associates with each index \(i\) a non-terminal symbol \(F^p_i\) of type: \[\Sigma \to \langle A_1 \rangle \to \dotsm \to \langle A_n \rangle \to [A_i]\] where \(\langle A_1 \rangle, \ldots, \langle A_n \rangle\) are the “counter-evidence types” of \(A_1,\ldots, A_n\) and \([A_i]\) is the evidence type of the \(i\)-th formula \(A_i\), and \(\Sigma\) is a distinguished type of “substitution stacks” (which will not be used here). Here, we will similarly associate with each proof of end sequent \(A_1,\ldots, A_n\) and index \(i\) a term of type \([A_i]\) parametric in given terms of types \(\langle A_1 \rangle,\ldots,\langle A_n \rangle\); we will call this assignment a term constructor. In contrast with Herbrand schemes, however, there is no need to specify particular ad hoc rewrite rules for these terms; once the term has been constructed, its behaviour follows from the basic rewrite rules of the type theory.

The approach of assigning explicit “evidence” and “counter-evidence” types to formulas has appeared before in connection with functional interpretation, in Pédrot’s “functional functional interpretation” [12] which build’s on de Paiva’s category-theoretical treatment of functional interpretation [13]. As far as we are aware, this approach has not previously been developed for classical logic and classical sequent calculus.

We believe this work provides further evidence of how natural the connection between functional interpretation and Herbrand’s theorem is: it turns out that Herbrand schemes can be reformulated as a functional interpretation of sequent calculus proofs. Furthermore, the functional interpretation described here has a conceptual connection with the game-theoretic analysis of Herbrand’s theorem described in [8], and provides a computational interpretation of sequent calculus as concurrent computation in the same spirit. We elaborate on this point in Section 4.3.

2 Types and terms↩︎

We begin by presenting the underlying type theory of our functional interpretation. We fix a first-order vocabulary \(\mathcal{L}\) and assume that it contains at least one individual constant \(c\) and at least one unary predicate \(P\), and we assume an infinite supply of individual variables. The set of \(\mathcal{L}\)-terms is formed in the usual way, where terms are formed from individual constants, variables and function symbols.

Our types are generated by the following grammar: \[U : = \iota \mid \Box \mid U \times U \mid U \to U\] We thus have two atomic types, a type \(\iota\) of individuals and a “null type” \(\Box\). These appear also in [9]–[11]. We will equate individual variables with variables of type \(\iota\). Complex types are formed by products and function space types.

Terms are constructed and typed according to the following rules, where we define the set \(\mathsf{Prop}\) of well-formed propositions by mutual recursion below:

We refer to terms that can be typed by these rules as \(\mathcal{L}^+\)-terms. Free variables of terms are defined as usual, and a closed term is one with no free variables. The operator \([*\;\mathsf{if}\; A \;\mathsf{else}\; *]\) is the case distinction operator from Gerhardy and Kohlenbach [1], and uses a proposition as parameter. The set of propositions is defined as follows:

Propositions: \[\begin{prooftree} \hypo{A \in \mathsf{Prop}} \hypo{B \in \mathsf{Prop}} \infer2{A \vee B \in \mathsf{Prop}} \end{prooftree} \qquad\qquad \begin{prooftree} \hypo{A \in \mathsf{Prop}} \infer1{\neg A \in \mathsf{Prop}} \end{prooftree}\] \[\begin{prooftree} \hypo{t_1 :\iota} \hypo{\dotsm} \hypo{t_n : \iota} \infer3{R(t_1,\ldots,t_n) \in \mathsf{Prop}} \end{prooftree} \quad\quad \begin{prooftree} \hypo{u_1 : U} \hypo{u_2 : U} \infer2{u_1 \equiv u_2 \in \mathsf{Prop}} \end{prooftree}\]

A first observation about our type theory is the following:

To give operational meaning to our terms we take the following rewrite rules:

The rewrite rule for \(\lambda\)-abstractions will be referred to as \(\beta\)-reduction as usual.

We introduce the propositional connectives \(\to, \wedge, \leftrightarrow\) by the usual abbreviations. We shall define a quantifier-free calculus \(\mathsf{QF}\) for reasoning with propositions as follows. As axioms we take every instance of a propositional tautology, every equation \(u \equiv v\) for convertible terms \(u,v\), plus the following axioms:

\[A \to [u\;\mathsf{if}\; A \;\mathsf{else}\; v] \equiv u \qquad \neg A \to [u\;\mathsf{if}\; A \;\mathsf{else}\; v] \equiv v\] As rules of inference, we take substitution and modus ponens:

\[\begin{prooftree} \hypo{A[u/x]} \hypo{u \equiv v} \infer2{A[v/x]} \end{prooftree} \qquad \begin{prooftree} \hypo{A} \hypo{A \to B} \infer2{B} \end{prooftree}\]

We write \(\vdash_{\mathsf{QF}}A\) if \(A\) is provable in \(\mathsf{QF}\), and sometimes write \(A_1,\ldots,A_n \vdash_{\mathsf{QF}}B\) to abbreviate the statement \(\vdash_{\mathsf{QF}}A_1 \wedge \ldots \wedge A_n \to B\). We write \(A \equiv B\), overloading notation, if \(\vdash_{\mathsf{QF}}A \leftrightarrow B\).

2.1 Semantics↩︎

Given a set \(D\) we define the full set theoretic type structure \(\{D_U\}_{U \in \mathsf{Types}}\) on \(D\) by induction on types as usual, so that \(D_{U \to V}\) is the set of all functions \(D_U \to D_V\), etc.

Given a first order structure \(M = (D,V)\), where \(D\) is the domain and \(V\) is the valuation of constants, function symbols and predicates, an assignment \(a\) is a map sending a variable \(z : U\) to an element of \(D_U\). We extend the assignment \(a\) to a map from arbitrary terms \(t : U\) to elements \(a(t) \in D_U\), and simultaneously define a satisfaction relation \(M,a \vDash A\) for \(A \in \mathsf{Prop}\), by the following clauses:

• \(a(c) = V(c)\) for an individual constant \(c\),

• \(a(f) = V(f)\) for a function symbol \(f\),

• \(a(uv) =\) the unique \(d \in D_V\) such that \((a(v),d) \in a(u)\), where \(u : U \to V\) and \(v : U\),

• \(a(\lambda x.u) = \{(d, a[d/x](u)) \mid d \in D_U\}\) where \(u : V\), \(x : U\) and the assignment \(a[d/x]\) is like \(a\) except \(a[d/x](x) = d\),

• \(a([u\;\mathsf{if}\; A \;\mathsf{else}\; v] ) = a(u)\) if \(M,a \vDash A\), otherwise \(a([u\;\mathsf{if}\; A \;\mathsf{else}\; v] ) = a(v)\),

• \(M, a \vDash R(u_1,\ldots,u_n)\) if \((a(u_1),\ldots,a(u_n)) \in V(R)\),

• \(M, a \vDash u \equiv v\) if \(a(u) = a(v)\),

• standard clauses for \(\vee, \neg\).

We can now state a soundness result for the quantifier free system:

3 Sequent calculus↩︎

3.1 Two-sided sequent calculus↩︎

Given our vocabulary \(\mathcal{L}\) we define \(\mathcal{L}\)-formulas and closed \(\mathcal{L}\)-sentences as usual, where as basic connectives we take disjunction, negation and the existential quantifier. As our proof system we shall take Gentzen’s \(\mathbf{G1c}\) sequent calculus as presented in [14], but restricted to our basic connectives.

Sequents are pairs of multisets of formulas. As our single axiom we take: \[\begin{prooftree} \hypo{} \infer1[\mathsf{id}]{A \vdash A} \end{prooftree}\] The remaing rules are given as follows:

In the rule \(\exists_L\), the eigenvariable \(\alpha\) is subject to the usual condition that it must not appear in the conclusion.

3.2 One-sided sequent calculus↩︎

The aim here is to extract a functional interpretation directly from sequent calculus proofs, so we want as much as possible to take proofs as they are and avoid proof-theoretic pre-processing. We will only perform a rather trivial proof translation in order to simplify notational matters a bit, and turn the two-sided sequent calculus \(\mathbf{G1c}\) into a one-sided sequent calculus. The usual approach to one-sided sequent calculus is to present formulas in negation-normal form, and regard negation as a recursively defined operation on formulas. However, it is implicit in that approach that left and right formula occurrences can be treated in a completely dual manner, and it turns out that we need an asymmetric treatment of left and right formula occurrences here. To retain this asymmetry, we will present the one-sided sequent calculus with an explicit negation.

Sequents are single multisets of formulas. As our single axiom we take: \[\begin{prooftree} \hypo{} \infer1[\mathsf{lem}]{\neg A, A} \end{prooftree}\] The remaining rules are given as follows:

In the \(\exists\)-rule, the term \(t\) occurring in the premiss is an \(\mathcal{L}\)-term. We can also consider an extended proof system that allows arbitrary \(\mathcal{L}^+\)-terms of type \(\iota\) to occur in formulas, and to occur in the premiss of an \(\exists\)-rule; we shall occasionally do this when convenient.

It is easy to translate any \(\mathbf{G1c}\)-proof of the sequent \(A_1,\ldots, A_k \vdash B_1,\ldots, B_m\) to a one-sided proof of the sequent \(\neg A_1,\ldots, \neg A_k, B_1,\ldots, B_m\). The only slight catch is that the \(\vee\)-rules in \(\mathbf{G1c}\) are presented as additive rules; again, it will be convenient here to break the symmetry and interpret the left rule as multiplicative while the right rule is treated as additive. This means that in the translation, we have to insert a series of contractions when we interpret the left \(\vee\)-rule.

If \(\Gamma\) is \(A_1,\ldots,A_n\) then we abbreviate \(\neg A_1,\ldots,\neg A_n\) by \(\neg \Gamma\). The translation \(\tau\) is defined recursively as follows:

\[\begin{prooftree} \hypo{} \infer1[\mathsf{id}]{A \vdash A} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{} \infer1[\mathsf{lem}]{\neg A, A} \end{prooftree}\]

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A \vdash \Delta} \infer1[\neg L]{\Gamma \vdash \neg A, \Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_0)} \infer1{\neg \Gamma, \neg A, \Delta} \end{prooftree}\] \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma \vdash A, \Delta} \infer1[\neg_R]{\Gamma,\neg A \vdash\Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_0)} \infer1{\neg \Gamma, A, \Delta} \infer1[\neg\neg]{\neg \Gamma, \neg \neg A, \Delta} \end{prooftree}\]

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma \vdash A[t/x],\Delta} \infer1[\exists_R]{\Gamma \vdash\exists x A, \Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_0)} \infer1{\neg \Gamma, A[t/x], \Delta} \infer1[\exists]{\neg \Gamma, \exists x A, \Delta} \end{prooftree}\]

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A[\alpha/x] \vdash\Delta} \infer1[\exists_L]{\Gamma, \exists x A \vdash\Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_0)} \infer1{\neg \Gamma, \neg A[\alpha/x], \Delta} \infer1[\neg \exists]{\neg \Gamma, \neg \exists x A, \Delta} \end{prooftree}\]

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma \vdash A_i,\Delta} \infer1[\vee_R]{\Gamma \vdash A_1 \vee A_2, \Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_0)} \infer1{\neg \Gamma, A_i, \Delta} \infer1[\vee]{\neg \Gamma, A_1 \vee A_2, \Delta} \end{prooftree}\]

\[\begin{prooftree} \hypo{p_1} \infer1{\Gamma, A_1 \vdash \Delta} \hypo{p_2} \infer1{\Gamma, A_2 \vdash \Delta} \infer2[\vee_L]{\Gamma, A_1 \vee A_2 \vdash\Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_1)} \infer1{\neg \Gamma, \neg A_1, \Delta} \hypo{\tau(p_2)} \infer1{ \neg \Gamma, \neg A_2, \Delta} \infer2[\neg \vee]{\neg \Gamma, \neg \Gamma, \neg(A_1 \vee A_2), \Delta} \infer1[\mathsf{c}^*]{\neg \Gamma, \neg(A_1 \vee A_2), \Delta} \end{prooftree}\]

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma \vdash A,A,\Delta} \infer1[\mathsf{c}_R]{\Gamma \vdash A,\Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_0)} \infer1{\neg \Gamma, A,A, \Delta} \infer1[\mathsf{c}]{\neg \Gamma, A ,\Delta} \end{prooftree}\] \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A, A \vdash \Delta} \infer1[\mathsf{c}_L]{\Gamma,A\vdash \Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_0)} \infer1{\neg\Gamma,\neg A,\neg A, \Delta} \infer1[\mathsf{c}]{\neg \Gamma, \neg A, \Delta} \end{prooftree}\] \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma \vdash \Delta} \infer1[\mathsf{w}_R]{\Gamma \vdash A,\Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_0)} \infer1{\neg \Gamma,\Delta} \infer1[\mathsf{w}]{\neg \Gamma, A ,\Delta} \end{prooftree}\] \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma \vdash \Delta} \infer1[\mathsf{w}_L]{\Gamma,A\vdash \Delta} \end{prooftree} \quad \mapsto \quad \begin{prooftree} \hypo{\tau(p_0)} \infer1{\neg\Gamma, \Delta} \infer1[\mathsf{w}]{\neg \Gamma, \neg A, \Delta} \end{prooftree}\] \[\begin{prooftree} \hypo{p_1} \infer1{\Gamma_1 \vdash A, \Delta_1} \hypo{p_2} \infer1{\Gamma_2, A, \vdash \Delta_2} \infer2[\mathsf{cut}]{\Gamma_1,\Gamma_2 \vdash \Delta_1,\Delta_2} \end{prooftree} \quad\mapsto \quad \begin{prooftree} \hypo{\tau(p_1)} \infer1{\neg \Gamma_1, A, \Delta_1} \hypo{\tau(p_2)} \infer1{\neg \Gamma_2, \neg A, \Delta_2} \infer2[\mathsf{cut}]{\neg \Gamma_1,\neg \Gamma_2, \Delta_1,\Delta_2} \end{prooftree}\]

We will assume without loss of generality that all proofs are regular, i.e. that each eigen-variable \(\alpha\) is introduded by exactly one occurrence of the \(\neg \exists\)-rule. Given a proof \(p\) and an eigenvariable \(\alpha\), we denote by \(p[t/\alpha]\) the result of substituting everywhere in \(p\) the variable \(\alpha\) by \(t\). Here, \(t\) is any \(\mathcal{L}^+\)-term of type \(\iota\).

4 Formulas as types, proofs as terms↩︎

4.1 Formulas as types↩︎

For each formula \(A\), the associated evidence type \([A]\) and counter-evidence type \(\langle A \rangle\) are defined as follows:

- \([A] = \langle A \rangle = \Box\) for \(A\) atomic.

- \([\exists x A] = \iota \times \langle \neg A \rangle\)

- \(\langle \exists x A \rangle = [\exists x A] \to [\neg A]\)

- \([\neg A] = (\langle A \rangle \to [A]) \to \langle A \rangle\)

- \(\langle \neg A \rangle = \langle A \rangle \to [A]\)

- \([A \vee B] = \langle \neg A \rangle \times \langle \neg B \rangle\)

- \(\langle A \vee B \rangle = (\langle \neg A \rangle \to [\neg A]) \times (\langle \neg B \rangle \to [\neg B])\)

We shall write \(E_A\) for an arbitrary closed inhabitant of \([A]\), which exists by Proposition 1. Given a formula \(A\) and given closed \(\mathcal{L}^+\)-terms \(u : [A]\) and \(v : \langle A \rangle\), we define a formula \(A \; \begin{array}{| c |} u \\ v \end{array} \;\) as follows:

\[\begin{align} R(t_1,\ldots, t_n) \; \begin{array}{| c |} u \\ v \end{array} \; & = R(t_1,\ldots,t_n) \\ \exists x A \; \begin{array}{| c |} u \\ v \end{array} \; & = A[\pi_1(u)/x] \; \begin{array}{| c |} (\pi_2(u))((v(u))(\pi_2(u))) \\ (v(u))(\pi_2(u)) \end{array} \;\\ A \vee B \; \begin{array}{| c |} u \\ v \end{array} \; & = A \; \begin{array}{| c |} (\pi_1(u))(((\pi_1(v))(\pi_1(u)))(\pi_1(u))) \\ ((\pi_1(v))(\pi_1(u)))(\pi_1(u)) \end{array} \; \vee B \; \begin{array}{| c |} (\pi_2(u))(((\pi_2(v))(\pi_2(u)))(\pi_2(u))) \\ ((\pi_2(v))(\pi_2(u)))(\pi_2(u)) \end{array} \; \\ \neg A \; \begin{array}{| c |} u \\ v \end{array} \; & = \neg \left(A \; \begin{array}{| c |} v(u(v)) \\ u(v) \end{array} \; \right) \end{align}\]

Intuitively, the formula \(A \; \begin{array}{| c |} u \\ v \end{array} \;\) means that the evidence \(u\) beats the counter-evidence \(v\); or, in game-theoretic terms, that the strategy \(u\) for the Verifier beats the strategy \(v\) for the Falsifier. The functional interpretation of a closed sentence \(A\) is: \[\forall x \exists y \left(A \; \begin{array}{| c |} y \\ x \end{array} \; \right)\] We need to check that our definition of the formula \(A \; \begin{array}{| c |} u \\ v \end{array} \;\) is sound, in the sense that the terms introduced on the right-hand sides of the equations are all of the appropriate types.

In the case of the existential quantifier, we have: \[\begin{align} u : & \; [\exists x A ] \\ & = \iota \times \langle \neg A \rangle \\ & = \iota \times (\langle A \rangle \to [A]) \end{align}\] and: \[\begin{align} v : & \; \langle \exists x A \rangle \\ & = [\exists x A] \to [\neg A] \\ & = (\iota \times (\langle A \rangle \to [A])) \to [\neg A] \\ & = (\iota \times (\langle A \rangle \to [A])) \to ((\langle A \rangle \to [A]) \to \langle A \rangle) \end{align}\] It follows that \(\pi_1(u) : \iota\), \(\pi_2(u) : \langle A \rangle \to [A]\) and \(v(u) : (\langle A \rangle \to [A]) \to \langle A \rangle\). So \((v(u))(\pi_2(u)) : \langle A \rangle\) and therefore \((\pi_2(u))((v(u))(\pi_2(u))) : [A]\), as required.

For the case of disjunction, we have: \[\begin{align} u : & \; [A \vee B] \\ & = \langle \neg A \rangle \times \langle \neg B \rangle \\ \end{align}\] and: \[\begin{align} v: & \; \langle A \vee B \rangle \\ & = (\langle \neg A \rangle \to [\neg A]) \times (\langle \neg B \rangle \to [\neg B])\\ \end{align}\] It follows that: \[\begin{align} (\pi_1(v))(\pi_1(u)) : & \; [\neg A] \\ & = (\langle A \rangle \to [A]) \to \langle A\rangle \\ & = \langle \neg A \rangle \to \langle A \rangle \end{align}\] We have \(\pi_1(u) : \langle \neg A \rangle\) so we get \[((\pi_1(v))(\pi_1(u)))(\pi_1(u)) : \langle A \rangle\] as required. Furthermore, as \(\pi_1(u) : \langle \neg A \rangle = \langle A \rangle \to [A]\) we also get: \[(\pi_1(u))(((\pi_1(v))(\pi_1(u)))(\pi_1(u))) : [A]\] as required. Similarly, we get \[((\pi_2(v))(\pi_2(u)))(\pi_2(u)) : \langle B \rangle\] and \[(\pi_2(u))(((\pi_2(v))(\pi_2(u)))(\pi_2(u))) : [B]\]

Finally, for the case of negation, we have \(u : [\neg A] = (\langle A \rangle \to [A]) \to \langle A \rangle\) and \(v : \langle \neg A \rangle = \langle A \rangle \to [A]\). So \(u(v) : \langle A \rangle\), and hence \(v(u(v)) : [A]\) as required.

The following proposition will be used freely without mention.

We also note the following simple observation:

4.2 Term extraction from proofs↩︎

To extract witnessing terms from proofs, we introduce the concept of a term transformer, which plays the same role here as non-terminal symbols play in Herbrand schemes.

Given a proof \(p\) of the end sequent \(A_1,\ldots,A_n\) we shall associate with each index \(i\) a term transformer \(F^p_i\) of signature \((\langle A_1 \rangle,\ldots,\langle A_n\rangle, [A_i])\). Note that, since sequents are technically speaking multisets with no internal order, the use of indices to refer to formula occurrences in a sequent is somewhat imprecise. Rather than being overly pedantic about this, we trust that the definitions will be sufficiently clear that the reader could easily work out the tedious task of formulating them in a fully precise way.

We shall define our term transformers by structural recursion on proofs, making a case distinction on the last rule of inference used in the proof \(p\). The size of a multiset \(\Gamma\) of formulas will be denoted by \(\vert \Gamma \vert\).

4.2.0.1 Case \(\mathsf{lem}\):

The proof \(p\) is: \[\begin{prooftree} \hypo{} \infer1{\neg A, A} \end{prooftree}\]

We define corresponding term transformers by setting:

\[F^p_2 uv = u(v)\] \[F^p_1 uv = \lambda z. v\]

To verify that these are well-defined term transformers, we focus on checking that the terms have the appropriate types. By assumption, \(u : \langle \neg A \rangle = \langle A \rangle \to [A]\) and \(v : \langle A \rangle\). Hence \(F^p_2 uv = u(v) : [A]\) as required. In the definition of \(F^p_1 uv\) as \(\lambda z.v\), we have implicitly assumed that the variable \(z\) is of type \(\langle A \rangle \to [A]\), and so \(\lambda z.v : (\langle A \rangle \to [A]) \to \langle A \rangle = [\neg A]\) as required.

4.2.0.2 Case \(\mathsf{w}\):

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma} \infer1{\Gamma,A} \end{prooftree}\]

Recall that \(E_A\) is an arbitrarily chosen inhabitant of \([A]\). We set: \[F^p_{\vert \Gamma \vert + 1}\vec{u}v = E_A\] For \(i \leq \vert \Gamma \vert\): \[F^p_i \vec{u}v = F^{p_0}_i \vec{u}\] It is trivial to check that these are well-defined term transformers.

4.2.0.3 Case \(\mathsf{cut}\):

\[\begin{prooftree} \hypo{p_1} \infer1{\Gamma, A} \hypo{p_2} \infer1{\Delta, \neg A} \infer2{\Gamma, \Delta} \end{prooftree}\]

Set \(k = \vert \Gamma \vert\) and \(m = \vert \Delta \vert\). We let \(h\) abbreviate \(\lambda z. F^{p_1}_{k + 1} \vec{u} z\). For \(i > k\): \[F^p_i \vec{u}\vec{v} = F^{p_2}_{i-m} \vec{v}h\] For \(i \leq k\): \[F^p_i \vec{u}\vec{v} = F^{p_1}_i \vec{u}((F^{p_2}_{k + 1} \vec{v} h)h)\]

Again, to check that these are well-defined term transformers, we check the types. In the definition of \(h\) as \(\lambda z. F^{p_1}_{k + 1} \vec{u} z\) it is implicit that \(z : \langle A \rangle\), hence \(h : \langle A \rangle \to [A] = \langle \neg A \rangle\). Hence \(F^{p_2}_{k + 1} \vec{v} h\) has the type \([\neg A] = (\langle A \rangle \to [A]) \to \langle A \rangle\), which means that \((F^{p_2}_{k + 1} \vec{v} h)h\) has type \(\langle A \rangle\). From these observations follows immediatly from the induction hypothesis on \(p_1\) and \(p_2\) that each term \(F^p_i \vec{u} \vec{v}\) has the appropriate type.

4.2.0.4 Case \(\mathsf{c}\):

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A, A} \infer1{\Gamma, A} \end{prooftree}\]

Let \(k = \vert \Gamma \vert\). We set: \[F^p_{k + 1} \vec{u}v = [F^{p_0}_{k + 1} \vec{u}vv\;\mathsf{if}\; W \;\mathsf{else}\; F^{p_0}_{k+ 2} \vec{u}vv]\] where: \[W := A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}vv \\ v \end{array} \;\] For \(i \leq \vert \Gamma \vert\) set: \[F^p_i \vec{u}v = F^{p_0}_i \vec{u}vv\] It is trivial to check that these are well-defined term transformers.

4.2.0.5 Case \(\exists\):

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A[t/x]} \infer1{\Gamma, \exists x A} \end{prooftree}\]

Let \(h\) abbreviate \(\lambda z. F^{p_0}_{\vert \Gamma \vert + 1}\vec{u}z\). Set: \[F^p_{\vert \Gamma \vert + 1} \vec{u} v = (t, h)\] For \(i \leq \vert \Gamma \vert\): \[F^p_i \sigma \vec{u} v = F^{p_0}_i \vec{u}((v((t, h)))h)\]

We assume that \(v\) is of type \(\langle \exists x A \rangle = [\exists x A] \to [\neg A]\). The variable \(z\) in the term \(h\) is implicitly assumed to have type \(\langle A \rangle\) so that \(h : \langle A \rangle \to [A] = \langle \neg A \rangle\). Hence \((t,h) : \iota \times \langle \neg A \rangle = [\exists x A]\) as required. Furthermore, it follows that \[\begin{align} v((t,h)) : & \; [\neg A] \\ & = (\langle A \rangle \to [A]) \to \langle A \rangle \\ & \langle \neg A \rangle \to \langle A \rangle \end{align}\] Since \(h: \langle \neg A \rangle\) it follows that \((v((t,h)))h : \langle A \rangle\) as required.

4.2.0.6 Case \(\neg \exists\):

Here \(p\) is of the form:

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, \neg A[\alpha/x]} \infer1{\Gamma, \neg \exists x A} \end{prooftree}\]

We define a term \(h : \langle \exists x A \rangle\) by: \[h = \lambda y. (F^{p_0}_{\vert \Gamma \vert + 1}\vec{u}(\pi_2(y)))[\pi_1(y)/\alpha]\] We set: \[F^p_{\vert \Gamma \vert + 1}\vec{u}v = \lambda z.h\] For \(i \leq \vert \Gamma \vert\): \[F^p_i \vec{u}v = (F^{p_0}_i \vec{u}(\pi_2(v(h))))[\pi_1(v(h)))/\alpha]\]

We check the types. First, the bound variable \(y\) in \(h\) is assumed to be of type \([\neg \exists x A]\), so that \(h : [\neg \exists x A ] \to [\neg A] = \langle \exists x A \rangle\) as we claimed. Assuming the variable \(z\) has type \(\langle \exists x A \rangle \to [\exists x A]\), we have \[\lambda z.h : (\langle \exists x A \rangle \to [\exists x A]) \to \langle \exists x A \rangle = [\neg \exists x A]\] as required. Furthermore, \(v\) is assumed to have the type \(\langle \neg \exists x A \rangle = \langle \exists x A \rangle \to [\exists x A]\). Hence \(v(h) : [\exists x A]\). Since \(\exists x A = \iota \times \langle \neg A \rangle\) we have \(\pi_2(v(h)) : \langle \neg A \rangle\), and \(\pi_1(v(h)) : \iota\). This ensures the definitions give the appropriate types.

4.2.0.7 Case \(\vee\):

There are two instances of this rule. In the first case the proof \(p\) is of the form:

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A} \infer1{\Gamma, A \vee B} \end{prooftree}\]

Let \(k = \vert \Gamma \vert\). Let \(q\) abbreviate \((\lambda z. F^{p_0}_{k+1} \vec{u} z, \lambda z. E_ B)\), where we recall that \(E_B\) is an arbitrary inhabitant of \([B]\). Set: \[F^{p}_{k + 1} \vec{u} v = q\] For \(i \leq \vert \Gamma \vert\): \[F^{p}_{i} \vec{u} v = F^{p_0}_i \vec{u}(((\pi_1(v))(\pi_1(q)))(\pi_1(q)))\] We check the types. We have: \[\begin{align} q : & \; (\langle A \rangle \to [A]) \times (\langle B \rangle \to [B]) \\ & = \langle \neg A \rangle \times \langle \neg B \rangle \\ & [A \vee B] \end{align}\] as required. It also follows that \(\pi_1(q) : \langle \neg A \rangle\).

By assumption we have: \[\begin{align} v : & \; \langle A \vee B \rangle \\ & = (\langle \neg A \rangle \to [\neg A]) \times (\langle \neg B \rangle \to [\neg B]) \end{align}\] so \(\pi_1(v) : \langle \neg A \rangle \to [\neg B]\). Hence: \[\begin{align} (\pi_1(v))(\pi_1(q)) : & \; [\neg A] \\ & = (\langle A \rangle \to [A]) \to \langle A\rangle \\ & = \langle \neg A \rangle \to \langle A \rangle \end{align}\] Since \(\pi_1(q) : \langle \neg A \rangle\) we get \(((\pi_1(v))(\pi_1(q)))(\pi_1(q)) : \langle A \rangle\), as required.

In the second case \(p\) is:

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, B} \infer1{\Gamma, A \vee B} \end{prooftree}\]

In this case let \(q\) abbreviate \((\lambda z. E_A, \lambda z. F^{p_0}_{k+1} \vec{u} z)\). Set: \[F^{p}_{k + 1} \vec{u} v = q\] For \(i \leq \vert \Gamma \vert\): \[F^{p}_{i} \vec{u} v = F^{p_0}_i \vec{u}(((\pi_2(v))(\pi_2(q)))(\pi_2(q)))\] Checking the types is similar to the first case.

4.2.0.8 Case \(\neg \vee\):

\[\begin{prooftree} \hypo{p_1} \infer1{\Gamma, \neg A} \hypo{p_2} \infer1{\Delta, \neg B} \infer2{\Gamma, \Delta, \neg (A \vee B)} \end{prooftree}\]

Let \(k = \vert \Gamma \vert\) and let \(m = \vert \Delta \vert\). Let \(q_1\) abbreviate \(\lambda z. F^{p_1}_{k+1} \vec{u} z\) and let \(q_2\) abbreviate \(\lambda z. F^{p_2}_{m+1} \vec{v} z\). Let \(q\) abbreviate \(\lambda z. (q_1,q_2)\). We set: \[F^p_{k + m +1} \vec{u}\vec{v} w = q\] For \(k < i \leq k+m\): \[F^p_i \vec{u} \vec{v} w = F^{p_2}_{i - k} \vec{v} (\pi_2(w(q(w)))\] For \(i \leq k\): \[F^p_i \vec{u} \vec{v} w = F^{p_1}_{i} \vec{u} (\pi_1(w(q(w)))\]

We check the types. First, we have \(q_1 : \langle \neg A \rangle \to [\neg A]\) and \(q_2 : \langle \neg B \rangle \to [\neg B]\). Hence:

\[\begin{align} (q_1,q_2) : & \; (\langle \neg A \rangle \to [\neg A]) \times ( \langle \neg B \rangle \to [\neg B]) \\ & = \langle A \vee B \rangle \end{align}\] Assuming that \(z\) is a variable of type \(\langle A \vee B \rangle \to [A \vee B]\), we thus have: \[\begin{align} \lambda z. (q_1,q_2) : & \; (\langle A \vee B \rangle \to [A \vee B ]) \to \langle A \vee B \rangle \\ & = [\neg( A \vee B)] \end{align}\] as required.

By assumption we have: \[\begin{align} w : & \; \langle \neg (A \vee B) \rangle \\ & = \langle A \vee B \rangle \to [A \vee B] \end{align}\] Hence \(q(w) : \langle A \vee B \rangle\), and so \[\begin{align} w(q(w)) : & \; [A \vee B] \\ & = \langle \neg A \rangle \times \langle \neg B \rangle \end{align}\] so \(\pi_1(w(q(w))) : \langle \neg A \rangle\) and \(\pi_2(w(q(w))) : \langle \neg B \rangle\) as required.

4.2.0.9 Case \(\neg\neg\):

The proof \(p\) is of the form: \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A} \infer1{\Gamma, \neg \neg A} \end{prooftree}\]

Let \(q\) abbreviate \(\lambda y. F^{p_0}_{\vert \Gamma \vert + 1} \vec{u} y\). We set: \[F^p_{\vert \Gamma \vert + 1} \vec{u} v = \lambda z.q\] For \(i \leq \vert \Gamma \vert\): \[F^p_i \vec{u}v = F^{p_0}_i \vec{u}((v(q))q)\]

We check the types. Assuming \(y\) is a variable of type \(\langle A \rangle\) we have \(q : \langle A \rangle \to [A] = \langle \neg A \rangle\). So assuming \(z\) is of type \(\langle \neg A \rangle \to [\neg A]\) we get: \[\begin{align} \lambda z. q : & \; (\langle \neg A \rangle \to [\neg A]) \to \langle \neg A \rangle \\ & = [\neg \neg A] \end{align}\] as required.

By assumption we have: \[\begin{align} v : & \; \langle \neg \neg A \rangle \\ & = \langle \neg A \rangle \to [\neg A] \end{align}\] so \(v(q) : [\neg A] = (\langle A \rangle \to [A]) \to \langle A \rangle\). Hence, as \(q: \langle A \rangle \to [A]\) we get \((v(q))q : \langle A \rangle\) as required.

With the definitions in place, the following proposition can be proved by a straightforward induction:

Note that, using Proposition 6, we can write the definition of terms transformers for a proof \(p\) of the form \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, \neg A[\alpha/x]} \infer1{\Gamma, \neg \exists x A} \end{prooftree}\] equivalently as follows. We let \[h = \lambda y. F^{p_0[\pi_1(y)/\alpha]}_{\vert \Gamma \vert + 1}\vec{u}(\pi_2(y))\] and set: \[F^p_{\vert \Gamma \vert + 1}\vec{u}v = \lambda z.h\] For \(i \leq \vert \Gamma \vert\): \[F^p_i \vec{u}v = F^{p_0[ \pi_1(v(h))/\alpha]}_i \vec{u}(\pi_2(v(h)))\]

We are now ready to state the main result:

The proof of Theorem 1 will occupy us in Section 5.

4.3 Sequent calculus, Herbrand’s theorem and concurrency↩︎

The sequent calculus has a close relationship with Herbrand’s theorem; indeed, the most well-known way to prove Herbrand’s theorem is probably via cut elimination for sequent calculus, extracting a Herbrand disjunction from a “mid-sequent” in a cut-free proof. This connection between sequent calculus and Herbrand’s theorem was explored by Alcolei et al. [8], in which game semantics was used to describe the computational content of sequent calculus proofs. The game takes place between two players, “Prover” and “Refuter”, and allows for several copies of a game to be played in parallell. The winning condition favors Prover, in that she essentially wins the game if she wins in one of the parallel copies of the game. The main result in [8] shows that one can extract a winning strategy for Prover for a sequent calculus proof, and that if the end sequent is \(\Sigma_1\) then that strategy naturally gives rise to a Herbrand disjunction.

To illustrate this game-theoretic perspective we can consider the following classic example, a sequent calculus proof of the formula known as the “drinker paradox”:

\[\begin{prooftree} \hypo{} \infer1{ P\alpha, \neg P\alpha} \infer1[\vee]{ P\alpha, P\alpha \to P\beta} \infer1[\neg \neg + \neg \exists]{ P\alpha, \forall y (P\alpha \to Py)} \infer1[\exists]{ P\alpha, \exists x \forall y (Px \to Py)} \infer1[\vee]{ Pc \to P\alpha, \exists x \forall y (Px \to Py)} \infer1[\neg \neg + \neg \exists]{ \forall y (Pc \to Py), \exists x \forall y (Px \to Py)} \infer1[\exists]{\exists x \forall y (Px \to Py), \exists x \forall y (Px \to Py)} \infer1[\mathsf{c}]{\exists x \forall y (Px \to Py)} \end{prooftree}\] Here we take \(\forall x : = \neg \exists x \neg\) and \(A \to B := \neg A \vee B\) as usual. In the game-theoretic interpretation of this proof, Prover’s main task is to come up with a witness for the existential quantifier. Howver, there is no one choice that will work for a single play of the game. So Prover immediately decides to split the game into two copies to be played in parallel, and aims to ensure a win in at least one of the copies. The way that Prover’s strategy plays out is directly reflected in the two “threads” of the proof; in the left thread, corresponding to one copy of the game, Prover simply chooses a witness \(c\) for the existential quantifier. Now, Refuter has to respond with some counter-example to the universal quantifier. The eigen-variable \(\alpha\) can be thought of as a generic proposed counter-example, so that Prover’s strategy does not assume anything about how Refuter is going to play. Prover has set a trap here: playing the first move \(c\) forces a response from Refuter, and this will then be used in the other copy of the game represented by the right thread in the proof. Here, Prover takes the counter-example \(\alpha\) from Refuter’s response and now plays that as a witness instead. In this sense there is communication between the parallel copies of the game: Prover can take a move of Refuter in one copy of the game and use it to find the right moves in a different copy of the game. All of this is plainly visible in the proof, and thinking of a sequent calculus proof as a concurrent process seems very natural indeed.

The aim of the present work is to see how functional interpretations fit into this picture. The important thing is not that we can extract realizing terms from a sequent calculus proof, but rather how this is done. Given a proof \(p\) of a sequent \(A_1,\ldots,A_n\), we can think of closed terms \[u_1 : \langle A_1\rangle, \ldots, u_n : \langle A_n \rangle\] as representing strategies for Refuter in \(n\) different games played in parallel. The term extraction finds strategies for Prover to ensure that she wins in at least one of these parallel games, expressing by the validity of the disjunction: \[A_1 \; \begin{array}{| c |} F^p_1 \vec{u} \\ u_1 \end{array} \; \vee \ldots \vee A_n \; \begin{array}{| c |} F^p_n \vec{u} \\ u_n \end{array} \;\] Thus we can think if these extracted terms as processes running concurrently. The connection between threads in a proof and individual processes is also preserved: each individual term \(F^p_i \vec{u}\) is constructed directly from the threads of the proof leading to the formula \(A_i\).

Furthermore, as in the game-semantics framework, there is communication between these individual processes. To isolate the relevant part of the above proof of the drinker paradox, consider a proof \(p\) of the form: \[\begin{prooftree} \hypo{\vdots} \infer1{ d.\; \neg \exists y A(\alpha,y), \neg A(c,\alpha)} \infer1{c.\;\exists x \neg \exists y A(x,y), \neg A(c,\alpha)} \infer1{b.\;\exists x \neg \exists y A(x,y), \neg \exists y A(c,y)} \infer1{a.\;\exists x \neg \exists y A(x,y), \exists x \neg \exists y A(x,y)} \end{prooftree}\]

Given terms \(u, v\) representing counter-evidence for each copy of the formula \(\exists x \neg \exists y A(x,y)\), we extract witnessing terms \(F^a_1 u v\) and \(F^a_2 u v\). The labels \(a,b,c,d\) help to refer to subproofs of \(p\), so that \(p\) itself has the label \(a\). The interesting thing is to look at how the term \(F^a_1 u v\) is extracted; the fact that this is a non-principal formula at the end-sequent of the proof can intuitively be thought of as Prover waiting for the second copy of the game to play out for a bit before making her move. According to the definition of term transformers from proofs, we get: \[F^a_1 u v = F^b_1 u ((v(c, h))h)\] where \(h\) abbreviates \(\lambda z. F^b_2 u z\). So here, Prover simply observes that given the strategy played in the parallel copy of the game, where Prover plays \(c\) as a witness, Refuter responds with \((v(c, h))h\) which is a term of type \(\langle \neg \exists y A(c,y) \rangle\). We abbreviate this term by \(w_c\), with the subscript to emphasize the dependence on the term \(c\) played by Prover. In the next step we compute: \[F^b_1 u w_c = (F^c_1 u (\pi_2(w_c(g))))[\pi_1(w_c(g))/\alpha]\] where \(g\) abbreviates \(\lambda z. (F^c_2 u (\pi_2(z))[\pi_1(z)/\alpha]\). In the next step, Prover makes her move, and gives \(\pi_1(w_c(g))\) as the witness for the existential quantifer due to the substitution of \(\pi_1(w_c(g))\) for \(\alpha\). So this move depends on a response of Refuter to a move made by Prover in another other copy of the game.

5 Proof of the main theorem↩︎

We shall prove Theorem 1 by induction on the size of a proof \(p\), verifying that soundness is preserved by each recursive clause of the definition. We exclude from the proof the trivial case of a proof ending with the weakening rule.

5.1 Interpretation of the axiom↩︎

Shape of \(p\): \[\begin{prooftree} \hypo{} \infer1{\neg A, A} \end{prooftree}\]

We recall that we defined: \[F^p_2 uv = u(v)\] \[F^p_1 uv = \lambda z. v\] We have: \[\begin{align} \neg A \; \begin{array}{| c |} F^p_1 \sigma u v \\ u \end{array} \; & \equiv \neg A \; \begin{array}{| c |} \lambda z. v \\ u \end{array} \; \\ & = \neg \left( A \; \begin{array}{| c |} u((\lambda z. v)u) \\ (\lambda z. v)u \end{array} \; \right) \\ & \equiv \neg \left( A \; \begin{array}{| c |} u(v) \\ v \end{array} \; \right) \\ \end{align}\] and: \[\begin{align} A \; \begin{array}{| c |} F^p_2 \sigma u v \\ v \end{array} \; & \equiv A \; \begin{array}{| c |} u(v) \\ v \end{array} \; \end{align}\] As a propositional tautology we have: \[\vdash_{\mathsf{QF}}\neg \left( A \; \begin{array}{| c |} u(v) \\ v \end{array} \; \right) \vee A \; \begin{array}{| c |} u(v) \\ v \end{array} \;\] hence: \[\vdash_{\mathsf{QF}}\neg A \; \begin{array}{| c |} F^p_1 \sigma u v \\ u \end{array} \; \vee A \; \begin{array}{| c |} F^p_2 \sigma u v \\ v \end{array} \;\] as required.

5.2 Interpretation of cut↩︎

Shape of \(p\):

\[\begin{prooftree} \hypo{p_1} \infer1{\Gamma, A} \hypo{p_2} \infer1{\Delta, \neg A} \infer2{\Gamma, \Delta} \end{prooftree}\]

We recall the definition of the corresponding term transformers. Set \(k = \vert \Gamma \vert\) and \(m = \vert \Delta \vert\). We let \(h\) abbreviate \(\lambda z. F^{p_1}_{k + 1} \vec{u} z\) so that \(h : \langle A \rangle \to [A]\). For \(i > k\): \[F^p_i \vec{u}\vec{v} = F^{p_2}_{i-m} \vec{v}h\] For \(i \leq k\): \[F^p_i \vec{u}\vec{v} = F^{p_1}_i \vec{u}((F^{p_2}_{k + 1} \vec{v} h)h)\] The induction hypothesis on \(p_1\) gives: \[(1)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq k} U_i \; \begin{array}{| c |} F^{p_1}_i \vec{u} w \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^{p_1}_{k+1} \vec{u} w \\ w \end{array} \;\] for all \(w\). Substituting \((F^{p_2}_{m + 1} \vec{v} h)h\) for \(w\) in \((1)\) gives: \[(2)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq k} U_i \; \begin{array}{| c |} F^{p_1}_i \vec{u} ((F^{p_2}_{m + 1} \vec{v} h)h) \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^{p_1}_{k+1} \vec{u} ((F^{p_2}_{m + 1} \vec{v} h)h) \\ (F^{p_2}_{m + 1} \vec{v} h)h \end{array} \;\] The induction hypothesis on \(p_2\) gives: \[(3)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq j \leq m} V_j \; \begin{array}{| c |} F^{p_2}_j \vec{v} w \\ v_j \end{array} \; \vee \neg A \; \begin{array}{| c |} F^{p_2}_{m+1} \vec{v} w \\ w \end{array} \;\] For all \(w\), in particular: \[(4)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq j \leq m} V_j \; \begin{array}{| c |} F^{p_2}_j \vec{v} h \\ v_j \end{array} \; \vee \neg A \; \begin{array}{| c |} F^{p_2}_{m+1} \vec{v} h \\ h \end{array} \;\] But we have: \[\begin{align} \neg A \; \begin{array}{| c |} F^{p_2}_{m+1} \vec{v} h \\ h \end{array} \; & = \neg \left( A \; \begin{array}{| c |} h((F^{p_2}_{m+1} \vec{v} h)h) \\ (F^{p_2}_{m+1} \vec{v} h)h \end{array} \; \right) \\ & = \neg \left( A \; \begin{array}{| c |} (\lambda z. F^{p_1}_{k+1} {u} z)((F^{p_2}_{m+1} \vec{v} h)h) \\ (F^{p_2}_{m+1} \vec{v} h)h \end{array} \; \right) \\ & \equiv \neg \left( A \; \begin{array}{| c |} F^{p_1}_{k+1} {u}((F^{p_2}_{m+1} \vec{v} h)h) \\ (F^{p_2}_{m+1} \vec{v} h)h \end{array} \; \right) \\ \end{align}\] So from \((4)\) we get: \[(5)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq j \leq m} V_j \; \begin{array}{| c |} F^{p_2}_j \vec{v} h \\ v_j \end{array} \; \vee \neg \left( A \; \begin{array}{| c |} F^{p_1}_{k+1} {u}((F^{p_2}_{m+1} \vec{v} h)h) \\ (F^{p_2}_{m+1} \vec{v} h)h \end{array} \; \right)\] A cut on \((5)\) and \((2)\) gives: \[(6)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq k} U_i \; \begin{array}{| c |} F^{p_1}_i \vec{u} ((F^{p_2}_{m + 1} \vec{v} h)h) \\ u_i \end{array} \; \vee \bigvee_{1 \leq j \leq m} V_j \; \begin{array}{| c |} F^{p_2}_j \vec{v} h \\ v_j \end{array} \;\] But this is: \[{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq k} U_i \; \begin{array}{| c |} F^{p}_i \vec{u} \vec{v} \\ u_i \end{array} \; \vee \bigvee_{k + 1 \leq j \leq k + m} V_j \; \begin{array}{| c |} F^{p}_{j} \vec{u}\vec{v} \\ v_j \end{array} \;\] as required.

5.3 Contraction↩︎

Shape of \(p\): \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A, A} \infer1{\Gamma, A} \end{prooftree}\]

We recall the definition of the corresponding term transformers: \[F^p_{\vert \Gamma \vert + 1} \vec{u}v = [F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}vv\;\mathsf{if}\; W \;\mathsf{else}\; F^{p_0}_{\vert \Gamma \vert + 2} \vec{u}vv]\] where: \[W = A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}vv \\ v \end{array} \;\] For \(i \leq \vert \Gamma \vert:\) \[F^p_i \vec{u}v = F^{p_0}_i \vec{u}vv\] The induction hypothesis on \(p_0\) gives: \[(1)\; {\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u}w_1 w_2 \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u} w_1 w_2 \\ w_1 \end{array} \; \vee A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 2} \vec{u} w_1 w_2 \\ w_2 \end{array} \;\] for all \(w_1,w_2\). Setting \(w_1 = w_2 = v\) in \((1)\) we get: \[(2)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u}v v \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u} vv \\ v \end{array} \; \vee A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 2} \vec{u} v v \\ v \end{array} \;\] We have: \[(3)\; W {\vdash_{\mathsf{QF}}}A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u} vv \\ v \end{array} \; \leftrightarrow A \; \begin{array}{| c |} [F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}vv\;\mathsf{if}\; W \;\mathsf{else}\; F^{p_0}_{\vert \Gamma \vert + 2} \vec{u}vv] \\ v \end{array} \;\] and: \[(4)\; \neg W {\vdash_{\mathsf{QF}}}A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 2} \vec{u} vv \\ v \end{array} \; \leftrightarrow A \; \begin{array}{| c |} [F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}vv\;\mathsf{if}\; W \;\mathsf{else}\; F^{p_0}_{\vert \Gamma \vert + 2} \vec{u}vv] \\ v \end{array} \;\] From \((2)\), \((3)\) and \((4)\) we get: \[(5)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u}v v \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} [F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}vv\;\mathsf{if}\; W \;\mathsf{else}\; F^{p_0}_{\vert \Gamma \vert + 2} \vec{u}vv] \\ v \end{array} \;\] But this is: \[{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^p_i \vec{u}v \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^p_i \vec{u} v \\ v \end{array} \;\] as required.

5.4 \(\exists\)-rule↩︎

Shape of \(p\): \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A[t/x]} \infer1{\Gamma, \exists x A} \end{prooftree}\]

We recall the definition of the corresponding term transformers. Let \(h\) abbreviate \(\lambda z. F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}z v\). We have: \[F^p_{\vert \Gamma \vert + 1} \vec{u} v = (t, h)\] For \(i \leq \vert \Gamma \vert\): \[F^p_i \vec{u} v = F^{p_0}_i \vec{u}((v((t, h)))h)\] We get: \[\begin{align} \exists x A \; \begin{array}{| c |} F^p_{\vert \Gamma \vert + 1} \vec{u} v \\ v \end{array} \; & \equiv \exists x A \; \begin{array}{| c |} (t, h) \\ v \end{array} \; \\ & \equiv A[\pi_1((t, h))/x] \; \begin{array}{| c |} (\pi_2((t, h)))((v((t, h)))(\pi_2((t, h)))) \\ (v((t, h)))(\pi_2((t, h))) \end{array} \; \\ & \equiv A[t/x] \; \begin{array}{| c |} h((v((t, h)))h) \\ (v((t, h)))h \end{array} \; \\ & \equiv A[t/x] \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}((v((t,h)))h)) \\ (v((t, h)))h \end{array} \; \\ \end{align}\]

Hence we have: \[(1)\; \exists x A \; \begin{array}{| c |} F^p_{\vert \Gamma \vert + 1} \vec{u} v \\ v \end{array} \; \equiv A[t/x] \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}((v((t,h)))h)) \\ (v((t, h)))h \end{array} \;\]

The induction hypothesis on \(p_0\) gives: \[(2)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u} w \\ u_i \end{array} \; \vee A[t/x] \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1}\vec{u}w \\ w \end{array} \;\] for all \(w\). Setting \(w = (v((t, h)))h\) in \((1)\) gives: \[(3)\;{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u} ((v((t, h)))h) v \\ u_i \end{array} \; \vee A[t/x] \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1}\vec{u}((v((t, h)))h) \\ (v((t, h)))h \end{array} \;\] But by \((1)\) this is: \[{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p}_i \vec{u} v \\ u_i \end{array} \; \vee \exists x A \; \begin{array}{| c |} F^{p}_{\vert \Gamma \vert + 1}\vec{u}v \\ v \end{array} \;\] as required.

5.5 \(\neg \exists\)-rule↩︎

Shape of \(p\): \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, \neg A[\alpha/x]} \infer1{\Gamma, \neg \exists x A} \end{prooftree}\]

We recall the definition of the corresponding term transformers. We set: \[h = \lambda y. F^{p_0[\pi_1(y)/\alpha]}_{\vert \Gamma \vert + 1} \vec{u}(\pi_2(y))\] Appealing to Proposition 6 the associated term transformers are: \[F^p_{\vert \Gamma \vert + 1} \vec{u}v = \lambda z.h\] For \(i \leq \vert \Gamma \vert\): \[F^p_i \vec{u}v = F^{p_0 [\pi_1(v(h))/\alpha]}_i \vec{u}(\pi_2(v(h)))\] We have: \[\begin{align} \neg \exists x A \; \begin{array}{| c |} F^p_{\vert \Gamma \vert + 1} \vec{u}v \\ v \end{array} \; & = \neg \exists x A \; \begin{array}{| c |} \lambda z. h \\ v \end{array} \; \\ & = \neg \left( \exists x A \; \begin{array}{| c |} v((\lambda z.h)v) \\ (\lambda z.h)v \end{array} \; \right) \\ & \equiv \neg \left( \exists x A \; \begin{array}{| c |} v(h) \\ h \end{array} \; \right) \\ & = \neg \left( A [\pi_1(v(h))/x] \; \begin{array}{| c |} (\pi_2(v(h)))((h(v(h)))(\pi_2(v(h))) ) \\ (h(v(h))) (\pi_2(v(h))) \end{array} \; \right) \\ & = \neg A [\pi_1(v(h))/\alpha] \; \begin{array}{| c |} h(v(h)) \\ \pi_2(v(h)) \end{array} \; \\ & = \neg A [\pi_1(v(h))/x] \; \begin{array}{| c |} (\lambda y. F^{p_0[\pi_1(y)/\alpha]}_{\vert \Gamma \vert + 1} \vec{u}(\pi_2(y)))(v(h)) \\ \pi_2(v(h)) \end{array} \; \\ & \equiv \neg A [\pi_1(v(h))/\alpha] \; \begin{array}{| c |} F^{p_0[\pi_1(v(h))/x]}_{\vert \Gamma \vert + 1} \vec{u}(\pi_2(v(h))) \\ \pi_2(v(h)) \end{array} \; \\ \end{align}\]

The induction hypothesis on \(p_0[\pi_1(v(h))/\alpha]\) gives: \[(1)\; \bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p_0 [\pi_1(v(h))/\alpha]}_i \vec{u}w \\ u_i \end{array} \; \vee \neg A [\pi_1(v(h))/\alpha] \; \begin{array}{| c |} F^{p_0[\pi_1(v(h))/\alpha]}_{\vert \Gamma \vert + 1} \vec{u}w \\ w \end{array} \;\] for all \(w\). Setting \(w = \pi_2(v(h))\) in \((1)\) gives: \[(2)\; \bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p_0 [\pi_1(v(h))/\alpha]}_i \vec{u}(\pi_2(v(h))) \\ u_i \end{array} \; \vee \neg A [\pi_1(v(h))/\alpha] \; \begin{array}{| c |} F^{p_0[\pi_1(v(h))/\alpha]}_{\vert \Gamma \vert + 1} \vec{u}(\pi_2(v(h))) \\ \pi_2(v(h)) \end{array} \;\] But \((2)\) is: \[{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^p_i \vec{u}v \\ u_i \end{array} \; \vee \neg \exists x A \; \begin{array}{| c |} F^p_{\vert \Gamma \vert + 1} \vec{u}v \\ v \end{array} \;\] as required.

5.6 \(\vee\)-rule↩︎

We consider only one instance of the \(\vee\)-rule since the two cases are similar.

\[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A} \infer1{\Gamma, A \vee B} \end{prooftree}\]

We recall the definition of the corresponding term transformers. Let \(k = \vert \Gamma \vert\). Let \(q\) abbreviate \((\lambda z. F^{p_0}_{k+1} \vec{u} z, \lambda z. E_ B)\). Set: \[F^{p}_{k + 1} \vec{u} v = q\]

For \(i \leq \vert \Gamma \vert\): \[F^{p}_{i} \vec{u} v = F^{p_0}_i \vec{u}(((\pi_1(v))(\pi_1(q)))(\pi_1(q)))\] We have: \[\begin{align} A \vee B \; \begin{array}{| c |} F^{p}_{k + 1} \vec{u} v \\ v \end{array} \; & = A \vee B \; \begin{array}{| c |} q \\ v \end{array} \; \\ & = A \; \begin{array}{| c |} \pi_1(q)(((\pi_1(v))(\pi_1(q)))(\pi_1(q))) \\ ((\pi_1(v))(\pi_1(q)))(\pi_1(q)) \end{array} \; \vee B \; \begin{array}{| c |} \pi_2(q)(((\pi_2(v))(\pi_2(q)))(\pi_2(q))) \\ ((\pi_2(v))(\pi_2(q)))(\pi_2(q)) \end{array} \; \\ & \equiv A \; \begin{array}{| c |} (\lambda z. F^{p_0}_{k+1} \vec{u} z)(((\pi_1(v))(\pi_1(q)))(\pi_1(q))) \\ ((\pi_1(v))(\pi_1(q)))(\pi_1(q)) \end{array} \; \vee B \; \begin{array}{| c |} (\lambda z. E_ B)(((\pi_2(v))(\pi_2(q)))(\pi_2(q))) \\ ((\pi_2(v))(\pi_2(q)))(\pi_2(q)) \end{array} \; \\ & \equiv A \; \begin{array}{| c |} F^{p_0}_{k+1} \vec{u} (((\pi_1(v))(\pi_1(q)))(\pi_1(q))) \\ ((\pi_1(v))(\pi_1(q)))(\pi_1(q)) \end{array} \; \vee B \; \begin{array}{| c |} E_ B \\ ((\pi_2(v))(\pi_2(q)))(\pi_2(q)) \end{array} \; \\ \end{align}\]

By the induction hypothesis on \(p_0\) we have: \[(1)\; {\vdash_{\mathsf{QF}}}\bigvee_{i \leq k} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u}w \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^{p_0}_{k+1} \vec{u}w \\ w \end{array} \;\] for all \(w\). Setting \(w = ((\pi_1(v))(\pi_1(q)))(\pi_1(q))\) gives: \[(2)\; {\vdash_{\mathsf{QF}}}\bigvee_{i \leq k} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u}(((\pi_1(v))(\pi_1(q)))(\pi_1(q))) \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^{p_0}_{k+1} \vec{u}(((\pi_1(v))(\pi_1(q)))(\pi_1(q))) \\ ((\pi_1(v))(\pi_1(q)))(\pi_1(q)) \end{array} \;\] But we have: \[(3)\quad (A \vee B) \; \begin{array}{| c |} F^p_{k+1} \vec{u}v \\ v \end{array} \; = A \; \begin{array}{| c |} F^{p_0}_{k+1} \vec{u}(((\pi_1(v))(\pi_1(q)))(\pi_1(q))) \\ ((\pi_1(v))(\pi_1(q)))(\pi_1(q)) \end{array} \;\vee B \; \begin{array}{| c |} E_ B \\ ((\pi_2(v))(\pi_2(q)))(\pi_2(q)) \end{array} \;\]

So from \((2)\) and propositional logic we get: \[(4)\; {\vdash_{\mathsf{QF}}}\bigvee_{i \leq k} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u}(((\pi_1(v))(\pi_1(q)))(\pi_1(q))) \\ u_i \end{array} \; \vee (A \vee B) \; \begin{array}{| c |} F^p_{k+1} \vec{u}v \\ v \end{array} \;\] which is: \[{\vdash_{\mathsf{QF}}}\bigvee_{i \leq k}U_i \; \begin{array}{| c |} F^p_i \vec{u}v \\ u_i \end{array} \; \vee (A \vee B) \; \begin{array}{| c |} F^p_{k+1} \vec{u}v \\ v \end{array} \;\] as required.

5.7 \(\neg \vee\)-rule↩︎

Shape of \(p\): \[\begin{prooftree} \hypo{p_1} \infer1{\Gamma, \neg A} \hypo{p_2} \infer1{\Delta, \neg B} \infer2{\Gamma, \Delta, \neg (A \vee B)} \end{prooftree}\] We recall the definition of the corresponding term transformers. Let \(k = \vert \Gamma \vert\) and let \(m = \vert \Delta \vert\). Let \(q_1\) abbreviate \(\lambda z. F^{p_1}_{k+1} \vec{u} z\) and let \(q_2\) abbreviate \(\lambda z. F^{p_2}_{m+1} \vec{v} z\). We set: \[F^p_{k + m +1} \vec{u}\vec{v} w = q\] For \(k < i \leq k+m\): \[F^p_i \vec{u} \vec{v} w = F^{p_2}_{i - k} \vec{v} (\pi_2(w(q(w)))\] For \(i \leq k\): \[F^p_i \vec{u} \vec{v} w = F^{p_1}_{i} \vec{u} (\pi_1(w(q(w)))\]

Note that, for all \(u,v\), we have: \[\begin{align} & \neg (A \vee B) \; \begin{array}{| c |} u \\ v \end{array} \; \\ & = \neg \left(A \vee B \; \begin{array}{| c |} v(u(v)) \\ u(v) \end{array} \; \right) \\ & = \neg (A \; \begin{array}{| c |} \pi_1(v(u(v)))(((\pi_1(u(v)))(\pi_1(v(u(v)))))(\pi_1(v(u(v))))) \\ ((\pi_1(u(v)))(\pi_1(v(u(v)))))(\pi_1(v(u(v)))) \end{array} \; \\ & \qquad \vee B \; \begin{array}{| c |} \pi_2(v(u(v)))(((\pi_2(u(v)))(\pi_2(v(u(v)))))(\pi_2(v(u(v))))) \\ ((\pi_2(u(v)))(\pi_2(v(u(v)))))(\pi_2(v(u(v)))) \end{array} \;) \\ & \equiv \neg \left(A \; \begin{array}{| c |} \pi_1(v(u(v)))(((\pi_1(u(v)))(\pi_1(v(u(v)))))(\pi_1(v(u(v))))) \\ ((\pi_1(u(v)))(\pi_1(v(u(v)))))(\pi_1(v(u(v)))) \end{array} \;\right) \\ & \qquad \wedge \neg \left( B \; \begin{array}{| c |} \pi_2(v(u(v)))(((\pi_2(u(v)))(\pi_2(v(u(v)))))(\pi_2(v(u(v))))) \\ ((\pi_2(u(v)))(\pi_2(v(u(v)))))(\pi_2(v(u(v)))) \end{array} \;\right) \\ & = \neg A \; \begin{array}{| c |} (\pi_1(u(v)))(\pi_1(v(u(v)))) \\ \pi_1(v(u(v))) \end{array} \; \wedge \neg B \; \begin{array}{| c |} (\pi_2(u(v)))(\pi_2(v(u(v)))) \\ \pi_2(v(u(v))) \end{array} \;\\ \end{align}\]

Hence we have: \[\begin{align} & \neg (A \vee B) \; \begin{array}{| c |} F^p_{k + m +1} \vec{u}\vec{v} w \\ w \end{array} \; \\ & = \neg (A \vee B) \; \begin{array}{| c |} q \\ w \end{array} \; \\ & \equiv \neg A \; \begin{array}{| c |} (\pi_1(q(w)))(\pi_1(w(q(w)))) \\ \pi_1(w(q(w))) \end{array} \; \wedge \neg B \; \begin{array}{| c |} (\pi_2(q(w)))(\pi_2(w(q(w)))) \\ \pi_2(w(q(w))) \end{array} \;\\ & \equiv \neg A \; \begin{array}{| c |} (\pi_1((\lambda z.(q_1,q_2))(w)))(\pi_1(w(q(w)))) \\ \pi_1(w(q(w))) \end{array} \; \wedge \neg B \; \begin{array}{| c |} (\pi_2((\lambda z.(q_1,q_2))(w)))(\pi_2(w(q(w)))) \\ \pi_2(w(q(w))) \end{array} \;\\ & \equiv \neg A \; \begin{array}{| c |} q_1(\pi_1(w(q(w)))) \\ \pi_1(w(q(w))) \end{array} \; \wedge \neg B \; \begin{array}{| c |} q_2(\pi_2(w(q(w)))) \\ \pi_2(w(q(w))) \end{array} \;\\ & \equiv \neg A \; \begin{array}{| c |} F^{p_1}_{k+1} \vec{u}(\pi_1(w(q(w)))) \\ \pi_1(w(q(w))) \end{array} \; \wedge \neg B \; \begin{array}{| c |} F^{p_2}_{m+1} \vec{v}(\pi_2(w(q(w)))) \\ \pi_2(w(q(w))) \end{array} \;\\ \end{align}\] The induction hypothesis on \(p_1\) gives: \[(1)\; {\vdash_{\mathsf{QF}}}\bigvee_{i \leq k} U_i \; \begin{array}{| c |} F^{p_1}_{i} \vec{u}r \\ u_i \end{array} \; \vee \neg A \; \begin{array}{| c |} F^{p_1}_{k+1} \vec{u}r \\ r \end{array} \;\] for all \(r\). Setting \(r = \pi_1(w(q(w)))\) gives: \[(2)\; {\vdash_{\mathsf{QF}}}\bigvee_{i \leq k} U_i \; \begin{array}{| c |} F^{p_1}_{i} \vec{u}(\pi_1(w(q(w)))) \\ u_i \end{array} \; \vee \neg A \; \begin{array}{| c |} F^{p_1}_{k+1} \vec{u}(\pi_1(w(q(w)))) \\ \pi_1(w(q(w))) \end{array} \;\] The induction hypothesis on \(p_2\) gives: \[(3)\; {\vdash_{\mathsf{QF}}}\bigvee_{k < i \leq k + m} V_{i} \; \begin{array}{| c |} F^{p_2}_{i - k} \vec{v}r \\ v_i \end{array} \; \vee \neg B \; \begin{array}{| c |} F^{p_2}_{m+1} \vec{v}r \\ r \end{array} \;\] for all \(r\). Setting \(r = \pi_2(w(q(w)))\) gives: \[(4)\; {\vdash_{\mathsf{QF}}}\bigvee_{k < i \leq k + m} V_{i} \; \begin{array}{| c |} F^{p_2}_{i - k} \vec{v}(\pi_2(w(q(w)))) \\ v_i \end{array} \; \vee \neg B \; \begin{array}{| c |} F^{p_2}_{m+1} \vec{v}(\pi_2(w(q(w)))) \\ \pi_2(w(q(w))) \end{array} \;\] From \((2)\) and \((4)\) we get: \[(5)\quad\quad \begin{align} & {\vdash_{\mathsf{QF}}}\bigvee_{i \leq k} U_i \; \begin{array}{| c |} F^{p_1}_{i} \vec{u}(\pi_1(w(q(w)))) \\ u_i \end{array} \; \\ & \vee \bigvee_{k < i \leq k + m} V_{i} \; \begin{array}{| c |} F^{p_2}_{i - k} \vec{v}(\pi_2(w(q(w)))) \\ v_i \end{array} \; \\ & \vee \left( \neg A \; \begin{array}{| c |} (\pi_1(u(v)))(\pi_1(v(u(v)))) \\ \pi_1(v(u(v))) \end{array} \; \wedge \neg B \; \begin{array}{| c |} (\pi_2(u(v)))(\pi_2(v(u(v)))) \\ \pi_2(v(u(v))) \end{array} \;\right) \end{align}\] But this is: \[{\vdash_{\mathsf{QF}}}\bigvee_{i \leq k} U_i \; \begin{array}{| c |} F^p_i \vec{u}\vec{v} w \\ u_i \end{array} \; \vee \bigvee_{k < i \leq k + m} V_i \; \begin{array}{| c |} F^p_i \vec{u}\vec{v} w \\ v_i \end{array} \; \vee \neg (A \vee B) \; \begin{array}{| c |} F^p_{k + m + 1} \vec{u} \vec{v} w \\ w \end{array} \;\] as required.

5.8 Double negation↩︎

Shape of \(p\): \[\begin{prooftree} \hypo{p_0} \infer1{\Gamma, A} \infer1{\Gamma, \neg \neg A} \end{prooftree}\] We recall the definition of the corresponding term transformers. Let \(f\) abbreviate \(\lambda y. F^{p_0}_{\vert \Gamma \vert + 1} \vec{u} y\). We set: \[F^p_{\vert \Gamma \vert + 1} \vec{u} v = \lambda z.f\] where \(z : \langle \neg A \rangle \to [\neg A]\) and \(v : \langle \neg \neg A \rangle = \langle \neg A \rangle \to [\neg A]\). For \(i \leq \vert \Gamma \vert\): \[F^p_i \vec{u}v = F^{p_0}_i \vec{u}((v(f))f)\]

We get: \[\begin{align} \neg\neg A \; \begin{array}{| c |} F^p_{\vert \Gamma \vert + 1} \vec{u} v \\ v \end{array} \; & = \neg\neg A \; \begin{array}{| c |} \lambda z. f \\ v \end{array} \; \\ & = \neg \left( \neg A \; \begin{array}{| c |} v((\lambda z. f)v) \\ (\lambda z.f)v \end{array} \;\right) \\ & \equiv \neg \left( \neg A \; \begin{array}{| c |} v(f) \\ f \end{array} \;\right) \\ & = \neg \neg \left( A \; \begin{array}{| c |} f((v(f))f) \\ (v(f))f \end{array} \;\right) \\ & = \neg \neg \left( A \; \begin{array}{| c |} (\lambda y. F^{p_0}_{\vert \Gamma \vert + 1} \vec{u} y)((v(f))f) \\ (v(f))f \end{array} \;\right) \\ & \equiv \neg \neg \left( A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}((v(f))f) \\ (v(f))f \end{array} \;\right) \\ & \equiv A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}((v(f))f) \\ (v(f))f \end{array} \; \\ \end{align}\]

The induction hypothesis on \(p_0\) gives: \[{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u}w \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}w \\ w \end{array} \;\] for all \(w\). Setting \(w = (v(f))f\) gives: \[{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^{p_0}_i \vec{u}((v(f))f) \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^{p_0}_{\vert \Gamma \vert + 1} \vec{u}((v(f))f) \\ (v(f))f \end{array} \;\] which is: \[{\vdash_{\mathsf{QF}}}\bigvee_{1 \leq i \leq \vert \Gamma \vert} U_i \; \begin{array}{| c |} F^p_i \vec{u}v \\ u_i \end{array} \; \vee A \; \begin{array}{| c |} F^{p}_{\vert \Gamma \vert + 1} \vec{u}v \\ v \end{array} \;\] as required.

This concludes the proof of Theorem 1.

6 Herbrand’s theorem↩︎

In this section we show how to extract Herbrand disjunctions from our functional interpretation. We first show a result that is of some independent interest, namely that any term transformer that serves as a suitable realizer of the functional interpretation of a \(\Sigma_1\)-formula yields a Herbrand disjunction.

We now get:

7 Future work↩︎

We conclude by mentioning a few possible directions for future work:

- Besides elucidating the connection between Herbrand schemes and functional interpretation, we claimed that the functional interpretation presented here could be viewed as a computational interpretation of the classical sequent calculus with concurrency. In the same vein we also pointed to some conceptual connections and analogies with the game-theoretic analysis of Herbrand’s theorem due to Alcolei et al [8]. This connection deserves to be explored further, in particular it would be interesting to see if the interpretation of realizing terms as strategies can be made formally precise.

- We handled the branching structure of traces due to contractions with the case distinction operator introduced by Gerhardy and Kohlenbach [1]. Another approach due to Ferreira and Ferreira [2] is to use a so called “Herbrandized” functional interpretation, which allows formation of terms for finite sets. This would perhaps be a more natural fit for the sequent calculus. It does however complicate the type structure a bit, which was already quite intricate here; this is why we used the case distinction operator instead. Formulating our results using a Herbrandized functional interpretation is thus left as a task for future work.

- Finally, as Herbrand schemes have been developed also for cyclic proofs in [11], it seems natural to try to extend the present results to cyclic proofs as well. There is also some encouraging background to build on here, as a cyclic version of Gödel’s System \(\mathbf{T}\) has already been explored by Das [15].

References↩︎