Polymorphic Identity

Languages

PI is formulated in the predicative calculus of constructions (PCC), a pure type system. The principles here need only a fragment of it, in which every variable ranges over types or over the terms of a type. Their derivations and models are given for that fragment, and it is proved in Lean that, with a few exceptions described below, the results hold in PCC as a whole; the details shown for each principle say how its result carries over. The switch under the menu compares PCC with the simply typed lambda calculus, which has no type variables at all (see the last section). This page says what PCC is, what the fragment is, how its results carry over to PCC, and how PCC compares with the simply typed lambda calculus.

Pure type systems

A pure type system is specified by three sets: a set of sorts; a set of axioms, each of the form with ; and a set of rules, each a triple of sorts. Its expressions, called pseudo-terms, are built from variables, constants and sorts by application , abstraction and product . A context is a list of declarations . The typing judgment , read “in , has category ”, is generated by the following rules, where means that and can be converted into one another by β-reduction, .

Here range over sorts. In each rule that extends with , is a variable not already declared in ; and replaces the free occurrences of in by , changing the names of bound variables where needed so that no variable free in becomes bound. The product rule is what distinguishes one pure type system from another: a product exists, with sort , just in case has a sort and has a sort with . When does not occur in , is written .

The best-known pure type systems form the λ-cube. Each has the sorts and and the axiom ; read as the sort of types and as the sort of kinds. With the rule alone, which gives function types between types, the result is the simply typed lambda calculus. Adding , which gives types such as that quantify over types, yields System F (Girard 1972); with and as well, which give type operators and types that depend on terms, the result is the calculus of constructions (Coquand and Huet 1988).

The predicative calculus of constructions (PCC)

PCC has the sorts and , the axiom , and the rules

It differs from the calculus of constructions in one rule: in place of it has . So a product over types, such as , has the sort rather than : it is not itself a type. A type variable can be replaced only by something of category , and so only by a type, never by a category such as . That is the sense in which the calculus is predicative: its type quantifiers range over the types, and the categories of polymorphic terms are not among the types.

Three sorts of category matter here. A type is a term of category : (entities), (propositions), type variables, and the types built from these, such as ; in PCC also types such as , for a type operator , and and , for a family of types . A kind is or a product built from it, such as or . A polymorphic category is any other category of sort , such as , or ; the terms of the first two apply to types, and those of the third apply to polymorphic terms. The constants of PCC, and their categories, are these.

As usual, is short for , and is short for .

The fragment

The principles here need only part of PCC: the fragment in which every variable is either a type variable, such as , or a variable for the terms of a type, such as . Its types are built from , and type variables by . Polymorphic expressions still occur, as abstractions over types: for instance the type predicate , of category , and the polymorphic predicate , of category ; the constants and apply to such expressions, and , , and are themselves polymorphic: they apply to types. But no variable ranges over them, nor over type operators or families of types. Every principle on this site is a sentence of the fragment, or a schema whose instances are, and the derivations, models and Lean proofs here are for the fragment. Below, "the full calculus" means PCC as a whole.

In the fragment, PI⁻ has these axioms and rules: every instance of a tautology of classical propositional logic; instantiation and distribution, and the definition of the existential quantifier, for and , with instances given by terms whose category is a type (substituted so that none of their free variables becomes bound), and with distribution requiring the quantified variable not to be free in the antecedent; the same for and , with instances given by types, and with distribution requiring the type variable not to be free in the antecedent, nor in the type of any term variable free there; β-conversion; Ref≡, Sym≡, Trans≡ and Ref≈; LL≈ for every term of category in which the two quantified type variables are not free; modus ponens; generalization over a variable of a type; and generalization over a type variable , provided is not free in the type of any term variable free in the formula; and the structural rules, which rename the variables of a context (weakening, exchange, contraction) and drop from a context a variable that no longer occurs. PI adds LL≡, and PIC adds Classicism. In the full calculus the axioms and rules are the same, but the schemas (LL≈, Classicism, LL×, LL≈/≡, DLF and the Barcan schemas for types) have further instances, built from the new variables. There is β-conversion but no η: η holds in the standard, worlds, tagged, algebraic and Kripke models, but fails in 𝔐_if, where a function and are distinct functions; so PI does not prove η.

From the fragment to the full calculus

A derivation in the fragment is a derivation in the full calculus, so whatever follows in the fragment follows there too. The converse is the substantial part, and it is proved in Lean: from any set of sentences of the fragment, together with any of the schemas Classicism, LL≈/≡, LL×, Booleanism, TBF and TCBF (each with all its instances in the full calculus), PI⁻ and PI in the full calculus derive a formula of the fragment just in case PI⁻ and PI in the fragment do. So the two agree about what follows, what is consistent with what, and what is independent of what. The proof first erases every dependence of a type on a term (each type becomes , and each dependent product a function type), which takes each derivation in the full calculus to one in which no type depends on a term; it then evaluates each formula, reading type operators as functions on types, to a normal form in the fragment, and the normal form of each instance of a schema is an instance of the same schema. The proofs need the Church–Rosser theorem for the full calculus, which is proved too.

One rule of the full calculus needs care. A variable may be dropped from a context, once it no longer occurs, only if its category is a type or . Without that restriction, a variable of category , which chooses a member of every type, would let PI prove a choice principle: if certain sets of entities, one for each type in a family, are disjoint, then some property of entities picks exactly one member from each. That is a sentence of the fragment which the fragment does not prove; it fails in a permutation model, of the kind Fraenkel and Mostowski used to show that the axiom of choice does not follow from the other axioms of set theory.

What does not carry over. In the Lean proofs, Classicism is taken in the form that identifies the propositions φ and ψ as well as the properties λy.φ and λy.ψ. Given LL≡ the two forms are equivalent, which is proved in Lean; without LL≡ the first is stronger, since it yields every instance of Booleanism. DLF is not among the schemas covered, and in the full calculus it has new instances. The negation of a schema is not covered either, since it is not a set of sentences. So the following are established for the fragment only: any result that assumes the negation of a schema; any result that something fails to follow from, or is consistent with, a selection that includes DLF, or that includes Classicism over PI⁻ without LL≡; and any result that DLF, or Classicism over PI⁻ without LL≡, is consistent with a selection or follows from it. Everything else carries over: a derivation from assumed principles is a derivation in the full calculus, and an instance of DLF or of Classicism that does not follow in the fragment does not follow in the full calculus either. The details shown for each principle say when a result is established for the fragment only.

Full models

The results here concern what PI proves, and full models of the full calculus can make more true. In a full model each category denotes the set of all functions of the relevant sort, so a variable of category ranges over every function from types to truth values, including one which is true of a single type. LL≈ must hold for that value of too; so in every full model of the full calculus, ≈ is identity of types, and Inj≈ and Recovery are true. But PI does not prove them: in 𝔐_δ, for instance, while and are distinct. In the fragment none of this arises, since no variable has the category .

Infinite types are similar. In the full calculus a type may depend on a term: if , then is a type. So the types of a full model must be closed under products of families of types indexed by the members of a type, and a full model of the full calculus with an infinite type exists just in case there is a strongly inaccessible cardinal. In the fragment the types need only be closed under forming sets of functions, and models with infinite types need no large cardinal (see “Infinite types” under Other results, in the All results tab). Nor does consistency: since the full calculus derives the same formulas of the fragment, PI with infinitely many entities is consistent in the full calculus too, without any large cardinal.

The simply typed lambda calculus

The natural alternative to all of this is the simply typed lambda calculus with an identity predicate for each pair of types; call it STLC. Its types are , and . It has the logical constants at every type and, for each two types and , a constant of type . It has no type variables, no quantifiers over types, and no ≈. Its sentences can be evaluated in the models here: a type denotes the set it names, and is true just in case is. Say that a set of STLC sentences expresses a principle over a class of models when, in each model in the class, the sentences are all true just in case the principle is; and that the principle is simply typed over the class when some set of STLC sentences expresses it there.

Which models. Whether a principle is simply typed depends on the class of models, and three classes matter here. (1) The standard models of PI whose types are all named. A standard model has the types e and t and the function types built from them, but it may have further types as well: base types besides e and t, such as the type X in some of the models below. Call a type named when some simple type, such as e, t, or (e→t)→t, denotes it. In a model whose types are all named, a statement about every type can be replaced by its instances at the simple types, which are STLC sentences; so this is the class most favourable to STLC. (2) All standard models of PI. Here a model may have types that no simple type names, and an STLC sentence says nothing about them: two models that differ only at such a type make the same STLC sentences true. (3) All models of PI, standard or not. In a standard model the propositions are the two truth values; in the models with worlds and in the algebraic models they are finer, and so principles that hold in every standard model can fail. The Models switch, shown when the Simply Typed Lambda Calculus is chosen, picks one of these classes: Every type named, All standard models, or All models.

Everything STLC can say, the fragment can say too. Each STLC sentence translates into a sentence of the fragment with the same truth value in every model: becomes , and the rest stays as it is. So a principle that is simply typed over a class of models is also expressed there by sentences of the fragment.

The converse fails. Over the models of PI, Poly Cross is not simply typed, and neither is its negation. Poly Cross speaks of every type, including types which no simple type names. Take a model with one further type , in which each member of each type is identified with its haecceity, so that Poly Cross is true; then cut the members of off from everything else, so that Poly Cross is false. The two models agree at every simple type, so every STLC sentence has the same truth value in both.

Unnamed types are not the only obstacle. Over the models of PI whose types are built from one entity and the truth values, so that every type is named by a simple type, Poly Cross is still not simply typed. In , each member is identified with the -th member of its chain of haecceities, so Poly Cross is true; in 𝔐(∼₀), E = 1, nothing is identified across types, so Poly Cross is false. But an STLC sentence uses = at only finitely many types, and once exceeds their sizes, and agree at all of them. So a set of STLC sentences true in every is true in 𝔐(∼₀), E = 1, as well, and cannot express Poly Cross. The obstacle is the shape of Poly Cross: each member must have a partner at some other type, and no finite stock of types serves for every model.

The same holds for principles with polymorphic constants. Give STLC a constant , of type , for each type . Physicalism, , says that everything is identical to something physical, of some type. Over the models of PI, with interpreted in any way, neither Physicalism nor its negation is simply typed; and even when every type is named, Physicalism is not simply typed, since the physical things can sit at types larger than any given sentence mentions. The same goes, for each , for FC_n, the principle that everything is identical to a purely logical function of fundamental things, , where is and and are polymorphic constants for being purely logical and being fundamental. With no fundamental things (), FC₀ is simply typed over the models in which every type is named.

Every principle here has been classified in this way, over all standard models of PI and over those whose types are all named; choose the Simply Typed Lambda Calculus in the language switch to see each verdict, with its Lean proofs. In a standard model of PI, identity within a type is sameness, so propositions are truth values: 32 of the principles hold in every such model, and DLF in none, so these are simply typed trivially. Frege, Hae, Bundle, Vacuous, Cong×, Partial Cong, Partial Ext, Ext×, Ext×⁺, SingId and Graph× are simply typed over the models whose types are all named, since each is a universal statement about types whose instances are STLC sentences; but none of them is simply typed over all models. Disjoint, LL×, Poly Cross, Inj≈, Recovery, Ext≈ and Int≈ are not simply typed even over the models whose types are all named: all of them but Poly Cross concern ≈, which STLC cannot see. Nor is the negation of any of these principles simply typed, even over the models whose types are all named. For the eleven listed first, models in which the principle fails agree, at every type up to any given size, with a model in which it holds, so a set of STLC sentences true in all of them is true in that model too; for the rest, two named models with the same identities between terms but different identities between types give the negation different truth values.

Twelve further principles concern how ≡ relates the types. Write for . Ascent (every type is properly included in some type), ObjProp (every entity is identical to a property of some type), Monism, Unit, QAtom, Directed (any two types are included in a common type), Pairing and CumSucc each ask for something at some type or other; none of them is simply typed, even over the models whose types are all named, since models that agree with 𝔐(∼₀), E = 1 at larger and larger types make them true while they are false there. Nor are their negations, except that of QAtom, which says that nothing is identical to its own haecceity and is expressed by its instances. Univ≈ concerns ≈, and is not simply typed either. Cumulation and Linear are universal statements about types, expressed by their instances over the named models, and Closure holds in every named model; none of these three is simply typed over all models.

All of these classes contain only standard models, in which propositions are truth values; that is why 33 of the first 51 principles have the same truth value in every model there, and are simply typed trivially. Models with worlds change this. Over the models of PI in which propositions are sets of worlds and every type is named, NI≈, ND≈, Type Necessitism and Classicism are not simply typed, and nor are their negations: 𝔐_w, 𝔐_ni and 𝔐_nd have one universe and one identity of terms, and differ only in which types are identified at the second world, so every STLC sentence, which has no ≈, has the same truth value in all three, while these principles do not. A model with worlds that has only one world is a standard model, so a principle stated by a sentence which is not simply typed over the standard models whose types are all named is not simply typed over these models either. Over all models of PI with worlds, including those with a type that no simple type names, NI≡, NI×, ND×, the Identity Identity and Necessitism are not simply typed either, and nor are their negations: two such models whose identity agrees, at every world, at the simple types, but varies from world to world at the extra type, make the same STLC sentences true while these principles differ.

Kripke models, in which a type may exist at some worlds and not at others, do the same for the Barcan formula (BF): over all Kripke models of PI, BF is not simply typed, and nor is its negation, since two such models that differ only in the worlds at which a type which no simple type names exists give BF different truth values, while every STLC sentence has the same truth value in both; its converse, CBF, by contrast holds in every Kripke model of PI. Functional Choice, by contrast, is simply typed over the Kripke models of PI, and so is its negation: in every Kripke model, Choice holds just in case its instance at t and t, an STLC sentence, holds, since each holds just in case every world that the actual world sees also sees the actual world. Over all models of PI, though, Choice is not simply typed, and nor is its negation. In a model with restricted function types, a function type need not hold every function. Two such models of PIC, one of them with a further base type of two members, differ only at that type, which no simple type names, so every STLC sentence has the same truth value in both; but Choice holds in the first and fails in the second, where every function from t to the further type is constant.

Algebraic models go further. In them propositions form any set with a truth predicate, and each model supplies the operations for the connectives and the quantifiers. Over the algebraic models of PI whose types are all named, the Barcan formula for types (TBF), its converse (TCBF) and DLF are not simply typed, and nor are their negations: an STLC sentence has no quantifier over types, so changing the operations for 𝔸 and 𝔼 changes the truth value of no STLC sentence, while it can make each of these three fail. CBF, which holds in every Kripke model of PI, is not simply typed over all algebraic models of PI, and nor is its negation, since changing the operation for the quantifier at a type which no simple type names changes the truth value of no STLC sentence but can make CBF fail; its negation is not simply typed even over the algebraic models whose types are all named. CBF itself, though, is simply typed over those models: its instances at the simple types, the STLC sentences ∀_{σ→t}F (∀_σ F =_{t,t} ⊤ → ∀_σ x (F x =_{t,t} ⊤)) with ⊤ the sentence ¬∀_t p p, express it, but no finite set of STLC sentences does, since the negation of their conjunction would then express the negation of CBF. Booleanism, by contrast, is simply typed, and so is its negation, over the models of PI in each of these semantics: the standard models, the models with worlds, the algebraic models (including those whose functions are finer than their graphs), the tagged models, the Kripke models and the models with restricted function types. Over PI, twelve of its instances yield all the others, so over the standard models, the models with worlds, the algebraic models, the tagged models and the models with restricted function types, their conjunction, a single STLC sentence, expresses Booleanism, and the negation of that conjunction expresses its negation. Over the Kripke models, Booleanism and the twelve instances hold in every one, as Booleanism does in every standard model, so the same two sentences express Booleanism and its negation there too.

PI⁻. Switching the base logic changes the class of models: the standard models of PI⁻ include models in which LL≡ fails, and the standard models of PI do not. Over the models of PI, nine of the principles below hold in every model, so they are constant; over the larger class, they can fail, and whether they are simply typed becomes a real question. Since every model of PI is a model of PI⁻, a set of sentences that expresses a principle over the models of PI⁻ also expresses it over the models of PI. So the switch to PI⁻ can only take away simple typedness, never add it. With PI⁻ as the base logic, the classes are the standard models of PI⁻, in which LL≡ may fail, so that identity within a type can be coarser than sameness. Over these models, LL≡, Classicism, Cong≈/≡, Cantor and the Identity Identity are no longer constant: they are simply typed over the models whose types are all named, but not over all of them. Their negations are not simply typed even over the models whose types are all named: models in which such a principle fails only at types larger than any given size agree, at the smaller types, with a model in which it holds. ⊤≢⊥, ≡ₜ to ↔ and T are no longer constant either, but each is equivalent to the STLC sentence ¬(¬⊥ =_{t,t} ⊥), so each stays simply typed. LL≈/≡ is not simply typed over the standard models of PI⁻, even when every type is named, and nor is its negation. For LL≈/≡ itself, take as entities the infinite sequences of 0s and 1s with infinitely many 0s, all of them identified, and at each type e→δ let identification have two classes: the non-constant maps that depend only on one coordinate of their argument (the coordinate given by the number of arrows in δ), and the rest; every other type is one class. LL≈/≡ fails in this model: the polymorphic property of agreeing with each entity at some coordinate or other holds of the sequence of 0s but not of 0101…. Splitting only the types e→δ in which δ has at most k arrows gives models in which LL≈/≡ holds, and each agrees with the first model on every STLC sentence whose identity signs are all at simple types of size at most k; so a set of STLC sentences true in all of them is true in the first as well. The other verdicts are as for PI.

PIC. With PIC as the base logic, the verdicts over the standard models do not change: Classicism holds in every standard model of PI, so the standard models of PIC are those of PI. Over all models, the models of PIC are fewer. In each semantics they are the models of PI in which Classicism is valid (in a Kripke model, true at the actual world), and each theorem of PIC holds in all of them. So the ten principles that PIC settles, but PI does not, now have the same truth value in every model of PIC: PIC proves Classicism, NI≡, NI≈, Booleanism, the Identity Identity, TCBF, Type Necessitism, CBF, Necessitism and the negation of DLF. These ten and their negations are simply typed, trivially, as are the principles that hold in every model of PI. ↔ to ≡ₜ and Collapse are still expressed by themselves, though they hold in every standard model and fail in a model of PIC with worlds. The rest are still not simply typed, and nor are their negations. For the principles that are not simply typed over the standard models, the same standard models serve; for Choice, the same models with restricted function types, which are models of PIC; for BF, the same two Kripke models, which validate Classicism. The pairs used before for NI× and ND× are not pairs of models of PIC. The two pairs share their first model, which is a model of PIC; but NI≡ fails in the second model of the first pair, and in the second model of the second pair LL≡ fails at the other world, while in a model of PIC with worlds every theorem of PI holds at every world. Three other models of PIC with worlds, though, in which the one entity is identified with the one member of a further type, which no simple type names, at the actual world, at the other world, or at neither, make the same STLC sentences true, while NI× fails in the first, ND× in the second, and both hold in the third. ND≈ holds in every model of PIC with worlds, but not in every Kripke model of PIC: two such models that differ only in ≈ give it different truth values. TBF holds in every algebraic model of PIC, but two Kripke models of PIC that differ only in whether a type of one member and the types built from it exist at the actual world, or only at a world it sees, give it different truth values. No verdict over the models of PIC is open.

References

• Barendregt, H. P. (1992). Lambda calculi with types. In S. Abramsky, D. M. Gabbay and T. S. E. Maibaum (eds.), Handbook of Logic in Computer Science, vol. 2. Oxford University Press.
• Coquand, T. and Huet, G. (1988). The calculus of constructions. Information and Computation 76.
• Girard, J.-Y. (1972). Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thèse d'État, Université Paris VII.