# Church's Type Theory

*First published Fri Aug 25, 2006; substantive revision Wed Feb 25, 2009*

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
- 2. Semantics
- 3. Metatheory
- 4. Automation
- Bibliography
- Other Internet Resources
- Related Entries

## 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:

- 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 , ι, and . 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.]
- ο is a type symbol (denoting the type of truth values).
- 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:

- Improper symbols: [, ], λ
- For each type symbol α, a denumerable list of
*variables*of type α:*a*_{α},*b*_{α},*c*_{α}… - Logical constants: ∼
_{(οο)}, ∨_{((οο)ο)}, Π_{(ο(οα))}, ι_{(α(οα))}(for each type symbol α). [The types of these constants are indicated by their subscripts.] The symbol ∼_{(οο)}denotes negation, ∨_{((οο)ο)}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. - 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* (*wff*s). We
write *wff*_{α} as an abbreviation for *wff of
type* α, and define this concept inductively as follows:

- A primitive variable or constant of type α is a wff
_{α}. - If
**A**_{αβ}and**B**_{β}are wffs of the indicated types, then [**A**_{αβ}**B**_{β}] is a wff_{α}. - 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:

- [
A_{ο}∨B_{ο}] stands for [[∨_{((oo)o)}A_{ο}]B_{ο}].- [
A_{ο}⊃B_{ο}] stands for [[∼_{(οο)}A_{ο}] ∨B_{ο}].- [∀
x_{α}A_{ο}] stands for [Π_{(ο(οα))}[λx_{α}A_{ο}]].- Other propositional connectives, and the existential quantifier, are defined in familiar ways. In particular,
[A_{ο}≡B_{ο}] stands for [[A_{ο}⊃B_{ο}] ∧ [B_{ο}⊃A_{ο}]].- Q
_{οαα}stands for [λx_{α}λy_{α}∀f_{(οα)}[f_{(οα)}x_{α}⊃f_{(οα)}y_{α}]].- [
A_{α}=B_{α}] stands for Q_{οαα}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*_{ο}
and
*Napoleon*_{},
with the types indicated by their subscripts and the obvious
meanings, and assert the wff

Charismatic_{ο}Napoleon_{}

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*_{ο}
is added to the formal language, this can be expressed by the wff

∀p_{ο}[∀g_{}[GreatGeneral_{ο}g_{}⊃p_{ο}g_{}] ⊃p_{ο}Napoleon_{}].

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

∀x_{}[Soldier_{ο}x_{}∧ [CommanderOf_{}x_{}=Napoleon_{}] ⊃

Admires_{ο}x_{}Napoleon_{}].

By λ-conversion, this is equivalent to

[λ

n_{}∀x_{}[Soldier_{ο}x_{}∧ [CommanderOf_{}x_{}=n_{}] ⊃Admires_{ο}x_{}n_{}]]Napoleon_{}.

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

[λn_{}∀x_{}[Soldier_{ο}x_{}∧ [CommanderOf_{}x_{}=n_{}] ⊃Admires_{ο}x_{}n_{}]].

##### 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_{ρ}∧LocationOfOstrich_{ρσ}[p_{στ}Start_{τ}] =Hotel_{ρ}∧LocationOfCheetah_{ρσ}[p_{στ}Start_{τ}] =Hotel_{ρ}∧LocationOfSheila_{ρσ}[p_{στ}Finish_{τ}] =Farm_{ρ}∧LocationOfOstrich_{ρσ}[p_{στ}Finish_{τ}] =Farm_{ρ}∧LocationOfCheetah_{ρσ}[p_{στ}Finish_{τ}] =Farm_{ρ}∧∀ 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_{στ}∧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+_{ο()()} *f*_{} *g*_{}]
means that
*g*_{}
is an iterate of
*f*_{}.
ITERATE+_{ο()()}
is defined (inductively) as

λf_{}λg_{}∀p_{ο()}[p_{ο()}f_{}∧ ∀j_{}[p_{ο()}j_{}⊃p_{ο()}[λx_{}f_{}[j_{}x_{}]]] ⊃p_{ο()}g_{}].

Thus, *g* is an iterate of *f* if *g* is in every
set *p* of functions which contains *f* and which
contains the function [λ*x*_{}*f*_{}[*j*_{}*x*_{}]]
(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

∀f_{}[∃g_{}[ITERATE+_{ο()()}f_{}g_{}∧ ∃x_{}[g_{}x_{}=x_{}∧ ∀z_{}[g_{}z_{}=z_{}⊃z_{}=x_{}] ] ] ⊃

∃y_{}[f_{}y_{}=y_{}] ].

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

*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**_{α}.- β-
*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**_{α}. - β-
*expansion*. To infer**C**from**D**if**D**can be inferred from**C**by a single application of β-contraction. *Substitution*. From**F**_{(οα)}**x**_{α}, to infer**F**_{(οα)}**A**_{α}, provided that**x**_{α}is not a free variable of**F**_{(οα)}.*Modus Ponens*. From [**A**_{ο}⊃**B**_{ο}] and**A**_{ο}, to infer**B**_{ο}.*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_{ο}
∨
p_{ο}] ⊃ p_{ο} |

(2) | p_{ο} ⊃
[p_{ο}
∨
q_{ο}] |

(3) | [p_{ο}
∨
q_{ο}] ⊃
[q_{ο}
∨
p_{ο}] |

(4) | [p_{ο} ⊃
q_{ο}] ⊃
[[r_{ο}
∨
p_{ο}]
⊃
[r_{ο}
∨
q_{ο}] ] |

(5^{α}) |
Π_{ο(οα)} f_{(οα)}
⊃ f_{(οα)} x_{α} |

(6^{α}) |
∀x_{α}[p_{ο}
∨
f_{(οα)}x_{α}]
⊃
[p_{ο}
∨
Π_{ο(οα)} 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
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
T .
(The proof is actually quite inefficient, since line 3 is not used later,
and line 7 can be derived directly from line 5 without using line 6.)
Following each wff of the proof, we indicate how it was
inferred.^{[1]}

1. | ∀x_{}[p_{ο}
∨
f_{ο}x_{}]
⊃ [p_{ο}
∨
Π_{ο(ο)}
f_{ο}] |
Axiom 6^{} |

2. | [λf_{ο} [∀x_{}[p_{ο}
∨
f_{ο}x_{}]
⊃
[p_{ο}
∨
Π_{ο(ο)} f_{ο}] ] ]f_{ο} |
β-expansion: 1 |

3. | Π_{ο(ο(ο))}[λf_{ο} [∀x_{}[p_{ο}
∨
f_{ο}x_{}]
⊃
[p_{ο}
∨
Π_{ο(ο)}f_{ο}] ] ] |
Generalization: 2 |

4. | [λf_{ο} [∀x_{}[p_{ο}∨f_{ο}x_{}]
⊃
[p_{ο} ∨
Π_{ο(ο)}f_{ο}] ] ] [λx_{} r_{ο}x_{}] |
Substitution: 2 |

5. | ∀x_{}[p_{ο}
∨
[λx_{} r_{ο}x_{}]x_{}]
⊃
[p_{ο}
∨
Π_{ο(ο)}[λx_{} r_{ο}x_{}] ] |
β-contraction: 4 |

6. | ∀x_{}[p_{ο}
∨
[λy_{} r_{ο}y_{}]x_{}]
⊃
[p_{ο}
∨
Π_{ο(ο)}[λx_{} r_{ο}x_{}] ] |
α-conversion: 5 |

7. | ∀x_{}[p_{ο}
∨
r_{ο}x_{}]
⊃
[p_{ο}
∨
Π_{ο(ο)}[λx_{} r_{ο}x_{}] ] |
β-contraction: 6 |

Note that (3) can be written as

(3′) ∀f_{ο}[∀x_{}[p_{ο}∨f_{ο}x_{}] ⊃ [p_{ο}∨ Π_{ο(ο)}f_{ο}] ]

and (7) can be written as

(7′) ∀x_{}[p_{ο}∨r_{ο}x_{}] ⊃ [p_{ο}∨ ∀x_{}r_{ο}x_{}]

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
,
interpret *p*_{ο} to mean "the gate was closed",
and interpret
*r*_{ο}
so that *r*_{ο}*x*_{} asserts
"*x*_{}
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

∃_{1}x_{α}A_{ο}

stands for

[λp_{οα}∃y_{α}[p_{οα}y_{α}∧ ∀z_{α}[p_{οα}z_{α}⊃z_{α}=y_{α}] ] [λx_{α}A_{ο}].

For example,

∃_{1}x_{α}P_{οα}x_{α}

stands for

[λp_{οα}∃y_{α}[p_{οα}y_{α}∧ ∀z_{α}[p_{οα}z_{α}⊃z_{α}=y_{α}] ] [λx_{α}P_{οα}x_{α}].

By λ-conversion, this is equivalent to:

∃y_{α}[[λx_{α}P_{οα}x_{α}]y_{α}∧ ∀z_{α}[[λx_{α}P_{οα}x_{α}]z_{α}⊃z_{α}=y_{α}] ]

which reduces by λ-conversion to:

∃y_{α}[P_{οα}y_{α}∧ ∀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,
∃_{1}**x**_{α} **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
**x**_{α}**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
**x**_{α}**A**_{ο}
is defined as
ι_{α(οα)}[λ**x**_{α} **A**_{ο}].
Thus, 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^{α}) ∃_{1}x_{α}[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
∃_{1}**x**_{α}**A**_{ο},
then by using Axiom 8^{α}
one can derive

[λx_{α}A_{ο}][ι_{α(οα)}[λx_{α}A_{ο}] ],

which can also be written as

[λx_{α}A_{ο}](x_{α})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_{ρ}(x_{ρ})[×_{ρρρ}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
∃_{1}*x*_{ρ}[×_{ρρρ}*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
(**x**_{α})**A**_{ο}
means "an **x**_{α} such that
**A**_{ο}" when there is some such
element **s**_{α}.

It is natural to call
a definite description operator in contexts where
(**x**_{α})**A**_{ο}
means "the **x**_{α} such that
**A**_{ο}", and to call it an
indefinite description operator in contexts where
(**x**_{α})**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.
Q_{0}
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:

- If α ≥ β, then
Q
_{0}⊦ AC^{α}⊃ AC^{β}. - Given a set
*S*of types, none of which is propositional, there is a model of Q_{0}in which AC^{α}fails if and only if α ≥ β for some β in*S*.

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, ∼_{(οο)},
∨_{((οο)ο)},
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
Q_{0}
of Church's type theory in which there are primitive constants
Q_{οαα}
detnoting equality, and ∼_{(οο)},
∨_{((οο)ο)},
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.
Q_{0}
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.

- Type symbols, improper symbols, and variables are defined as in Section 1.2.1.
- Logical constants:
Q
_{((οα)α)}, and ι_{((ο))}. - 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 [Q_{οοο}**A**_{ο}B_{ο}] -
*T*_{ο}stands for [Q_{οοο}= Q_{οοο}] -
*F*_{ο}stands for [λ*x*_{ο}*T*_{ο}] = [λ*x*_{ο}*x*_{ο}] -
Π
_{ο(οα)}stands for [Q_{ο(οα)(οα)}[λ*x*_{α}*T*_{ο}] ] -
[∀
**x**_{α}**A**] stands for [Π_{ο(οα)}[λ**x**_{α}**A**] ] -
∧
_{οοο}stands for [λ*x*_{ο}λ*y*_{ο}[[λ*g*_{οοο}[*g*_{οοο}*T*_{ο}*T*_{ο}]] = [λ*g*_{οοο}[*g*_{οοο}*x*_{ο}*y*_{ο}]]]] -
[
**A**_{ο}∧**B**_{ο}] stands for [∧_{οοο}**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*_{ο}
∧
*y*_{ο}
is true iff *x*_{ο} and
*y*_{ο} are both true, i.e., iff
⟨*T*_{ο},*T*_{ο}⟩
= ⟨*x*_{ο},*y*_{ο}⟩.
Hence
*x*_{ο}
∧
*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
ι_{((ο))}, one can define description
operators ι_{α(οα)}
for all types α.

Q_{0}
has the following single rule of inference and axioms:

Rule R:

FromCandA_{α}=B_{α}, to infer the result of replacing one occurrence ofA_{α}inCby an occurrence ofB_{α}, provided that the occurrence ofA_{α}inCis not (an occurrence of a variable) immediately preceded by λ.

Axioms forQ_{0}:

(1) [ g_{οο}T_{ο}∧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 thatA_{α}is free forxinB_{β}.(5) ι _{(ο)}[Q_{ο}y_{}] =y_{}

## 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
{D_{α}}_{α}
of nonempty domains (sets)
D_{α},
one for each type symbol α, such that
D_{ο} =
{T,F}
(where T represents truth and
F represents falsehood),
and
D_{αβ}
is some collection of functions mapping
D_{β}
into
D_{α}.
The members of
D_{}
are called *individuals*.

An *interpretation*
⟨{D_{α}}_{α},
ℑ⟩
consists of a frame and a function ℑ
which maps each constant
*C* of type α
to an appropriate element of
D_{α},
which is called the *denotation of* *C*.

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

An interpretation
M =
⟨{D_{α}}_{α},
ℑ⟩
is a *general model* iff there is a binary function
V
such that
V_{φ}**A**_{α}
∈
D_{α}
for each assignment φ and wff
**A**_{α},
and the following conditions are satisfied for all assignments and
all wffs:

- V
_{φ}**x**_{α}= φ**x**_{α}for each variable**x**_{α}. - V
_{φ}*A*_{α}= ℑ*A*_{α}if*A*_{α}is a primitive constant. - V
_{φ}[**A**_{αβ}**B**_{β}] = (V_{φ}**A**_{αβ})(V_{φ}**B**_{β}) (the value of a function V_{φ}**A**_{αβ}at the argument V_{φ}**B**_{β}). - V
_{φ}[λ**x**_{α}**B**_{β}] = that function from D_{α}into D_{β}whose value for each argument*z*∈ D_{α}is V_{ψ}**B**_{β}, where ψ is that assignment such that ψ**x**_{α}=*z*and ψ**y**_{β}= φ**y**_{β}if**y**_{β}≠**x**_{α}.

If an interpretation
M
is a general model, the function
V
is uniquely determined.
V_{φ}**A**_{α}
is called the *value* of **A**_{α}
in
M
with respect to φ.

An interpretation
⟨{D_{α}}_{α},
ℑ⟩
is a *standard model* iff
for all α and β,
D_{αβ}
is the set of all functions from
D_{β}
into
D_{α}.
Clearly a standard model is a general model.

We say that a wff **A** is *valid* in a model
M
iff
V_{φ}**A**
= T
for every assignment φ into
M.
A model for a set
H
of wffs is a model in which each wff of
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
Q_{0}
is standard (Andrews 2002, Theorem 5404), but every set of sentences
of
Q_{0}
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
M
= ⟨{D_{α}}_{α},
ℑ⟩
in which
D_{}
is infinite, and all the domains
D_{α}
are countable. Thus
D_{}
and
D_{ο}
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
D_{}
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.,
∼∃*g*_{ο}∀*f*_{ο}∃*j*_{}[*g*_{ο}*j*_{}
=
*f*_{ο}],
and considering what it means in a model. The theorem says that there is
no function
*g* ∈
D_{ο}
from
D_{}
into
D_{ο}
which has every set
*f*_{ο}
∈
D_{ο}
in its range. The usual interpretation of the statement is that
D_{ο}
is bigger (in cardinality) than
D_{}.
However, what it actually means in this model is that *h*
cannot be in
D_{ο}.
Of course, M must be nonstandard.

While the Axiom of Choice is presumably true in all standard models,
there is a nonstandard model for
Q_{0}
in which
AC^{}
is false (Andrews 1972b). Thus,
AC^{}
is not provable in
Q_{0}.

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, Brown 2004,
Brown 2007, and Muskens 2007.

## 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 byB_{αβ}, providedy_{β}does not occur free inB_{αβ}.

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. Ahigher-order unifierfor a pair ⟨A,B⟩ of wffs is a substitution θ for free occurrences of variables such that θAand θBhave 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:

- Even when a unifier for a pair of wffs exists, there may be no most general unifier (Gould 1966).
- 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 T of section Section 1.3.2) in Andrews 1971 by applying ideas in Takahashi 1967.

This Unifying Principle for T has been used to establish cut-elimination for 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 wffs_{0}is anabstract consistency propertyiff for all finite sets S of wffs_{0}, the following properties hold (for all wffsA, B):

- If Γ(S), then there is no atom
Asuch thatA∈ S and [∼A] ∈ S.- If Γ(S ∪ {
A}), then Γ(S ∪ ↓A}).- If Γ(S ∪ {∼ ∼
A}), then Γ(S ∪ {A}).- If Γ(S ∪ {[
A∨B]}), then Γ (S ∪ {A}) or Γ(S ∪ {B}).- If Γ (S ∪ {∼[
A∨B]}), then Γ(S ∪ {∼A,∼B}).- If Γ(S ∪ {Π
_{ο(οα)}A_{οα}}), then Γ(S ∪ {Π_{ο(οα)}A_{οα},A_{οα}B_{α}}) for each wffB_{α}.- If Γ(S ∪ {∼Π
_{ο(οα)}A_{οα}}), then Γ(S ∪ {∼A_{οα}c_{α}}), for any variable or parameterc_{α}which does not occur free inA_{οα}or any wff in S.

Note that *consistency* is an abstract consistency property.

Unifying Principle forT .

If Γ is an abstract consistency property and Γ(S), then S is consistent in T .

Here is a typical application of the Unifying Principle. Suppose
there is a procedure
M
which can be used to refute sets of sentences,
and we wish to show it is complete for
T .
For any set of sentences, let
Γ(S)
mean that
S
is not refutable by
M,
and show that Γ is an abstract consistency property. Now
suppose that **A** is a theorem of
T .
Then {∼**A**} is inconsistent in
T ,
so by the Unifying Principle not
Γ({∼**A**}),
so {∼**A**} is refutable by
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 and Brown 2007, 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
Q_{0}^{1}
obtained by adding to
Q_{0}
the additional axiom
∀*x*_{}∀*y*_{}[*x*_{}=*y*_{}]
is decidable.

Although the system 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 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
∃**x**^{1}…∃**x**^{n}[**A**=**B**]
is a theorem of T
iff there is a substitution θ
such that
θ**A**
conv θ**B**. In particular,
⊦**A**=**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
T
changes drastically when axioms of extensionality are
added to
T .
⊦∃**x**_{β}[**A**=**B**]
iff there is a wff
**E**_{β} such that
⊦[λ**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
∀**x**^{1}…∀**x**^{n}**C**, where **C** is
quantifier-free, is provable in
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 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),
LEO-II (Benzmüller *et al*. 2008),
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

- Andrews, P., 1963, "A Reduction of the Axioms for the Theory of
Propositional Types",
*Fundamenta Mathematicae*, 52: 345–350. - Andrews, P., 1971, "Resolution in Type Theory",
*Journal of Symbolic Logic*, 36: 414–432. - Andrews, P., 1972a, "General Models and Extensionality",
*Journal of Symbolic Logic*, 37: 395–397. - Andrews, P., 1972b, "General Models, Descriptions, and Choice in
Type Theory",
*Journal of Symbolic Logic*, 37: 385–394. - Andrews, P., 1974, "Provability in Elementary Type Theory",
*Zeitschrift fur Mathematische Logic und Grundlagen der Mathematik*, 20: 411–418. - Andrews, P., 2001, "Classical Type Theory", in A. Robinson and
A. Voronkov (eds.),
*Handbook of Automated Reasoning*, Volume 2/Chapter 15, Amsterdam: Elsevier Science, pp. 965–1007. - Andrews, P., 2002,
*An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof*, Dordrecht: Kluwer Academic Publishers, second edition. - Andrews, P., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., and
Xi, H., 1996, "TPS: A Theorem Proving System for Classical Type Theory",
*Journal of Automated Reasoning*, 16: 321–353. - Andrews, P., and Brown, C., 2006, "TPS: A Hybrid
Automatic-Interactive System for Developing Proofs",
*Journal of Applied Logic*, 4: 367-395. - Baader, F., and Snyder, W., 2001, "Unification theory", in
A. Robinson and A. Voronkov (eds.),
*Handbook of Automated Reasoning*, Volume 1/Chapter 8, Amsterdam: Elsevier Science, pp. 445–533. - Barendregt, H. P., 1984,
*The λ-Calculus*, Series: Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland. - Benzmüller, C., 1999,
*Equality and Extensionality in Automated Higher-Order Theorem Proving*, Ph.D. dissertation, Computer Science Department, Universität des Saarlandes. - Benzmüller, C., Brown, C., and Kohlhase, M., 2004,
"Higher-Order Semantics and Extensionality",
*Journal of Symbolic Logic*, 69: 1027–1088. - Benzmüller, C., and Kohlhase, M., 1998a, "Extensional Higher-Order Resolution", in Kirchner and Kirchner 1998, pp. 56–71.
- Benzmüller, C., and Kohlhase, M., 1998b, "System Description: LEO — A Higher-Order Theorem Prover", in Kirchner and Kirchner 1998, pp. 139–143.
- Benzmüller, C., Paulson, L, Theiss, F., and Fietzke, A., 2008,
"LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic."
in A. Armando and P. Baumgartner and G. Dowek (eds.),
*Fourth International Joint Conference on Automated Reasoning (IJCAR'08)*, Lecture Notes in Artifical Intelligence, volume 5195, Springer, pp. 162–170. - Brown, C., 2004,
*Set Comprehension in Church's Type Theory*, Ph.D. dissertation, Department of Mathematical Sciences, Carnegie Mellon University. - Brown, C., 2007,
*Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church's Type Theory*, Studies in Logic: Logic and Cognitive Systems, volume 10, College Publications. - Büchi, J. R., 1953, "Investigation of the Equivalence of the
Axiom of Choice and Zorn's Lemma from the Viewpoint of the Hierarchy
of Types",
*Journal of Symbolic Logic*, 18: 125–135. - Church, A., 1932, "A set of postulates for the foundation of logic
(1)",
*Annals of Mathematics*, 33: 346–366. - Church, A., 1940, "A Formulation of the Simple Theory of Types",
*Journal of Symbolic Logic*, 5: 56–68. - Church, A., 1941,
*The Calculi of Lambda-Conversion*. Series: Annals of Mathematics Studies, Volume 6, Princeton: Princeton University Press. - Dowek, G., 2001, "Higher-Order Unification and Matching",
in A. Robinson and A. Voronkov, editors,
*Handbook of Automated Reasoning*, Volume 2/Chapter 16, Amsterdam: Elsevier Science, pp. 1009–1062. - Dowek, G., and Werner, B., 2003, "Theorem Proving Modulo",
*Journal of Symbolic Logic*, 68: 1289–1316. - Farmer, W., 2008,
"Seven Virtues of Simple Type Theory",
*Journal of Applied Logic*, 6:267–286. - Gödel, K., 1931, "Über formal unentscheidbare Sätze
der Principia Mathematica und verwandter Systeme I",
*Monatshefte für Mathematik und Physik*, 38: 173–198. - Goldfarb, W., 1981, "The Undecidability of the Second-Order
Unification Problem",
*Theoretical Computer Science*, 13: 225–230. - Gordon, M., 1986, "Why higher-order logic is a good formalism for
specifying and verifying hardware", in G. J. Milne and
P. A. Subrahmanyam (eds.),
*Formal Aspects of VLSI Design*, Amsterdam: North-Holland, pp. 153–177. - Gordon, M. J. C., 1988, "HOL: A Proof Generating System for
Higher-Order Logic", in G. Birtwistle and P.A. Subrahmanyam (eds.),
*VLSI Specification, Verification, and Synthesis*, Dordrecht: Kluwer Academic Publishers, pp. 73–128. - Gordon, M.J., and Melham, T.F., 1993,
*Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic*, Cambridge: Cambridge University Press. - Gould, W. E., 1966,
*A Matching Procedure for ω-order Logic*, Ph.D. dissertation, Mathematics Department, Princeton University. - Henkin, L., 1950, "Completeness in the Theory of Types",
*Journal of Symbolic Logic*, 15: 81–91. - Henkin, L., 1963, "A Theory of Propositional Types",
*Fundamenta Mathematicae*, 52: 323–344. - Hilbert, D., 1928, "Die Grundlagen der Mathematik",
*Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität*, 6: 65–85; translated in van Heijenoort 1967, pp. 464–479. - Huet, G. P., 1973a, "A Mechanization of Type Theory", in
*Proceedings of the Third International Joint Conference on Artificial Intelligence*(Stanford University), Los Altos, CA: William Kaufman, pp. 139–146. - Huet, G. P., 1973b, "The Undecidability of Unification in
Third-order Logic",
*Information and Control*, 22: 257–267. - Huet, G. P., 1975, "A Unification Algorithm for Typed
λ-Calculus",
*Theoretical Computer Science*, 1: 27–57. - Jensen, D. C., Pietrzykowski, T., 1976,
"Mechanizing ω-Order Type Theory Through Unification",
*Theoretical Computer Science*, 3: 123–171. - Kirchner, C., and Kirchner, H. (eds.), 1998,
*Proceedings of the 15th International Conference on Automated Deduction*, Series:*Lecture Notes in Artificial Intelligence*, Volume 1421, London: Springer-Verlag. - Kohlhase, M., 1993, "A Unifying Principle for Extensional Higher-Order Logic", Technical Report 93-153, Department of Mathematics, Carnegie Mellon University.
- Kohlhase, M., 1995, "Higher-Order Tableaux", in P. Baumgartner,
R. Hähnle, and J. Posegga (eds.),
*Theorem Proving with Analytic Tableaux and Related Methods*(4th International Workshop, TABLEAUX '95, Schloß; Rheinfels, St. Goar, Germany, May 1995), Series: Lecture Notes in Artificial Intelligence, Volume 918, Berlin: Springer-Verlag. - Kohlhase, M., 1998, "Higher-Order Automated Theorem Proving", in
Wolfgang Bibel and Peter Schmitt (eds.),
*Automated Deduction — A Basis for Applications*, Volume 1, Dordrecht: Kluwer, pp. 431–462. - Konrad, K., 1998, "HOT: A Concurrent Automated Theorem Prover
Based on Higher-Order Tableaux", in J. Grundy and M. Newey (eds.),
*Theorem Proving in Higher Order Logics*(11th International Conference, TPHOLs'98, Canberra, Australia), Series: Lecture Notes in Computer Science, Volume 1479, Berlin: Springer-Verlag, pp. 245–261. - Maslov, S. Ju., 1967, "An Inverse Method for Establishing
Deducibility of Nonprenex Formulas of Predicate Calculus",
*Soviet Mathematics Doklady*, 8: 16–19. - Miller, D. A., 1983,
*Proofs in Higher-Order Logic*, Ph.D. dissertation, Mathematics Department, Carnegie Mellon University. - Miller, D. A., 1987, "A Compact Representation of Proofs",
*Studia Logica*, 46/4: 347–370. - Muskens, R., 2007, "Intensional Models for the Theory of Types",
*Journal of Symbolic Logic*, 72: 98–118. - Owre, S., Rajan, S., Rushby, J.M., Shankar, N., and Srivas, M.,
1996, "PVS: Combining Specification, Proof Checking, and Model
Checking", in R. Alur and T. A. Henzinger (eds.),
*Computer-Aided Verification*, Series: Lecture Notes in Computer Science, Volume 1102, Berlin: Springer-Verlag, pp. 411–414. - Prawitz, D., 1968, "Hauptsatz for Higher Order Logic",
*Journal of Symbolic Logic*, 33: 452–457. - Quine, W. V., 1937, "Logic Based on Inclusion and Abstraction",
*Journal of Symbolic Logic*, 2: 145–152. - Russell, B., 1903,
*The Principles of Mathematics*, Cambridge: Cambridge University Press. - Russell, B., 1908, "Mathematical Logic as Based on the Theory of
Types",
*American Journal of Mathematics*, 30: 222–262; reprinted in van Heijenoort 1967, pp. 150–182. - Schönfinkel, M., 1924, "Über die Bausteine der
mathematischen Logik",
*Mathematische Annalen*, 92: 305–316; translated in van Heijenoort 1967, pp. 355–366. - Shankar, N., 2001, "Using Decision Procedures with a Higher-Order
Logic", in R. J. Boulton and P. B. Jackson (eds.),
*Theorem Proving in Higher Order Logics*(14th international conference, TPHOLs 2001, Edinburgh, Scotland), Series: Lecture Notes in Computer Science, Volume 2152, Berlin: Springer-Verlag, pp. 5–26. - Smullyan, R. M., 1963, "A Unifying Principle in Quantification Theory",
*Proceedings of the National Academy of Sciences*(U.S.A.), 49: 828–832. - Smullyan, R. M., 1995,
*First-Order Logic*, New York: Dover, second corrected edition. - Stenlund, S., 1972,
*λ-terms and Proof Theory*, Dordrecht: D. Reidel. - Takahashi, M., 1967, "A Proof of Cut-Elimination Theorem in Simple
Type Theory",
*Journal of the Mathematical Society of Japan*, 19: 399–410. - Takahashi, M., 1970, "A System of Simple Type Theory of Gentzen
Style with Inference on Extensionality, and the Cut Elimination in it",
*Commentarii Mathematici Universitatis Sancti Pauli*, 18: 129–147. - Tarski, A., 1923, "Sur le terme primitif de la Logistique",
*Fundamenta Mathematicae*, 4: 196–200; translated in Tarski 1956, 1–23. - Tarski, A., 1956,
*Logic, Semantics, Metamathematics*, Oxford: Oxford University Press. - van Heijenoort, J., 1967,
*From Frege to Gödel. A Source Book in Mathematical Logic 1879–1931*, Cambridge, MA: Harvard University Press. - Whitehead, A. N., and Russell, B., 1927a,
*Principia Mathematica*, Volume 1, Cambridge: Cambridge University Press, second edition. - Whitehead, A. N., and Russell, B., 1927b, "Incomplete Symbols", in Whitehead & Russell 1927a, 66–84; reprinted in van Heijenoort 1967, 216–223.
- Yasuhara, M., 1975, "The Axiom of Choice in Church's Type Theory"
(abstract),
*Notices of the American Mathematical Society*, 22 (January): A-34.

## Other Internet Resources

- Mathematics Genealogy Project, Mathematics Department, North Dakota State University.

## Related Entries

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

### Acknowledgments

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