Church's Type Theory

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. It also plays an important role in the study of the formal semantics of natural language.

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
  • 1.2 Formulas
  • 1.3 Axioms and Rules of Inference
  • 1.4 A Formulation Based on Equality
• 2. Semantics
• 3. Metatheory
  • 3.1 λ-conversion
  • 3.2 Higher-order Unification
  • 3.3 A Unifying Principle
  • 3.4 Cut-elimination
  • 3.5 Expansion Proofs
  • 3.6 The Decision Problem
• 4. Application of Church's Type Theory to Semantics of Natural Language
• 5. Automation
• Bibliography
• Academic Tools
• 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 2 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. 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.]
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: ∼_(οο), ∨_((οο)ο), Π_(ο(οα)), ι_(α(οα)) (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.
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_ο ∨ B_ο] stands for [[∨_((oo)o) A_ο] B_ο].
2. [A_ο ⊃ B_ο] stands for [[∼_(οο) A_ο] ∨ B_ο].
3. [∀x_αA_ο] stands for [Π_(ο(οα)) [λx_α A_ο]].
4. Other propositional connectives, and the existential quantifier, are defined in familiar ways. In particular,

   [A_ο ≡ B_ο] stands for [[A_ο ⊃ B_ο] ∧ [B_ο ⊃ A_ο]].

5. Q_οαα stands for [λx_αλy_α ∀f_(οα)[f_(οα)x_α ⊃ f_(οα)y_α]].
6. [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_ο()[λxf[jx]]] ⊃ 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 [λxf[jx]] (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[gx = x ∧ ∀z[gz = z ⊃ z = x] ] ] ⊃
       ∃y[fy = 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

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ο ∨ 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

∃₁x_αA_ο

stands for

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

For example,

∃₁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, ∃₁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^α) ∃₁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 ∃₁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⁻¹. Thus z⁻¹ is defined to be that x such that z × x = 1. When Z is provably not 0, we will be able to prove ∃₁x_ρ[×_ρρρZ x_ρ = 1_ρ] and Z × Z⁻¹ = 1, but if we cannot establish that Z is not 0, nothing significant about Z⁻¹ 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₀ 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₀ ⊦ AC^α ⊃ AC^β.
• Given a set S of types, none of which is propositional, there is a model of Q₀ 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, section 57 of Church 1956, and section 60 of Andrews 2002.

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₀ of Church's type theory in which there are primitive constants Q_οαα denoting 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 (1956) showed how both quantifiers and connectives can be defined in terms of equality and the abstraction operator λ in the context of Church's type theory. Henkin (1963) rediscovered these definitions, and developed a formulation of Church's type theory based on equality in which he restricted attention to propositional types. Andrews (1963) simplified the axioms for this system.

Q₀ 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. More details about Q₀ can be found in Andrews 2002.

1. Type symbols, improper symbols, and variables are defined as in Section 1.2.1.
2. Logical constants: Q_((οα)α), and ι_((ο)).
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 [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₀ 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 Q₀:

(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 that Aα is free for x in Bβ.
(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:

1. V_φx_α = φx_α for each variable x_α.
2. V_φA_α = ℑA_α if A_α is a primitive constant.
3. V_φ[A_αβB_β] = (V_φA_αβ)(V_φB_β) (the value of a function V_φA_αβ at the argument V_φB_β).
4. 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₀ is standard (Andrews 2002, Theorem 5404), but every set of sentences of Q₀ 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₀ in which AC is false (Andrews 1972b). Thus, AC is not provable in Q₀.

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, Henkin 1975, 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 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 T  of 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_ο is an abstract consistency property iff for all finite sets S of wffs_ο, the following properties hold (for all wffs A, B):

1. If Γ(S), then there is no atom A such that A ∈ S and [∼A] ∈ S.
2. If Γ(S ∪ {A}), then Γ(S ∪ ↓A}).
3. If Γ(S ∪ {∼ ∼A}), then Γ(S ∪ {A}).
4. If Γ(S ∪ {[A ∨ B]}), then Γ (S ∪ {A}) or Γ(S ∪ {B}).
5. If Γ (S ∪ {∼[A ∨ B]}), then Γ(S ∪ {∼A,∼B}).
6. If Γ(S ∪ {Π_ο(οα)A_οα}), then Γ(S ∪ {Π_ο(οα)A_οα, A_οαB_α}) for each wff B_α.
7. If Γ(S ∪ {∼Π_ο(οα)A_οα}), then Γ(S ∪ {∼A_οαc_α}), for any variable or parameter c_α which does not occur free in A_οα or any wff in S.

Note that consistency is an abstract consistency property.

Unifying Principle for T .
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. A form of the Unifying Principle is used in Backes & Brown 2011 to prove the completeness of a tableau calculus for type theory which incorporates the Axiom of Choice.

3.4 Cut-elimination

Cut-elimination proofs for Church's type theory, which are often closely related to such proofs (Takahashi 1967 and 1970, Prawitz 1968, Mints 1999) for other formulations of type theory, may be found in Andrews 1971, Dowek & Werner 2003, and Brown 2004. In Benzmüller et al. 2009 it is shown how certain wffs_ο, such as axioms of extensionality, descriptions, choice, and induction, can be used to justify cuts in cut-free sequent calculi for elementary type theory.

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₀¹ obtained by adding to Q₀ 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¹…∃xⁿ[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¹…∀xⁿ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. Application of Church's Type Theory to Semantics of Natural Language

Church's type theory plays an important role in the study of the formal semantics of natural language. Pioneering work on this was done by Richard Montague. See his papers “English as a formal language”, “Universal grammar”, and “The proper treatment of quantification in ordinary English”, which are reprinted in Montague 1974. A crucial component of Montague's analysis of natural language is the definition of a tensed intensional logic (Montague 1974, 256), which is an enhancement of Church's type theory. Montague Grammar had a huge impact, and has since been developed in many further directions, not least in Categorical Grammar.

5. 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. 2008b), HOT (Konrad 1998), PVS (Owre et al. 1996, Shankar 2001), ProofPower, Isabelle/HOL (Nipkow et al. 2002), and Satallax (Brown 2012). 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.
• –––, 1971, “Resolution in Type Theory”, Journal of Symbolic Logic, 36: 414–432; reprinted in Siekmann & Wrightson 1983 and in Benzmüller et al. 2008b.
• –––, 1972a, “General Models and Extensionality”, Journal of Symbolic Logic, 37: 395–397; reprinted in Benzmüller et al. 2008b.
• –––, 1972b, “General Models, Descriptions, and Choice in Type Theory”, Journal of Symbolic Logic, 37: 385–394 reprinted in Benzmüller et al. 2008b.
• –––, 1974, “Provability in Elementary Type Theory”, Zeitschrift fur Mathematische Logic und Grundlagen der Mathematik, 20: 411–418.
• –––, 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.
• –––, 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; reprinted in Benzmüller et al. 2008b.
• 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.
• Backes, J., and Brown, C., 2011, “Analytic tableaux for higher-order logic with choice”, Journal of Automated Reasoning, 47(4): 451-479.
• 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., and Kohlhase, M., 1998a, “Extensional Higher-Order Resolution”, in Kirchner and Kirchner 1998, pp. 56–71.
• –––, 1998b, “System Description: LEO — A Higher-Order Theorem Prover”, in Kirchner and Kirchner 1998, pp. 139–143.
• Benzmüller, C., Brown, C., and Kohlhase, M., 2004, “Higher-Order Semantics and Extensionality”, Journal of Symbolic Logic, 69: 1027–1088.
• –––, 2009, “Cut-simulation and impredicativity”, Logical Methods in Computer Science, 5(1:6): 1–21.
• Benzmüller, C., Brown, C., Siekmann, J., and Statman, R. (eds.), 2008, Reasoning in Simple Type Theory (Festschrift in Honor of Peter B. Andrews on his 70th Birthday), King's College London: College Publications.
• 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), Berlin: Springer, pp. 162–170.
• Brown, C., 2004, Set Comprehension in Church's Type Theory, Ph.D. dissertation, Department of Mathematical Sciences, Carnegie Mellon University.
• –––, 2007, Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church's Type Theory (Studies in Logic: Logic and Cognitive Systems: Volume 10Z), London: College Publications.
• –––, 2012, ``Satallax: An automated higher-order prover'', in 6th International Joint Conference on Automated Reasoning (IJCAR 2012), U. Sattler, B. Gramlich, and D. Miller (eds.), Dordrecht: Springer, 111–117.
• 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.
• –––, 1940, “A Formulation of the Simple Theory of Types”, Journal of Symbolic Logic, 5: 56–68; reprinted in Benzmüller et al. 2008b.
• –––, 1941, The Calculi of Lambda-Conversion. Series: Annals of Mathematics Studies, Volume 6, Princeton: Princeton University Press.
• –––, 1956, Introduction to Mathematical Logic, Princeton, N.J.: Princeton University Press.
• Dowek, G., 2001, “Higher-Order Unification and Matching”, in A. Robinson and A. Voronkov (eds.), 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. Translated in Gödel 1986, 144–195, and in van Heijenoort 1967, 596–616.
• –––, 1986, Collected Works (Volume I), Oxford: Oxford University Press.
• Goldfarb, W., 1981, “The Undecidability of the Second-Order Unification Problem”, Theoretical Computer Science, 13: 225–230.
• Gordon, M. J. C., 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.
• –––, 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; reprinted in Hintikka 1969 and in Benzmüller et al. 2008b.
• –––, 1963, “A Theory of Propositional Types”, Fundamenta Mathematicae, 52: 323–344.
• –––, 1975, “Identity as a logical primitive”, Philosophia, 5(1–2): 31–45.
• 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.
• Hintikka, J. (ed.), 1969, The Philosophy of Mathematics, Oxford: Oxford University Press.
• 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.
• –––, 1973b, “The Undecidability of Unification in Third-order Logic”, Information and Control, 22: 257–267.
• –––, 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.
• –––, 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.
• –––, 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.
• –––, 1987, “A Compact Representation of Proofs”, Studia Logica, 46/4: 347–370.
• Mints, G., 1999, “Cut-elimination for simple type theory with an axiom of choice”, Journal of Symbolic Logic, 64: 479–485.
• Montague, Richard, 1974, Formal Philosophy. Selected Papers Of Richard Montague, edited and with an introduction by Richmond H. Thomason, New Haven: Yale University Press.
• Muskens, R., 2007, “Intensional Models for the Theory of Types”, Journal of Symbolic Logic, 72: 98–118.
• Nipkow, T., Paulson, L., and Wenzel, M., 2002, Isabelle/HOL – A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science: Vol. 2283), Berlin: Springer.
• 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., 1956, “Unification of universes in set theory” (abstract), Journal of Symbolic Logic, 21: 216.
• Russell, B., 1903, The Principles of Mathematics, Cambridge: Cambridge University Press.
• –––, 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.
• Siekmann, J., and Wrightson, G. (eds.), 1983, Automation of Reasoning (Classical Papers on Computational Logic 1967–1970: Vol. 2), Berlin: Springer-Verlag.
• Smullyan, R. M., 1963, “A Unifying Principle in Quantification Theory”, Proceedings of the National Academy of Sciences (U.S.A.), 49: 828–832.
• –––, 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.
• –––, 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.
• –––, 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.
• –––, 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): A34.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at the Friends of the SEP Society.
	Look up this entry topic at the Indiana Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entry at PhilPapers, with links to its database.

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.