Theory and Applications of Categories, Vol. 17, No. 4, 2006, pp. 49–79.

THE DIALECTICA INTERPRETATION OF FIRST-ORDER CLASSICAL AFFINE LOGIC

MASARU SHIRAHATA

Abstract. We give a Dialectica-style interpretation of first-order classical affine logic. By moving to a contraction-free logic, the translation (a.k.a. D-translation) of a firstorder formula into a higher-type ∃∀-formula can be made symmetric with respect to duality, including exponentials. It turned out that the propositional part of our Dtranslation uses the same construction as de Paiva’s dialectica category 𝔾ℂ and we show how our D-translation extends 𝔾ℂ to the first-order setting in terms of an indexed category. Furthermore the combination of Girard’s ?!-translation and our D-translation results in the essentially equivalent ∃∀-formulas as the double-negation translation and Gödel’s original D-translation.

1. Introduction

Gödel’s Dialectica interpretation is a functional interpretation of Peano Arithmetic (PA) [Troelstra 1973, Hindley and Seldin 1986, Gödel 1990, Avigad and Feferman 1998]. He translated a formula of PA into a formula of the form ∃u∀x α(u, x), where u and x are sequences of higher-type variables and α is a formula of the quantifier free system T of higher-type functionals. He then showed that for every provable formula of PA one can find higher-type terms u such that α(u, x) is provable in T. The consistency of PA is thus reduced to the consistency of T, which Gödel thought is intuitively justifiable.

The translation consists of two parts. The first part is the Gödel-Gentzen doublenegation translation (¬¬-translation) of classical logic into intuitionistic logic. The second part is the so-called Dialectica translation (D-translation) of the first-order intuitionistic arithmetic (HA) into formulas of the form ∃u∀x α(u, x). For the purpose of this paper we focus only on the first-order logic, neglecting the arithmetic.

The formulas ∃u∀x α(u, x) obtained by Gödel’s D-translation easily become very much complicated. We analyze his D-translation and find that contraction is mainly responsible for this. We hence move to a contraction-free logic, specifically affine logic, although part of our work is carried out in linear logic regarded as a subsystem of affine logic. The Dtranslation can then be further decomposed and made symmetric with respect to duality, including exponentials.

It turned out that the propositional part of our D-translation uses the same construction as de Paiva’s dialectica category 𝔾ℂ [de Paiva 1991, de Paiva 2006], which is a categorical model of propositional classical linear logic. This leads us to the idea to achieve a categorical model of first-order classical linear logic. We indeed show how our D-translation extends 𝔾ℂ to the first-order setting in terms of an indexed category.

I would like to thank Valeria de Paiva and anonymous referees for their helpful comments.

Received by the editors 2004-05-17 and, in revised form, 2006-11-17.

Published on 2006-12-16 in the volume Chu spaces: theory and applications.

2000 Mathematics Subject Classification: 03B47.

Key words and phrases: linear logic, dialectica interpretation, categorical logic.

\begin{matrix}c \\ ◯ \end{matrix} Masaru Shirahata, 2006. Permission to copy for private use granted.

Furthermore the combination of Girard’s ?!-translation [Girard 1987] and our D-trans-lation results in the essentially equivalent formulas, in the sense we will define later, as the ¬¬-translation and Gödel’s original D-translation with respect to formulas of classical logic. We may hence say that our D-translation is a refinement of Gödel’s original one. We have even better correspondence if we consider Shoenfield’s version of D-translation [Shoenfield 1967] instead of Gödel’s.

Since our D-translation gives the essentially equivalent formulas as Gödel’s original with respect to classical formulas it would not be fair to say that ours simplifies Gödel’s in general. We would rather claim only that our D-translation gives us a more fine-grained control in the construction of witness terms and enables us to find simpler terms when the use of contraction is limited.

The symmetry of our D-translation suggests that it can be recapitulated in terms of games. We are hoping to be able to analyze the computational meaning of the Dialectica interpretation further in this direction.

2. Background and motivation

2.1. Gödel’s Dialectica interpretation. Gödel’s Dialectica interpretation (D-interpretation) is intended to be a technique to prove the consistency of PA [Troelstra 1973, Hindley and Seldin 1986, Gödel 1990, Avigad and Feferman 1998]. Gödel’s idea is the use of higher-type functionals to reduce the complexity of quantifier alternations. Any formula of PA is first translated (¬¬-translation) into a formula of HA, and then further translated (D-translation) into a formula of the form

∃u_{1} ⋯ ∃u_{m}∀x_{1} ⋯ ∀x_{n} α(u_{1}, …, u_{m}, x_{1}, …, x_{n}, z_{1}, …, z_{l})

where α(u_{1}, … u_{m}, x_{1}, …, x_{n}, z_{1}, …, z_{l}) is a formula of the quantifier-free system T whose free variables are among possibly higher-type variables u_{1}, …, u_{m}, x_{1}, …, x_{n} and number variables z_{1}, …, z_{l}. The propositional connectives in α(u_{1}, …, u_{m}, x_{1}, …, x_{n}, z_{1}, …, z_{l}) can be taken as classical ones since only decidable predicates are considered.

Hereafter we use a single letter v for the list of variables v_{1}, … v_{m}, and simply write α(u, x, z) for the formula α(u_{1}, … u_{m}, x_{1}, …, x_{n}, z_{1}, …, z_{l}). The list v may be empty. Furthermore we let vy stand for the list of application terms

v_{1}y_{1} ⋯ y_{n}, v_{2}y_{1} ⋯ y_{n}, …, v_{m}y_{1} ⋯ y_{n}

while vy is the empty list if v is. The variables u and x in ∃u∀x α(u, x, z) will be called positive and negative, respectively. We often suppress the free variables z and write simply ∃u∀x α(u, x) for readability.

THE DIALECTICA INTERPRETATION OF FIRST-ORDER CLASSICAL AFFINE LOGIC 51

2.2. Gödel-Gentzen ¬¬-translation. For a formula ϕ of PA, its ¬¬-translation ϕ^{N} into HA is inductively defined as follows.

1. If ϕ is atomic then ϕ^{N} ≡ ¬¬ϕ.

2. (ϕ ∧ ψ)^{N} ≡ ϕ^{N} ∧ ψ^{N}.

3. (ϕ ∨ ψ)^{N} ≡ ¬ (¬ϕ^{N} ∧ ¬ψ^{N}).

4. (ϕ ⊃ ψ)^{N} ≡ ϕ^{N} ⊃ ψ^{N}.

5. (∀x ϕ)^{N} ≡ ∀x ϕ^{N}.

6. (∃x ϕ)^{N} ≡ ¬∀x ¬ϕ^{N}. The negation ¬ϕ is regarded as the abbreviation of ϕ ⊃ ⊥ in both PA and HA. 2.3. Theorem. [Gödel-Gentzen] If ϕ is provable from ψ_{1}, ψ_{2}, …, ψ_{n} in PA then ϕ^{D} is provable from ψ_{1}^{D}, ψ_{2}^{D}, … ψ_{n}^{D} in HA. 2.4. Gödel’s D-translation. For a formula ϕ of HA, its D-translation ϕ^{D} is inductively defined together with ϕ_{D} such that ϕ^{D} ≡ ∃u∀x ϕ_{D}. For formulas ϕ and ψ which appear in the inductive clauses we rename the bound variables if necessary so that we have

ϕ^{D} ≡ ∃u∀x ϕ_{D}(u, x), ψ^{D} ≡ ∃v∀y ψ_{D}(v, y)

where there is no overlapping of variables among u, x, v, y and free variables in ϕ^{D} or ψ^{D}. 1. If ϕ is atomic then ϕ^{D} ≡ ϕ.

2. (ϕ ∧ ψ)^{D} ≡ ∃uv∀xy (ϕ_{D}(u, x) ∧ ψ_{D}(v, y)).

3. (ϕ ∨ ψ)^{D} ≡ ∃cuv∀xy ((c = 0 ∧ ϕ_{D}(u, x)) ∨ (c ≠ 0 ∧ ψ_{D}(v, y))).

4. (ϕ ⊃ ψ)^{D} ≡ ∃xv∀uy (ϕ_{D}(u, xuy) ⊃ ψ_{D}(vu, y)).

5. (∀z ϕ)^{D} ≡ ∃u∀zx ϕ_{D}(uz, x, z).

6. (∃z ϕ)^{D} ≡ ∃zu∀x ϕ_{D}(u, x, z). 2.5. Theorem. [Gödel] If ϕ is provable in HA, then there exist terms u such that u contains no negative variables in ϕ^{D} and ϕ_{D}(u, x) is provable in T.

The terms u will be called witnesses. The theorem is often formulated so that the terms u are closed terms and ϕ_{D}(uz, x, z) holds. Assuming that there is a closed term for each type we can easily convert our witnesses into this form.

2.6. The analysis of Gödel’s D-translation. The most important case in Gödel’s D-translation is (ϕ ⊃ ψ)^{D}. It quickly yields a very complicated formula due to the presence of u in xuy within the antecedent of ϕ_{D}(u, xuy) ⊃ ψ_{D}(vu, y). We analyze why u is necessary in xuy or why x needs to depend on u, and find that there are three reasons.

1. To obtain the logical equivalence of ϕ ⊃ (ψ ⊃ τ) and (ϕ ∧ ψ) ⊃ τ.

2. To make x the choice functions of u in ∃u∀x (ϕ(u, x) ⊃ ψ).

3. To obtain the validity of ϕ ⊃ ϕ ∧ ϕ, i.e., contraction.

This leads us to the idea that if we move to a contraction-free logic, and supply necessary dependency for conjunction and existential quantifier, we can dispense with u in xuy.

Guided by the above idea we will modify the D-translation to the following which we distinguish from Gödel’s by the superscript and subscript L.

2’. (ϕ ∧ ψ)^{L} ≡ ∃uv∀xy (ϕ_{L}(u, xv) ∧ ψ_{L}(v, yu)).

4’. (ϕ ⊃ ψ)^{L} ≡ ∃xv∀uy (ϕ_{L}(u, xy) ⊃ ψ_{L}(vu, y)).

6’. (∃z ϕ)^{L} ≡ ∃zu∀x ϕ_{L}(u, xu, z).

The key difference from Gödel’s original D-translation is that we erase the dependency of positive x on negative u in implication and raise instead the types of negative variables in conjunction and existential quantification.

2.7. De Paiva’s dialectica category 𝔾ℂ. Inspired by Gödel’s D-interpretation de Paiva defined two categories 𝔻ℂ and 𝔾ℂ [de Paiva 1991]. It turned out that the propositional part of our D-translation uses the same construction as 𝔾ℂ. We note that 𝔾ℂ is very closely related to Chu’s general construction of ∗-autonomous category [de Paiva 2006, Devarajan et al. 1999].

An object of 𝔾ℂ is a relation, i.e. an equivalence class of monics A [figure: α] U × X, in a base category ℂ which is required to be finitely complete.

THE DIALECTICA INTERPRETATION OF FIRST-ORDER CLASSICAL AFFINE LOGIC 53

A morphism from A [figure: α] U × X to B [figure: β] V × Y in 𝔾ℂ is a pair (f, F) of morphisms f : U → V and F : Y → X in ℂ such that there exists a morphism k which makes the diagram commute in ℂ, where the upper right and the lower left squares are pullback squares.

[figure: B′; U × Y; A′; B′; k; A′; U × Y; U × Y; U × X; id_{U} ×F; A′; U × Y; A′; A; A; U × X; α; B; V × Y; β; B′; B; B′; U × Y; U × Y; V × Y; f×id_{Y}]

The category 𝔾ℂ can be formulated more abstractly in terms of a pre-ordered fibration p : ℙ → ℂ as Hyland does with respect to 𝔻ℂ [Hyland 2002]. We regard

ℙ(I) = ({α ∈ ℙ | p(α) = I}, ⊢_{I})

as a pre-ordered collection of the predicates on I for each object I of ℂ. An Object of 𝔾ℂ is then (α, U, X) with α ∈ ℙ(U × X) and a morphism of 𝔾ℂ from (α, U, X) to (β, V, Y) is (f, F) with f : U → V and F : Y → X in ℂ such that

α_{id_{U} ×F} ⊢_{U×Y} β_{f×id_{Y}}

holds for the Cartesian liftings α_{id_{U} ×F} → α of α along id_{U} × F and β_{f×id_{Y}} → β of β along f × id_{Y}.

We will however focus entirely on the concrete case with ℂ = 𝕊𝔼𝕋 since this case is most perspicuous and sufficient to motivate our work. An object is then simply a subset of U ×X for a pair of sets U and X. Let us write α(u, x) for (u, x) ∈ α. A morphism from α ⊆ U × X to β ⊆ V × Y is then a pair (f, F) of functions f : X → Y and F : V → U such that

{(u, y) ∈ U × Y | α(u, F y)} ⊆ {(u, y) ∈ U × Y | β(fu, y)}.

holds.

The tensor product α ⊗ β of α ⊆ U × X and β ⊆ V × Y is defined as

α ⊗ β = {(u, v, x, y) ∈ (U × V) × (X^{V} × Y^{U}) | α(u, xv) ∧ β(v, yu)}.

and the internal hom object α −∘ β is

α −∘ β = {(x, v, u, y) ∈ (X^{Y} × V^{U}) × (U × Y) | α(u, xy) ⊃ β(vu, y)}.

Furthermore the linear negation α^{⊥} of α ⊆ U × X can be defined just as

α^{⊥} = {(x, u) ∈ X × U | ¬α(u, x)}

and then α⅋β = (α^{⊥} ⊗ β^{⊥})^{⊥} is

α⅋β = {(u, v, x, y) ∈ (U^{Y} × V^{X}) × (X × Y) | α(uy, x) ∨ β(vx, y)}.

The additive product α&β and coproduct α ⊕ β can also be defined.

For the exponential ! α we have two choices. One is to define

! α = {(u, x) ∈ U × (X^{∗})^{U} | ∀i ≤ ℓ(xu). α(u, proj_{i}(xu))}

where the set X^{∗} is the set of finite sequences of elements of X and ℓ(s) is the length of s ∈ X^{∗}, and the other is

! α = {(u, x) ∈ U × X^{U} | α(u, xu)}.

De Paiva uses the former definition while the latter is also indicated. As we will see later the former corresponds to the Diller-Nahm variant of D-translation and the latter to Gödel’s original.

3. The Dialectica interpretation of first-order classical affine logic

3.1. The first-order classical affine logic. In the Gentzen-style sequent calculus of classical logic we have the structural rules

\frac{⊢ Γ, ϕ, ψ, Δ}{⊢ Γ, ψ, ϕ, Δ}  \frac{⊢ Γ, ϕ, ϕ}{⊢ Γ, ϕ}  \frac{⊢ Γ}{⊢ Γ, ϕ}

called exchange, contraction and weakening, respectively, where Γ and Δ are lists of formulas. By restricting the use of some of them we obtain a family of logical systems, which are generally called substructural logics.

Linear logic is a kind of substructural logic introduced by Girard, in which we have the propositional operators ? and ! , and the use of contraction and weakening is restricted to formulas of the form ? ϕ.

For the computational aspect of logic the contraction rule is critical while weakening is often turned out not so much. For our work weakening is also admissible. We hence accept the weakening rule from the beginning and consider the first-order classical affine logic where the weakening rule

\frac{⊢ Γ}{⊢ Γ, ? ϕ}

of linear logic is replaced by the weakening for any formula ϕ. As a result of this we no longer need to distinguish multiplicative and additive constants.

We use the one-sided sequent calculus where cut has the form

\frac{⊢ Γ, ϕ ⊢ Δ, ϕ^{⊥}}{⊢ Γ, Δ}

while the linear negation of ϕ is defined by the DeMorgan duality. For the standard formulation of linear logic we refer the reader to Girard’s original paper [Girard 1987]. The following should however be noted.

1. We assume a collection of the pair of atomic n-ary predicate symbols P and P̄ such that (P(t_{1}, t_{2}, …, t_{n}))^{⊥} ≡ P̄(t_{1}, t_{2}, …, t_{n}) and (P̄(t_{1}, t_{2}, …, t_{n}))^{⊥} ≡ P(t_{1}, t_{2}, …, t_{n}). The atomic formulas with P are called positive while those with P̄ are negative.

2. We do not consider the propositional constants, not for any difficulty but for simplicity.

3. We assume the use of exchange rule freely and implicitly.

3.2. The equational system S of lambda calculus with the conditional. We consider the equational system of simply typed lambda calculus with the conditional constructor. The system will be called S for the time being. The types are constructed inductively from the single base type 0 by the operation (σ, τ) ↦ σ → τ. We assume that there are infinitely many variables and regard the pair (x, σ) of a variable x and a type σ as a variable of type σ. We write x^{σ} for (x, σ). The set of terms is defined as the smallest set satisfying

THE DIALECTICA INTERPRETATION OF FIRST-ORDER CLASSICAL AFFINE LOGIC 55

• any variable of σ is a term of σ,

• if f is an n-ary function symbol of the first-order affine logic then f is a term of

\underbrace{0 → ⋯ → 0}_{n} → 0,

• 0 and 1 are terms of 0,

• E is a term of 0 → 0 → 0,

• if P is an n-ary positive predicate symbol of the first-order affine logic then P_{f} is a

term of \underbrace{0 → ⋯ → 0}_{n} → 0,

• If s is a term of τ → σ and t is a term of τ then st is a term of σ,

• K_{σ,τ} is a term of σ → τ → σ for each pair of σ and τ,

• S_{ρ,σ,τ} is a term of (ρ → σ → τ) → (ρ → σ) → (ρ → τ) for each triple of ρ, σ and τ,

• Cond_{σ} is a term of 0 → σ → σ → σ for each σ. We will suppress the reference to types as much as possible by assuming that terms have always the matching types. From S and K we can define the lambda abstraction λx. t as usual. E and P_{f} are intended as the characteristic functions of the equality = and the predicate P, respectively.

The set of formulas is defined as the smallest set satisfying

• if P is a positive n-ary predicate symbol of the first-order affine logic and t_{1}, t_{2}, …, t_{n}

are terms of type 0 then

P(t_{1}, t_{2}, …, t_{n})

is a formula,

• if s and t are terms of type 0 then s = t is a formula,

• if α and β are formulas then ¬α, α ∧ β, α ∨ β and α ⊃ β are formulas. Formulas with no ¬, ∧, ∨, ⊃ are called atomic. We write s ≠ t for ¬s = t.

We use the axioms and inference rules of classical propositional logic and equality. In addition we have the axioms

⊢ 0 ≠ 1, ⊢ K(x, y)w = xw, ⊢ S(x, y, z)w = xz(yz)w,

⊢ x = 0 ⊃ Cond(x, y_{1}, y_{2})w = y_{1}w, ⊢ x ≠ 0 ⊃ Cond(x, y_{1}, y_{2})w = y_{2}w,
⊢ x = y ↔ E(x, y) = 0, ⊢ P (x_{1}, x_{2}, …, x_{n}) ↔ P_{f}(x_{1}, x_{2}, …, x_{n}) = 0

with fresh variables w, and the inference rules

\frac{⊢ ϕ}{⊢ ϕ[t/x]}  \frac{⊢ ϕ[s/y] ⊢ sx = tx}{⊢ ϕ[t/y]}

for any terms s and t of the matching type. The first inference rule is the rule of substitution and the second is the rule of weakly extensional equality between terms of a higher type in the style of Spector. For a higher-type terms s and t we use the expression s = t only as the abbreviation to mean that sx = tx is provable with an arbitrary x.

Note that we have the characteristic function ⌈α⌉(u, x, z) available for any formula α(u, x, z) since we can define all the classical propositional functions from the conditional constructor. The negation is

λx. Cond(x, 1, 0)

and the conjunction is

λxy. Cond(x, (Cond(y, 0, 1)), 1).

3.3. D-translation of first-order affine logic. For a formula ϕ of the first-order classical affine logic we inductively define its D-translation ϕ^{L} together with the quantifier free formula ϕ_{L} such that ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x). For formulas ϕ and ψ appearing in the inductive clauses we assume the renaming of bound variables so that

ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x), ψ^{L} ≡ ∃v∀y ψ_{L}(v, y)

where there is no overlapping of variables among u, v, x, y and free variables in ϕ^{L} or ψ^{L}.

3.4. Definition.

• P^{L} ≡ P_{L} ≡ P for a positive atomic formula P ≡ P(t_{1}, …, t_{n}).

• Q^{L} ≡ Q_{L} ≡ ¬P(t_{1}, …, t_{n}) for a negative atomic formula Q ≡ P̄(t_{1}, …, t_{n}).

• (ϕ ⊗ ψ)^{L} ≡ ∃uv∀xy (ϕ ⊗ ψ)_{L} ≡ ∃uv∀xy [ϕ_{L}(u, xv) ∧ ψ_{L}(v, yu)] .

• (ϕ⅋ψ)^{L} ≡ ∃uv∀xy (ϕ⅋ψ)_{L} ≡ ∃uv∀xy [ϕ_{L}(uy, x) ∨ ψ_{L}(vx, y)] .

• (ϕ&ψ)^{L} ≡ ∃uv∀cxy (ϕ&ψ)_{L} ≡ ∃uv∀cxy [(c = 0 ⊃ ϕ_{L}(u, x)) ∧ (c ≠ 0 ⊃ ψ_{L}(v, y))] .

• (ϕ ⊕ ψ)^{L} ≡ ∃cuv∀xy (ϕ ⊕ ψ)_{L} ≡ ∃cuv∀xy [(c = 0 ∧ ϕ_{L}(u, x)) ∨ (c ≠ 0 ∧ ψ_{L}(v, y))] .

• (∀z ϕ(z))^{L} ≡ ∃u∀xz (∀z ϕ(z))_{L} ≡ ∃u∀xz ϕ_{L}(uz, x, z).

• (∃z ϕ(z))^{L} ≡ ∃uz∀x (∃z ϕ(z))_{L} ≡ ∃uz∀x ϕ_{L}(u, xz, z).

• ( ! ϕ)^{L} ≡ ∃u∀x ( ! ϕ)_{L} ≡ ∃u∀x ϕ_{L}(u, xu).

• ( ? ϕ)^{L} ≡ ∃u∀x ( ? ϕ)_{L} ≡ ∃u∀x ϕ_{L}(ux, x).

3.5. Lemma. Suppose ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x). Then

(ϕ^{⊥})^{L} ≡ ∃x∀u (ϕ^{⊥})_{L}(u, x) ≡ ∃x∀u ¬ϕ_{L}(u, x).

Proof. The proof is by induction on the construction of affine logic formulas. The atomic case is obvious. The inductive cases are shown as follows.

[(ϕ ⊗ ψ)^{⊥}]^{L} ≡ (ϕ^{⊥}⅋ψ^{⊥})^{L}
≡ ∃xy∀uv [(ϕ^{⊥})_{L}(u, xv) ∨ (ψ^{⊥})_{L}(v, yu)]
≡ ∃xy∀uv [¬ϕ_{L}(u, xv) ∨ ¬ψ_{L}(v, yu)]
≡ ∃xy∀uv ¬ [ϕ_{L}(u, xv) ∧ ψ_{L}(v, yu)] .

[(ϕ&ψ)^{⊥}]^{L} ≡ (ϕ^{⊥} ⊕ ψ^{⊥})^{L}
≡ ∃cxy∀uv [(c = 0 ∧ (ϕ^{⊥})_{L}(u, x)) ∨ (c ≠ 0 ∧ (ψ^{⊥})_{L}(v, y))]
≡ ∃cxy∀uv [(c = 0 ∧ ¬ϕ_{L}(u, x)) ∨ (c ≠ 0 ∧ ¬ψ_{L}(v, y))]
≡ ∃cxy∀uv ¬ [(c = 0 ⊃ ϕ_{L}(u, x)) ∧ (c ≠ 0 ⊃ ψ_{L}(v, y))] .

[( ! ϕ)^{⊥}]^{L} ≡ (! ϕ^{⊥})^{L}
≡ ∃x∀u (ϕ^{⊥})_{L}(ux, x)
≡ ∃x∀u ¬ϕ_{L}(ux, x).

The cases for ϕ⅋ψ, ϕ ⊕ ψ and ? ϕ are shown similarly.

3.6. The Dialectica interpretation of first-order classical affine logic. We will prove the theorem analogous to Theorem 2.5 for the first-order classical affine logic using ϕ^{L} and S instead of ϕ^{D} and T.

3.7. Theorem. If ϕ is provable in first-order classical affine logic, then there exist terms u such that u contains no negative variables in ϕ^{L} and ϕ_{L}(u, x) is provable in S.

The proof is by induction on the construction of proofs. We suppress the variables z in α(u, x, z) as much as possible as before. First let us prepare some preliminary lemmas.

3.8. Lemma. Let ϕ ≡ ϕ_{1}⅋ϕ_{2} and ψ ≡ ϕ_{2}⅋ϕ_{1}. Then ϕ_{L}(u, x) ↔ ψ_{L}(u, x) holds.

Proof. Let (ϕ_{i})^{L} ≡ ∃u_{i}∀x_{i}(ϕ_{i})_{L}(u_{i}, x_{i}). Then ϕ_{L} ≡ (ϕ_{1})_{L}(u_{1}x_{2}, x_{1}) ∨ (ϕ_{2})_{L}(u_{2}x_{1}, x_{2}) and ψ_{L} ≡ (ϕ_{2})_{L}(u_{2}x_{1}, x_{2}) ∨ (ϕ_{1})_{L}(u_{1}x_{2}, x_{1}).

3.9. Lemma. Let ϕ ≡ (ϕ_{1}⅋ϕ_{2})⅋ϕ_{3} and ψ ≡ ϕ_{1}⅋(ϕ_{2}⅋ϕ_{3}). There exist closed terms t_{i} and s_{i} such that

\{ \begin{matrix}ϕ_{L}(u_{1}, u_{2}, …, u_{n}, x) ↔ ψ_{L}(t_{1}u_{1}, t_{2}u_{2}, …, t_{n}u_{n}, x) \\ ϕ_{L}(s_{1}u_{1}, s_{2}u_{2}, …, s_{n}u_{n}, x) ↔ ψ_{L}(u_{1}, u_{2}, …, u_{n}, x) \end{matrix}

hold where u_{1}, u_{2}, …, u_{n} is the list of all positive variables.

Proof. For each positive u_{ik} of (ϕ_{i})_{L} we have (ϕ_{i})_{L}(u_{ik}y, x_{i}) in ϕ_{L} and (ϕ_{i})_{L}(u_{ik}z, x_{i}) in ψ_{L} where y and z are permutations of negative x_{j}’s with i ≠ j. Let t_{ik} ≡ λuz. uy and s_{ik} ≡ λuy. uz.

3.10. Lemma. Let ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x) and ψ^{L} ≡ ∃v∀y ψ_{L}(v, y). There exist closed terms t_{i} and s_{i} such that

\{ \begin{matrix}( ? ϕ⅋ψ)_{L}(u_{1}, …, u_{n}, v, x, y) ↔ ϕ_{L}(t_{1}u_{1}z_{1}, …, t_{n}u_{n}z_{n}, x) ∨ ψ_{L}(vx, y) \\ ( ? ϕ⅋ψ)_{L}(s_{1}u_{1}, …, s_{n}u_{n}, v, x, y) ↔ ϕ_{L}(u_{1}z_{1}, …, u_{n}z_{n}, x) ∨ ψ_{L}(vx, y) \end{matrix}

hold where z_{i} is a permutation of x, y and u_{1}, u_{2}, …, u_{n} is the list u.

Proof. Recall ( ? ϕ⅋ψ)_{L} ≡ ϕ_{L}(u_{1}yx, …, u_{n}yx, x) ∨ ψ_{L}(vx, y). Let t_{i} ≡ λuz_{i}. uyx and s_{i} ≡ λyx. uz_{i}.

Lemma 3.9 takes care of the parenthesizing with respect to ⅋ and lets us handle the list Γ as a single formula. Lemma 3.8 together with Lemma 3.9 justifies the implicit use of exchange. Lemma 3.10 is used for the promotion rule. With this preparation in mind let us begin the proof of Theorem 3.7.

Axioms.

⊢ ϕ, ϕ^{⊥}

Let ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x). By Lemma 3.5 we have (ϕ^{⊥})^{L} ≡ ∃x∀u ¬ϕ_{L}(u, x). Renaming variables we need to find u and x such that

ϕ_{L}(uv, y) ∨ ¬ϕ_{L}(v, xy)

holds. The identities λv. v and λy. y suffice for them.

⊗-rule.

\frac{⊢ Γ, ϕ ⊢ Δ, ψ}{⊢ Γ, Δ, ϕ ⊗ ψ}

Let

\begin{matrix}Γ^{L} ≡ ∃w_{1}∀z_{1} Γ_{L}(w_{1}, z_{1}), & ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x), \\ Δ^{L} ≡ ∃w_{2}∀z_{2} Δ_{L}(w_{2}, z_{2}), & ψ^{L} ≡ ∃v∀y ψ_{L}(v, y). \end{matrix}

By the inductive hypothesis we have already found the witness terms u, v, w_{1} and w_{2} such that we can prove

Γ_{L}(w_{1}x, z_{1}) ∨ ϕ_{L}(uz_{1}, x) and Δ_{L}(w_{2}y, z_{2}) ∨ ψ_{L}(vz_{2}, y),

and we need to find witnesses ũ, ṽ, w̃_{1} and w̃_{2} such that

Γ_{L}(w̃_{1}xyz_{2}, z_{1}) ∨ Δ_{L}(w̃_{2}xyz_{1}, z_{2}) ∨ [ϕ_{L}(ũz_{1}z_{2}, x(ṽz_{1}z_{2})) ∧ ψ_{L}(ṽz_{1}z_{2}, y(ũz_{1}z_{2}))]

holds. We may choose them so that we have

ũz_{1}z_{2} = uz_{1}, ṽz_{1}z_{2} = vz_{2}

and

w̃_{1}xyz_{2} = w_{1}(x(ṽz_{1}z_{2})) = w_{1}(x(vz_{2})), w̃_{2}xyz_{1} = w_{2}(y(ũz_{1}z_{2})) = w_{2}(y(uz_{1})).

where x and y have the types assigned in the lower sequent. From the inductive hypothesis we can prove

Γ_{L}(w_{1}(x(vz_{2})), z_{1}) ∨ ϕ_{L}(uz_{1}, x(vz_{2})) and Δ_{L}(w_{2}(y(uz_{1})), z_{2}) ∨ ψ_{L}(vz_{2}, y(uz_{1}))

by substitution. The conclusion then follows by the propositional calculus.

⅋-rule.

\frac{⊢ Γ, ϕ, ψ}{⊢ Γ, ϕ⅋ψ}

The case reduces to Lemma 3.9.

&-rule.

\frac{⊢ Γ, ϕ ⊢ Γ, ψ}{⊢ Γ, ϕ&ψ}

For two copies of Γ in the upper sequents we let

Γ^{L} ≡ ∃w_{1}∀z_{1} Γ_{L}(w_{1}, z_{1}), Γ^{L} ≡ ∃w_{1}∀z_{1} Γ_{L}(w_{2}, z_{2})

and for Γ in the lower sequent

Γ^{L} ≡ ∃w∀z Γ_{L}(w, z).

Let ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x) and ψ^{L} ≡ ∃v∀y ψ_{L}(v, y). By inductive hypothesis there exist u, v, w_{1} and w_{2} such that

Γ_{L}(w_{1}x, z_{1}) ∨ ϕ_{L}(uz_{1}, x), Γ_{L}(w_{2}y, z_{2}) ∨ ψ_{L}(vz_{2}, y)

hold. We need to find ũ, ṽ and w̃ such that

Γ_{L}(w̃cxy, z) ∨ [(c = 0 ⊃ ϕ_{L}(ũz, x)) ∧ (c ≠ 0 ⊃ ψ_{L}(ṽz, y))]

holds. We choose ũ and ṽ so that we have ũz = uz and ṽz = vz, and choose w̃ according to c so that

w̃cxy = \{ \begin{matrix}w_{1}x & if c = 0 \\ w_{2}y & otherwise \end{matrix}

holds. Since we have the conditional we can in fact extract w̃ from the equation

w̃cxy = Cond(c, w_{1}x, w_{2}y).

The conclusion then follows from the inductive hypothesis by the propositional calculus.

⊕-rule.

\frac{⊢ Γ, ϕ_{i}}{⊢ Γ, ϕ_{1} ⊕ ϕ_{2}} (i = 1, 2)

For ϕ_{i} in the upper sequent we let (ϕ_{i})^{L} ≡ ∃u∀x (ϕ_{i})_{L}(u, x) and for ϕ_{1} and ϕ_{2} in the lower sequent

(ϕ_{1})^{L} ≡ ∃u_{1}∀x_{1} (ϕ_{1})_{L}(u_{1}, x_{1}), (ϕ_{2})^{L} ≡ ∃u_{2}∀x_{2} (ϕ_{2})_{L}(u_{2}, x_{2}).

Let Γ^{L} ≡ ∃v∀y Γ_{L}(v, y). By the inductive hypothesis we have u and v such that

Γ_{L}(vx, y) ∨ (ϕ_{i})_{L}(uy, x)

holds. We need to find c̃, ũ_{1}, ũ_{2} and ṽ such that

Γ_{L}(ṽx_{1}x_{2}, y) ∨ [(c̃y = 0 ∧ (ϕ_{1})_{L}(ũ_{1}y, x_{1})) ∨ (c̃y ≠ 0 ∧ (ϕ_{2})_{L}(ũ_{2}y, x_{2}))]

holds. If i = 1 we choose c̃, ũ_{1} and ṽ so that we have

c̃y = 0, ũ_{1}y = ũy, ṽx_{1}x_{2} = vx_{1}

while ũ_{2} can be any term of the matching type. If i = 2 we choose c̃, ũ_{2} and ṽ so that we have

c̃y = 1, ũ_{2}y = ũy, ṽx_{1}x_{2} = vx_{2}

while ũ_{1} can be any term of the matching type. The conclusion then follows from the inductive hypothesis by the propositional calculus.

∀-rule.

\frac{⊢ Γ, ϕ}{⊢ Γ, ∀y ϕ}

Let Γ^{L} ≡ ∃w∀z Γ_{L}(w, z) and ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x, y). By the inductive hypothesis we have u and w such that

Γ_{L}(wx, z) ∨ ϕ_{L}(uz, x, y)

holds, and we need to find ũ and w̃ such that

Γ_{L}(w̃xy, z) ∨ ϕ_{L}(ũyz, x, y)

holds. We choose them in such a way that we have

ũyz = uz,  w̃xy = wx

where ũ and w̃ may contain y as a free variable. The conclusion then immediately follows from the hypothesis.

The eigenvariable condition is crucial since if Γ contained a free y we would have to rename y in (∀y ϕ)^{L} resulting in

Γ_{L}(w̃xy′, z, y) ∨ ϕ_{L}(ũy′z, x, y′)

which is no longer derivable from the hypothesis.

∃-rule.

\frac{⊢ Γ, ϕ[t/v]}{⊢ Γ, ∃v ϕ}

Let Γ^{L} ≡ ∃w∀z Γ_{L}(w, z) and (ϕ[t/v])^{L} ≡ ∃u∀x (ϕ[t/v])_{L}(u, x) where u and x are different from v and any free variable in t. We hence have

∃u∀x (ϕ[t/v])_{L}(u, x) ≡ ∃u∀x (ϕ_{L}(u, x, v)[t/v]) ≡ ∃u∀x ϕ_{L}(u, x, t).

By the inductive hypothesis there exist w and u such that

Γ_{L}(wx, z) ∨ ϕ_{L}(uz, x, t)

holds. We need to find w̃, ũ and ṽ such that

Γ_{L}(w̃x, z) ∨ ϕ_{L}(ũz, x(ṽz), ṽz)

holds. It suffices to have

ũz = uz, ṽz = t, w̃x = w(x(ṽz)) = w(xt)

where x has the type in the lower sequent. Since t contains neither x nor z we can construct ṽ without using x, and w̃ without using z. The conclusion follows from the hypothesis by substitution.

Cut.

\frac{⊢ Γ, ϕ ⊢ Δ, ϕ^{⊥}}{⊢ Γ, Δ}

Let

\begin{matrix}Γ^{L} ≡ ∃v∀y Γ_{L}(v, y), Δ^{L} ≡ ∃w∀z Δ_{L}(w, z), \\ ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x). \end{matrix}

Then (ϕ^{⊥})^{L} ≡ ∃x∀u ¬ϕ_{L}(u, x) by Lemma 3.5. By the inductive hypothesis we have v, w, u and x such that

Γ_{L}(vx, y) ∨ ϕ_{L}(uy, x), Δ_{L}(wu, z) ∨ ¬ϕ_{L}(u, xz)

both hold. We need to find ṽ and w̃ such that

Γ_{L}(ṽz, y) ∨ Δ_{L}(w̃y, z)

hold. Consider the substitution instances

Γ_{L}(v(xz), y) ∨ ϕ_{L}(uy, xz), Δ_{L}(w(uy), z) ∨ ¬ϕ_{L}(uy, xz)

from the inductive hypothesis. It follows from them by the propositional calculus that

Γ_{L}(v(xz), y) ∨ Δ_{L}(w(uy), z).

We hence choose ṽ and w̃ so that we have

ṽz = v(xz),  w̃y = w(uy).

The conclusion then holds immediately.

Weakening.

\frac{⊢ Γ}{⊢ Γ, ϕ}

Let Γ^{L} ≡ ∃v∀y Γ_{L}(v, y) and ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x). By the inductive hypothesis there exists v such that

Γ_{L}(v, y)

holds. We need to find ũ and ṽ such that

Γ_{L}(ṽx, y) ∨ ϕ_{L}(ũy, x)

holds. For this it suffices to have ṽx = ṽ. Any term of the matching type would do for ũ.

Dereliction.

\frac{⊢ Γ, ϕ}{⊢ Γ, ? ϕ}

Let Γ^{L} ≡ ∃v∀y Γ_{L}(v, y) and ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x). By the inductive hypothesis there exist u and v such that

Γ_{L}(vx, y) ∨ ϕ_{L}(uy, x)

holds. We need to find ũ and ṽ such that

Γ_{L}(ṽx, y) ∨ ϕ_{L}(ũxy, x)

holds. It suffices to have ṽx = vx and ũxy = ux.

Contraction.

\frac{⊢ Γ, ? ϕ, ? ϕ}{⊢ Γ, ? ϕ}

Let Γ^{L} ≡ ∃v∀y Γ_{L}(v, y). For two copies of ? ϕ in the upper sequent we let

( ? ϕ)_{L} ≡ ∃u_{1}∀x_{1} ϕ_{L}(u_{1}x_{1}, x_{1}), ( ? ϕ)_{L} ≡ ∃u_{2}∀x_{2} ϕ_{L}(u_{2}x_{2}, x_{2})

respectively. For ? ϕ in the lower sequent we let

( ? ϕ)^{L} ≡ ∃u∀x ϕ^{L}(ux, x).

By the inductive hypothesis we have u_{1}, u_{2} and v such that

Γ_{L}(vx_{1}x_{2}, y) ∨ ϕ_{L}(u_{1}x_{1}x_{2}y, x_{1}) ∨ ϕ_{L}(u_{2}x_{1}x_{2}y, x_{2})

holds. We need to find ũ and ṽ such that

Γ_{L}(ṽx, y) ∨ ϕ_{L}(ũxy, x)

holds. To find them we first force x_{1} and x_{2} in the inductive hypothesis to the identical x by substitution so that

Γ_{L}(vxx, y) ∨ ϕ_{L}(u_{1}xxy, x) ∨ ϕ_{L}(u_{2}xxy, x).

We then choose ũ and ṽ in such a way that

ṽx = vxx, ũxy = \{ \begin{matrix}u_{1}xxy & if ϕ_{L}(u_{1}xxy, x) \\ u_{2}xxy & otherwise. \end{matrix}

Since we have the characteristic function ⌈ϕ_{L}(u_{1}xxy, x)⌉(x, y) of ϕ_{L}(u_{1}xxy, x) with

ϕ_{L}(u_{1}xxy, x) ↔ ⌈ϕ_{L}(u_{1}xxy, x)⌉(x, y) = 0

we can in fact extract ũ from the equation

ũxy = (Cond(⌈ϕ_{L}(u_{1}xxy, x)⌉(x, y), u_{1}, u_{2})) xyy.

The conclusion then follows by the propositional logic, using proof by cases.

The above tactics would not work if ? ϕ was just ϕ. The inductive hypothesis would then become

Γ_{L}(vx_{1}x_{2}, y) ∨ ϕ_{L}(u_{1}x_{2}y, x_{1}) ∨ ϕ_{L}(u_{2}x_{1}y, x_{2})

and the conclusion

Γ_{L}(ṽx, y) ∨ ϕ_{L}(ũy, x).

We would then not be able to choose between u_{1}xy and u_{2}xy in ũ since x would not be available to ũ.

Promotion.

\frac{⊢ ? Γ, ϕ}{⊢ ? Γ, ! ϕ}

Let ? Γ be the list ? ψ_{1}, ? ψ_{2}, … ? ψ_{n} and (ψ_{i})^{L} ≡ ∃v_{i}∀y_{i} (ψ_{i})_{L}(v_{i}, y_{i}) for 1 ≤ i ≤ n. By Lemma 3.10 we may write

( ? Γ)^{L} ≡ ∃v∀y [(ψ_{1})_{L}(v_{1}y, y_{1}) ∨ (ψ_{2})_{L}(v_{2}y, y_{2}) ∨ ⋯ ∨ (ψ_{n})_{L}(v_{n}y, y_{n})]

with v and y being the concatenations of v_{1}, v_{2}, …, v_{n} and y_{1}, y_{2}, …, y_{n}, respectively. We write ψ(z, y) for the quantifier free formula

(ψ_{1})_{L}(z_{1}, y_{1}) ∨ (ψ_{2})_{L}(z_{2}, y_{2}) ∨ ⋯ ∨ (ψ_{n})_{L}(z_{n}, y_{n}).

with z being the concatenation of z_{1}, z_{2}, …, z_{n} so that ( ? Γ)^{L} ≡ ∃v∀y ψ(vy, y). Let ϕ^{L} ≡ ∃u∀x ϕ_{L}(u, x). By the inductive hypothesis we have u and v such that

ψ(vxy, y) ∨ ϕ_{L}(uy, x)

holds, and we need to find ũ and ṽ such that

ψ(ṽxy, y) ∨ ϕ_{L}(ũy, x(ũy))

holds. We choose ũ and ṽ so that we have

ũy = uy,  ṽxy = v(x(ũy))y = v(x(uy))y

where x has the type in the lower sequent. The conclusion then follows from the inductive hypothesis by substitution.

The above tactics would not work if ? Γ was just Γ. The inductive hypothesis would then become

Γ_{L}(vx, y) ∨ ϕ_{L}(uy, x)

and the conclusion

Γ_{L}(ṽx, y) ∨ ϕ_{L}(ũy, x(ũy)).

We would then not be able to choose ṽ so that ṽx = v(x(uy)) since some of the variables in y would not be available to ṽ.

3.11. The Diller-Nahm variant of the Dialectica interpretation. In Gödel’s original Dialectica interpretation we need first evaluate the truth value of a formula within a witness term for the contraction, in the same way as we have just seen. This causes no problem since the only predicate considered is the equality between natural numbers, whose characteristic function is primitive recursive.

The Dialectica interpretation can be naturally extended to higher-order systems. We then need to consider the equality between higher-type functionals, whose characteristic function is, however, neither continuous nor provably recursive. This observation motivated Diller and Nahm to give a variant of the Dialectica interpretation, in which the use of characteristic function is no longer necessary [Diller and Nahm 1974].

The Diller-Nahm variant of the Dialectica interpretation is also important from the viewpoint of categorical logic, as pointed out by Hyland [Hyland 2002]. The categorical counterpart of the standard Dialectica interpretation forms a symmetric monoidal closed category, while the Diller-Nahm variant immediately yields a Cartesian closed category.

We can modify our D-translation in the style of Diller-Nahm simply by adopting the definition ! α = {(u, x) ∈ U × (X^{∗})^{U} | ∀i ≤ ℓ(xu). α(u, proj_{i}(xu))} and its dual form for ? α in de Paiva’s 𝔾ℂ [de Paiva 1991]. We first need to extend types so that we have the type σ^{∗} for each type σ. Its intended interpretation ⟦σ^{∗}⟧ is the free commutative monoid X^{∗} generated from ⟦σ⟧ = X. We also need to extend terms to represent the monoid unit e ∈ X^{∗}, the monoid multiplication · : X^{∗} × X^{∗} → X^{∗}, the unit map η_{X} : X → X^{∗} and the counit map ϵ_{X^{∗}} : X^{∗∗} → X^{∗}. For a ∈ X and s ∈ X^{∗} we write a ∈ s if s = s′η_{X}(a) for some s′ ∈ X^{∗}.

For the sake of simplicity we only consider the case where the formula α has a single positive variable u and a single negative variable x.

We define the operations ( )^{∘} and ( )^{•} on the formula α(u, v) by

α^{∘}(u, x) iff for some w ∈ u, α(w, x)

where the type of u is raised from τ → σ to τ → σ^{∗}, and

α^{•}(u, x) iff for all z ∈ x, α(u, z)

where the type of x is raised as before.

The modified translation ϕ^{DN} is the same as ϕ^{L} except for

• ( ? ϕ)^{DN} ≡ ∃u∀x (ϕ_{DN})^{∘} (ux, x),

• ( ! ϕ)^{DN} ≡ ∃u∀x (ϕ_{DN})^{•} (u, xu).

This gives us the translation

( ! ϕ −∘ ψ)^{DN} ≡ ∃xv∀uy [(ϕ_{DN})^{•} (u, xyu) ⊃ ψ_{DN}(vu, y)]

as Hyland defined for the intuitionistic implication ϕ ⊃ ψ.

3.12. The first-order extension of 𝔾ℂ. De Paiva’s 𝔾ℂ gives us a categorical model of propositional classical linear logic. We show how our D-translation extends 𝔾ℂ to the first-order setting in terms of an indexed category. Such an extension is already given for variants of 𝔻ℂ [Hyland 2002, Streicher 2000]. We however think that it is worthwhile looking into our construction in some detail since it is concrete and simple. The construction is quite general, but we again focus on the the case where ℂ = 𝕊𝔼𝕋.

We first define the category 𝔾ℂ(Z) for each object Z in ℂ. An object is a subset of U × X × Z for a pair of sets U and X with the fixed Z.

{(u, x, z) ∈ U × X × Z | α(u, x, z)}.

A morphism from α ⊆ U × X × Z to β ⊆ V × Y × Z is a pair (f, F) of morphisms f : U × Z → V and F : Y × Z → X such that

{(u, y, z) ∈ U × Y × Z | α(u, F yz, z)} ⊆ {(u, y, z) ∈ U × Y × Z | β(fuz, y, z)}

holds. The composition of a morphism (f, F) from α to β and a morphism (g, G) from β to γ is then defined as (g ∘ ⟨f, proj_{2}⟩, F ∘ ⟨G, proj_{2}⟩). It amounts to derive

α(u, F (Gz′z)z, z) ⊃ γ(g(fuz)z, z′, z)

from

\{ \begin{matrix}α(u, F yz, z) ⊃ β(fuz, y, z) \\ β(v, Gz′z, z) ⊃ γ(gvz, z′, z) \end{matrix}

by substituting fuz for v and Gz′z for y.

The ∗-autonomous structures of 𝔾ℂ can be naturally extended to 𝔾ℂ(Z) by defining

α^{⊥} = {(x, u, z) ∈ X × U × Z | ¬α(u, x, z)},
α ⊗ β = {(u, v, x, y, z) | (U × V) × (X^{V} × Y^{U}) × Z | α(u, xv, z) ∧ β(v, yu, z)}

for α ⊆ U × X × Z and β ⊆ V × Y × Z. The monoidal closedness is established by the bijection between (f, ⟨F_{1}, F_{2}⟩) and (⟨f̃_{1}, f̃_{2}⟩, F̃) in

\begin{matrix}α(u, (F_{1}z′z)v, z) ∧ β(v, (F_{2}z′z)u, z) ⊃ γ(fuvz, z′, z), \\ α(u, F̃vz′z, z) ⊃ β(v, (f̃_{1}uz)z′, z) ⊃ γ((f̃_{2}uz)v, z′, z). \end{matrix}

Furthermore we have a functor f^{−1} from 𝔾ℂ(Z) to 𝔾ℂ(Z′) for any f : Z′ → Z in ℂ defined by

\{ \begin{matrix}f^{−1}(α) = \{(u, x, z′) ∈ U × X × Z′ | α(u, x, fz′)\}, \\ f^{−1}(g, G) = (g ∘ (id_{U} × f), G ∘ (id_{Y} × f)) \end{matrix}

for α ⊆ U × X × Z and g : U × Z → V, G : Y × Z → X. It just changes α(u, Gyz, z) ⊃ β(guz, y, z) into

α(u, Gy(fz′), fz′) ⊃ β(gu(fz′), y, fz′).

We hence established that the pair of maps

\{ \begin{matrix}Z ↦ 𝔾ℂ(Z), \\ f ↦ f^{−1} \end{matrix}

is a contravariant functor from ℂ = 𝕊𝔼𝕋 to ℂ𝔸𝕋, i.e. an indexed category.

The quantifiers ∀ and ∃ are functors from 𝔾ℂ(Z × Z′) to 𝔾ℂ(Z′) defined according to our D-translation. The functor ∀ is given by

\{ \begin{matrix}∀(α) = \{(u, x, z, z′) ∈ U^{Z} × X × Z × Z′ | α(uz, x, z, z′)\}, \\ ∀(f, F) = (λuz′λz. f(uz)zz′, ⟨F, proj_{2}⟩) \end{matrix}

for α ⊆ U × X × (Z × Z′) and f : U × Z × Z′ → V, F : Y × Z × Z′ → X. It just changes

α(u, F yzz′, z, z′) ⊃ β(fuzz′, y, z, z′)

into ∀α(u, F yzz′, z, z′) ⊃ ∀β(λz.f(uz)zz′, y, z, z′) which is further equivalent to

α(uz, F yzz′, z, z′) ⊃ β(f(uz)zz′, y, z, z′).

The functor ∃ is similarly defined.

The functors ∀ and ∃ are the right and left adjoints to the functor proj_{2}^{−1}, respectively. The adjunction of proj_{2}^{−1} and ∀ is given by the bijection (F, f) ↦ (F, λuz′λz. fuzz′) as seen by

proj_{2}^{−1}(α)(u, F yzz′, z, z′) ⊃ β(fuzz′, y, z, z′)

and

α(u, F yzz′, z′) ⊃ ∀(β)((λuz′λz. fuzz′) uz′, y, z, z′)

both of which are equivalent to

α(u, F yzz′, z′) ⊃ β(fuzz′, y, z, z′).

Similarly for the adjunction of ∃ and proj_{2}^{−1} due to the symmetry.

The Beck-Chevalley condition for ∀ is f^{−1} ∘ ∀(α) ≅ ∀ ∘ (id_{Z} × f)^{−1}(α) which holds immediately, and similarly for ∃. Hence we have the following.

3.13. Theorem. The indexed category Z ↦ 𝔾ℂ(Z) is a hyperdoctrine with ℂ = 𝕊𝔼𝕋.

4. The double negation and ? ! translations

4.1. Gödel-Gentzen double-negation translation. Formulas of classical logic can be translated either into intuitionistic logic by ¬¬-translation or into classical linear logic by ?!-translation. We hence have the situation depicted as below.

[figure: Intuitionistic Logic; Higher-type ∃∀-formulas; _{( )}_{D}; Classical Logic; Intuitionistic Logic; ¬¬; Classical Logic; Classical Linear Logic; ?!; Classical Linear Logic; Higher-type ∃∀-formulas; ^{( )}^{L}]

where we regard linear logic as a subsystem of affine logic. We can in fact modify the ¬¬- and ?!-translations to logically equivalent ones and establish that the modified ?!- translation and ϕ^{L} give the essentially equivalent ∃∀-formulas, in the sense we will define, as the modified ¬¬-translation and ϕ^{D}.

We start with the Gödel-Gentzen double-negation translation of classical logic to intuitionistic logic. It is defined inductively [Avigad and Feferman 1998] by

1. ϕ^{N} ≡ ¬¬ϕ for ϕ atomic,

2. (ϕ ∧ ψ)^{N} ≡ ϕ^{N} ∧ ψ^{N},

3. (ϕ ∨ ψ)^{N} ≡ ¬(¬ϕ^{N} ∧ ¬ψ^{N}),

4. (ϕ ⊃ ψ)^{N} ≡ ϕ^{N} ⊃ ψ^{N},

5. (¬ϕ)^{N} ≡ ¬ϕ^{N},

6. (∀xϕ)^{N} ≡ ∀xϕ^{N},

7. (∃xϕ)^{N} ≡ ¬∀x¬ϕ^{N} where the logical symbols on the left of ≡ are classical while those on the right are intuitionistic.

This translation is known as the double-negation translation (a.k.a. ¬¬-translation). In fact ϕ^{N} is equivalent to ¬¬ϕ^{N} in intuitionistic logic. We can hence safely modify the Gödel-Gentzen double-negation translation to the following.

1. ϕ^{N} ≡ ¬¬ϕ for ϕ atomic,

2. (ϕ ∧ ψ)^{N} ≡ ¬¬(ϕ^{N} ∧ ψ^{N}),

3. (ϕ ∨ ψ)^{N} ≡ ¬(¬ϕ^{N} ∧ ¬ψ^{N}),

4. (¬ϕ)^{N} ≡ ¬ϕ^{N},

5. (∀xϕ)^{N} ≡ ¬¬∀xϕ^{N},

6. (∃xϕ)^{N} ≡ ¬∀x¬ϕ^{N} where we no longer use ⊃ as a primitive logical connective in classical logic.

68  MASARU SHIRAHATA

4.2. Proposition. ϕ^{N} is equivalent to ϕ^{N} in intuitionistic logic. Proof. The proof is by induction on ϕ. It suffices to check the cases of ϕ ∧ ψ and ∀xϕ.

(ϕ ∧ ψ)^{N} ≡ ¬¬(ϕ^{N} ∧ψ^{N}) is equivalent to ¬¬(ϕ^{N} ∧ψ^{N}) ≡ ¬¬(ϕ ∧ ψ)^{N} by the inductive hypothesis, which is in turn equivalent to (ϕ ∧ ψ)^{N}.

(∀xϕ)^{N} ≡ ¬¬∀xϕ^{N} is equivalent to ¬¬∀xϕ^{N} ≡ ¬¬(∀xϕ)^{N} by the inductive hypothesis which is in turn equivalent to (∀xϕ)^{N}. 4.3. Girard’s ? ! translation. The Gödel-Gentzen double-negation translation can be understood as the interior-closure operation on open sets. In the phase semantics of linear logic the exponentials ? and ! are the closure and interior operations on facts. Girard extends this analogy to the translation of classical logic to linear logic [Girard 1987] given by

1. ϕ^{†} ≡ ? ! ϕ for ϕ atomic,

2. (ϕ ∨ ψ)^{†} ≡ ϕ^{†}⅋ψ^{†},

3. (¬ϕ)^{†} ≡ ? (ϕ^{†⊥}),

4. (∀xϕ)^{†} ≡ ? ! ∀xϕ^{†},

5. (ϕ ∧ ψ)^{†} ≡ (¬(¬ϕ ∨ ¬ψ))^{†} ≡ ? ( ! ϕ^{†} ⊗ ! ψ^{†}),

6. (∃xϕ)^{†} ≡ (¬∀x¬ϕ)^{†} ≡ ? ! ? ∃x ! (ϕ^{†}). We call this translation ?!-translation. In fact ϕ^{†} is equivalent to ? ! ϕ^{†} in linear logic as seen from the following equivalences.

• ? ! ϕ and ? ! ? ! ϕ,

• ? ! ϕ⅋ ? ! ψ and ? ! ( ? ! ϕ⅋ ? ! ψ),

• ? ( ! ϕ ⊗ ! ψ) and ? ! ? ( ! ϕ ⊗ ! ψ). Furthermore we can simplify the translation of ∃xϕ to ? ∃x ! ϕ which is equivalent to ? ! ? ∃x ! ϕ.

We can then safely modify Girard’s ?!-translation to the following.

1. ϕ^{+} = ? ! ϕ for ϕ atomic,

2. (ϕ ∨ ψ)^{+} = ? ! ϕ^{+}⅋ ? ! ψ^{+},

3. (¬ϕ)^{+} = ? (ϕ^{+⊥}),

4. (∀xϕ)^{+} = ? ! ∀xϕ^{+},

5. (ϕ ∧ ψ)^{+} = ? ( ! ϕ^{+} ⊗ ! ψ^{+}),

6. (∃xϕ)^{+} = ? ∃x ! ϕ^{+}.

4.4. Proposition. ϕ^{+} is equivalent to ϕ^{†} in linear logic.

Proof. The proof is by induction on ϕ. It suffices to check the disjunction. (ϕ ∨ ψ)^{†} = ϕ^{†}⅋ψ^{†} is equivalent to ? ! ϕ^{†}⅋ ? ! ψ^{†}, which is equivalent to ? ! ϕ^{+}⅋ ? ! ψ^{+} = (ϕ ∨ ψ)^{+} by the inductive hypothesis.

4.5. Relating the two translations. Let us consider the set V T of terms which are constructed from variables and application only. V T is defined as the smallest set satisfying

• u ∈ V T for any variable u,

• if s ∈ V T and t ∈ V T then st ∈ V T.

Any term s in V T has the form

u_{s}t_{1}t_{2} … t_{n}

with a variable u_{s}. We call u_{s} the head variable of s as usual.

Let us then consider the set Θ of pairs (p, q) of closed terms

\{ \begin{matrix}p : (τ_{1} → τ_{2} → ⋯ → τ_{n} → 0) → (τ′_{π(1)} → τ′_{π(2)} → ⋯ → τ′_{π(n)} → 0) \\ q : (τ′_{π(1)} → τ′_{π(2)} → ⋯ → τ′_{π(n)} → 0) → (τ_{1} → τ_{2} → ⋯ → τ_{n} → 0) \end{matrix}

defined inductively on the construction of types τ_{1} → ⋯ → τ_{n} → 0 so that

• (λx. x, λx. x) ∈ Θ for variables x of the base type,

• if (p_{i}, q_{i}) ∈ Θ with p_{i} : τ_{i} → τ′_{i}, q_{i} : τ′_{i} → τ_{i} for 1 ≤ i ≤ n and π is a permutation on {1, 2, …, n} then (p, q) ∈ Θ for

\{ \begin{matrix}p ≡ λux_{π(1)}x_{π(2)} … x_{π(n)}. u(q_{1}x_{1})(q_{2}x_{2}) … (q_{n}x_{n}) \\ q ≡ λux_{1}x_{2} … x_{n}. u(p_{π(1)}x_{π(1)})(p_{π(2)}x_{π(2)}) … (p_{π(n)}x_{π(n)}). \end{matrix}

The intended interpretation of p in a Cartesian closed category ℂ is an isomorphism

(A_{1} → A_{2} → ⋯ → A_{n} → D) → (A′_{π(1)} → A′_{π(2)} → ⋯ → A′_{π(n)} → D)

generated from the family of canonical isomorphisms

A × B → B × A, (A × B) × C → A × (B × C)

by composition, the adjunction ℂ(A × B, C) ≅ ℂ(B, A → C), the functor ( ) × ( ) and the functor ( ) → D for a fixed object D. The interpretation of q is its inverse.

4.6. Lemma. Let (p, q) ∈ Θ. Then q(pu) = u and p(qu) = u.

Proof. The proof is by induction on types. One of the inductive case is shown as follows.

q(pu) = λx_{1}x_{2} … x_{n}. u(q_{1}(p_{1}x_{1}))(q_{2}(p_{2}x_{2})) … (q_{n}(p_{n}x_{n}))
= λx_{1}x_{2} … x_{n}. ux_{1}x_{2} … x_{n} = u.

Let θ be a function from the pairs u^{σ} = (u, σ) of a variable x and a type σ to Θ such that p_{(u,σ)} : σ → τ and p_{(u,τ)} = q_{(u,σ)} where we write (p_{(u,σ)}, q_{(u,σ)}) for θ(u, σ). We suppress the reference to types as much as possible and often simply write θ(u) and so on. We also write π_{u} for the permutation π such that

p_{u} : (τ_{1} → τ_{2} → ⋯ → τ_{n} → 0) → (τ′_{π_{u}(1)} → τ′_{π_{u}(2)} → ⋯ → τ′_{π_{u}(n)} → 0)

while π_{u} is the empty function if u has the base type. Furthermore we write p_{i}^{u} and q_{i}^{u} for p_{i} and q_{i} used in the inductive definitions of p_{u} and q_{u}, and define

\{ \begin{matrix}p_{s} ≡ λvx_{π_{u}(k+1)}x_{π_{u}(k+2)} … x_{π_{u}(n)}. v(q_{k+1}^{u}x_{k+1})(q_{k+2}^{u}x_{k+2}) … (q_{n}^{u}x_{n}) \\ q_{s} ≡ λvx_{k+1}x_{k+2} … x_{n}. v(p_{π_{u}(k+1)}^{u}x_{π_{u}(k+1)})(p_{π_{u}(k+2)}^{u}x_{π_{u}(k+2)}) … (p_{π_{u}(n)}^{u}x_{π_{u}(n)}) \end{matrix}

for s ≡ us_{1}s_{2} … s_{k} when the restriction of π_{u} to {k + 1, k + 2, …, n} is a permutation. They are intended as isomorphisms for the type of s.

4.7. Lemma. π_{(u,σ)} = π_{(u,τ)}^{−1} when p_{(u,σ)} : σ → τ.

Proof. Suppose otherwise. We then have p_{i}^{(u,σ)}y_{i} = q_{j}^{(u,τ)}y_{j} for i ≠ j. Substitute λw.0 and λw.1 for y_{i} and y_{j}, respectively, and derive the contradiction.

4.8. Lemma. q_{(u,τ)} = p_{(u,σ)} and p_{i}^{(u,σ)} = q_{i}^{(u,τ)} when p_{(u,σ)} : σ → τ.

Proof. For the first equation we have

q_{(u,τ)}x = p_{(u,σ)}(q_{(u,σ)}(q_{(u,τ)}x)) = p_{(u,σ)}(p_{(u,τ)}(q_{(u,τ)}x)) = p_{(u,σ)}x.

For the second equation let s = λy_{1} … y_{n}. y_{i}z_{1} … z_{k}. Then

p_{(u,τ)}(q_{(u,τ)}s) = p_{(u,τ)}(p_{(u,σ)}s) = λy_{1}y_{2} … y_{n}. q_{i}^{(u,σ)}(q_{i}^{(u,τ)}y_{i})z_{1} … z_{k} = s.

We hence have q_{i}^{(u,σ)}(q_{i}^{(u,τ)}y_{i})z_{1} … z_{k} = y_{i}z_{1} … z_{k} and

p_{i}^{(u,σ)}y_{i} = p_{i}^{(u,σ)}(q_{i}^{(u,σ)}(q_{i}^{(u,τ)}y_{i})) = q_{i}^{(u,τ)}y_{i}.

4.9. Definition. For a given θ we define the relation s ∼_{θ} s′ on V T as the smallest relation satisfying

• u^{σ} ∼_{θ} u^{τ} for any variable u if p_{(u,σ)} : σ → τ,

• if u^{σ} ∼_{θ} u^{τ} and s_{i} ∼_{θ} t_{i} for 1 ≤ i ≤ k ≤ n so that

– the restriction of π_{u} on {1, 2, …, n} to {1, 2, …, k} is a permutation,

– p_{i}^{u} = p_{s_{i}} and q_{i}^{u} = q_{s_{i}} for 1 ≤ i ≤ k

then u^{σ}s_{1}s_{2} … s_{n} ∼_{θ} u^{τ}t_{π_{u}(1)}t_{π_{u}(2)} … t_{π_{u}(n)}. If there is θ such that s ∼_{θ} t we simply say s is essentially equivalent to t.

4.10. Lemma. The relation s ∼_{θ} s′ is symmetric.

Proof. By induction on s using Lemma 4.8 4.11. Lemma. Suppose the list x of variables in s is a permutation of y in t and x does not include the variable u. If s is essentially equivalent to t then s[ux/u] is essentially equivalent to t[uy/u].

Proof. Suppose s ∼_{θ′} t and y_{1}, y_{2}, …, y_{k} is x_{π(1)}, x_{π(2)}, …, x_{π(k)}. We write (p′_{u}, q′_{u}) for θ′(u) and so on. Let θ(u) be such that

π_{u}(i) = \{ \begin{matrix}π(i) & for 1 ≤ i ≤ k \\ π′_{u}(i − k) + k & for k < i ≤ n, \end{matrix} p_{i}^{u} = \{ \begin{matrix}p′_{x_{i}} & for 1 ≤ i ≤ k \\ p′_{i−k}^{u} & for k < i ≤ n \end{matrix}

and similarly for q_{i}^{u}. Let θ(v) = θ′(v) for v ≢ u.

4.12. Theorem. Suppose s ∼_{θ} t and the head variable of s is u. Suppose further x_{k+1}, x_{k+2}, …, x_{n} is the list of fresh variables so that sx_{k+1}x_{k+2} … x_{n} is a term of 0. Then

sx_{k+1}x_{k+2} … x_{n} = t[pv/v]r_{π_{u}(k+1)}r_{π_{u}(k+2)} … r_{π_{u}(n)}

where r_{i} ≡ p_{i}^{u}x_{i} for k + 1 ≤ i ≤ n and pv is the list p_{v_{1}}v_{1}, …, p_{v_{j}}v_{j} with v including all the variables of s.

Proof. The proof is by induction on the construction of s. If s is a variable u then

pur_{π_{u}(1)}r_{π_{u}(2)} … r_{π_{u}(n)} = u(q_{1}(p_{1}x_{1})) … (q_{n}(p_{n}x_{n})) = ux_{1} … x_{n}.

Suppose s ≡ us_{1} … s_{k} and t ≡ ut_{π_{u}(1)} … t_{π_{u}(k)}. Suppose further the head variable of s_{i} is w. By the inductive hypothesis we have

s_{i}y_{l+1}y_{l+2} … y_{m} = t_{i}[pv/v]r_{π_{w}(l+1)}r_{π_{w}(l+2)} … r_{π_{w}(m)}

where r_{j} ≡ p_{j}^{w}y_{j} for l + 1 ≤ j ≤ m. We then have

q_{i}^{u}(t_{i}[pv/v])y_{l+1} … y_{m} = q_{s_{i}}(t_{i}[pv/v])y_{l+1} … y_{m}
= t_{i}[pv/v](p_{π_{w}(l+1)}^{w}y_{π_{w}(l+1)}) … (p_{π_{w}(m)}^{w}y_{π_{w}(m)})
= s_{i}y_{l+1} … y_{m}

so that q_{i}^{u}(t_{i}[pv/v]) = s_{i}. Hence

t[pv/v]r_{π_{u}(k+1)} … r_{π_{u}(n)}
= pu(t_{π_{u}(1)}[pv/v]) … (t_{π_{u}(k)}[pv/v])r_{π_{u}(k+1)} … r_{π_{u}(n)}
= u(q_{1}^{u}(t_{1}[pv/v])) … (q_{k}^{u}(t_{k}[pv/v]))(q_{k+1}^{u}(p_{k+1}^{u}x_{k+1})) … (q_{n}^{u}(p_{n}^{u}x_{n}))
= us_{1} … s_{k}x_{k+1} … x_{n}.

4.13. Corollary. Use the same assumptions as Theorem 4.12. Suppose further that y and w are disjoint lists of variables such that every variable in v is either in y or w. Then

s[qy/y]x_{k+1}x_{k+2} … x_{n} = t[pw/w]r_{π_{u}(k+1)}r_{π_{u}(k+2)} … r_{π_{u}(n)}.

Proof.

s[qy/y]x_{k+1} … x_{n} = (t[pv/v]) [qy/y]r_{π_{u}(k+1)} … r_{π_{u}(n)}
= t[pw/w, p_{y_{1}}(q_{y_{1}}y_{1})/y_{1}, …, p_{y_{m}}(q_{y_{m}}y_{m})/y_{m}]r_{π_{u}(k+1)} … r_{π_{u}(n)}
= t[pv/v]r_{π_{u}(k+1)} … r_{π_{u}(n)}

Let u and x be the lists of variables of type 0 with the length m and n, respectively. Furthermore let U, U′ be the lists of terms of 0 in V T with the length m and X, X′ be the lists of terms of 0 in V T with the length n.

4.14. Definition. α and α′ are essentially equivalent under θ, denoted α ∼_{θ} α′, if

• there are quantifier-free formulas β(u, x, z) and β′(u, x, z) such that β ↔ β′ holds, which contain exactly the same free variables of type 0 and no others,

• U_{i} ∼_{θ} U′_{i} and X_{j} ∼_{θ} X′_{j} for each 1 ≤ i ≤ m and 1 ≤ j ≤ n,

• α ≡ β(U, X, z) and α′ ≡ β′(U′, X′, z).

If α ∼_{θ} α′ for some θ we simply say α is essentially equivalent to α′, denoted α ∼ α′. The terms U, U′, X and X′ are called primary terms.

4.15. Theorem. For any formula ϕ of first-order classical logic (ϕ^{N} )_{D} and (ϕ^{+})_{L} are essentially equivalent.

The proof is by induction on the construction of formulas and we use Lemma 4.11 to conclude α[ux/u] ∼ β[uy/u] from α ∼ β when y is a permutation of x.

Nothing is to be proved for the atomic case. Assuming ϕ_{D}(u, x) ∼ ψ_{L}(u, x) we have

(¬ϕ)_{D} ≡ ¬ϕ_{D}(u, xu) ∼ ¬ψ_{L}(u, xu) ≡ (? ϕ^{⊥})_{L},
(¬¬ϕ)_{D} ≡ ¬¬ϕ_{D}(ux, x(ux)) ∼ ψ_{L}(ux, x(ux)) ≡ ( ? ! ψ)_{L} ≡ (? ( ? ψ^{⊥})^{⊥})_{L}.

The cases of ¬ϕ and ∀xϕ follow from them. The rest of the cases are treated by the following step-by-step calculations.

(ϕ ∧ ψ)^{N} and (ϕ ∧ ψ)^{+}. ((ϕ ∧ ψ)^{N} )_{D} is computed as follows.

[figure: ϕ^{N}; ϕ^{N} ∧ ψ^{N}; ϕ^{N}; ψ^{N}; ψ^{N}; ϕ^{N} ∧ ψ^{N}; ‘; ϕ^{N} ∧ ψ^{N}; ¬(ϕ^{N} ∧ ψ^{N}); ¬(ϕ^{N} ∧ ψ^{N}); ¬¬(ϕ^{N} ∧ ψ^{N}); (ϕ^{N} )_{D}(u, x); (ϕ^{N} )_{D}(u, x) ∧ (ψ^{N} )_{D}(v, y); (ϕ^{N} )_{D}(u, x); (ψ^{N} )_{D}(v, y); (ψ^{N} )_{D}(v, y); (ϕ^{N} )_{D}(u, x) ∧ (ψ^{N} )_{D}(v, y); ‘; (ϕ^{N} )_{D}(u, x) ∧ (ψ^{N} )_{D}(v, y); ¬((ϕ^{N} )_{D}(u, xuv) ∧ (ψ^{N} )_{D}(v, yuv)); ¬((ϕ^{N} )_{D}(u, xuv) ∧ (ψ^{N} )_{D}(v, yuv)); ¬¬((ϕ^{N} )_{D}(uxy, x(uxy)(vxy)) ∧ (ψ^{N} )_{D}(vxy, y(uxy)(vxy)))]

((ϕ ∧ ψ)^{+})_{L} is as follows. We only need to permute u and v in xuv in the third step.

[figure: ϕ^{+}; _{! ϕ^{+}}; ψ^{+}; _{! ψ^{+}}; _{! ϕ^{+}}; ! ϕ^{+} ⊗ ! ψ^{+}; _{! ϕ^{+}}; _{! ψ^{+}}; _{! ψ^{+}}; ! ϕ^{+} ⊗ ! ψ^{+}; ‘; ! ϕ^{+} ⊗ ! ψ^{+}; _{? ( ! ϕ^{+} ⊗ ! ψ^{+})}; (ϕ^{+})_{L}(u, x); (ϕ^{+})_{L}(u, xu); (ψ^{+})_{L}(v, y); (ψ^{+})_{L}(v, yv); (ϕ^{+})_{L}(u, xu); (ϕ^{+})_{L}(u, xvu) ∧ (ψ^{+})_{L}(v, yuv); (ϕ^{+})_{L}(u, xu); (ψ^{+})_{L}(v, yv); (ψ^{+})_{L}(v, yv); (ϕ^{+})_{L}(u, xvu) ∧ (ψ^{+})_{L}(v, yuv); ‘; (ϕ^{+})_{L}(u, xvu) ∧ (ψ^{+})_{L}(v, yuv); (ϕ^{+})_{L}(uxy, x(vxy)(uxy)) ∧ (ψ^{+})_{L}(vxy, y(uxy)(vxy))]

(ϕ ∨ ψ)^{N} and (ϕ ∨ ψ)^{+}. ((ϕ ∨ ψ)^{N} )_{D} is as follows.

[figure: ϕ^{N}; ¬ϕ^{N}; ψ^{N}; ¬ψ^{N}; ¬ϕ^{N}; ¬ϕ^{N} ∧ ¬ψ^{N}; ¬ϕ^{N}; ¬ψ^{N}; ¬ψ^{N}; ¬ϕ^{N} ∧ ¬ψ^{N}; ‘; ¬ϕ^{N} ∧ ¬ψ^{N}; ¬ (¬ϕ^{N} ∧ ¬ψ^{N} ); (ϕ^{N} )_{D}(u, x); ¬(ϕ^{N} )_{D}(u, xu); (ψ^{N} )_{D}(v, y); ¬(ψ^{N} )_{D}(v, yv); ¬(ϕ^{N} )_{D}(u, xu); ¬(ϕ^{N} )_{D}(u, xu) ∧ ¬(ψ^{N} )_{D}(v, yv); ¬(ϕ^{N} )_{D}(u, xu); ¬(ψ^{N} )_{D}(v, yv); ¬(ψ^{N} )_{D}(v, yv); ¬(ϕ^{N} )_{D}(u, xu) ∧ ¬(ψ^{N} )_{D}(v, yv); ‘; ¬(ϕ^{N} )_{D}(u, xu) ∧ ¬(ψ^{N} )_{D}(v, yv); ¬(¬(ϕ^{N} )_{D}(uxy, x(uxy)) ∧ ¬(ψ^{N} )_{D}(vxy, y(vxy)))]

((ϕ ∨ ψ)^{+})_{L} is as follows. We only need to permute x and y in uxy in the last step.

[figure: ϕ^{+}; _{! ϕ^{+}}; ψ^{+}; _{! ψ^{+}}; _{! ϕ^{+}}; ? _{! ϕ^{+}}; _{! ψ^{+}}; ? _{! ψ^{+}}; ? _{! ϕ^{+}}; ? ! ϕ^{+}⅋ ? ! ψ^{+}; ? _{! ϕ^{+}}; ? _{! ψ^{+}}; ? _{! ψ^{+}}; ? ! ϕ^{+}⅋ ? ! ψ^{+}; ‘; (ϕ^{+})_{L}(u, x); (ϕ^{+})_{L}(u, xu); (ψ^{+})_{L}(v, y); (ψ^{+})_{L}(v, yv); (ϕ^{+})_{L}(u, xu); (ϕ^{+})_{L}(ux, x(ux)); (ψ^{+})_{L}(v, yv); (ψ^{+})_{L}(vy, y(vy)); (ϕ^{+})_{L}(ux, x(ux)); (ϕ^{+})_{L}(uyx, x(uyx)) ∨ (ψ^{+})_{L}(vxy, y(vxy)); (ϕ^{+})_{L}(ux, x(ux)); (ψ^{+})_{L}(vy, y(vy)); (ψ^{+})_{L}(vy, y(vy)); (ϕ^{+})_{L}(uyx, x(uyx)) ∨ (ψ^{+})_{L}(vxy, y(vxy)); ‘]

(∃y ϕ)^{N} and (∃y ϕ)^{+}. ((∃y ϕ)^{N} )_{D} is as follows.

ϕ^{N} ¬ϕ^{N} ¬ϕ^{N} ∀y ¬ϕ^{N} ∀y ¬ϕ^{N} ¬∀y ¬ϕ^{N}  (ϕ^{N} )_{D}(u, x, y) ¬(ϕ^{N} )_{D}(u, xu, y) ¬(ϕ^{N} )_{D}(u, xu, y) ¬(ϕ^{N} )_{D}(u, xyu, y) ¬(ϕ^{N} )_{D}(u, xyu, y) ¬¬(ϕ^{N} )_{D}(ux, x(yx)(ux), yx)

((∃y ϕ)^{+})_{L} is as follows. There is no need for permutation.

ϕ^{+}_{! ϕ^{+}}_{! ϕ^{+}} ∃y ! ϕ^{+} ∃y ! ϕ^{+}_{? ∃y ! ϕ^{+}}  (ϕ^{+})_{L}(u, x, y) (ϕ^{+})_{L}(u, xu, y) (ϕ^{+})_{L}(u, xu, y) (ϕ^{+})_{L}(u, xyu, y) (ϕ^{+})_{L}(u, xyu, y) (ϕ^{+})_{L}(ux, x(yx)(ux), yx)

4.16. Corollary. (ϕ^{N} )_{D}(u, x) has witnesses if and only if (ϕ^{+})_{L}(u, x) has witnesses. Proof. Let (ϕ^{N} )_{D}(u, x) ≡ α(U, X) and (ϕ^{+})_{L}(u, x) ≡ β(U′, X′). Assuming that (ϕ^{N} )_{D}(u, x) ≡ α(U[u/u], X[u/u]) holds we have

α(U[u/u, qx/x], X[u/u, qx/x])

by substitution for negative variables. Since primary terms are of type 0 we have

α(U[qx/x], X[qx/x]) ↔ β(U′[pu/u], X′[pu/u])

by Corollary 4.13 and Theorem 4.15. We then have

α(U[u/u, qx/x], X[u/u, qx/x]) ↔ β(U′[pu/u], X′[pu/u])

by substitution for positive variables. It follows from them that

(ϕ^{+})_{L}(pu, x) ≡ β(U′[pu/u], X′[pu/u])

holds. The other direction is entirely similar.

THE DIALECTICA INTERPRETATION OF FIRST-ORDER CLASSICAL AFFINE LOGIC 75

4.17. Shoenfield’s version of Dialectica translation. In his textbook Mathematical Logic, Shoenfield gave a consistency proof of PA, using a version of Dialectica interpretation which interprets classical formulas directly [Shoenfield 1967]. His version of D-translation is the translation of a classical formula ϕ into a classical higher-type formula ϕ^{S} of the form

∀x∃u ϕ_{S}(u, x).

which is defined inductively by • ϕ^{S} ≡ ϕ_{S} ≡ ϕ for atomic ϕ,

• (¬ϕ)^{S} ≡ ∀u∃x ¬ϕ_{S}(ux, x),

• (ϕ ∨ ψ)^{S} ≡ ∀xy∃uv (ϕ_{S}(u, x) ∨ ψ_{S}(v, y)),

• (∀z ϕ)^{S} ≡ ∀zx∃u ϕ_{S}(u, x, z). ϕ ∧ ψ and ∃z ϕ are defined as ¬ (¬ϕ ∨ ¬ψ) and ¬∀z ¬ϕ, respectively. They do not appear in Shoenfield’s consistency proof at all. If we compute their D-translations according to the definitions, however, they become the following.

• (ϕ ∧ ψ)^{S} ≡ ∀xy∃uv ¬ (¬ϕ_{S}(u(xuv), xuv) ∨ ¬ψ_{S}(v(yuv), yuv)).

• (∃z ϕ)^{S} ≡ ∀x∃zu ϕ_{S}(u(xuz), xuz, z, z′). Shoenfield then showed that if ϕ is provable in PA then there exists the list u of witness terms such that ϕ_{S}(u, x) holds. The witnesses are, however, allowed to contain free variables from x. Hence we can instead consider the Skolemization

ϕ^{SS} ≡ ∃u∀x ϕ_{SS}(u, x) ≡ ∃u∀x ϕ_{S}(ux, x)

of ϕ^{S} and obtain witnesses with no free variables from x.

Let us regard our D-interpretations of linear logic operators as the operations on quantifier-free formulas with designated positive and negative variables. We then have the following observation.

• ϕ_{SS} ≡ ϕ_{S}(ux, x) ≡ ? ϕ_{S}(u, x).

• If ϕ is atomic, then ϕ_{SS} ≡ ϕ ≡ ? ! ϕ since ϕ has no bound variables.

• (¬ϕ)_{SS} ≡ ¬ϕ_{S}(u(xu), xu) ≡ ? ( ? ϕ_{S}(u, x))^{⊥} ≡ ? (ϕ_{SS})^{⊥}.

• (ϕ ∨ ψ)_{SS} ≡ ϕ_{S}(uxy, x) ∨ ψ_{S}(vxy, y) ∼ ? ϕ_{S}(u, x)⅋ ? ψ_{S}(v, y) ∼ ϕ_{SS}⅋ψ_{SS}.

• (ϕ ∧ ψ)_{SS} ≡ ¬ (¬ϕ_{S}(uxy(x(uxy)(vxy)), x(uxy)(vxy)) ∨ ¬ψ_{S}(vxy(y(uxy)(vxy)), y(uxy)(vxy))) ∼ ? ( ! ? ϕ_{S}(u, x) ⊗ ! ? ψ_{S}(v, y)) ≡ ? ( ! ϕ_{SS} ⊗ ! ψ_{SS}).

• (∀z ϕ)_{SS} ≡ ϕ_{S}(uxz, x, z) ≡ ∀z ? ϕ_{S}(u, x, z) ≡ ∀zϕ_{SS}.

• (∃z ϕ)_{SS} ≡ ϕ_{S}(ux(x(ux)(zx)), x(ux)(zx), zx) ∼ ? ∃z ! ? ϕ_{S}(u, x, z) ≡ ? ∃z ! ϕ_{SS}.

ϕ^{SS} thus corresponds almost exactly to the composition of ?!-translation and our Dtranslation, where we use ϕ^{†} for the disjunction and ϕ^{+} for the existential quantifier. The only exception is the universal quantification. ((∀zϕ)^{+})^{L} corresponds to (¬¬∀zϕ)^{SS} rather than (∀zϕ)^{SS}.

Hyland analyzed ϕ^{S} ≡ ∀x∃u ϕ_{S}(u, x) by converting it into ϕ_{S}(ux, x) ⊃ ⊥, which can be regarded as the object Rϕ̄ in the categorical setting, where ϕ̄ and R are objects ϕ_{S}(u, x) and ⊥, respectively [Hyland 2002]. We can write ϕ_{S}(ux, x) ⊃ ⊥ as

? ¬ϕ_{S}(ux, x) ≡ ? (ϕ_{S}(u, x))^{⊥}

and our description of ϕ^{SS} fits with Hyland’s analysis. We note however that we are able to give a more direct description due to the presence of ? .

4.18. The translation ϕ^{♭}. It is interesting to think about why ¬¬ is not necessary in (∀xϕ)^{SS}. This is also the case in the combination of the original ¬¬-translation ϕ^{N} and ϕ^{D}. Shoenfield’s D-translation suggests the following translation ϕ^{♭} of classical logic into classical linear logic.

1. ϕ^{♭} ≡ ? ϕ for ϕ atomic.

2. (ϕ ∨ ψ)^{♭} ≡ ϕ^{♭}⅋ψ^{♭}.

3. (¬ϕ)^{♭} ≡ ? (ϕ^{♭})^{⊥}.

4. (ϕ ∧ ψ)^{♭} ≡ ? (! ϕ^{♭} ⊗ ! ψ^{♭}).

5. (∀xϕ)^{♭} ≡ ∀xϕ^{♭}.

6. (∃xϕ)^{♭} ≡ ? ∃x ! ϕ^{♭}.

ϕ^{♭} is logically equivalent to ? ϕ^{♭}. Furthermore ϕ^{♭} is sufficient to capture the provability of classical logic in the following sense.

4.19. Theorem. If a sequent ϕ_{1}, …, ϕ_{n} ⊢ ψ_{1}, …, ψ_{m} is provable in classical logic, then the sequent

! ϕ_{1}^{♭}, …, ! ϕ_{n}^{♭} ⊢ ψ_{1}^{♭}, …, ψ_{n}^{♭}

is provable in classical linear logic.

Proof. The proof is by induction on the construction of classical proof. Interesting cases are the left ∨ rule and the left ∀ rule, where we use the fact that

! (ϕ^{♭}⅋ψ^{♭}) ⊢ ? ! ϕ^{♭}⅋ ? ! ψ^{♭} and ! ∀xϕ^{♭} ⊢ ∀x ! ϕ^{♭}

are provable in classical linear logic.

In classical affine logic (ϕ ∧ ψ)^{♭} can be simplified to ? (ϕ^{♭} ⊗ ψ^{♭}) for the similar result, since ! ? (ϕ^{♭} ⊗ ψ^{♭}) ⊢ ! ϕ^{♭} ⊗ ! ψ^{♭} is then provable, using the left weakening on ϕ^{♭} and ψ^{♭}.

5. Conclusion

We have obtained a structurally symmetric reformulation of Gödel’s Dialectica interpretation by way of a contraction-free logic. We would like to finish our work by making three additional comments.

First of all although our work is motivated mostly by a theoretical concern our interpretation may be useful for practical purposes such as program extraction. There have been attempts to refine a logical system so that one can extract optimized programs from proofs, for example Berger’s uniform Heyting arithmetic [Berger 2005]. By keeping track of the use of contraction we can certainly curtail unnecessary dependencies and obtain a smaller witness term.

Secondly when we extend our interpretation to arithmetic we need to add to our logical system the axioms for equality and primitive recursive functions, and the rule of inference for induction. Every atomic formula s = t is then contractible since we can derive

s = t ⊢ s = t ⊗ s = t

from the axioms

⊢ s = s, s = t, s = s ⊗ s = s ⊢ s = t ⊗ s = t

where we use the two-sided sequent calculus for readability. Things are otherwise straightforward up to the induction rule, of which we can consider the four versions

\frac{⊢ ϕ(0) ϕ(x) ⊢ ϕ(sx)}{⊢ ϕ(t)}  \frac{⊢ ϕ(0) ! ϕ(x) ⊢ ϕ(sx)}{⊢ ϕ(t)}

\frac{Γ, ! Δ ⊢ ϕ(0) ! Δ, ϕ(x) ⊢ ϕ(sx)}{Γ, ! Δ ⊢ ϕ(t)}  \frac{! Γ, ! Δ ⊢ ϕ(0) ! Δ, ! ϕ(x) ⊢ ϕ(sx)}{! Γ, ! Δ ⊢ ϕ(t)}

where s is the successor and t is an arbitrary term. If we allow ϕ to be an arbitrary formula they are admissible from one another. The interesting thing would be, however, to investigate the Dialectica interpretations of weaker forms of induction, obtained by restricting ϕ to a certain class of formulas or restricting the exponentials as Girard’s light linear logic [Girard 1998]. This would be analogous to the work of Cook and Urquhart on bounded arithmetic [Cook and Urquhart 1993].

Finally our Dialectica interpretation seems to be related to two types of games. One is the game semantics of propositional linear logic and PCF [Abramsky and Jagadeesan 1994, Abramsky et al. 2000]. The other is the Henkin-Hintikka game for first-order classical logic [Hintikka 1996]. Our study has been guided by the observation that the game semantics of PCF is immediately applicable to its subsystem T, and by the intuition that the Dialectica interpretation is a constructive version of the Henkin-Hintikka game.

References

[Abramsky and Jagadeesan 1994] Abramsky, S. and Jagadeesan, R. (1994). Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 59(2):543 – 574.

[Abramsky et al. 2000] Abramsky, S., Malacaria, P., and Jagadeesan, R. (2000). Full abstraction for PCF. Information and Computation, 163:409–470.

[Avigad and Feferman 1998] Avigad, J. and Feferman, S. (1998). Gödel’s functional (“dialectica”) interpretation. In Buss, S., editor, Handbook of Proof Theory, chapter V. Elsevier.

[Berger 2005] Berger, U. (2005). Uniform Heyting arithmetic. Annals of Pure and Applied Logic, 133(1-3):125-148.

[Cook and Urquhart 1993] Cook, S. A. and Urquhart, A. (1993). Functional interpretations of feasibly constructive arithmetic. Annals of Pure and Applied Logic, 63:103-200.

[de Paiva 1991] de Paiva, V. (1991). The dialectica categories. Technical Report 213, University of Cambridge, Computer Laboratory.

[de Paiva 2006] de Paiva, V. (2006). Dialectica and chu constructions: Cousins ? In this Volume.

[Devarajan et al. 1999] Devarajan, H., Hughes, D. J. D., Plotkin, G. D., and Pratt, V. R. (1999). Full completeness of the multiplicative linear logic of chu spaces. In Logic in Computer Science, pages 234–242.

[Diller and Nahm 1974] Diller, V. J. and Nahm, W. (1974). Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen. Archiv für Mathematische Logik und Grundlagenforschüng, 16:49–66.

[Girard 1987] Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science, 50:2–102.

[Girard 1998] Girard, J.-Y. (1998). Light linear logic. Information and Computation, 143:175–204.

[Gödel 1990] Gödel, K. (1990). Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. In Feferman, S., Dawson, Jr., J. W., Kleene, S. C., Moore, G. H., Solovay, R. M., and van Haijenoort, J., editors, Collected Works, volume II, pages 240–251. Oxford University Press.

[Hindley and Seldin 1986] Hindley, J. R. and Seldin, J. P. (1986). Introduction to the Combinators and λ-Calculus. Cambridge University Press.

[Hintikka 1996] Hintikka, J. (1996). The Principles of Mathematics Revisited. Cambridge University Press.

[Hyland 2002] Hyland, J. M. E. (2002). Proof theory in the abstract. Annals of Pure and Applied Logic, 114:43–78.

[Shoenfield 1967] Shoenfield, J. R. (1967). Mathematical Logic. Addison-Wesley.

[Streicher 2000] Streicher, T. (2000). A semantic version of the diller-nahm variant of gödel’s dialectica interpretation. Available at his web site.

[Troelstra 1973] Troelstra, A. E., editor, (2000). Metamathematical Investigation of Intuitionistic Arithmetic and Analysis Lecture Notes in Mathematics 344. Springer.

Mathematics Laboratory Keio University, Hiyoshi Campus Hiyoshi 4-1-1, Kohoku-ku, Yokohama Kanagawa, 223-8521 Japan

Email: sirahata@math.hc.keio.ac.jp

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/17/4/17-04.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh,

rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: mbarr@barrs.org

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com

Ezra Getzler, Northwestern University: getzler(at)math(dot)northwestern(dot)edu

Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca