Carnap’s remarks on Impredicative Definitions and the Genericity Theorem. ^{∗}

Thomas Fruchart

DMI Ecole Normale Supérieure 45 rue d’Ulm 75005 Paris, France fruchart@dmi.ens.fr

Giuseppe Longo

LIENS(CNRS) and DMI Ecole Normale Supérieure 45 rue d’Ulm 75005 Paris, France longo@dmi.ens.fr

December 5, 1996

Abstract

In a short, but relevant paper [Car31], Rudolf Carnap summarizes the logicist foundation of mathematics, largely following Frege and Russell’s view. Carnap moves away though from Russell’s approach on a crucial aspect: a detailed justification of impredicative definitions (a formal version of Russell’s “vicious circle”), that he accepts. In this note we revisit Carnap’s justification of impredicativity, within the frame of impredicative Type Theory. More precisely, we recall the treatment of impredicativity given in Girard’s System F and justify it by reference to a recent result, the Genericity Theorem in [LMS93], which may help to set on mathematical grounds Carnap’s informal remark. We then discuss the logical complexity of (the proof of) that theorem. Finally, the role of the Genericity Theorem in understanding the surprising “uniformities” of the consistency proof of Arithmetic, via System F, is hinted.

The problem

A definition is said to be impredicative, if it defines a concept in terms of a totality to which the concept belongs. Impredicative definitions, in general, use universal or existensial quantifiers over a variable that could be instanciated by the object being defined. For example, a set S is impredicatively defined, if, for some predicate P, possibly depending on X and y, one has S = {y/∀X.P(X, y)}, where the universally quantified variable X ranges over all sets, including the one which is being defined. Similarly, a predicate or a proposition is impredicatively given, if it contains a (quantified) variable which ranges on the collection of predicates or propositions.

∗to appear in Logic in Florence, 1995 (A. Cantini et al. eds), Kluwer, 1997

The “vicious circle” should be clear, as well as the problem it poses, in view also of its frequent use in mathematics (in Analysis in particular). We will discuss it in the frame of todays’ Type Theory, where “Types are Propositions” (that is, where Type Theory is seen as a constructive system of Logic, whose “formulae” are given by the types.)

Some History

In Russell’s view, a sound foundation of mathematics should not permit vicious circles nor other forms of reflexivity or self-reference, as these could lead to paradoxes. In particular, he claimed that “no whole may contain parts that are definable only in terms of the whole”.

The notion of impredicative definition, as considered here, was set on precise grounds also by Poincaré and Weyl ([Poi13], [Wey18]). The first observed as well that, thought doubtful, these definitions did not need to generate paradoxes. Both authors referred to this form of “circularity” in the framework of Set Theory. Weyl, in particular, was essentially interested in Analysis, in his 1918 book, and his contribution turns out today to be a anticipation of a long lasting and informative debate on whether predicative tools in Analysis (and other area of mathematics) suffice for the expressiveness of these topics (see the work of Kreisel, Wang, Feferman, Shutte, Simpson...; see, for example, [Kreis60], [Fefe64], [Fefe75], [Fefe88], [Lon87], [Lon93] for results, discussions and more references; Per Martin-Löf developped a predicative system of Intuitionistic Type Theory, [ML84]).

Carnap’s discussion on this matter begins by a criticism of Ramsey’s solution to the “vicious circle”. Ramsey’s solution to the problem of circularity is based on the usual platonist approach to mathematics: the totality of sets or properties already exists in itself, thus the possibility of defining one of them by reference to this totality is an empirical fact that nothing has to do with logic (see [Car31]). Carnap departs from the metaphysics (the absolutism, as he says) of platonic realms and proposes a constructive understanding of predicative definitions, inspired by the practice of mathematics.

Prototype Proofs

Consider first a universally quantified proposition of everyday mathematics, such as ∀xP(x), where x ranges on some intended collection of individuals (the reals, the complex numbers ...). This is a first order quantification. How do mathematicians prove a universal proposition of this kind? Assume, for instance, that in P(x), x is a real number variable. We seek to prove ∀xP(x), i.e. that for any real x, P(x) holds for this specific real. Any working mathematician would prove ∀xP(x) by saying: ≪ let x be an arbitrary or “generic” real number, then observe ...≫ and would write one single proof, valid for any particular real, as there is no way to inspect all reals, one by one. In other words, his/her core remark would be that the proof does not depend on the specific (and arbitrary) real chosen, but only on the assumption that x is a real number. In type-theoretic terms, a sound proof would only depend on the type of x, not on its value. Thus, if we want to prove P for a specific real, π say, we only need to replace everywhere in our proof, the “generic real” by the specific value, π. This is sound, as we used in the proof only properties that are verified by any real.

Herbrand called that kind of “uniform” proofs prototype:

≪... when we say that a theorem is true for all x, we mean that for each x individually it is possible to iterate its proof, which may just be considered a prototype of each individual proof.≫ (pp. 288-9, note 5 in [Gold87]).

Impredicatively given Sets and Propositions

Impredicativity explicitly shows up, though, when quantification is given over sets or predicates, not just individuals, as in the first order case: in this case the definiens may use the definiendum, which is a set or a predicate. That is, in order to deal formally with a “totality” of concepts or predicates or sets, one needs a second order language, namely a formalized language that may represent, internally, quantifications over collections of predicates or sets. Note that Analysis may be viewed as second order Arithmetic, since real numbers may be defined as sets of integers.

As already mentioned, the set S above is impredicatively defined, since, for some predicate P, one has S = {y/∀X.P(X, y)}, where y is an individualvariable and X is an set-variable (that is, X is intended to range over sets of individuals). Thus, S is a particular set and, if one wants to check wether a given a is in S, one needs to consider the property ∀XP(X, a), with X ranging over all sets. In particular, one has to handle the “circular” case P(S, a). One may then wonder if a proof of ∀XP(X, a) is still possible by the use of a “prototype proof” in the sense given above for first order sentences. In particular, one may wonder what it may mean exactly for an instance of variable X to be “generic”, in the second order case.

Carnap’s answer to the first question is a positive one. He gives a conceptual justification of this possibility:

≪ If we had to examine every single property, an unbreakable circle would indeed result. [...] But the verification of a universal logical or mathematical sentence does not consist in running through a series of individual cases. [...] The belief that we must run through all individual cases rests on a confusion of “numerical” generality. [...] We do not establish specific generalities by running through individual cases but by logically deriving certain properties from certain others. ≫ [Car31] In our example, assume that S is a set of integers. In order to check whether n is in S, one should logically derive P(X, n) from the only assumption that X has the property of “being a set of integers” (i.e. from an assumption on its type and nothing else); thus, we do not run throughout all sets of integers, including the one we are defining, but we just make a logical derivation based on the properties of the “type of the sets of integers”.

Carnap continues:

≪ That proofs that the defined property obtains (or does not obtain) in individual cases can be given shows that the definition is meaningful. If we reject the belief that it is necessary to run through individual cases and rather make it clear to ourselves that the complete verification of a statement means nothing more than its logical validity for an arbitrary property, we will come to the conclusion that impredicative definitions are logically admissible. ≫ [Car31]

Carnap claims that the fact that a proof may be (correctly and logically) given ≪shows that the definition is meaningful≫. In modern terms, this seems very close to the “realizability interpretation” in Intuitionistic Logic: according to the intuitionistic approach, that we follow in this paper, the meaning of a statement is given by the “set of its realizers” (that is, its possible or candidate proofs - if any, as this set may be empty), [Troe73]. This constructive understanding of logical systems is also related the so called BHK explanation of the intuistionistic meaning of the logical connectives (BHK stands for Brouwer-Heyting-Kolmogorov, [Troe73]). In both semantics, one constructively gives meaning to a statement, to a defined mathematical concept, by discussing its provability, as truth is provability. Carnap seems to claim that the possibility of an analysis of provability justifies “logical admissibility”. We share this opinion.

However, some technical questions need to be clarified. How can we be sure that the proof given is actually independent from the specific X used throughout the proof? How can we prove that from the given proof of a specific case, we can actually reconstruct uniformly a proof of the general case, that is of ∀X.P(X, a)? Or that X is truely generic and that the proof is a prototype, in the sense of Herbrand?

Mathematicians solve these questions, in the practice, by handwaving, experience and a common insight into proofs. This is perfectly sound in the first order case, where the stratification of individuals and predicates (or sets) poses no problem. It is a more delicate point in second order systems, when the issue of impredicativity actually raises.

Constructive logical systems, Type Theory in particular, by looking at proofs explicitly, as terms or computations, gives a precise answer to these questions, as a simple corollary of a (difficult) result. In our views, this may contribute to set on more solid grounds impredicatively given properties.

System Fc and Impredicativity

System F is known as Impredicative Type Theory, or Polymorphic Lambda Calculus; it was introduced by Girard, [Gir71] (see [GLT89] for a recent presentation). It consists of types and terms (well typed terms). One has to stress that the type system of F allows explicit quantification on type variables (second order quantification); its proof-theoretic strenght is such as to prove, by the normalization theorem, the consistency of (II order) Arithmetic. Let us first recall the syntax and rules for this calculus.

A type is either a type variable, an arrow type or a polymorphic type (one may add atomic types, when dealing with specific extension of the “pure theory” presented here; however, most key predicates for Logic and Computer Science are codable in the pure system, see [GLT89]). Types then are constructed using the following schemes:

• variables: X, Y ... are types.

• arrow types: τ → σ is a type, if σ and τ are types.

• universal types: ∀X.τ is a type, if τ is a type.

A term is either a variable, an abstraction, an application, a type abstraction, or a type application. Thus, terms are constructed using the following schemes:

• variables: x^{τ} of type τ, if τ is a type.

• abstraction: λx^{τ} .M of type τ → σ, if σ is the type of M (λ binds termvariables in terms, or x^{τ} is not free in λx^{τ} .M).

• application: MN of type σ, if M is of type τ → σ and N of type τ.

• type abstraction: ΛX.M of type ∀X.τ, if M is of type τ and X is not free in the type of any free term-variable of M (Λ binds type-variables in terms).

• type application: Mσ of type τ[σ/X], if M is of type ∀X.τ (where τ[σ/X] is the result of the replacement of all free occurrences of X by σ in τ.)

Reduction rules

(λx^{τ} .M)N \underrightarrow{β_{1}} M[N/x]  λx^{τ} .(Mx) \underrightarrow{η_{1}} M if x is not free in M
(ΛX.M)τ \underrightarrow{β_{2}} M[τ/X]  ΛX.(MX) \underrightarrow{η_{2}} M if X is not free in M

We will write ⟶^{F} for the reflexive and transitive closure of the union of these reductions, and =_{F} for the symetric closure of ⟶^{F}.

Second order quantification is explicitly given by the rule of type abstraction, which binds second order variables, both in types and terms. Thus, ∀X.τ is defined, as a type, by a quantification over the collection of all types, which includes ∀X.τ, the “definiendum”. Moreover, by virtue of the Curry-Howard isomorphism, polymorphic types can be viewed as second order logical propositions. Hence, a type of the form ∀X.τ “means” that the property τ is possessed by all types (in particular, by ∀X.τ itself). Finally, the terms of system F compute functions, either on terms (see the β_{1} axiom) or on types (see the β_{2} axiom). In particular, a polymorphic term takes types as inputs (including, possibly, its own type) and gives terms as outputs, by β_{2}. Here is then a the typical form of impredicativity, namely a type-theoretic formalization of the “vicious circle”. It even shows up at two levels, for types and for terms. However, exactly because of this constructive frame, where proofs are seen as computations (are coded by terms), it will be possible to look closely at the nature of “prototype proofs”. Indeed, we want to argue that these impredicative constructions are safe along the lines of Carnap’s argument, by showing that system F contains a precise notion of prototype proof, in the sense of Herbrand, and of generic types, with strong “coherence” properties.

Axiom C and its meaning

The key point of our analysis relies on the observation that all types in system F are “generic”, in the sense to be specified, and that, from a computational point of view, they act like variables. In short, in the constructive frame of second order Type Theory, outputs do not depend on inputs, when the input is a type: in this case, only the type of the output may depend on the input, not its “value” (see below). This is blatantly false for first order terms, in Type Theory or everywhere in mathematics: functions and computations do depend on inputs as first order individuals, as soon as a sufficiently expressive system is given.

This observation will be established in two steps. First, in this section, by a simple remark on the compatibility of an axiomatic extension of system F; later on, by the Genericity Theorem.

The first remark is inspired by a result in [Gir71]: in system F, there is no definable term that discriminates between types. That is, there is no term J_{σ} such that J_{σ} applied to type ρ is 1 if σ = ρ, and is 0 if σ ≠ ρ. In other words, there is no term whose output values are all in the same type (the type of integers, or any other type with at least two elements) and depend on the input type. This idea was taken up in [LMS93] by extending system F with the following axiom, some sort of a “generalized dual” of Girard’s result ^{1}:

1Independently of Girard’s remark, in [CMMS91] a similar extension was proposed, for the purposes of subtyping, a notion motivated by programming.

Axiom C: If M : ∀X.σ and X ∉ F V (σ) then for all τ, τ′, Mτ = Mτ′ : σ.

Axiom C intuitively means that an input type (τ), which is not used to establish the type (as σ does not depend on X) of the corresponding output value (Mτ), bears no information as input. So if M has the type ∀X.σ and X is not free in the type σ (i.e. σ is not a function of X), then it does not matter whether one applies M to τ or τ′ and one may consider both results to be equal. Equivalently, since there are no type discriminators by Girard’s remark, Axiom C forces terms of universally quantified type, whose outputs live in the same type, to be constant. Informally, this is sound, because we are in a constructive frame and types have the intended meaning of a possibly infinite domain of interpretation. Thus a term, as effective computation, cannot compare nor discriminate on the grounds of possibly infinite information.

We write F c for the extension of F by Axiom C. Axiom C is not derivable in system F. Indeed, let x : ∀X.σ and X ∉ F V (σ) then for any τ and τ′, xτ is a normal form, different from xτ′. However, Axiom C is formally compatible with F, as there are models of F c. As a matter of fact, all known and nontrivial models (e.g. not term-models nor models of Type:Type) realize Axiom C. In short, all “parametric” models of F, in the sense of Reynolds, [MR92], the coherent domains, [Gir86], and the PER models are all models of F c ^{2}. It is also possible to extend system F by a reduction relation which is strongly normalizing, Church-Rosser and induces exactly the F c-equality (which is thus decidable, [Bel97]).

The soundness of F c gives the first hint towards the “generic” nature of types as inputs, in system F. That is, we may consistently consider each type exactly as a variable, at least under the special circumstances that it is an input for a term M of type ∀X.σ, where X ∉ F V (σ)

The Genericity Theorem, Prototype Proofs, Generic Types.

In [LMS93], Axiom C was introduced in order to prove the Genericity Theorem below (note that there is no restriction on σ).

Theorem (Genericity). Let M and N have type ∀X.σ. Then:

(Exists τ, Mτ =_{F c} Nτ) ⟹ M =_{F c} N.

This theorem shows that two polymorphic terms that are equal on one input type are equal on any input type. In other words, the behaviour of polymorphic terms is so “uniform” that one can reduce F c equality on every possible types to F c equality on one single type τ (no matter which one!). That is, if (Mτ =_{F c} Nτ) then MX =_{F c} NX.

2The categorical significance of the PER models, i.e. the meaning of “quantification as product” as well as the meaning of Axiom C are both given by the validity in the Effective Topos of the Uniformity Principle, see [Lon87], [LM91], [Lon95].

For the purposes of our forthcoming application, observe that the Genericity Theorem in [LMS93] is actually shown by proving the following Main Lemma:

Let M and N have type σ. Then:

(Exists τ, [τ/X]M =_{F c} [τ/X]N) ⟹ M =_{F c} N.

With reference to very different matters, as an anology, one may remember the “regular behaviour” of analytic functions of complex variable: when known on the border of a regular shape, they are known everywhere inside. Thus, if two of these functions coincide on the border, they coincide everywhere [Rud80].

This regularity or uniformity could be surprising, and perhaps it is, but this is actually what makes second order impredicative Type Theory become safe (and allows the proof of the Normalization Theorem, see the last section).

Recall now that, if M is a polymorphic term, it can take as input any type, and in particular types that are more complex that its own type. One can then wonder what happens in these “circular” cases. The answer inspired by the Genericity theorem is: “It happens the same as on a simpler input type, because the computational behaviour of M “in extenso” is determined by its behaviour on a single type”. In this sense, the term or computation does not depend on the input type.

As shown in the next section, the proof of Genericity is (difficult but) “elementary”. More precisely, it is possible to code it into P RA (Primitive Recursive Arithmetic), provided that the Church-Rosser property for system F is assumed (but this is elementary and easy). Indeed, P RA is an elementary arithmetic theory, where one can handle basic mathematical computations and deductions. Thus, in spite of the circularity generated by polymorphism, a strong “regularity” property of terms in system F c is established by the Genericity Theorem and the proof of this regularity is elementary, i.e. logicaly complex reasonings are not necessary to deal with this key property of the impredicativity of F c.

According to the realizability or BHK interpretations, the constructive meaning of ∀X.σ, the crucial, impredicatively given type, is the following. A proofterm M: ∀X.σ is a computation or function that takes any type ρ to a proof Mρ: [ρ/X]σ. Thus, from a term M: ∀X.σ one can reconstruct the terms or proofs Mρ for each specific instance [ρ/X]σ of σ. However, as Carnap stresses, a proof of ∀X.σ is not constructed by running through all specific cases or input types ρ, but by giving a prototype proof, in the sense of Herbrand, w.r.t. a “generic” instance ρ. The most obvious prototype proof and generic case is given by MX: σ. However, this does not save us from the circularity of impredicativity, as variables in Type Theory have a double “status”: they are atomic entities (types in this case) but they also formally represent the mathematical use of “variable” as arbitrary elements of the intended domain of variation, since they may be instantiated by any element of that domain. Then, in particular, the variable X which may occur in σ can be instantiated by σ or even ∀X.σ.

Our thesis though, in view of the Genericity Theorem, is that an arbitrary specific instance type, possibly simpler than σ, may suffice to determine a fully general proof. The idea then is to start from a specific instance [ρ/X]σ and discuss the prototype nature of its proof, if any. In a sense we want to describe the backwards process, w.r.t. the one described above, as we want to go from a proof of [ρ/X]σ to one of ∀X.σ.

Assume then that from a proof N of an instance [ρ/X]σ one tries to reconstruct a proof of the universal proposition ∀X.σ. In general, this may not be possible. It is possible, though, when the structure of a specific proof N of [ρ/X]σ, that is of N: [ρ/X]σ, is “parametric” in ρ or it may be described uniformely as a substitution of a type variable by ρ. In that case, we call N a prototype proof, in the sense of Herbrand. This is formalized by the following definition:

Definition. Given a type σ, we say that a type ρ is generic and a proof N: [ρ/X]σ is a prototype if there exists M: σ, such that X is not free in the type of a free term variable of M and

[ρ/X]M =_{F c} N: [ρ/X]σ.

Notice that if ρ and a proof N: [ρ/X]σ are, respectively, generic and prototype, by M: σ, then ΛX.M: ∀X.σ. That is, the construction (existence) of M, from the prototype and generic proof and type N and ρ, allows to give a proof of the universal statement. As the converse is trivial, given a type, there exist a generic and prototype type and proof if and only if the corresponding universal statement is provable. Clearly, not any proof nor type of a specific instanciated type need be prototype and generic: for example, [ρ/X]X has no prototype proof with ρ generic, otherwise the universal statement ∀X.X, the absurdum or empty type, would be provable. We claim that, given N,σ and ρ, it is decidable whether N is a prototype proof with ρ generic (ongoing work).

We focused on a second order notion of prototype proof and generic type. Of course, the definition can be easily extended to first order statements, the more usual ground of “prototype” proofs in mathematics: if r is an arbitrary real and the proof of P (r) = [r/x]P does not depend on r (or r is generic and the proof is a prototype similarly as in the definition above), any mathematician would say that we actually proved ∀x.P (x). However, as already mentioned, the first order case is not problematic at all: individuals are distinct from propositions and there is no apparent vicious circle. This is not so in the impredicative case, which motivates the doubts of many in the use of impredicative second order quantifications (and variables). Thus, the very simple notions of generic types and prototype proof turn out to be a more delicate issue in impredicative systems.

However, exactly because of the relevant property of System F given by the Genericity Theorem, we are now able to assure that prototype proofs are sound, also when the generic type may be as complex as the universal assertion to be proved. The soundness is given, as in Category Theory, by a “coherence result”, which states the independence of the reconstruction of the proof of the universal statement from specific prototype proof and generic types.

Corollary (Coherence). Given a type σ, let ρ and a proof N: [ρ/X]σ be generic and prototype, respectively. Then, if [ρ/X]M =_{F c} N =_{F c} [ρ/X]M′: [ρ/X]σ, one has M =_{F c} M′ and, thus, ΛX.M =_{F c} ΛX.M′: ∀X.σ.

This immediate corollary to the Genericity Theorem says that no matter how we extract a proof of a universal statement from a prototype one of a specific instance, in any case we obtain just one proof (modulo “=_{F c}”). Thus, also the type ρ does not matter, or it is truely generic, since from the unique proof ΛX.M of ∀X.σ we can obtain, uniformely and effectively, proofs for each instance [ρ′/X]σ, just by application (ΛX.M)ρ′.

The independence of the proof of the universal statement from the specific “structure” of a proof of a specific instance, as well as from the generic type used, garanties that, exactly in the “shaky” second order case, the mathematical soundness of those statements. The system is “coherent” both in the categoricaltechnical sense, and in the sense of the possibility of disregarding the complexity of the instantiating type, since all types are generic and act like variables.

As already mentioned, this garanty is given “exactly” in the critical second order case, as the (obvious variant of the) Genericity Theorem is clearly (and fortunately) false in the first order case.

The proof of Genericity Theorem in P RA.

So far we tried to justify the “non-elementary” tools of impredicativity by an application of the Genericity Theorem. We next show that the proof of the Genericity Theorem is elementary. Our goal is to focus here on the main points that allow to encode the Genericity Theorem into Primitive Recursive Arithmetic (P RA) without many detail, since the complete coding would be very long (and not very interesting). Hence, we first recall the basics of P RA, then we explain how to code types, terms, and properties of system F into P RA, and finally how to code the Genericity proof into P RA.

Primitive Recursive Arithmetic

The language of this theory contains one function letter for each primitive recursive function, and one predicate letter for each primitive recursive predicate. The axioms of P RA are the (usual) equality axioms, the definitional axioms— that define the behaviour of primitive recursive functions letters (resp predicates letters) as expected— and the induction axiom:

P(0) ∧ ∀x(P(x) → P(Sx)) → P(y)

where P is quantifier free, and Sx stands for the successor of x.

In P RA, one may express the usual mathematical reasonings. Some difficult theorems can be proved in this theory (Gödel first incompleteness theorem, for instance). The core of its expressive power is the induction axiom.

This axiom defines primitive recursive induction, that is induction on ω. More complex forms of induction (like induction on ω^{2}, used to prove the totality of the Ackerman function) are not possible in P RA. In what follows, we sketch the proof that induction on ω suffices for coding and proving the Genericity Theorem in P RA. For more details see [Fru96].

Coding F into P RA

Types and terms of F will be coded by integers, type assignment by a function letter, reductions by predicate letters, and finally equalities by formulas of P RA. This coding is rather long, so we just mention here the key points.

We first define the code of types and terms of system F by induction respectively on types and terms. We will write ^{†}M^{†} for the code of M, and < a_{0}, …, a_{n−1} > for the integer 2^{a_{0}+1} × ⋯ × p_{n}^{a_{n−1}+1}, where p_{n} stands for the n^{st} prime number:

T ypes  T erms
†t_{1} t_{2} ^{†} = < 3,^{†}t_{1} ^{†},^{†}t_{2} ^{†} >
†∀X_{i}.T ^{†} = < 5,^{†}X_{i} ^{†},^{†}T ^{†} > ^{†}λx_{i}^{τ} . t^{†} = < 7,^{†}x_{i}^{τ} ^{†},^{†}t^{†} >
†T_{1} → T_{2} ^{†} = < 9,^{†}T_{1} ^{†},^{†}T_{2} ^{†} >  ^{†}t.T ^{†} = < 11,^{†}t^{†},^{†}T ^{†} >
†X_{i} ^{†} = 13 + 4i  ^{†}ΛX_{i}.t^{†} = < 15,^{†}X_{i} ^{†},^{†}t^{†} >
†x_{i}^{τ} ^{†} = 19 + 4 < i,^{†}τ^{†} >

Both coding and decoding are primitive recursive. Hence this allows to define functions and predicates by induction on the code of types (respectively terms). Since codes are integers, those inductions are usual “course of value” inductions, i.e, ordinary primitive recursive inductions.

For instance, one may define the (primitive recursive) predicates T ype(n) and T erm(n) which mean respectively “n is the code of a type of F ”, and “n is the code of a (well typed) term of F ”, by course of value induction on ω.

The main function, that is also defined in this way, associates the code of its type to each code of a well typed term. This function is called typing, and its definition codes formally the following property:

typing(^{†}M^{†}) = ^{†}T_{2} ^{†} if M ≡ t_{1}t_{2}, t_{2} : T_{1}, and t_{1} : T_{1} → T_{2}

†T_{1} → T_{2} ^{†} if M ≡ λx^{T_{1}}.t, and t : T_{2} †T_{1}[T_{2}/X]^{†} if M ≡ t.T_{2}, and t : ∀X.T_{1} †∀X_{i}.T ^{†} if M ≡ ΛX_{i}.t, and t : T , and X_{i} is not free in the type of a free term variable of t †τ^{†} if M ≡ x^{τ} 0 else

F cEqual is the main predicate used in the proof of the Genericity Theorem in P RA. It is not a predicate letter of P RA, but it is defined directly by the use of the primitive recursive predicate letter F cEqualproof such that:

F cEqualproof(a, b, c) means “c is the code of an F c equality proof between both terms coded respectively by a and b”.

The definition of F cEqualproof is complex, and requires in particular the coding of F reductions (β_{1}, β_{2}, η_{1}, and η_{2}), which would be too long to present here in detail. Thus, we just mention the possibility of coding F c equality, M =_{F c} N with the predicates F cEqual:

F cEqual(^{†}M^{†},^{†}N^{†}) ≡ ∃c F cEqualproof(^{†}M^{†},^{†}N^{†}, c)

By this coding, one can express the Genericity Theorem by the following formula of P RA:

T ype(σ) ∧ (typing(^{†}M^{†}) = ^{†}∀X_{0}.σ^{†}) ∧ (typing(^{†}N^{†}) = ^{†}∀X_{0}.σ^{†})∧
(∃τ(T ype(τ) ∧ F cEqual(^{†}Mτ^{†},^{†}Nτ^{†}))
⇓
F cEqual(^{†}M^{†},^{†}N^{†})

Now we know how to code the Genericity Theorem by a formula of P RA, we have to find how to code its proof.

Structure of the proof

The proof of the Genericity Theorem is rather long, and divided in several lemmas. As it would be extraordinarily tiresome to code the proof lemma after lemma, and line after line, we just point out the main arguments that are used in the proof, and we explain how they can be coded by deductions in P RA.

In what follows, we will not consider the basic logical reasonings (that can be coded easily), but, first the main direct arguments used for proving a “type generalization” lemma, and then the inductive arguments.

Direct arguments (no induction)

As a matter of fact, the Genericity Theorem deals with type substitution: actually, a (trivially) equivalent wording for it (we just apply a β_{2} reduction) is the following (formulated as the Main Lemma in [LMS93]):

M, N : σ ∧ [τ/X]M =_{F c} [τ/X]N ⟹ M =_{F c} N

Thus, the use of type-substitution properties in the Genericity proof is absolutely not surprising. The most important properties of type substitution are called “type generalization”, and “term generalization”. We focus here on the first one that deals with type substitution in types themselves (Lemma 5.1 in [LMS93]):

If σ_{1} and σ_{2} are two types such that σ_{1}[τ/X] ≡ σ_{2}[ρ/Y], then exists
σ_{0} (type generalizer of σ_{1} and σ_{2}) such that, for suitable μ_{1} and μ_{2}:
σ_{0}[μ_{1}/Z] ≡ σ_{1}, σ_{0}[μ_{2}/Z] ≡ σ_{2}

The proof of this lemma is based on the notion of occurrence.

Occurrences are usually defined by induction on the structure of terms. We can here code this notion with integers, by the use of a (primitive recursive) induction on codes of terms, and then code the following notions by induction on the codes of occurrences:

• substitution at an occurrence: σ[u ← τ] is the result of the substitution of τ at the occurrence u.

• subterm (σ_{|u}) taken (from σ) at the occurrence (u).

Since all those notions are defined by primitive recursive induction, it is possible to prove the following properties, also by primitive recursive induction (on the occurrences):

σ[u ← σ_{|u}] = σ
(σ[u ← X])[Y/X] = σ[u ← Y] for X ∉ V ar(σ)

Now, these properties are essentially sufficient to prove Lemma 5.1. Other arguments that are also used in this proofs are not inductive, (propositional reasoning, case analysis) and easy to formulate by the corresponding deduction in P RA.

Although induction is not explicitly used in the proof of Lemma 5.1 above, the easiest way to formalize it in the frame of P RA is based on induction, as induction is the key tool in P RA and the notion of occurrence is given inductively.

Coding inductions

Different kinds of inductions are used in the proof of Genericity: inductions on types, on terms, on type derivation, on the length of an equalities (or reduction) chain, and on the number of C-equalities in chains of F c-equalities .

Since types, terms, and chains are coded by integers, one may code inductions on them by inductions on integers. This does not present any problem as the code of a truncated type (resp. term, chain) is strictly less than the code of the original type (resp. term, chain).

As for induction on type derivations, proving P(M) by such an induction is a “pleasant way” of proving T erm(M) → P(M) by induction on terms, (T erm is the predicate letter that codes the fact that its argument is a well typed term of F).

In short, the coding of induction is relatively straightforward, because all inductions used in the Genericity proof are primitive recursive, hence codable into P RA.

Conclusion

The Church-Rosser property (CR) for system F is the only non logical assumption in the proof of the Genericity Theorem ^{3}: If M ⟶^{F} M_{1} and M ⟶^{F} M_{2}, then exists M_{0} such that:

M_{1}  M_{2}
↘^{F}  ↙_{F}
M_{0}

This property is not more difficult to establish for system F than for the typefree λ-calculus. Hence, the Genericity Theorem is based on a (elementary) property of system F and its proof can be given in P RA. In this sense, one can say that Genericity Theorem is elementary.

Second order arithmetic (P A_{2})

System F verifies the strong normalisation property: all terms of F have a normal form (i.e: are F -equal to an irreducible term). From a logical point of view, the strong normalisation theorem for system F implies the consistency of second order arithmetic, P A_{2}, and — in virtue of Gödel’s second incompleteness theorem — it can not be proved within P A_{2}. As we will see, the strength and main difficulties of the proof of this theorem are due to the presence of polymorphism, and are related to impredicativity.

The proof of F normalisation is due to Girard, who adapted Tait’s notion of reducibility [GLT89][Tait67]. At first trial, an intuitive notion of reducibility for F terms could be the following:

≪We would like to say that t of type ∀X.τ is reducible iff for all types σ, tσ is reducible (of type τ[σ/X]). […] But σ is arbitrary—it may be ∀X.τ—and we need to know the meaning of reducibility of type σ before we can define it! We shall never get anywhere like this.≫ [GLT89, p. 115]

As a matter of fact, the impredicativity of F creates logical difficulties. The key idea that makes the proof possible is based on the notion of reducibility with parameters. The parameter is called “reducibility candidate”, and it is taken as a temporary definition of reducibility on some types, to break the “circle” discribed in the citation above. The point is that no matter which collection of candidates is chosen, its use as a (type) parameter does not affect the computation (nor the proof).

3CR is used in several places in [LMS93]. As a matter of fact, in the proof of Theorem 6.2, there is a reference to Strong Normalization. However, this reference, which is just a shortpath to the proof, may be easily replaced by a simple application of CR (see [Fru96]).

≪A term t of type ∀X.τ is reducible when, for every type σ and every reducibility candidate R of type σ, the term tσ is reducible of type τ[σ/X], where reducibility for this type is defined taking R as the definition of reducibility for σ. Of course, if R is the “true” reducibility of type σ, then the definition we shall be using for τ[σ/X] will also be the “true” one. In other words, everything works as if the rule of universal abstraction (which forms functions defined for arbitrary types) were so uniform that it operates without any information at all about its arguments.≫ [GLT89, p. 115]

The main definitions (and properties) that are necessary for the proof of F normalisation use implicitely the essential feature of F, that is informally described above: the regularity of polymorphic terms behaviour. Since this “uniformity” allows the (difficult) proof of strong normalisation, it is then at the core of this consistency proof of P A_{2}.

In conclusion, one can now consider the Genericity theorem as a (partial) formalisation of this feature. The regularity of the universal abstraction rule, that operates ≪without any information at all about its argument≫ corresponds in our views, to the fact that any type is generic is the sense described above. One can then wonder about a possible use of the Genericity Theorem for a better understanding of the “mysteries” of the consistency proof of Arithmetic. This issue is part of our current research project.

Aknowledgement

We would like to thank Sergei Soloviev for his detailed comments to this paper. Longo would also like to thank Sergei for the long lasting stimulating collaboration in Type Theory and for the many discussions on key issues in Logic and the foundation of Mathematics.

References

[Bel97] G. Bellè. Syntactical properties of an extension of Girard’s System F where types can be taken as “generic” inputs. Preliminary note, DISI - Università di Genova. E-mail: gbelle@disi.unige.it.

[Car31] R. Carnap. The logicist foundation of mathematics, in P. Benacerraf, H. Putnam, Philosophy of mathematics; selected readings, Prentice-Hall philosophy series, 1964.

[CMMS91] L. Cardelli, S. Martini, J.C. Mitchell, and A. Scedrov. An extension of system F with subtyping. Information and Computation 94, pages 4–56, 1994. First appeared in the proceedings of the Conference on Theoretical Aspects of Computer Software (Sendai, Japan), T. Ito and R. Meyer, eds., Lecture Notes in Computer Science 526, pages 750–770, Springer-Verlag, 1991.

[Fefe64] S. Feferman. Systems of predicative Analysis, Journal of Symbolic Logic vol. 29, pages 1–30, 1964.

[Fefe75] S. Feferman. A language and axioms for explicit mathematics, in Lecture Notes in Mathematics 450, Springer-Verlag, pages 87–139, 1975.

[Fefe88] S. Feferman. Weyl vindicated: “Das Kontinuum” 70 years later, Proceedings of the Cesena Conference in Logic and Philosophy of Science, 1988.

[Fru96] T. Fruchart. Normalisation et Généricité dans le système F, rapport de stage de DEA. Available on author’s Home page: http://www.ens.fr/∼fruchart/publi.html.

[Gir71] J.-Y. Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. Proceedings of the 2nd Scandinavian Logic Symposium, J.E. Fenstad, ed., pages 63–92, North-Holland, 1971.

[Gir86] J.-Y. Girard. The system F of variable types, fifteen years later, Theoretical Computer Science, vol 45, pages 159–192.

[GLT89] J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and types. Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press, 1989.

[Gold87] H. Goldfarb, Jacques Herbrand: logical writings, 1987.

[Kreis60] G. Kreisel. La prédicativité, in Bulletin de la Société Mathématique Française, vol. 88, pages 371–391, 1960.

[Lon87] G. Longo. Some aspects of impredicativity: notes on Weyl’s philosophy of Mathematics and on todays Type Theory, Logical Colloquium 87, Studies in Logic (Ebbinghaus et al. eds), North Holland, 1989.

[Lon93] G. Longo. Review of Feferman’s paper “Weyl vindicated, Das Continuum 70 years later”, Journal of Symbolic Logic, vol 58, n. 3, 1993.

[Lon95] G. Longo. Parametric and type-dependent polymorphism. Fundamenta Informaticae, 22(1-2):69–92, 1995.

[LM91] G. Longo and E. Moggi. Constructive natural deduction and its ω-set interpretation. Mathematical Structures in Computer Science vol. 1, pages 215–253, 1991.

[LMS93] G. Longo, K. Milsted, and S. Soloviev. The Genericity Theorem and the notion of parametricity in the polymorphic λ-calculus. Theoretical Computer Science 121, pages 323–349, 1993.

[MR92] Q. Ma and J.C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. Proceedings of the Conference on Mathematical Foundations of Programming Semantics, S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, eds., Lecture Notes in Computer Science 598, pages 1–40, Springer-Verlag, 1992.

[ML84] P. Martin-Löf Intuitionistic Type Theory, Bibliopolis, Napoli, 1984.

[Poi13] H. Poincaré. Dernières pensées, english edition, Dover publ., New York 1963.

[Rud80] F. Rudin. Real and Complex Analysis, MacGraw Hill, 1980.

[Tait67] W.W. Tait. Intensional interpretation of functionals of finite type I, Journal of Symbolic Logic 32, 1967.

[Troe73] A. Troelstra. Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics 344, Springer Verlag, 1973.

[Wey18] H. Weyl. Das Kontinuum, italian edition, care of B. Veit, Bibliopolis, Napoli, 1977.