Stanford Encyclopedia of Philosophy
This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Church's Type Theory

First published Fri 25 Aug, 2006

Church's type theory is a formal logical language which includes first-order logic, but is more expressive in a practical sense. It is used, with some modifications and enhancements, in most modern applications of type theory. It is particularly well suited to the formalization of mathematics and other disciplines and to specifying and verifying hardware and software. A great wealth of technical knowledge can be expressed very naturally in it. With possible enhancements, Church's type theory constitutes an excellent formal language for representing the knowledge in automated information systems, sophisticated automated reasoning systems, systems for verifying the correctness of mathematical proofs, and certain projects involving logic and artificial intelligence. Some examples are given in Section 1.2.2 below.

Type theories are also called higher-order logics, since they allow quantification not only over individual variables (as in first-order logic), but also over function, predicate, and even higher order variables. Type theories characteristically assign types to entities, distinguishing, for example, between numbers, set of numbers, functions from numbers to sets of numbers, and sets of such functions. As illustrated in Section 1.2.2 below, these distinctions allow one to discuss the conceptually rich world of sets and functions without encountering the paradoxes of naive set theory.

Church's type theory is a formulation of type theory that was introduced by Alonzo Church in Church 1940. In certain respects, it is simpler and more general than the type theory introduced by Bertrand Russell in Russell 1908 and Whitehead & Russell 1927a. Since properties and relations can be regarded as functions from entities to truth values, the concept of a function is taken as primitive in Church's type theory, and the λ-notation which Church introduced in Church 1932 and Church 1941, is incorporated into the formal language.

1. Syntax

1.1 Fundamental Ideas

We start with an informal description of the fundamental ideas underlying the syntax of Church's formulation of type theory.

All entities have types, and if α and β are types, the type of functions from elements of type β to elements of type α is written as (αβ). (This notation was introduced by Church, but some authors write (β → α) instead of (αβ). See, for example, Section 4 of the entry on type theory.)

As noted by Schonfinkel (1924), functions of more than one argument can be represented in terms of functions of one argument when the values of these functions can themselves be functions. For example, if f is a function of two arguments, for each element x of the left domain of f there is a function g (depending on x) such that gy = fxy for each element y of the right domain of f. We may now write g = fx, and regard f as a function of a single argument, whose value for any argument x in its domain is a function fx, whose value for any argument y in its domain is fxy.

For a more explicit example, consider the function + which carries any pair of natural numbers to their sum. We may denote this function by +((σσ)σ), where σ is the type of natural numbers. Given any number x, [+((σσ)σ)x] is the function which, when applied to any number y, gives the value [[+((σσ)σ)x]y], which is ordinarily abbreviated as x + y. Thus [+((σσ)σ)x] is the function of one argument which adds x to any number. When we think of +((σσ)σ) as a function of one argument, we see that it maps any number x to the function [+((σσ)σ)x].

More generally, if f is a function which maps n-tuples <wβ, xγ, …, yδ, zτ> of elements of types β,γ,…,δ,τ, respectively, to elements of type α, we may assign to f the type ((…((ατ)δ)...γ)β). It is customary to use the convention of association to the left to omit parentheses, and write this type symbol simply as (ατδ…γβ).

A set or property can be represented by a function which maps elements to truth values, so that an element is in the set, or has the property, in question iff the function representing the set or property maps that element to truth. When a statement is asserted, the speaker means that it is true, so that sx means that sx is true, which also expresses the assertions that s maps x to truth and that x ∈ s. In other words, x ∈ s iff sx. We take ο as the type symbol denoting the type of truth values, so we may speak of any function of type (οα) as a set of elements of type α. A function of type ((οα)β) is a binary relation between elements of type β and elements of type α. For example, if σ is the type of the natural numbers, and < is the order relation between natural numbers, < has type (οσσ), and for all natural numbers x and y, <xy (which we ordinarily write as x<y) has the value truth iff x is less than y. Of course, < can also be regarded as the function which maps each natural number x to the set <x of all natural numbers y such that x is less than y. Thus sets, properties, and relations may be regarded as particular kinds of functions.

Expressions which denote elements of type α are called wffs of type α. Thus, statements of type theory are wffs of type ο.

If Aα is a wff of type α in which uαβ is not free, the function uαβ such that ∀vβ[uαβvβ = Aα] is denoted by [λvβ Aα]. Thus λvβ is a variable-binder, like ∀vβ or ∃vβ (but with a quite different meaning, of course); λ is known as an abstraction operator. [λvβ Aα] denotes the function whose value on any argument vβ is Aα, where vβ may occur free in Aα. For example, [λnσ [4·nσ+3]] denotes the function whose value on any natural number n is 4·n + 3. Hence when we apply this function to the number 5 we obtain [λnσ [4·nσ+3]]5 = 4·5 + 3 = 23.

We use Sub(B,v,A) as a notation for the result of substituting B for v in A, and SubFree(B,v,A) as a notation for the result of substituting B for all free occurrences of v in A. The process of replacing [λvβ Aα]Bβ by SubFree(Bβ,vβ,Aα) (or vice-versa) is known as β-conversion, which is one form of λ-conversion. Of course, when Aο is a wff of type ο, [λvβ Aο] denotes the set of all elements vβ (of type β) of which Aο is true; this set may also be denoted by {vβ | Aο}. For example, [λx x<y] denotes the set of x such that x is less than y (as well as that property which a number x has it if is less than y. In familiar set-theoretic notation, [λvβ Aο]Bβ = SubFree(Bβ,vβ,Aο) would be written Bβ ∈ {vβ | Aο} ≡ SubFree(Bβ,vβ,Aο). (By the Axiom of Extensionality for truth values, when Cο and Dο are of type ο, Cο ≡ Dο is equivalent to Cο = Dο.)

Propositional connectives and quantifiers can be assigned types and can be denoted by constants of these types. The negation function maps truth values to truth values, so it has type (οο). Similarly, disjunction and conjunction (etc.) are binary functions from truth values to truth values, so they have type (οοο).

The statement ∀xαAο is true iff the set [λxα Aο] contains all elements of type α. A constant Πο(οα) can be introduced (for each type symbol α) to denote a property of sets: a set sοα has the property Πο(οα) iff sοα contains all elements of type α. With this interpretation

∀sοα[Πο(οα)sοα ≡ ∀xα[sοαxα]]

should be true, as well as

Πο(οα)[λxα Aο] ≡ ∀xα[[λxα Aο]xα] (*)

for any wff Aο and variable xα. Since by λ-conversion we have

[λxα Aο]xα ≡ Aο

equation (*) can be written more simply as

Πο(οα)[λxα Aο] ≡ ∀xαAο.

Thus, ∀xα can be defined in terms of Πο(οα), and λ is the only variable-binder that is needed.

1.2 Formulas

1.2.1 Definitions

Type symbols are defined inductively as follows:

  1. imath is a type symbol (denoting the type of individuals). There may also be additional primitive type symbols which are used in formalizing disciplines where it is natural to have several sorts of individuals. [Editors Note: In what follows, the entry distinguishes between the symbols imath, ι, and imath. The first is the symbol used for the type of individuals; the second is the symbol used for a logical constant (see below); the third is the symbol used as a variable-binding operator that represents the definite description "the". The reader should check to see that the browser is displaying these symbols correctly.]
  2. ο is a type symbol (denoting the type of truth values).
  3. If α and β are type symbols, then (αβ) is a type symbol (denoting the type of functions from elements of type β to elements of type α).

The primitive symbols are the following:

  1. Improper symbols: [,   ],   λ
  2. For each type symbol α, a denumerable list of variables of type α: aα, bα, cα …
  3. Logical constants: ∼(οο), vel((οο)ο), Π(ο(οα)), ι(α(οα)) (for each type symbol α). [The types of these constants are indicated by their subscripts.]

    ∼(οο) denotes negation, vel((οο)ο) denotes disjunction, and Π(ο(οα)) is used in defining the universal quantifier as discussed above. ι(α(οα)) serves either as a description or selection operator as discussed in Section 1.3.4 and Section 1.3.5 below.

  4. In addition, there may be other constants of various types, which will be called nonlogical constants or parameters.

    Each choice of parameters determines a particular formulation of the system of type theory. Parameters are typically used as names for particular entities in the discipline being formalized.

Before we state the definition of a "formula", a word of caution is in order. The reader may be accustomed to thinking of a formula as an expression which plays the role of an assertion in a formal language, and of a term as an expression which designates an object. Church's terminology is somewhat different, and provides a uniform way of discussing expressions of many different types.

A formula is a finite sequence of primitive symbols. Certain formulas are called well-formed formulas (wffs). We write wffα as an abbreviation for wff of type α, and define this concept inductively as follows:

  1. A primitive variable or constant of type α is a wffα.
  2. If Aα β and Bβ are wffs of the indicated types, then [Aαβ Bβ] is a wffα.
  3. If xβ is a variable of type β and Aα is a wff, then [λxβ Aα] is a wff(αβ).

Note, for example, that by (a) ∼(οο) is a wff(οο), so by (b) if Aο is a wffο, then [∼(οο) Aο] is a wffο. Usually, the latter wff will simply be written as ∼A.

Definitions and abbreviations:
  1. [Aο vel Bο] stands for [[vel((oo)o) Aο] Bο].
  2. [Aο ⊃ Bο] stands for [[∼{oo} Aο] vel Bο].
  3. [∀xαAο] stands for [Π(o(oα)) [λxα Aο]].
  4. Other propositional connectives, and the existential quantifier, are defined in familiar ways. In particular,
    [Aο ≡ Bο] stands for [[Aο ⊃ Bο] and [Bο ⊃ Aο]].
  5. Qοαα stands for [λxαλyα ∀f(oα)[f(oα)xα ⊃ f(oα)yα]].
    [Aα = Bα] stands for QoααAαBα.

The last definition is known as the Leibnizian definition of equality. It asserts that x and y are the same if y has every property that x has. Actually, Leibniz called his definition "the identity of indiscernibles" and gave it in the form of a biconditional: x and y are the same if x and y have exactly the same properties. It is not difficult to show that these two forms of the definition are logically equivalent.

1.2.2 Examples

We now provide a few examples to illustrate how various assertions and concepts can be expressed in Church's type theory. It is often convenient to omit type symbols from some or all occurrences of variables and constants, and use conventions for omitting parentheses and brackets, but this is mostly avoided here. However, in writing type symbols we often omit outer parentheses and use the convention of association to the left; thus οι ι is an abbreviation for ((οι)ι).

Example 1

To express the assertion that Napoleon is charismatic we introduce constants Charismaticοimath and Napoleonimath, with the types indicated by their subscripts and the obvious meanings, and assert the wff

Charismaticοimath Napoleonimath

If we wish to express the assertion that "Napoleon has all the properties of a great general", we might consider interpreting this to mean that "Napoleon has all the properties of some great general", but it seems more appropriate to interpret this statement as meaning that "Napoleon has all the properties which all great generals have". If the constant GreatGeneralοimath is added to the formal language, this can be expressed by the wff

∀pοimath[∀gimath[GreatGeneralοimath gimath ⊃ pοimath gimath] ⊃ pοimath Napoleonimath].

As an example of such a property, we note that the sentence "Napoleon's soldiers admire him" can be expressed in a similar way by the wff

∀ximath[Soldierοimath ximath and [CommanderOfimathimath ximath = Napoleonimath] ⊃ Admiresοimathimath ximath Napoleonimath].

By λ-conversion, this is equivalent to

[λnimath ∀ximath[Soldierοimath ximath and [CommanderOfimathimath ximath = nimath] ⊃ Admiresoimathimath ximath nimath]]Napoleonimath.

This statement asserts that one of the properties which Napoleon has is that of being admired by his soldiers. The property itself is expressed by the wff

[λnimath ∀ximath[Soldierοimath ximath and [CommanderOfimathimath ximath = nimath] ⊃ Admiresoimathimath ximath nimath]].
Example 2

We illustrate some potential applications of type theory with the following fable.

A rich and somewhat eccentric lady named Sheila has an ostrich and a cheetah as pets, and she wishes to take them from her hotel to her remote and almost inaccessible farm. Various portions of the trip may involve using elevators, boxcars, airplanes, trucks, very small boats, donkey carts, suspension bridges, etc., and she and the pets will not always be together. She knows that she must not permit the ostrich and the cheetah to be together when she is not with them. We consider how certain aspects of this problem can be formalized so that Sheila can use an automated reasoning system to help analyze the possibilities.

There will be a set Moments of instants or intervals of time during the trip. She will start the trip at the location Hotel and moment Start, and end it at the location Farm and moment Finish. Moments will have type τ, and locations will have type ρ. A state will have type σ and will specify the location of Sheila, the ostrich, and the cheetah at a given moment. A plan will specify where the entities will be at each moment according to this plan. It will be a function from moments to states, and will have type (στ). The exact representation of states need not concern us, but there will be functions from states to locations called LocationOfSheila, LocationOfOstrich, and LocationOfCheetah which provide the indicated information. Thus, LocationOfSheilaρσ[pστ tτ] will be the location of Sheila according to plan pστ at moment tτ. The set Proposalsο(στ) is the set of plans Sheila is considering.

We define a plan p to be acceptable if, according to that plan, the group starts at the hotel, finishes at the farm, and whenever the ostrich and the cheetah are together, Sheila is there too. Formally, we define Acceptableο(στ) as

[λpστ [LocationOfSheilaρσ [pστ Startτ] = Hotelρ   and
LocationOfOstrichρσ[pστ Startτ] = Hotelρ   and
LocationOfCheetahρσ[pστ Startτ] = Hotelρ   and
LocationOfSheilaρσ[pστ Finishτ] = Farmρ   and
LocationOfOstrichρσ[pστ Finishτ] = Farmρ   and
LocationOfCheetahρσ[pστ Finishτ] = Farmρ   and
∀tτ[Momentsοτ tτ ⊃
      [[LocationOfOstrichρσ[pστ tτ] = LocationOfCheetahρσ[pστ tτ]] ⊃
      [LocationOfSheilaρσ[pστ tτ] = LocationOfCheetahρσ[pστ tτ] ] ] ] ] ].

We can express the assertion that Sheila has a way to accomplish her objective with the formula

∃pστ[Proposalsο(στ) pστ and Acceptableο(στ) pστ].
Example 3

We now provide a mathematical example. Mathematical ideas can be expressed in type theory without introducing any new constants. An iterate of a function f which maps a set to itself is a function which applies f one or more times. For example, if g(x) = f(f(f(x))), then g is an iterate of f. [ITERATE+ο(imathimath)(imathimath) fimathimath gimathimath] means that gimathimath is an iterate of fimathimath. ITERATE+ο(imathimath)(imathimath) is defined (inductively) as

λfimathimath λgimathimath ∀pο(imathimath)[pο(imathimath) fimathimath and ∀jimathimath[pο(imathimath) jimathimath ⊃ pο(imathimath)[λximath fimathimath[jimathimath ximath] ] ] ⊃ pο(imathimath) gimathimath].

Thus, g is an iterate of f if g is in every set p of functions which contains f and which contains the function [λximath fimathimath[jimathimath ximath] ] (i.e., f composed with j) whenever it contains j.

A fixed point of f is an element y such that f(y) = y.

It can be proved that if some iterate of a function f has a unique fixed point, then f itself has a fixed point. This theorem can be expressed by the wff

∀fimathimath[∃gimathimath[ITERATE+ο(imathimath)(imathimath) fimathimath gimathimath and ∃ximath[gimathimathximath = ximath and ∀zimath[gimathimathzimath = zimath ⊃ zimath = ximath] ] ] ⊃
       ∃yimath[fimathimathyimath = yimath] ].

See Andrews et al. 1996, for a discussion of how this theorem, which is called THM15B, can be proved automatically.

Example 4

Suppose we omit the use of type symbols in the definitions of wffs. Then we can write the formula [λx ∼x x], which we shall call R. It can be regarded as denoting the set of all sets x such that x is not in x. We may then consider the formula [R R], which expresses the assertion that R is in itself. We can clearly prove [R R] ≡ [λx ∼x x]R, so by λ-conversion we can derive [R R] ≡ ∼[R R], which is a contradiction. This is Russell's paradox. Russell's discovery of this paradox (Russell 1903, 101-107) played a crucial role in the development of type theory. Of course, when type symbols are present, R is not well-formed, and the contradiction cannot be derived.

1.3 Axioms and Rules of Inference

1.3.1 Rules of Inference

  1. Alphabetic Change of Bound Variables (α-conversion). To replace any well-formed part [λxβ Aα] of a wff by [λyβ Sub(yβ,xβ,Aα)], provided that yβ does not occur in Aα and xβ is not bound in Aα.
  2. β-contraction. To replace any well-formed part [[λxα Bβ] Aα] of a wff by Sub(Aα,xα,Bβ), provided that the bound variables of Bβ are distinct both from xα and from the free variables of Aα.
  3. β-expansion. To infer C from D if D can be inferred from C by a single application of β-contraction.
  4. Substitution. From F(οα)xα, to infer F(οα)Aα, provided that xα is not a free variable of F(οα).
  5. Modus Ponens. From [Aο ⊃ Bο] and Aο, to infer Bο.
  6. Generalization. From F(οα)xα to infer Πο(οα)F(οα), provided that xα is not a free variable of F(οα).

1.3.2 Elementary Type Theory

We start by listing the axioms for what we shall call elementary type theory.

(1) [pο vel pο] ⊃ pο
(2) pο ⊃ [pο vel qο]
(3) [pο vel qο] ⊃ [qο vel pο]
(4) [pο ⊃ qο] ⊃ [[rο vel pο] ⊃ [rο vel qο] ]
(5α) Πο(οα) f(οα) ⊃ f(οα) xα
(6α) ∀xα[pο vel f(οα)xα] ⊃ [pο vel Πο(οα) f(οα)]

The theorems of elementary type theory are those theorems which can be derived from Axioms 1–6α (for all type symbols α). We shall sometimes refer to elementary type theory as calligraphic-T. It embodies the logic of propositional connectives, quantifiers, and λ-conversion in the context of type theory.

To illustrate the rules and axioms introduced above, we give a short and trivial proof in calligraphic-T. Following each wff of the proof, we indicate how it was inferred.[1]

1. ∀ximath[pο or fοimathximath] ⊃ [pο or Πο(οimath) fοimath] Axiom 6imath
2. [λfοimath ∀ximath[pο or fοimathximath] ⊃ [pο or Πο(οimath) fοimath] ]fοimath β-expansion: 1
3. Πο(ο(οimath))[λfοimath ∀ximath[pο or fοimathximath] ⊃ [pο or Πο(οimath)fοimath] ] Generalization: 2
4. [λfοimath ∀ximath[pο or fοimathximath] ⊃ [pο or Πο(οimath)fοimath] ] [λximath rοimathximath] Substitution: 2
5. ∀ximath[pο or [λximath rοimathximath]ximath] ⊃ [pο or Πο(οimath)[λximath rοimathximath] ] β-contraction: 4
6. ∀ximath[pο or [λyimath rοimathyimath]ximath] ⊃ [pο or Πο(οimath)[λximath rοimathximath] ] α-conversion: 5
7. ∀ximath[pο or rοimathximath] ⊃ [pο or Πο(οimath)[λximath rοimathximath] ] β-contraction: 6

Note that (3) can be written as

(3′) ∀fοimath[∀ximath[pο or fοimathximath] ⊃ [pο or Πο(οimath)fοimath] ]

and (7) can be written as

(7′) ∀ximath[pο or rοimathximath] ⊃ [pο or ∀ximath rοimathximath]

We have thus derived a well known law of quantification theory. We illustrate one possible interpretation of the wff (7′) (which is closely related to Axiom 6) by considering a situation in which a rancher puts some horses in a corral and leaves for the night. Later, he cannot remember whether he closed the gate to the corral. While reflecting on the situation, he comes to a conclusion which can be expressed by (7′) if we take the horses to be the elements of type imath, interpret pο to mean "the gate was closed", and interpret rοimath so that rοimathximath asserts "ximath left the corral". With this interpretation, (7′) says "If it is true of every horse that the gate was closed or that horse left the corral, then the gate was closed or every horse left the corral."

To the axioms listed above we add the axioms below to obtain Church's type theory.

1.3.3 Axioms of Extensionality

(7ο) [xο ≡ yο] ⊃ xο = yο
(7αβ) ∀xβ[fαβ xβ = gαβ xβ] ⊃ fαβ = gαβ

Church did not include Axiom 7ο in his list of axioms in Church 1940, but he mentioned the possibility of including it. Henkin did include it in Henkin 1950.

1.3.4 Descriptions

The expression

∃1xαAο

stands for

[λpοα ∃yα[pοα yα and ∀zα[pοα zα ⊃ zα = yα] ] [λxα Aο].

For example,

∃1xαPοαxα

stands for

[λpοα ∃yα[pοα yα and ∀zα[pοα zα ⊃ zα = yα] ] [λxα Pοαxα].

By λ-conversion, this is equivalent to:

∃yα[[λxα Pοαxα]yα and ∀zα[[λxα Pοαxα]zα ⊃ zα = yα] ]

which reduces by λ-conversion to:

∃yα[Pοαyα and ∀zα[Pοαzα ⊃ zα = yα] ]

This asserts that there is a unique element which has the property Pοα. From this example we can see that in general, ∃1xα Aο expresses the assertion that "there is a unique xα such that Aο".

When there is a unique such element xα, it is convenient to have the notation inverted iotaxαAο to represent the expression "the xα such that Aο". Russell showed in Whitehead & Russell 1927b how to provide contextual definitions for such notations in his formulation of type theory. In Church's type theory inverted iotaxαAο is defined as ια(οα)[λxα Aο]. Thus, inverted iota behaves like a variable-binding operator, but it is defined in terms of λ with the aid of the constant ια(οα). Thus, λ is still the only variable-binding operator that is needed.

Since Aο describes xα, ια(οα) is called a description operator. Associated with this notation is the following:

Axiom of Descriptions:
(8α) ∃1xα[pοαxα] ⊃ pοα [ια(οα) pοα]

This says that when the set pοα has a unique member, then ια(οα)pοα is in pοα, and therefore is that unique member. Thus, this axiom asserts that ια(οα) maps one-element sets to their unique members.

If from certain hypotheses one can prove ∃1xαAο, then by using Axiom 8α one can derive

[λxαAο][ια(οα)[λxαAο] ],

which can also be written as

[λxαAο](inverted iotaxα)Aο.

We illustrate the usefulness of the description operator with a small example. Suppose we have formalized the theory of real numbers, and our theory has constants 1ρ and ×ρρρ to represent the number 1 and the multiplication function, respectively. (Here ρ is the type of real numbers.) To represent the multiplicative inverse function, we can define the wff INVρρ as:

[λzρ(inverted iotaxρ)[×ρρρzρxρ = 1ρ]].

Of course, in traditional mathematical notation we would not write the type symbols, and we would write ×ρρρzρxρ as z × x and write INVρρz as z−1. Thus z−1 is defined to be that x such that z × x = 1. When Z is provably not 0, we will be able to prove ∃1xρ[×ρρρZ xρ = 1ρ] and Z × Z−1 = 1, but if we cannot establish that Z is not 0, nothing significant about Z−1 will be provable.

1.3.5 Axiom of Choice

The Axiom of Choice can be expressed as follows in Church's type theory:

(9α) ∃xα pοαxα ⊃ pοα[ια(οα) pοα]

(9α) says that the choice function ια(οα) chooses from every nonempty set pοα an element (which is designated as ια(οα)pοα) of that set. When this form of the Axiom of Choice is included in the list of axioms, ια(οα) is called a selection operator[2] instead of a description operator, and (inverted iotaxα)Aο means "an xα such that Aο" when there is some such element sα.

It is natural to call inverted iota a definite description operator in contexts where (inverted iotaxα)Aο means "the xα such that Aο", and to call it an indefinite description operator in contexts where (inverted iotaxα)Aο means "an xα such that Aο".

Clearly the Axiom of Choice implies the Axiom of Descriptions, but sometimes formulations of type theory are used which include the Axiom of Descriptions, but not the Axiom of Choice.

Another formulation of the Axiom of Choice simply asserts the existence of a choice function without explicitly naming it:

(ACα) ∃jα(οα) ∀pοα [∃xα pοαxα ⊃ pοα [jα(οα) pοα] ]

Normally when one assumes the Axiom of Choice in type theory, one assumes it as an axiom schema, and asserts ACα for each type symbol α.

Before proceeding, we need to introduce some terminology. cal Q0 is an alternative formulation of Church's type theory which will be described in Section 1.4 and is equivalent to the system described above using Axioms 1–8. A type symbol is propositional if the only symbols which occur in it are ο and parentheses.

Yasuhara (1975) defined the relation ‘≥’ between types as the reflexive transitive closure of the minimal relation such that (α β) ≥ α. and (α β) ≥ β. He established that:

Büchi (1953) has shown that while the schemas expressing the Axiom of Choice and Zorn's Lemma can be derived from each other, the relationships between the particular types involved are complex.

1.3.6 Axioms of Infinity

One can define the natural numbers (and therefore other basic mathematical structures such as the real and complex numbers) in type theory, but to prove that they have the required properties (such as Peano's Postulates), one needs an Axiom of Infinity. There are many viable possibilities for such an axiom, such as those discussed in Church 1940.

1.4 A Formulation Based on Equality

In Section 1.2.1, ∼(οο), or((οο)ο), and the Π(ο(οα))'s were taken as primitive constants, and the wffs Qοαα which denote equality relations at type α were defined in terms of these. We now present an alternative formulation cal Q0 of Church's type theory in which there are primitive constants Qοαα detnoting equality, and ∼(οο), or((οο)ο), and the Π(ο(οα))'s are defined in terms of the Qοαα's.

Tarski (1923) noted that in the context of higher-order logic, one can define propositional connectives in terms of logical equivalence and quantifiers. Quine (1937) showed how to define quantifiers in terms of inclusion and abstraction. Henkin (1963) developed a formulation of Church's type theory based on equality in which he restricted attention to propositional types, and Andrews (1963) simplified the axioms for this system. cal Q0 is based on these ideas, and can be shown to be equivalent to a formulation of Church's type theory using Axioms 1–8 of the preceding sections. This section provides an alternative to the material in the preceding Sections 1.2.1 – 1.3.4.

  1. Type symbols, improper symbols, and variables are defined as in Section 1.2.1.
  2. Logical constants: Q((οα)α), and ι(imath(οimath)).
  3. Wffs are defined as in Section 1.2.1.

We employ the following definitions and abbreviations:

[Aα = Bα] stands for [Qοαα Aα Bα]
[Aο ≡ Bο] stands for [QoooAο Bο]
Tο stands for [Qοοο = Qοοο]
Fο stands for [λxο Tο] = [λxο xο]
Πο(οα) stands for [Qο(οα)(οα) [λxα Tο] ]
[∀xα A] stands for [Πο(οα) [λxα A] ]
andοοο stands for [λxολyο [ [λgοοο [gοοοTοTο] ] = [λgοοο [gοοοxοyο] ] ] ]
[Aο and Bο] stands for [andοοο Aο Bο]
∼οο stands for [Qοοο Fο]

Tο denotes truth. The meaning of Πο(οα) was discussed in Section 1.1. To see that this definition of Πο(οα) is appropriate, note that [λxα T] denotes the set of all elements of type α, and that Πο(οα)sοα stands for [Qο(οα)(οα) [λxα T] ]sοα and for [λxα T] = sοα. Therefore Πο(οα)sοα asserts that sοα is the set of all elements of type α, so sοα contains all elements of type α. It can be seen that Fο can also be written as ∀xο xο, which asserts that everything is true. This is false, so Fο denotes falsehood. The expression [λgοοο [gοοοxοyο] ] can be used to represent the ordered pair <xο,yο>, and the conjunction xο and yο is true iff xο and yο are both true, i.e., iff <Tο,Tο> = <xο,yο>. Hence xο and yο can be expressed by the formula [λgοοο [gοοοTο Tο] ] = [λgοοο [gοοοxο yο] ].

Other propositional connectives and the existential quantifier are easily defined. By using ι(imath(οimath)), one can define description operators ια(οα) for all types α.

cal Q0 has the following single rule of inference and axioms:

Rule R:
From C and Aα = Bα, to infer the result of replacing one occurrence of Aα in C by an occurrence of Bα, provided that the occurrence of Aα in C is not (an occurrence of a variable) immediately preceded by λ.

Axioms for cal Q0:

(1) [gοο Tο and gοο Fο] = ∀xο[gοο xο]
(2α) [xα = yα] ⊃ [hοα xα = hοα yα]
(3αβ) [fαβ = gαβ] = ∀xβ[fαβ xβ = gαβ xβ]
(4) [λxα Bβ]Aα = SubFree(Aα,xα,Bβ), provided that Aα is free for x in Bβ.
(5) ιimath(οimath)[Qοimathimath yimath] = yimath

2. Semantics

It is natural to compare the semantics of type theory with the semantics of first-order logic, where the theorems are precisely the wffs which are valid in all interpretations. From an intuitive point of view, the natural interpretations of type theory are standard models, which are defined below. However, it is a consequence of Gödel's Incompleteness Theorem (Gödel 1931) that axioms 1–9 do not suffice to derive all wffs which are valid in all standard models, and there is no consistent recursively axiomatized extension of these axioms which suffices for this purpose. Nevertheless, experience shows that these axioms are sufficient for most purposes, and Leon Henkin considered the problem of clarifying in what sense they are complete. The definitions and theorem below constitute Henkin's (1950) solution to this problem.

A frame is a collection {cal-Dα}α of nonempty domains (sets) cal-Dα, one for each type symbol α, such that cal-Dο = {T, F} (where T represents truth and F represents falsehood), and cal-Dαβ is some collection of functions mapping cal-Dβ into cal-Dα. The members of cal-Dimath are called individuals.

An interpretation <{cal-Dα}α, frak I> consists of a frame and a function frak I which maps each constant C of type α to an appropriate element of cal-Dα, which is called the denotation of C.

An assignment of values in the frame {cal-Dα}α to variables is a function φ such that φxα ∈ cal-Dα for each variable xα.

An interpretation cal M = <{cal-Dα}α, frak I> is a general model iff there is a binary function cal V such that cal VφAα ∈ cal-Dα for each assignment φ and wff Aα, and the following conditions are satisfied for all assignments and all wffs:

  1. cal Vφxα = φxα for each variable xα.
  2. cal VφAα = frak IAα if Aα is a primitive constant.
  3. cal Vφ[AαβBβ] = (cal VφAαβ) (cal VφBβ) (the value of a function cal VφAαβ at the argument cal VφBβ).
  4. cal Vφ[λxαBβ] = that function from cal-Dα into cal-Dβ whose value for each argument z ∈ cal-Dα is cal VψBβ, where ψ is that assignment such that ψxα = z and ψyβ = φyβ if yβ ≠ xα.

If an interpretation cal-M is a general model, the function cal-V is uniquely determined. cal VφAα is called the value of Aα in cal-M with respect to φ.

An interpretation <{cal-Dα}α, frak I> is a standard model iff for all α and β, cal-Dαβ is the set of all functions from cal-Dβ into cal-Dα. Clearly a standard model is a general model.

We say that a wff A is valid in a model cal-M iff cal VφA = T for every assignment φ into cal-M. A model for a set cal-H of wffs is a model in which each wff of cal-H is valid.

A wff A is valid in the general [standard] sense iff A is valid in every general [standard] model. Clearly a wff which is valid in the general sense is valid in the standard sense, but the converse of this statement is false.

Henkin's Completeness and Soundness Theorem.
A wff is a theorem if and only if it is valid in the general sense.

Not all frames belong to interpretations, and not all interpretations are general models. In order to be a general model, an interpretation must have a frame satisfying certain closure conditions which are discussed further in Andrews 1972b. Basically, in a general model every wff must have a value with respect to each assignment.

A model is said to be finite iff its domain of individuals is finite. Every finite model for cal Q0 is standard (Andrews 2002, Theorem 5404), but every set of sentences of cal Q0 which has infinite models also has nonstandard models (Andrews2002, Theorem 5506).

An understanding of the distinction between standard and nonstandard models can clarify many phenomena. For example, it can be shown that there is a model cal M = <{cal-Dα}α, frak I> in which cal-Dimath is infinite, and all the domains cal-Dα are countable. Thus cal-Dimath and cal-Doimath are both countably infinite, so there must be a bijection h between them. However, Cantor's Theorem (which is provable in type theory and therefore valid in all models) says that cal-Dimath has more subsets than members. This seemingly paradoxical situation is called Skolem's Paradox. It can be resolved by looking carefully at Cantor's Theorem, i.e., ∼∃goimathimath∀foimath∃jimath[goimathimath jimath = foimath], and considering what it means in a model. The theorem says that there is no function g ∈ cal-Doimathimath from cal-Dimath into cal-Doimath which has every set foimath ∈ cal-Doimath in its range. The usual interpretation of the statement is that cal-Doimath is bigger (in cardinality) than cal-Dimath. However, what it actually means in this model is that h cannot be in cal-Doimathimath. Of course, must be nonstandard.

While the Axiom of Choice is presumably true in all standard models, there is a nonstandard model for cal Q0 in which ACimath is false (Andrews 1972b). Thus, ACimath is not provable in cal Q0.

Thus far, investigations of model theory for Church's type theory have been far less extensive than for first-order logic. Nevertheless, there has been some work on methods of constructing nonstandard models of type theory and models in which various forms of extensionality fail, models for theories with arbitrary (possibly incomplete) sets of logical constants, and on developing general methods of establishing completeness of various systems of axioms with respect to various classes of models. Relevant papers include Andrews 1971, 1972a,b, Benzmüller et al. 2004, and Brown2004.

3. Metatheory

3.1 λ-conversion

The first three rules of inference in Section 1.3.1 are called rules of λ-conversion. If D and E are wffs, we write D conv E to indicate that D can be converted to E by applications of these rules. This is an equivalence relation between wffs. A wff D is in β-normal form iff it has no well-formed parts of the form [ [λxαBβ] Aα]. Every wff is convertible to one in β-normal form. Indeed, every sequence of contractions (applications of rule 2, combined as necessary with alphabetic changes of bound variables) of a wff is finite; obviously, if such a sequence cannot be extended, it terminates with a wff in β-normal form. (This is called the strong normalization theorem.) By the Church-Rosser Theorem, this wff in β-normal form is unique modulo alphabetic changes of bound variables. For each wff A we denote by ↓A the first wff (in some enumeration) in β-normal form such that A conv ↓A. Then D conv E if and only if ↓D = ↓E.

By using the Axiom of Extensionality one can obtain the following derived rule of inference:

η-Contraction. Replace a well-formed part [λyβ [Bαβyβ]] of a wff by Bαβ, provided yβ does not occur free in Bαβ.

This rule and its inverse (which is called η-Expansion) are sometimes used as additional rules of λ-conversion. See Church 1941, Stenlund 1972, and Barendregt 1984 for more information about λ-conversion.

3.2 Higher-order Unification

Consider the following:

Definition. A higher-order unifier for a pair <A,B> of wffs is a substitution θ for free occurrences of variables such that θA and θB have the same β-normal form. A higher-order unifier for a set of pairs of wffs is a unifier for each of the pairs in the set.

Higher-order unification differs from first-order unification (Baader & Snyder 2001) in a number of important respects. In particular:

  1. Even when a unifier for a pair of wffs exists, there may be no most general unifier (Gould 1966).
  2. Higher-order unification is undecidable (Huet 1973b), even in the "second-order" case (Goldfarb 1981).

Nevertheless, an algorithm has been devised (Huet 1975, Jensen & Pietrzykowski 1976) which will find a unifier for a set of pairs of wffs if one exists. The algorithm generates a search tree, certain branches of which may not terminate. See Dowek 2001 for more information.

3.3 A Unifying Principle

Smullyan's Unifying Principle was introduced in Smullyan 1963 (see also Smullyan 1995) as a tool for deriving a number of basic metatheorems about first-order logic in a uniform way. It was extended to elementary type theory (the system cal-T of section Section 1.3.2) in Andrews 1971 by applying ideas in Takahashi 1967.

This Unifying Principle for cal-T has been used to establish cut-elimination for cal-T in Andrews 1971 and completeness proofs for various systems of type theory in Huet 1973a, Kohlhase 1995, and Miller 1983. We first give a definition and then state the principle.

Definition. A property Γ of finite sets of wffs0 is an abstract consistency property iff for all finite sets cal-S of wffs0, the following properties hold (for all wffs A, B):
  1. If Γ(cal-S), then there is no atom A such that A ∈ cal-S and [∼A] ∈ cal-S.
  2. If Γ(cal-S ∪ {A}), then Γ(cal-S ∪ ↓A}).
  3. If Γ(cal-S ∪ {∼∼A}), then Γ(cal-S ∪ {A}).
  4. If Γ(cal-S ∪ {[A vel B]}), then Γ (cal-S ∪ {A}) or Γ(cal-S ∪ {B}).
  5. If Γ (cal-S ∪ {∼[A vel B]}), then Γ(cal-S ∪ {∼A,∼B}).
  6. If Γ(cal-S ∪ {Πο(οα) Aοα}), then for each wff Bα, Γ(cal-S ∪ {Πο(οα) Aοα, AοαBα}).
  7. If Γ(cal-S ∪ {∼Πο(οα) Aοα}), then Γ(cal-S ∪ {∼Aοαcα}), for any variable or parameter cα which does not occur free in Aοα or any wff in cal-S.

Note that consistency is an abstract consistency property.

Unifying Principle for cal-T.
If Γ is an abstract consistency property and Γ(cal-S), then cal-S is consistent in cal-T.

Here is a typical application of the Unifying Principle. Suppose there is a procedure cal-M which can be used to refute sets of sentences, and we wish to show it is complete for cal-T. For any set of sentences, let Γ(cal-S) mean that cal-S is not refutable by cal-M, and show that Γ is an abstract consistency property. Now suppose that A is a theorem of cal-T. Then {∼A} is inconsistent in cal-T, so by the Unifying Principle not Γ({∼A}), so {∼A} is refutable by cal-M.

Kohlhase (1993) extended the Unifying Principle to systems with extensionality. This extended principle was used in Benzmüller & Kohlhase 1998a to obtain a completeness proof for a system of extensional higher-order resolution. This extended principle also appears in Kohlhase 1998, where it is used to obtain a completeness proof for an extensional higher-order tableau calculus, which has been implemented under the name HOT (Konrad 1998). In Benzmüller et al. 2004 the principle and associated completeness proofs are presented in a very general way which allows for various possibilities concerning the treatment of extensionality and equality.

3.4 Cut-elimination

Cut-elimination proofs for Church's type theory, which are often closely related to such proofs (Prawitz 1968, Takahashi 1967 and 1970) for other formulations of type theory, may be found in Andrews 1971, Dowek & Werner 2003, and Brown 2004.

3.5 Expansion Proofs

An expansion proof is a generalization of the notion of a Herbrand expansion of a theorem of first-order logic; it provides a very elegant, concise, and nonredundant representation of the relationship between the theorem and a tautology which can be obtained from it by appropriate instantiations of quantifiers and which underlies various proofs of the theorem. Miller (1987) proved that a wff A is a theorem of elementary type theory if and only if A has an expansion proof.

In Brown 2004, this concept is generalized to that of an extensional expansion proof to obtain an analogous theorem involving type theory with extensionality.

3.6 The Decision Problem

Since type theory includes first-order logic, it is no surprise that most systems of type theory are undecidable. However, one may look for solvable special cases of the decision problem. For example, the system cal Q01 is obtained by adding to cal Q0 the additional axiom ∀ximath∀yimath[ximath = yimath] is decidable.

Although the system cal T of elementary type theory is analogous to first-order logic in certain respects, it is a considerably more complex language, and special cases of the decision problem for provability in cal T seem rather intractable for the most part. Information about some very special cases of this decision problem may be found in Andrews 1974, and we now summarize this.

A wff of the form ∃x1…∃xn[A = B] is a theorem of cal T iff there is a substitution θ such that θA conv θB. In particular, provesA = B iff A conv B, which solves the decision problem for wffs of the form [A = B]. Naturally, the circumstance that only trivial equality formulas are provable in cal T changes drastically when axioms of extensionality are added to cal T. proves∃xβ[A = B] iff there is a wff Eβ such that proves[λxβ [A = B]]Eβ, but the decision problem for the class of wffs of the form ∃xβ[A = B] is unsolvable.

A wff of the form ∀x1…∀xnC, where C is quantifier-free, is provable in cal T iff ↓C is tautologous. On the other hand, the decision problem for wffs of the form ∃zC, where C is quantifier-free, is unsolvable. (By contrast, the corresponding decision problem in first order logic with function symbols is known to be solvable (Maslov 1967).) Since irrelevant or vacuous quantifiers can always be introduced, this shows that the only solvable classes of wffs of cal T in prenex normal form defined solely by the structure of the prefix are those in which no existential quantifiers occur.

4. Automation

Computer systems for proving theorems of Church's type theory (or extensions of it) interactively or automatically include HOL (Gordon 1988, Gordon & Melham 1993), TPS (Andrews et al. 1996, Andrews & Brown 2006), LEO (Benzmüller 1999, Benzmüller & Kohlhase 1998b), HOT (Konrad 1998), PVS (Owre et al. 1996), Shankar 2001), and ProofPower. Extensive work using Church's type theory to verify hardware and software is discussed in Gordon 1986 and the TPHOLS conferences. A survey of ideas on automating the development of proofs in Church's type theory may be found in Andrews 2001.

Bibliography

Other Internet Resources

Related Entries

artificial intelligence: logic and | logic: classical | reasoning: automated | Russell, Bertrand | type theory

Acknowledgements

Portions of this material are adapted from Andrews 2002 and Andrews 2001, with permission from the author and Elsevier.