Proof-functional connectives and realizability

Franco Barbanera^{∗} Simone Martini^{†}

January 1993

Abstract

The meaning of a formula built out of proof-functional connectives depends in an essential way upon the intensional aspect of the proofs of the component subformulas. We study three such connectives, strong equivalence (where the two directions of the equivalence are established by mutually inverse maps), strong conjunction (where the two components of the conjunction are established by the same proof) and relevant implication (where the implication is established by an identity map). For each of these connectives we give a type-assignment system, a realizability semantics, and a completeness theorem. This form of completeness has a corollary the semantic completeness of the type-assignment system.

1 Introduction

Usual connectives of classical propositional logic are truth-functional, the meaning of a compound formula being dependent only on the truth value of its subformulas. In the constructive analysis of logical constants, on the other hand, it is the concept of proof (or justification, or reason, or realizer) for a formula to become of paramount importance. In the Brouwer-Heyting-Kreisel interpretation, for instance, a realizer for A & B is given once a realizer for A and a realizer for B are given, while a realizer for A → B is given once we have an (effective) way of transforming any realizer for A into a realizer for B. Several variations on this paradigm have been studied, trying to better specify what has to be counted as a valid “realizer” (for instance, which operations are available on them), or, once fixed a formal notion of realizer, trying to identify the relations between constructive proofs and properties of their (formal) realizers. The intensional character of realizers, however, has no part in these analysis. Beside the fact that it has to be assumed that we are able to recognize that a realizer realizes something, no other requirement is usually issued. In particular no commitment is made on the ability to recognize whether two realizers are equal.

Provability for proof-functional connectives [Lopez-Escobar 85], on the other hand, depends on the actual shape of the proofs (realizers) for the components of a complex formula. This connectives arise as an attempt to clarify the logical status of constructions introduced, with different aims, in λ-calculus and theoretical computer science. It is well known that, by the Curry-Howard isomorphism, any type of (first or second order) λ-calculus corresponds to a formula of (first or second order) intuitionistic logic, whose proofs correspond to the terms of that type. In [Coppo & Dezani 80] a new type system for λ-calculus was introduced, whose notable characteristic was the presence of an intersection (∧) type constructor. It is a very important system for the study of typed and untyped λ-calculus (some of its features will be listed in Section 4), but it does not fit into the Curry-Howard paradigm. While the elimination rule for intersection types exactly matches the elimination rule for conjunction, the introduction rule

\begin{matrix}M : α M : β \\ M : α ∧ β \end{matrix}  (1)

∗Università di Torino, Dipartimento di Informatica, Corso Svizzera 185, 10149 Torino, Italy. E-mail: barba@di.unito.it

†Università di Pisa, Dipartimento di Informatica, Corso Italia 40, 56125 Pisa, Italy. E-mail: martini@di.unipi.it

prevents the interpretation of α ∧ β as “α and β”, since its realizer M has to be the same realizer of both α and β. It is for giving a logical account of this type constructor that [Pottinger 80] introduces the proof-functional connective of strong conjunction, with the informal realizability analysis “to assert A & B is to assert that one has a reason for asserting A which is also a reason for asserting B.”

Proof-functional connectives can be used to study several other constructions. In this paper, in addition to strong conjunction (Section 4), we will study strong equivalence (Section 3), a connective arising from the study of provable isomorphisms in λ-theories, and relevant implication (Section 5), a well-known connective with also some computer science motivations in the background.

Main focus of the paper will be the realizability analysis of such connectives, outlined in the following section. Indipendently of one’s opinion about their relevance per se, however, proof-functional connectives bears an interest also from a foundational point of view, especially for the relation between mathematical concepts and their formalization, a subject we will briefly touch in the rest of this section.

As soon as the (informal) definition of a proof-functional connective comes into one’s mind, indeed, it is clear that even the problem of its “soundness” — that is, of spelling it out in a mathematically acceptable way — reduces to the possibility of considering decidable relations, like (extensional or intensional) equality, between constructions (representatives of constructive proofs). If one agrees with Brouwer’s viewpoint on the non formalizability of mathematical thought, one could simply get rid of the problems by simply stating that one cannot go beyond recognizing that a construction (realizer) justifies a formula. If, however, we divert from Brouwer’s extremist point of view, and build formal systems — which we believe embodying our logical reasoning — relational aspects between proofs have to be given full citizenship into our logical investigations. Accepting this last fact leads immediately to Lopez-Escobar’s consideration [Lopez-Escobar 85] that

accepting proof-functional connectives, such as strong conjunction, requires rejecting the assumption that a construction proves a unique sentence and thus forces us to distinguish between a construction as an object and a construction as a method.

To see constructions as methods means to consider them separately from the sentences they prove;hence they are formalized separately and separately they are included in rules for proof-functional connectives. In this way, such formal systems come to be more strongly dependent than other sorts of logical systems on how one decides to formalize constructions and the intended relations between them. This is well exemplified by the rule rule (1), which will be shown to be a sound introduction rule for strong conjunction. In formalizing with this rule the notion of a construction proving two different sentences, one makes the choice of formalizing equality between constructions as syntactical equality between λ-terms. Moreover, one makes the further choice, among the many possible and different ones, of considering the logical steps regarding strong conjunction as being, in a sense, non-existent from the point of view of constructions, since in the term corresponding to the construction for α ∧ β no information is contained about the fact that to get to this point we passed through one and the same construction for α and β. This makes us recall that formalization, in general, necessarily brings with it elements external to what we are trying to formalize and consequently enforces, somewhat paradoxically, Brouwer’s viewpoint on unformalizability of mathematical reasoning seen as pure mental process in its widest sense. Hoping things to be otherwise would lead to the well known paradox of the dove dreaming of freely flying into a sky where the air which obstacles its flight is absent, so forgetting that it is the air which enables its flight.

Thus, even if not supporting the formalistic viewpoint, one could hardly disregard the fact that the interest of logic, in particular if one deals with proof-functional notions, is somewhat interleaved between the mathematical concept and its formalization. About the latter, in a proof-functional context, the notion of “formal” rule is relevant and surely cannot be an absolute one, being tightly tied at least to the rest of the formalization choices such as, in the previously considered case, how to formalize constructions and equality between them. It is then misleading to follow the (frequent) judgment of people who have a (too) clear (to be true) idea of what a logical rule must be. Rules like (1), probably are not rules at all for them. But, then, can one deny that refusing them would considerably limit the scope of the logical investigation and debate?

We shall refrain, in the rest of the paper, from this sort of considerations, but stress how they testify how the notion of proof functional connective, besides its relations with computer science, far from being a notion without citizenship into the world of logic investigation, can, in the worst of cases, make debates arise. Debates that have hardly been unfruitful for logics.

Section 2 rests on [Martini 92], while Section 3 borrows results and techniques from [Alessi & Barbanera 91].

2 Provable realizability

The informal discussion of realizability of the introduction can be pushed one step further, by formalizing the requirements on the provability of compound propositional formulas inside a formal logical system. Following Kleene’s approach, this is achieved by associating to any propositional formula A a predicate r_{A}[x] together with suitable axioms formalizing that x realizes the formula A. The definition of r_{A}[x] is given inductively on the structure of A, while the intended domain for x is some universe of “realizers” for which the notions of applying a proof (of an implication) to another, or splitting a proof (of a conjunction) in the proofs of its components make sense. One obvious choice is to take any (partial) combinatory algebra A = (A, ·). Notice that we did not require a typed combinatory algebra; realizers come from an untyped universe, and, as a consequence, a single element may realize different formulas.

The following definition introduces realizability predicates for minimal propositional logic. Extensions to logics with other connectives will be given in the following sections. Assume first that for any propositional variable ϕ there exists a corresponding (atomic) realizability predicate P_{ϕ}. Application between realizers will be denoted by juxtaposition.

Definition 2.1 For any positive propositional formula A, its realizability predicate, r_{A}, is inductively defined as follows.

• r_{ϕ}[x] ≡ P_{ϕ}(x)

• r_{σ→τ} [x] ≡ ∀y(r_{σ}[y] → r_{τ} [xy])

The analysis of provable realizability for a propositional formal system P, then, consists in studying the relation between formal provability in P of a formula A and the provability of the formula ∃xr_{A}[x], in an another formal system K. A standard completeness result for P with respect to provable realizability in K assumes then the form

For all formulas A : ⊢_{P} A ⟺ ⊢_{K} ∃xr_{A}[x].

A result of this kind can be interpreted as evidence of the fact that P embodies (from the “point of view” of system K) our informal specification of the connectives composing the well formed formulas of P. Suppose, now, that P has connectives somewhat related to ”constructivism” and, in particular, to the intensional behaviour of proofs, like the proof functional connectives; it is then natural to require P to be a system dealing, in some way, with “representations” of proofs, or proof-skeletons. If such proofs are encoded in a (partial) combinatory algebra structure (e.g. λ-terms representing skeletons of proofs in natural deduction), then completeness can be expressed more perspicuously as

For all formulas A : ⊢_{P} t : A ⟺ ⊢_{K} r_{A}[t],  (2)

where we have denoted with ⊢_{P} t : A the judgment that t codes (part of) a proof in P of A.

Given a system P, for which we want to investigate realizability, we have a choice both on the system K and on the algebra of realizers A.

For what concerns A, a standard and classical choice is to take Kleene’s partial applicative structure (ω, ·) where n·m = ϕ_{n}(m) for some suitable enumeration ϕ_{n} of the partial recursive functions. Another possible choice, the one used in the present paper, is to consider the total combinatory algebra of untyped λ-terms modulo β-equality. Recall that λ-terms are those expressions generated by the following grammar

t ::= x | λx.t | (tt)

modulo the equality given by the axiom

(λx.t)s =_{β} t[x ← s] (β)

and the other standard rules for making =_{β} a congruence; we shall omit the subscript β when there is no danger of confusion. As a variant of this approach, in Section 4.4 we will also deal with Combinatory Logic terms equipped with the so-called combinatory β-equality.

For what concerns the system K, its choice essentially depends on the notions P is intended to formalize and on the conceptual use one wish to make of a completeness result.

For instance, the standard choice for the investigation of provable realizability for intuitionistic propositional logic is to take the classical predicate calculus (thus, P is IL, K is CL and A is Kleene’s structure), for which [Mints 89] proved completeness. The more K is powerful and “far” from P, the stronger a completeness result appears as evidence that the formalization given by P to some logical concept is sound and robust. The choice of classical logic for K, however, does not give any additional bonus over the choice of intuitionistic logic. Due to a result of Mints, in fact, for judgments of the form of those involved in the completeness property (equivalence (2) above), the two systems coincide (see 3.2). This is the reason for which, in the following, we will always take intuitionistic predicate calculus for K.

We will carry over this kind of analysis for three type-assignment systems, proving for each of them a completeness theorem of the form (2). This result has as a corollary, the semantical completeness of the type-assignment system we started with (system P in (2)). This is detailed in section 4.4.2 for strong conjunction, where we obtain an easy proof of the completeness of the intersection type discipline.

In the following sections we will find useful to switch between different formulation of the same calculus. We denote with LK (LJ, respectively) Gentzen sequent calculus for classical (intuitionistic) logic with equality, where untyped λ-terms are used as terms and equality is β-conversion; with NK and NJ we denote the corresponding natural deduction systems. The following is a standard result, the presence of λ-terms being irrelevant.

Proposition 2.2 (i) Γ ⊢LK A ⟺ Γ ⊢NK A. (ii) Γ ⊢LJ A ⟺ Γ ⊢NJ A.

Notation We will use & for intuitionistic conjunction and ∧ for strong conjunction (or intersection for types).

3 Strong Equivalence

We consider in this section a proof functional connective for double implication. Although many connectives of this kind could be defined (e.g. requiring the two directions of the implication to be obtained by the same proof, cf. [Lopez-Escobar 85]), the one we are interested in, and that we call strong equivalence and denote with ≅, comes from independent work on provable isomorphisms in typed λ-calculi ([Bruce & Longo 85], [Bruce et al. 92] and [Di Cosmo 91]).

A justification for the propositional formula A ≅ B is given iff we have a justification t for A → B (that is a way of mapping any justification a for A into a justification ta for B), a justification s for B → A, and moreover for any justification a for A, and any justification b for B, we are able to recognize that a and s(ta) are the same justification for A, and that b and t(sb) are the same justification for B. Strong equivalences, thus, are those double implications for which we can give proofs of the two “directions” that are one the inverse of the other.

The reader will have noticed how isomorphisms come in. Indeed, given a typed λ-calculus λT, two types A and B are provably isomorphic iff there are two terms f : A → B and g : B → A such that λT ⊢ f ∘ g = id_{B} and λT ⊢ g ∘ f = id_{A}. The problem attacked in the cited papers is to characterize by means of an equational theory all the isomorphisms provable in a specific λT. ([Bruce & Longo 85] deals with simply typed λ-calculus; [Bruce et al. 92] with the simply typed λ-calculus extended with (surjective) pairs and a terminal type; [Di Cosmo 91] with second order λ-calculus.) From the computer science point of view, these results help to analyse extensions to typed functional languages, where in some cases it may be useful to relax the constraint on the application of a function to its arguments, allowing arguments from isomorphic types. (Indeed some preliminary studies [Rittri 90] on this subject had a key retrieval problem for library functions as explicit motivation.). From the logical point of view, by the Curry-Howard isomorphism, these results exactly characterize strong equivalences in fragments of intuitionistic logic. It appeared then natural to investigate how this new connective behaves with respect to provable realizability. The informal analysis of the realizability of strong equivalence we have just made can be formalized along the lines of Section 2. Note, first, that our algebra of realizers has to have a way of pairing realizers, since a realizer for A ≅ B is given via two different realizers, one for A → B and one for B → A. Instead of taking pure λ-terms, then, it is convenient to extend our combinatory algebra with explicit pairs and projections:

t ::= x | λx.t | (tt) |< t, t >| f t | s t.

Application associates to the left. Conversion between λ-terms is given by the following rules

\begin{aligned}(λx.t)s & = & t[x ← s] & (β) \\ f < s, t > & = & s & (π_{1}) \\ s < s, t > & = & t & (π_{2}) \end{aligned} ,

together with rules for making = a congruence; we will sometime write =_{β,π} for this relation. Composition of terms is defined as usual: M ∘ N ≡ λx.M(Nx); id denotes the term λx.x. With this machinery, we can extend Definition 2.1 with the following.

Definition 3.1 The realizability predicate for strong equivalence is defined as

r_{A≅B}[x] ≡ r_{A→B}[f x] & r_{B→A}[s x] & ((f x) ∘ (s x) = id) & ((s x) ∘ (f x) = id)

Next sections will introduce a very natural formal system for strong equivalence and then show its completeness.

3.1 A Type Assignment System for Strong Equivalence

Strong equivalence can be seen as a new type constructor for λ-calculus, embodying into type assignment rules the realizability analysis discussed above. Types are given by the following grammar (ϕ ranges over atomic types)

T ::= ϕ | T → T | T ≅ T.  (3)

A basis is a finite sequence x_{1} : A_{1}, …, x_{n} : A_{n}, where the x’s are distinct variables and the A’s are types; we usually denote a basis with Γ.

Definition 3.2 The type assignment system for Strong Equivalence is given in Figure 1, defining by mutual induction the relations Γ ⊢ t : A (a type judgment, to be read “t has type A in basis Γ”) and Γ ⊢ t = s (an equality judgment, to be read “t and s are equal terms in basis Γ).

Remark 3.1 1. In force of rules (Eq), the relation t : A holds up to =_{β,π}, a fact which is essential for completeness.

2. A type A ≅ B is inhabited (that is, ⊢ s : A ≅ B for some term s), iff A and B are provable isomorphic, iff A = B is derivable in Bruce and Longo’s equality theory for simply typed λ-calculus.

Γ x : A ⊢ x : A (Ax)
\frac{Γ ⊢ s : A → B Γ ⊢ t : B → A Γ ⊢ s ∘ t = id Γ ⊢ t ∘ s = id}{Γ ⊢ ⟨s, t⟩ : A ≅ B} ≅I

\frac{Γ ⊢ s : A ≅ B}{Γ ⊢ f s : A → B} ≅E^{f}  \frac{Γ ⊢ s : A ≅ B}{Γ ⊢ s s : B → A} ≅E^{s}
\frac{Γ ⊢ t : A ≅ B}{Γ ⊢ (f t) ∘ (s t) = id} ≅E_{=}^{1}  \frac{Γ ⊢ t : A ≅ B}{Γ ⊢ (s t) ∘ (f t) = id} ≅E_{=}^{2}

\frac{Γ x : A ⊢ b : B}{Γ ⊢ λx.b : A → B} →I  \frac{Γ ⊢ b : A → B Γ ⊢ a : A}{Γ ⊢ b(a) : B} →E

\frac{Γ x : A ⊢ tx : B}{Γ ⊢ t : A → B} (η)  \frac{Γ ⊢ f t : A → B Γ ⊢ s t : B → A Γ⊢(f t)∘(s t)=id Γ⊢(s t)∘(f t)=id}{Γ ⊢ t : A ≅ B} (SP)
\frac{s =_{β,π} t}{Γ ⊢ s = t} (Eq_{1})  \frac{Γ ⊢ s : A Γ ⊢ s = t}{Γ ⊢ t : A} (Eq_{2})
\frac{Γ ⊢ s = u Γ ⊢ u = t}{Γ ⊢ s = t} (Eq−t)  \frac{Γ ⊢ s = t}{Γ ⊢ t = s} (Eq−s)

Figure 1: Type-assignment system for Strong Equivalence

3.2 Provable realizability for strong equivalence

Following [Mints 89], and according to completeness (2), we will show that, for any A, r_{A}[t] is provable in intuitionistic predicate calculus LJ iff the type assignment system introduced in Definition 3.2 proves that t can be given the type A. For the purpose of this section, axioms of LJ are of the form ⊢_{LJ} s = t together with a justification for s =_{β,π} t, or of the form s = t, P (s) ⊢_{LJ} P (t). Recall (e.g. [Takeuti 75]) that for this system we can prove the elimination of essential cuts, a cut being inessential if the cut formula is an equation. All proofs and techniques are modifications of Mints’ ones, those for strong equivalence being similar to those for (standard) conjunction. The novelty is the presence of equations in the premises of sequents (coming from left introduction of strong equivalences), that forces us to choose a less compact form for the axioms and to consider normal proofs with inessential cuts (axioms in [Mints 89] are sequents Δ, P (s) ⊢ P (s′), together with a justification for s = s′.) In the following we will only give the cases for axioms and strong equivalences, all the other being either identical to Mints’ treatment, or trivially modifiable. The main idea for Mints’ result is a careful analysis of the structure of LJ proofs of sequents expressing provable realizability. The crucial points are expressed by the following proposition, showing that any sequent occurring in a proof of a formula of the form r_{A}[t] has a very special shape (thus allowing an easy inductive proof of theorem 3.4.) The following proposition considers (essential-) cut-free proofs of sequents of the form ⊢_{LJ} r_{F} [t]. By the subformula property, such derivations will only contain either formulas of the form r_{A}[t], with A subformula of F, or equations t = s (coming from formulas r_{A≅B}[t]), or instances

r_{A}[s] → r_{B}[ts]  (4)

(coming from formulas of the kind ∀y(r_{A}[y] → r_{B}[ty]).) By the permutability of inferences in sequent proofs ([Kleene 52], theorem 2, pag. 18) we can assume that in any proof of the kind at hand, any →-rule (introducing a formula of the shape 4) is immediately followed by a ∀-rule on the same side, thus producing proof structures of the shape

\frac{Γ, r_{A}[y] ⊢_{LJ} r_{B}[ty]}{Γ ⊢_{LJ} r_{A→B}[t]} ⊢→ and \frac{Γ ⊢_{LJ} r_{A}[y] Γ, r_{B}[ty] ⊢_{LJ} C}{Γ, r_{A→B}[t] ⊢_{LJ} C} →⊢ .

Similarly, we can always rearrange a proof in such a way that all & -rules introducing (on the left or on the right) a formula r_{A≅B}[t] occur together, giving rise to proof structures we will call ⊢≅ and ≅⊢. Once these proof structures have been isolated, the proof of the following proposition is straightforward; in its statement, these proof structures have to be counted as single inferences .

Notation: (i) t denotes a sequence of terms; E denotes a sequence of equations.

(ii) π denotes a finite (possibly empty) sequence of projections (e.g. f s f f ).

(iii) If π ≡ p_{1} … p_{n}, then π(t) stands for p_{1}(… (p_{n}(t)) …).

(iv) A term is a head projection term iff it is of the shape π_{n}(… π_{1}(π(xt)t_{1}) … t_{n}), for n ≥ 0.

(v) We will write rA[t] ⊢ r_{B}[s] for r_{A_{1}}[t_{1}], …, r_{A_{n}}[t_{n}] ⊢ r_{B}[s]

Proposition 3.3 Let F be any propositional formula. Any sequent occurring in a cut-free derivation of the sequent ⊢_{LJ} r_{F} [t] is of the form

r_{F_{1}}[h_{1}], …, r_{F_{n}}[h_{n}], E_{1}, …, E_{k} ⊢_{LJ} r_{G}[s]  (5)

or of the form

r_{F_{1}}[h_{1}], …, r_{F_{n}}[h_{n}], E_{1}, …, E_{k} ⊢_{LJ} Q  (6)

where n, k ≥ 0, s is a term, the h_{i}’s are head projection terms, and the E_{i}’s and Q are equations between terms.

Proof: By induction on the length of the derivation. The basis and the case of an inessential cut are obvious.

Case ≅⊢: We have four cases:

rF[h], r_{A→B}[f h′], E ⊢ r_{G}[s]
rF[h], r_{A≅B}[h′], E ⊢ r_{G}[s]

and its symmetric; or

rF[h], (f h′) ∘ (s h′) = id, E ⊢ r_{G}[s]
rF[h], r_{A≅B}[h′], E ⊢ r_{G}[s]

and its symmetric. In all the cases the premises are of the required form.

Case ⊢≅:

rF[h], E ⊢ r_{A→B}[f t] rF[h], E ⊢ r_{B→A}[s t] rF[h], E ⊢ (f t) ∘ (s t) = id rF[h], E ⊢ (s t) ∘ (f t) = id rF[h], E ⊢ r_{A≅B}[t].  (7)

□

Remark 3.2 Although we have stated the previous proposition in terms of the intuitionistic system LJ, the completeness theorem holds also for classical predicate calculus. Following [Mints 89], in fact, in [Martini 92] it is proved that

rA[t], E ⊢_{LJ} r_{B}[s] ⇔ rA[t], E ⊢_{LK} r_{B}[s].

Theorem 3.4 (Completeness)

(i) x_{1} : A_{1}, …, x_{n} : A_{n} ⊢≅ t : B ⟺ r_{A_{1}}[x_{1}], …, r_{A_{n}}[x_{n}] ⊢_{LJ} r_{B}[t] (ii) x_{1} : A_{1}, …, x_{n} : A_{n} ⊢≅ s = t ⟺ r_{A_{1}}[x_{1}], …, r_{A_{n}}[x_{n}] ⊢_{LJ} s = t Proof: (i) and (ii) are proved by combined induction on the derivations; for LJ it will be convenient to argue instead in its natural deduction version, NJ. (⇒): Basis: If x_{1} : A_{1}, …, x_{n} : A_{n} ⊢≅ x_{i} : A_{i}, then an inessential cut from ⊢_{LJ} x_{i} = x_{i} and x_{i} = x_{i}, r_{A_{i}}[x_{i}] ⊢_{LJ} r_{A_{i}}[x_{i}], followed by n − 1 weakenings gives the thesis.

Case ≅ I: By inductive hypothesis, for Γ′ ≡ r_{A_{1}}[x_{1}], …, r_{A_{n}}[x_{n}], we have Γ′ ⊢_{LJ} r_{A→B}[s], Γ′ ⊢_{LJ} r_{B→A}[t], Γ′ ⊢_{LJ} s ∘ t = id, and Γ′ ⊢_{LJ} t ∘ s = id. By the equality rules (which are derivable in LJ) we obtain

Γ′ ⊢_{LJ} r_{A→B}[f < s, t >] and Γ′ ⊢_{LJ} r_{B→A}[s < s, t >].

Noting that (f < s, t >) ∘ (s < s, t >) = s ∘ t, one (≅ I) (in NJ) allows to conclude.

Case (SP): Similarly.

Cases ≅ E: Immediate, by induction and & E.

Case (Eq_{1}): If s =_{β,π} t, then ⊢_{LJ} s = t is an axiom. Some weakenings give the thesis.

Case (Eq_{2}): By induction and the equality rules in LJ. (⇐): Assume rA[x] ⊢_{LJ} r_{B}[t]. We argue by induction on a normal natural deduction proof in NJ.

Basis: The proof consists of the single premise r_{B}[x]. Then x : B ⊢≅ x : B by (Ax).

Equality rules: If the conclusion is an equality, the induction hypothesis and the corresponding equality rule give the thesis. If the conclusion is a predicate

\begin{matrix}rA[x] ⊢_{NJ} s = t rA[x] ⊢_{NJ} r_{B}[s] \\ rA[x] ⊢_{NJ} r_{B}[t] \end{matrix}

conclude by induction hypothesis and rule (Eq_{2}).

& I:

\frac{rA[x] ⊢_{NJ} r_{B→C}[f t] rA[x] ⊢_{NJ} r_{C→B}[s t] rA[x] ⊢_{NJ} (f t) ∘ (s t) = id rA[x] ⊢_{NJ} (s t) ∘ (f t) = id}{rA[x] ⊢_{NJ} r_{B≅C}[t]} & I

Induction hypothesis and rule (SP) give the thesis.

& E: We have two main cases, one where the conclusion is a realizability predicate

\frac{rA[x] ⊢_{NJ} r_{B→C}[s] & ψ}{rA[x] ⊢_{NJ} r_{B→C}[s]} & E^{l}

and one where the conclusion is an equality

\frac{rA[x] ⊢_{NJ} s = s′ & ψ}{rA[x] ⊢_{NJ} s = s′} & E^{l}

In both cases, by Proposition 3.3 the premise has to be of the form rA[x] ⊢_{LJ} r_{B≅C}[t] for some term t (the right-hand side cannot be a single equation because we are applying an &-elimination rule). By the definition of the realizability predicate, the premise is thus

rA[x] ⊢_{NJ} r_{B→C}[f t] & r_{C→B}[s t] & (f t) ∘ (s t) = id & (s t) ∘ (f t) = id,

where s = f t, in the first case, and s = (f t) ∘ (s t), s′ = id in the second case. Conclude by induction and rule (≅ E^{f}) (in the first case) or (≅ E_{=}^{1}) (in the second). The two symmetrical cases are analogous. □

4 Strong Conjunction

The first logical system for strong conjunction is due to Lopez-Escobar [Lopez-Escobar 85], who first studied also its completeness with respect to provable realizability. The system can be seen as a variant of the type assignment system for λ-terms we will introduce in Definition 4.1. As it was shown in [Mints 89], however, Lopez-Escobar’s system is not complete with respect to provable realizability. The formula ((α → β) ∧ δ) → (((α ∧ γ) → β) ∧ δ) is not provable in that system, yet it is realized by (any representative of) the identity function (any realizer for α → β is also a realizer for (α ∧ γ) → β). This counterexample relies on the fact that the system lacks a rule of extensionality for proofs, which has then to be added in order to achieve completeness (this is the role of rule (η), cf. Lemma 4.2). A second system for strong conjunction is the one given in [Mints 89], which contains an extensionality rule, but which uses typed λ-terms as notation for proofs, taking then their type erasures (i.e. the untyped terms obtained by forgetting all type decorations) as realizers. In [Mints 89] it is further proved that the given system is complete with respect to provable realizability. The proof, however, does not work properly, for the presence of these typed terms. The difference between typed systems and type assignment systems is often overlooked and this can make problems arise. A typed system consists in a set of terms each possessing a precise, unique type; types are not, so to speak, autonomous objects, but just decorations recalling what the functionality of a term is, and they are used as a means of partitioning the set of terms. In type assignment systems, instead, types are objects themselves, and belong to a universe strictly separated from that of (untyped) terms. Types can be looked at as predicates denoting functional properties; the rules of the type assignment system allow one to infer which predicates hold for a given term. While typed terms have a unique type, in a type assignment system a term can have more than a functionality, that is, it can be given more than one type. Let us informally explain how having overlooked these differences prevented the completeness proof in [Mints 89] to work properly. It is not difficult to see that the untyped λ-term λx.x (i.e. a representative for the identity function) is a realizer for the formula (α → α) ∧ (β → β). In fact, in the notation of Section 2, it is provable that

⊢_{LJ} r_{(α→α)∧(β→β)}[λx.x].

However, it is not possible to have a typed term t such that the statement (α → α) ∧ (β → β)(t) is derivable, even if it is possible to derive the statements (α → α)(t_{1}) and (β → β)(t_{2}) for terms t_{1} and t_{2} such that their type erasures are both equal to λx.x (we have used the notation γ(t) for the judgment “γ is the type of the typed term t”, in order to stress the difference of this approach with a type-assignment system). This is because two typed terms with the same “structure”, but with different types (even if the difference between them consists only in the names of type variables), are two distinct terms, a fact that prevents Mints’ rule

\frac{Γ ⊢ γ(t) Γ ⊢ δ(t)}{Γ ⊢ γ ∧ δ(t)}

from applying in case we have α → α(t_{1}) and β → β(t_{2}) and we only know that t_{1} and t_{2} have the same type erasure, as it should be in the proof of Lemma 2.3 in [Mints 89]. To amend the completeness result we have to recast the system in a type assignment framework instead that in a typed one ([Mints 91] agrees with our remarks). With this modification, and with essentially the same rules and similar proofs, we will be able to show the completeness of the system (Theorem 4.13 below). The system we obtain, in conclusion, is an already existing one: the type assignment system for intersection types introduced in [Barendregt et al. 83].

4.1 A Type Assignment System for Strong Conjunction

Definition 4.1 (i) The set of intersection types is the set of types built out of a denumerable set of type variables and the type constant ω by means of two type constructors: → and ∧.

x : σ ⊢^{∧} x : σ (Ax)
B ⊢^{∧} M : ω (Ax−ω)
\frac{B ⊢^{∧} M : τ}{B, x : σ ⊢^{∧} M : τ} (weak)

\frac{B, x : σ ⊢^{∧} M : τ}{B ⊢^{∧} λx.M : σ → τ} (→I) (∗)

\frac{B ⊢^{∧} M : σ → τ B ⊢^{∧} N : σ}{B ⊢^{∧} (MN) : τ} (→E)

\frac{B ⊢^{∧} M : σ B ⊢^{∧} M : τ}{B ⊢^{∧} M : σ ∧ τ} (∧I)

\frac{B ⊢^{∧} M : σ ∧ τ}{B ⊢^{∧} M : σ} (∧E^{l}) \frac{B ⊢^{∧} M : σ ∧ τ}{B ⊢^{∧} M : τ} (∧E^{r})

\frac{B ⊢^{∧} M : σ σ ≤ τ}{B ⊢^{∧} M : τ} (≤)

(∗) if x does not occur in B.

Figure 2: The type assignment system for Strong Conjunction

(ii) A (type assignment) statement is an expression of the form M : σ where σ is a type and M is a λ-term. M is called the subject of the statement. A basis B is a set of statements with only variables as subjects. The same variable can occur several times in a basis B.

(iii) The relation ≤ among types is the smallest relation satisfying the following clauses:

1. τ ≤ τ  2. τ ≤ τ ∧ τ
3. σ ≤ ω  4. ω ≤ ω → ω
5. σ ∧ τ ≤ σ  6. σ ∧ τ ≤ τ
7. (σ → ρ) ∧ (σ → τ) ≤ σ → (ρ ∧ τ)  8. σ ≤ τ ≤ ρ ⇒ σ ≤ ρ
9. σ ≤ σ′, τ ≤ τ′ ⇒ σ ∧ τ ≤ σ′ ∧ τ′
10. σ′ ≤ σ, τ ≤ τ′ ⇒ (σ → τ) ≤ σ′ → τ′

σ ∼ τ is short for (σ ≤ τ and τ ≤ σ).

(iv) The type assignment system ⊢^{∧} is defined in Figure 2.

Remark 4.1 It is easy to check that if B ⊢^{∧} M : α then B ∪ B′ ⊢^{∧} M : α for any basis B′.

Lemma 4.2 [Barendregt et al. 83] Rule

\frac{B ⊢ λx.Mx : σ}{B ⊢ M : σ} (η) if x∉FV(M)

is admissible in ⊢^{∧}.

Lemma 4.3 (Subject conversion) [Coppo & Dezani 80] [B ⊢^{∧} M : α and M =_{β} M′] ⇒ B ⊢^{∧} M′ : α.

It is beyond the scope of this paper to give the detailed motivations and the main achievements obtained by means of system ⊢^{∧} and its variants. To show its relevance for the syntactical theory of pure λ-calculus we just quote the following theorem, where intersection types are used to characterize relevant classes of λ-terms.

Theorem 4.4 [Barendregt et al. 83, Coppo et al. 82]

(i) M is normalizable iff there exist B and α (B,α ω-free) such that B ⊢^{∧} M : α.

(ii) M is strongly normalizable iff there exist B and α (B,α ω-free) such that B ⊢_{−ω}^{∧} M : α, where ⊢_{−ω}^{∧} is the subsystem obtained from ⊢^{∧} by taking out the constant ω and axiom (Ax-ω).

(iii) M has head normal form iff there exist B and α ( α tail proper) such that B ⊢^{∧} M : α, where a type is tail proper if it is of the form ρ_{1} → … → ρ_{n} → ϕ with ϕ type variable.

Systems with intersection types have been used also in the construction of (filter) models of the type-free λ-calculus, see [Barendregt et al. 83, Coppo et al. 82].

To prove that ⊢^{∧} is a good formalization for the notion of strong conjunction, i.e. a sound and complete system for provable realizability, we shall first prove the equivalence of ⊢^{∧} to the type assignment system ⊢_{M} defined below. Then, by using this equivalence, a proof will be given of the fact that a statement ⊢^{∧} M : α is derivable iff it is possible to prove in intuitionistic first order logic that M is a realizer for α.

Definition 4.5 The system ⊢_{M} is defined from ⊢^{∧} by taking out the constant ω, axiom (Ax-ω) and rule (≤), and by adding the following rules.

\begin{matrix}\frac{B, x : α ⊢_{M} Mx : β}{B ⊢_{M} M : α → β} & (η_{1}) \\ \frac{B ⊢_{M} M : α M =_{β} N}{B ⊢_{M} N : α.} & (eq_{β}) \end{matrix}

Note that ⊢_{M} is an untyped version of the system for provable realizability given in [Mints 89] (the subscript M is used to recall this fact). The completeness result of next section could have been proved more directly, thus avoiding system ⊢_{M}. However, our formalization, which closely match Mints’ proof, helps to note how the untypedness of ⊢_{M} is essential in the proof, where Mints’ approach would break.

Lemma 4.6 Rule (≤) is admissible in ⊢_{M}.

Proof: By induction on the derivation of σ ≤ τ. □

Lemma 4.7 Let ω ∉ α, B. Then B ⊢^{∧} M : α ⇔ B ⊢_{M} M : α.

Proof: (⇐) It is enough to prove that rules (eq_{β}) and (η_{1}) are admissible in ⊢^{∧}.

(eq_{β}) By Lemma 4.3.

(η_{1}) By Lemma 4.2 the admissibility of this rule can be easily proved in the following way.

\frac{\frac{B, x : α ⊢^{∧} Mx : β}{B ⊢^{∧} λx.Mx : α → β} (→I)}{B ⊢^{∧} M : α → β} (η)

(⇒) B ⊢^{∧} M : α ⇒ B ⊢^{∧} \overline{M} : α by Lemma 4.3

\overline{M} is the normal form of M (which exists by Theorem 4.4)

⇒ B ⊢_{−ω}^{∧} \overline{M} : α by the subformula principle,

cf. Lemma 4.5

of [Barendregt et al. 83]

⇒ B ⊢_{M} \overline{M} : α by Lemma 4.6
⇒ B ⊢_{M} M : α by rule (eq_{β}).

□

4.2 Provable Realizability for Strong Conjunction

We will show in this section that the type assignment system of Definition 4.1 is complete with respect to provable realizabilty. We extend, first, the definition of the realizability predicate, Definition 2.1, to encompass strong conjunction.

Definition 4.8 The realizability predicate for strong conjunction is defined as

r_{A∧B}[x] ≡ r_{A}[x] & r_{B}[x].

Realizers are here pure λ-terms as defined in Section 2, modulo β-equality. As for LJ, we can use here the more compact form having as axioms sequents Δ, P (s) ⊢ P (s′), together with a justification for s = s′. Recall, now, from Section 3.2, that proofs in LJ of formulas of the form r_{A}[t] can be seen, by the subformula principle and the permutability of rules, as consisting of special proof structures, called there ⊢→ and →⊢. (Recall also the notation we used there: M stands for a sequence of terms, while r_{α}[M] ⊢ r_{B}[N] stands for r_{α_{1}}[M_{1}], …, r_{α_{n}}[M_{n}] ⊢ r_{B}[N]

Proposition 3.3 specializes now to the following proposition [Mints 89], showing that if we are interested only in deriving formulas of the form r_{A}[t], then it is enough to use a restriction of LJ where the sequences of formulas on the left of the entailment are of a special shape and the rules are only those for conjunction (& ⊢_{LJ} and ⊢_{LJ} &) and the two “condensed” proof structures for implication (→⊢ and ⊢→).

Proposition 4.9 Any sequent occurring in the cut-free derivation of the sequent

r_{α_{1}}[x_{1}M_{1}], … r_{α_{h}}[x_{h}M_{h}] ⊢_{LJ} r_{β}[M]

is of the form

r_{γ_{1}}[y_{1}M_{1}], … r_{γ_{k}}[y_{k}M_{k}] ⊢_{LJ} r_{δ}[M].

In order to show the equivalence of ⊢_{LJ} and ⊢_{M}, it is handy to introduce some further notation for comparing sequences of formulas in ⊢_{LJ} and basis in ⊢_{M}.

Definition 4.10 (i) A context Γ for ⊢_{LJ} is an r-context if all its elements are of the form r_{α}[M].

(ii) Let Γ be an r-context in which all terms M are variables and let B be a basis for ⊢^{∧} such that ω ∉ B.

1. Γ^{∘} is the basis for ⊢^{∧} obtained by replacing in Γ each element r_{γ}[x] by x : γ.

2. B^{⋄} is the r-context obtained by replacing in B each element x : γ by r_{γ}[x].

Lemma 4.11

B ⊢_{M} M : α ⇒ B^{⋄} ⊢_{LJ} r_{α}[M].

Proof: By the induction on the derivation of B ⊢_{M} M : α. We shall give only the non-trivial cases.

(∧E)

\begin{matrix}B ⊢_{M} M : α ∧ β \\ B ⊢_{M} M : α \end{matrix}

By the induction hypothesis B^{⋄} ⊢_{LJ} r_{α∧β}[M]. By Proposition 2.2 B^{⋄} ⊢_{NJ} r_{α∧β}[M] ≡ r_{α}[M]&r_{β}[M].

Then by &E) in ⊢_{NJ} we get B^{⋄} ⊢_{NJ} r_{α}[M] and, by 2.2 again, B^{⋄} ⊢_{LJ} r_{α}[M].

(→ I)

\begin{matrix}B, x : α ⊢^{∧} M : β \\ B ⊢^{∧} λx.M : α → β \end{matrix}

By the induction hypothesis B^{⋄}, x : α ⊢_{LJ} r_{β}[N] and hence, since ⊢_{LJ} is a system with equality and N = (λx.N)x, we get B^{⋄}, x : α ⊢_{LJ} r_{β}[(λx.N)x]. By applying rule ⊢→ we obtain B^{⋄} ⊢_{LJ} r_{α→β}[N].

(→ E)

\frac{B ⊢^{∧} M : α → β B ⊢^{∧} N : α}{B ⊢^{∧} (MN) : β}

By the induction hypothesis B^{⋄} ⊢_{LJ} r_{α→β}[M] and B^{⋄} ⊢_{LJ} r_{α}[N]. By Proposition 2.2 B^{⋄} ⊢_{NJ} r_{α→β}[M] ≡ ∀x(r_{α}[x] → r_{β}[Nx]). Then by rules (∀E) and (→ E) and 2.2 again, B^{⋄} ⊢_{LJ} r_{β}[MN].

□

Lemma 4.12 Let Γ ⊢_{LJ} r_{α}[M] with Γ = {r_{γ_{i}}[P_{i}]}_{i∈I} such that there exist bases B_{i} such that B_{i} ⊢^{∧} P_{i} : γ_{i}. Then ⋃_{i∈I} B_{i} ⊢^{∧} M : α.

Proof: By induction on the derivation of Γ ⊢_{LJ} r_{α}[M], exploiting Proposition 4.9.

(Ax) Γ, r_{α}[xM] ⊢_{LJ} r_{α}[N], with xM = N.

By hypothesis we know that, for some B, B ⊢^{∧} xM : α; Lemma 4.3 allows to conclude.

(⊢_{LJ} &)

\frac{Γ ⊢_{LJ} r_{α}[M] Γ ⊢_{LJ} r_{β}[M]}{Γ ⊢_{LJ} r_{α∧β}[M]}

By the induction hypothesis we have B_{1}, B_{2} such that B_{1} ⊢^{∧} M : α and B_{2} ⊢^{∧} M : β and hence the thesis follows by Remark 4.1 and rule (∧I)

(& ⊢_{LJ})

\begin{matrix}Γ, r_{δ}[P], r_{β}[P] ⊢_{LJ} r_{α}[M] \\ Γ, r_{δ∧β}[P] ⊢_{LJ} r_{α}[M] \end{matrix}

We have that there exists B′ such that B′ ⊢^{∧} P : δ ∧ β. By rule (∧E) it is possible to apply the induction hypothesis, which yields the thesis.

(→⊢_{LJ})

\frac{Γ ⊢_{LJ} r_{δ}[y] Γ, r_{β}[zPy] ⊢_{LJ} r_{α}[M]}{Γ, r_{δ→β}[zP] ⊢_{LJ} r_{α}[M]}

We have that there exists B_{1} such that B_{1} ⊢^{∧} zP : δ → β. As it is possible to apply the induction hypothesis to Γ ⊢_{LJ} r_{δ}[y], there exists B_{2} such that B_{2} ⊢^{∧} y : δ. The thesis then follows from the induction hypothesis on Γ, r_{β}[zPy] ⊢_{LJ} r_{α}[M], which is applicable since, by (→ E), B_{1} ∪ B_{2} ⊢^{∧} zPy : β.

(⊢_{LJ}→)

\begin{matrix}Γ, r_{α}[y] ⊢_{LJ} r_{β}[My] \\ Γ ⊢_{LJ} r_{α→β}[M] \end{matrix}

We can apply the induction hypothesis since y : α ⊢^{∧} y : α. Then ⋃_{i∈I} B_{i}, y : α ⊢^{∧} My : β and by rule (→ I) ⋃_{i∈I} B_{i} ⊢^{∧} λy.My : α → β. Since y ∉ F V (M), by rule (η), which is admissible in ⊢^{∧}, we get ⋃_{i∈I} B_{i} ⊢^{∧} M : α → β.

□

From the two lemmas above it is straightforward to obtain the following theorem, stating formally that ⊢^{∧} is sound and complete with respect to provable realizability for strong conjunction, and hence a good formalization of it. Of course we have to take care that ω does not appear in the types of assumptions and conclusions.

Theorem 4.13 Let ω ∉ α_{1}, …, α_{n}, α. Then

x_{1} : α_{1}, …, x_{n} : α_{n} ⊢^{∧} M : α ⟺ r_{α_{1}}[x_{1}], …, r_{α_{n}}[x_{n}] ⊢_{LJ} r_{α}[M]

It is worth pointing out that it would be possible to prove, in a more direct way, that ⊢_{NJ} is equivalent to ⊢^{∧}, without using Gentzen’s sequent calculus and ⊢_{M}. Their use is justified by our aim of comparing what is done in the present paper with what is done in [Mints 89].

4.3 Getting rid of ω

The type assignment system for implication and strong conjunction has the “non-logical” rules (≤) and (ω), not involving the operators “→” and “∧. Is it possible to have a (restricted) system without rule (≤) or (ω), for which still some completeness result is provable?

Let us observe, first, that the extensionality rule (η) is necessary in the proof of Lemma 4.12, case ⊢_{LJ}→ (similarly, extensionality for pairs, rule SP of definition 3.2, is necessary for the completeness of strong equivalence, Theorem 3.4). Its presence, in other words, it is not connected with strong conjunction, but with the implication connective. Rule (≤), therefore, is unavoidable, in view of its equivalence with (η), or (η_{1}) (see Lemmas 4.2 and 4.6).

What about rule (ω)? Its role is crucial in the proof of the Subject Conversion Lemma, 4.3, which is essential for completeness, since we use a logic equipped with β-equality between λ-terms. If we want to eliminate rule (ω), therefore, we must change our combinatory algebra of realizers in such a way that the preservation of their types could be guaranteed without making use of (ω). Such a system does exist: it is the system ⊢_{−ω}^{∧}, with the additional restriction that the terms have to be λI-terms (we will write ⊢_{−ω}^{∧I} for this system). Let us recall that the λI-calculus is a restriction of the pure λ-calculus, where it is possible to form a term λx.M only if x ∈ F V (M). We refer to [Barendegt 1984], Cap. 9, for the precise definition and properties.

The zealous reader will enjoy to check that if we restrict realizers to be λI-terms, a good formalization for strong conjunction, i.e. a system sound and complete w.r.t. provable realizability, is exactly ⊢_{−ω}^{∧I}.

Before starting such an exercise, however, it is likely that the reader will ask her/himself if this is not a too strong solution for getting rid of ω. Weaker restrictions, however, seem to prevent Theorem 4.13 from holding. As an example, maintain all λ-terms as realizers and restrict only the conversion among them in the following way : M = N iff both M and N are strongly normalizable, M =_{β} N, and F V (M) = F V (N) = F V (P) with P the normal form of M and N. With such a restriction it is still possible to prove the (⇐) half of Theorem 4.13, while the derivation of (λxy.x)zt : α from the basis z : α, t : β is a counterexample for the (⇒) direction.

4.4 Combinatory Logic

Realizers of implicational formulas have always been, so far, λ-terms. As mentioned in the Section 2, however, other choices are possible. We will consider in this section the combinatory algebra of Combinatory Logic (CL) terms, a well known and studied alternative to λ-terms ([Lopez-Escobar 85] uses CL-terms for his study of provable realizability).

As a corollary to Theorem 4.13, by building on some known results relating λ-terms and CL-terms, we will be able to obtain a completeness result also for CL-terms. Since CL is a first-order theory, this result, by appealing to the standard (Gödel’s) completeness theorem, will enable us to get an easy proof of some semantic consequences, like the equivalence of type judgement validity for CL-terms and their λ-calculus translation w.r.t. two different notions of model (λ-algebras and λ-models). It will be also possible to provide an alternative proof of system ⊢^{∧}’s semantic completeness.

Before going into the details, however, we have to decide which notion of equality between CL-terms to consider. Two notions of conversion are sensible in CL. The first, weak equality, is sufficient for combinatory completeness (and thus for considering CL as a good theory of functions, without having to deal with the notion of bound variables). It is equationally axiomatizable by

Kxy = x Sxyz = xz(yz).

The second notion of conversion, combinatory β-equality (whose theory will be denoted by CL_{β} and whose symbol will be =_{cβ}), enables a good correspondence between CL-terms and λ-terms with β-equality. It is possible to define translations

(−)_{λ} : CL − terms ⟶ λ−terms
(−)_{H} : λ−terms ⟶ CL − terms,

such that X =_{cβ} Y iff X_{λ} =_{β} Y_{λ}. In what follows we shall assume (−)_{H} to be one of the most powerful translations, for instance H^{η}, as defined in [Curry & Feys 58]. Also CL_{β} is equationally axiomatizable (we refer to [Barendegt 1984] par. 7.3 for the rather long list of axioms needed); the class of its models (λ-algebras) is larger than the class of models of the λ-calculus, which is first-order axiomatizable, but not with equations only (rule (ξ), a principle of weak extensionality, is an implication and does not hold in λ-algebras).

4.4.1 CL-terms with Combinatory β-equality

In the rest of this section we shall deal with provable realizability using CL-terms (with K, S and I as basic combinators) and combinatory β-equality.

The definition of the realizability predicate r_{α}[X] where X is a CL-term is obviously the same as the one with λ-terms. We shall use superscripts to stress the fact that we are using systems with CL-terms.

Definition 4.14 The system ⊢_{LJ}^{CL_{β}} is the intuitionistic sequent calculus with equality, where terms are CL-terms and equality is combinatory β-equality.

The following lemma is a straightforward check.

Lemma 4.15

⊢_{LJ}^{CL_{β}} r_{α}[X] ⟺ ⊢_{LJ} r_{α}[X_{λ}].

The type-assignment system corresponding to this notion of provable realizability uses CL-terms and intersection types, and was introduced in [Dezani & Hindley 89].

Definition 4.16 The system ⊢_{CL}^{∧} is defined by the following axiom schemes and rules. Axioms:

• B ⊢_{CL}^{∧} I : σ → σ

• B ⊢_{CL}^{∧} K : σ → τ → σ

• B ⊢_{CL}^{∧} S : (σ → τ → ρ) → (σ → τ) → σ → ρ

Rules: (→ E), (∧I), (∧E), (ω) and (≤).

Lemma 4.17 [Dezani & Hindley 89]

⊢_{CL}^{∧} X : α ⟺ ⊢^{∧} X_{λ} : α

The presence of rule (ω) allows ⊢_{CL}^{∧} to have rule (eq_{β}) admissible also for CL-terms.

Lemma 4.18 [Dezani & Hindley 89]

B ⊢_{CL}^{∧} X : α, X =_{cβ} Y ⇒ B ⊢_{CL}^{∧} Y : α

With these facts, completeness of provable realizability is now proved easily.

Theorem 4.19

⊢_{LJ}^{CL_{β}} r_{α}[X] ⟺ ⊢_{CL}^{∧} X : α (with ω ∉ α)

Proof:

⊢_{LJ}^{CL_{β}} r_{α}[X]  ⊢_{CL}^{∧} X : α
Lemma 4.15  ⇕  ⇕  Lemma 4.17
⊢_{LJ} r_{α}[X_{λ}]  ⟺  ⊢^{∧} X_{λ} : α
Theorem 4.13

□

4.4.2 Some Semantic Consequences

Theorem 4.19 allows easy and elegant proofs of several semantical equivalences, exploiting the fact that the semantic completeness of ⊢_{LJ}^{CL_{β}} and ⊢_{LJ} is an instance of usual (Gödel) completeness. Let us first define the notion of validity for type assignment systems.

Definition 4.20 [Barendregt et al. 83] Let M be a λ-model(λ-algebra) over the applicative structure < D, · >.

(i) If ξ is a valuation of variables in D, then [[P]]_{ξ}^{M} is the interpretation of the λ-term(CL-term) P in M via ξ.

(ii) Let V be a valuation of type variable in subsets of the domain D. Then the interpretation of a type

σ in M via V is defined as follows.

– [[ϕ]]_{V}^{M} = V(ϕ) where ϕ a type variable.

– [[ω]]_{V}^{M} = D

– [[σ → τ]]_{V}^{M} = {d ∈ D|∀e ∈ [[σ]]_{V}^{M} d · e ∈ [[τ]]_{V}^{M}}

– [[σ ∧ τ]]_{V}^{M} = [[σ]]_{V}^{M} ∩ [[τ]]_{V}^{M} (iii) M, V, ξ ⊧_{(CL)}^{∧} P : σ iff [[P]]_{ξ}^{M} ∈ [[σ]]_{V}^{M}

M, V, ξ ⊧_{(CL)}^{∧} B iff M, V, ξ ⊧_{(CL)}^{∧} x : σ for all x : σ ∈ B B ⊧_{(CL)}^{∧} P : σ iff for all M, V, ξ ⊧_{(CL)}^{∧} B, M, V, ξ ⊧_{(CL)}^{∧} P : σ.

We shall denote by CL_{β} ⊧_{CL}^{∧} X : α (with X a CL-term) the semantic validity of X : α in all λ-algebras. We can now give a new proof of the fact that both systems ⊢^{∧} and ⊢_{CL}^{∧} are complete with respect to this notion of validity.

Lemma 4.21 [Barendregt et al. 83] Let M be a λ-term.

B ⊢^{∧} M : α ⟺ B ⊧^{∧} M : α.

We can now give a new proof of the fact that both systems ⊢^{∧} and ⊢_{CL}^{∧} are complete with respect to this notion of validity, provided we restrict ourselves to bases and conclusions of derivations not containing ω in their types.

Since, via Meyer-Scott axioms [Meyer 82, Barendegt 1984], the theory of β-conversion for λ-terms is first order axiomatizable, an alternative proof of the above result can be easily obtained also from Gödel completeness theorem and Theorem 4.13, observing that, by definition of realizability predicate, it is straightforward to check that:

⊧ r_{α}[M] ⟺⊧^{∧} M : α

where the symbol ⊧ to the left of the double implication denotes validity in first order models.

Since we can easily get also

CL_{β} ⊧ r_{α}[X] ⟺ CL_{β} ⊧^{∧} X : α,

semantic completeness for ⊢_{CL}^{∧} can be obtained in the same way by Gödel’s completeness theorem for ⊢_{LJ}^{CL_{β}} and Theorem 4.19.

Theorem 4.22

⊢_{CL}^{∧} X : α ⟺ CL_{β} ⊧_{CL}^{∧} X : α.

Let us remark, that, of course, there are other, more direct way of proving the semantic completeness for ⊢_{CL}^{∧}; for instance, standard semantical arguments allow to derive the completeness direction of 4.22 from 4.21, while soundness is established with a routine induction. Provable realizability, however, offers, beside a new proof, a different perspective into the result.

Some more consequences can be obtained, relating the validity of a type judgment X : α in all λ-algebras to the validity of the judgment X_{λ} : α in all λ-models, and similarly for the translation (−)_{H}, in the other direction.

Observe first that, similarly to 4.15, we can easily establish the following relation

⊢_{LJ} r_{α}[M] ⟺ ⊢_{LJ}^{CL_{β}} r_{α}[M_{H}].  (8)

Corollary 4.23

CL_{β} ⊧_{CL}^{∧} X : α ⟺ ⊧^{∧} X_{λ} : α

Proof:

CL_{β} ⊧_{CL}^{∧} X : α  ⊧^{∧} X_{λ} : α
Lemma 4.22  ⇕  ⇕  Lemma 4.21
⊢_{CL}^{∧} X : α  ⟺  ⊢^{∧} X_{λ} : α
Lemma 4.17

□

Corollary 4.24

CL_{β} ⊧_{CL}^{∧} M_{H} : α ⟺ ⊧^{∧} M : α.

Proof:

CL_{β} ⊧_{CL}^{∧} M_{H} : α  ⊧^{∧} M : α
Gödel’s completeness ⇕  ⇕ Lemma 4.21
⊢_{LJ}^{CL_{β}} r_{α}[M_{H}]  ⟺  ⊢_{LJ} r_{α}[M]  ⟺  ⊢^{∧} M : α
Relation (8)  Theorem 4.13

□

We conclude by pointing out that it is not difficult to modify the systems described above in order to take into account also the case of weak equality on CL-term instead of combinatory β-equality.

5 Relevant implication

Realizers of usual intuitionistic implicative formulas are (intensional representatives of) functions transforming proofs of the antecedent formula into proofs of the consequent. The intuitionistic implication can then be seen consistently as a function space constructor for which only very limited restrictions are given on the extensional behaviour of the functions belonging to it. In the spirit of the previous sections, however, it is natural to investigate if and how this notion can be restricted and still have a sound logical meaning. In this foundational study on the notion of implication, moreover, it is natural to investigate to what extent the restrictions affect the provability of implications. In other words, given a restricted function space, is it possible to characterize those implications that are realized by elements of that space? To begin tackling such a problem, one is naturally led to investigate the implication whose related function space is the simplest one, namely the one containing only the identity function.

Let us note, en passant, that here, as in Section 3, computer science motivations lurk in the background. In the context of typed functional languages with subtypes, the notion of a type A being a subtype of B is naturally formalized as a coercion from A into B, that is a (typed) program c : A → B whose type-erasure is convertible to the identity function.

The problem of characterizing the implicative formulas realized by such a restricted set of functions can be rightly posed and solved in the context of proof-functionality, where the realizability analysis for a restricted implication (→_{r}) having only the identity as realizer can be rephrased , as:

To assert α →_{r} β is to assert that any proof of α is also a proof of β.

The realizability predicate corresponding to this informal analysis is the following.

Definition 5.1 The realizability predicate for →_{r} is defined as

r_{A→_{r}B}[x] ≡ r_{A→B}[x] & x =_{β} λx.x

This proof-functional implication will be considered in a propositional language with strong conjunction, and we will show in Theorem 5.5 that it corresponds to the implication of Relevant Logic [Anderson & Belnap 75], from which the r subscript. This result not only supports and justifies the study of proof functional connectives, but shed also some light in the field of the logic of relevance, by showing a possible interpretation and formalization of what (some of) the mental processes involved in relevant reasoning look like.

The system of relevant logic we shall consider is a restriction of the system B^{+} of [Meyer & Routley 72a, Meyer & Routley 72b], obtained by removing the “Church constant” t.

Definition 5.2 (Meyer, Routley) The Minimal Relevant Logic without constants is defined as follows:

Language: The formulas of the language L_{r} are the propositional formulas built out of propositional variables using the connectives → and ∧.

Axioms: a1 A → A

a2 (A ∧ B) → A
a3 (A ∧ B) → B
a4 (A → B) ∧ (A → C) → (A → (B ∧ C)
Rules: modus ponens \frac{A A → B}{B}
adjunction \frac{A B}{A ∧ B}
suffixing \frac{A → B}{(B → C) → (A → C)}

prefixing \frac{B → C}{(A → B) → (A → C)}

We shall denote with T H_{r} the set of theorems of the Minimal Relevant Logic without constants. It is a very basic system, in which there is no weakening rule. As a consequence it is not possible to prove for this logic any form of the deduction theorem, which would allow to derive, from the adjunction rule, the formula A → B → (A ∧ B) and so the exportation law (exp) (A ∧ B → C) → (A → B → C).

Any formula of L_{r} can be equivalently read as a type of ⊢_{−ω}^{∧} and vice-versa (recall that ⊢_{−ω}^{∧} is ⊢^{∧} without the constant ω, its related ≤-rules, and axiom (Ax-ω)). In what follows we shall explicitly say if an expression has to be considered as a type of ⊢^{∧} or as a formula of L_{r} only when it is not clear from the context.

The reader will have already noticed the strong similarity between the axioms and rules of the minimal relevant logic and the clauses defining the relation ≤ among types of ⊢_{−ω}^{∧}. This informal similarity is formally stated in Proposition 5.4, which enables the study of the relevant implication in a proof-functional context, where we will be able to apply the completeness result of the previous section.

Lemma 5.3 Let M be a closed λ-term such that M =_{β} λx.x and α a type of ⊢_{−ω}^{∧}.

⊢^{∧} M : α ⇔ α ∼ ⋀_{i=1}^{n} γ_{i} → β_{i}, n ≥ 1 and, for all 1 ≤ i ≤ n,
γ_{i} ≤ β_{i} with γ_{i}, β_{i} types of ⊢_{−ω}^{∧}.

Proof: Since in ⊢^{∧} typability is preserved under β-conversion (Lemma 4.3), if ⊢^{∧} M : α we get that ⊢^{∧} λx.x : α. Since α does not contain ω, it follows that ⊢_{−ω}^{∧} λx.x : α. By induction on a derivation ⊢_{−ω}^{∧} λx.x : α we get now the required condition on α. □

Proposition 5.4 ([Venneri 92]) Let α and β be types of ⊢_{−ω}^{∧}.

(i) α ≤ β ⇒ α → β ∈ T H_{r}

(ii) α ∈ T H_{r} ⇒ α ∼ ⋀_{i=1}^{n} γ_{i} → β_{i}, n ≥ 1 and, for all 1 ≤ i ≤ n, γ_{i} ≤ β_{i}

With these two results and those of the previous section it is now easy to see that a formula α → β is in T H_{r} iff its realizers are convertible to the identity function.

Theorem 5.5 Let M be a closed λ-term s.t. M =_{β} λx.x and let α a formula of L_{r}. Then

⊢_{LJ} r_{α}[M] ⟺ α ∈ T H_{r}.

Proof: (⇐): By Proposition 5.4(ii) and Lemma 5.3, ⊢_{−ω}^{∧} M : α and hence ⊢^{∧} M : α. Then ⊢_{LJ} r_{α}[M], by completeness of provable realizability (Theorem 4.13). (⇒): By completeness of provable realizability, ⊢^{∧} M : α; By Lemma 5.3, α ∼ ⋀(γ_{i} → β_{i}), and γ_{i} ≤ β_{i} for 1 ≤ i ≤ n. By Proposition 5.4(i), γ_{i} → β_{i} ∈ T H_{r}, for any i. With n − 1 applications of the adjunction rule we obtain ⋀(γ_{i} → β_{i}) ∈ T H_{r} and hence ⋀(γ_{i} → β_{i}) → α ∈ T H_{r} by Proposition 5.4(i). Then α ∈ T H_{r} by modus ponens (recall that α ∼ β is α ≤ β and β ≤ α). □

Acknowledgments

References

[Anderson & Belnap 75] A. Anderson and N. Belnap, Entailment vol.I, Princeton University Press (1975).

[Alessi & Barbanera 91] F. Alessi and F. Barbanera, “Strong conjunction and intersection types,” in volume 520 of Lecture Notes in Computer Science, Springer Verlag, (1991).

[Barendegt 1984] H. Barendregt, The Lambda Calculus: its Syntax and Semantics, North Holland (1984).

[Barendregt et al. 83] H. Barendregt, M. Coppo and M. Dezani, “A filter lambda model and the completeness of type assignment,” The Journal of Symbolic Logic, Vol. 48, no.4 (1983), pp. 931-940.

[Bruce & Longo 85] K. Bruce and G. Longo, “Provable isomorphisms and domain equations in models of typed languages,” in ACM Symposium on Theory of Computing (STOC 85), Providence (May 1985), pp. .

[Bruce et al. 92] K. Bruce, R. Di Cosmo and G. Longo, “Provable isomorphisms of types,” Math. Struct. in Comp. Science, vol. 2, no. 2 (1992), 231–247.

[Coppo & Dezani 80] M. Coppo and M. Dezani, “An extension of basic functionality theory for lambda-calculus,” Notre Dame Journal of Formal Logic, Vol. 21, no. 4 (1980), pp. 685–693.

[Coppo et al. 82] M. Coppo, M. Dezani, F. Honsell and G. Longo, “Extended type structures and filter lambda models”, Proceedings of Logic Colloquium ’82, eds. G. Lolli, G. Longo, A. Marcja, 241-262. North-Holland. (1984).

[Curry & Feys 58] H.B. Curry, R. Feys. Combinatory Logic,. Vol. I. North Holland. (1958).

[Dezani & Hindley 89] M. Dezani, R. Hindley. “Intersection Types for Combinatory Logic”, Theoretical Computer Science, 100(1992), 303–324.

[Di Cosmo 91] R. Di Cosmo, “Provable isomorphisms of second order types,” Rapport de Recherche du Laboratoire d’Informatique de l’Ecole Normal Supérieure, Paris (1991).

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

[Kleene 52] S.C. Kleene, “Permutability of inferences in Gentzen’s calculi LK and LJ,” Memoirs of the American Mathematical Society, no. 10 (1952), pp. 1–26.

[Lopez-Escobar 85] E.G.K. Lopez-Escobar, “Proof functional connectives,” in volume 1130 of Lectures Notes in Mathematics (1985), Springer Verlag, pp. 208–221.

[Martini 92] S. Martini, “Provable isomorphisms, strong equivalence, and realizability,” Proceedings IV Conferenza Italiana di Informatica Teorica, M. Venturini-Zilli, A. Marchetti-Spaccamela eds., World Scientific Pub., 1992.

[Meyer 82] A. Meyer, “What is a model of the Lambda Calculus ?,” Information and Computation, Vol. 52 (1982).

[Meyer & Routley 72a] R.K. Meyer and R. Routley, “Algebraic analysis of entailment I,” Logique et Analyse, Vol. 15 (1972).

[Meyer & Routley 72b] R.K. Meyer and R. Routley, “Semantics of entailment III,” Journal of Philosophical Logic, Vol. 1 (1972).

[Mints 89] G.E. Mints, “The completeness of provable realizability,” Notre Dame Journal of Formal Logic, Vol. 30, no. 3 (1989), pp. 420–441.

[Mints 91] G.E. Mints, Personal communication, (1991).

[Pottinger 80] G. Pottinger, “A type assignment for the strongly normalizable λ-terms,” in To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, R. Hindley and J. Seldin eds., Academic Press (1980), pp. 561–577.

[Rittri 90] M. Rittri, “Using types as search keys in function libraries,” Journal of Functional Programming, vol. 1, no. 1 (1990).

[Takeuti 75] G. Takeuti, Proof Theory, North-Holland Publishing Company (1975).

[Venneri 92] B. Venneri, “Intersection types as logical formulas”, internal report dipartimento di Informatica Universita’ di Torino, submitted for publication, 1992.