## 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 a and b are types, the type
of functions from elements of type b to elements of type a
is written as \((\alpha \beta)\). (This notation was introduced by
Church, but some authors write \((\beta \rightarrow \alpha)\) instead
of \((\alpha \beta)\). 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
\(+\_{((\sigma \sigma)\sigma)}\), where \(\sigma\) is the type of
natural numbers. Given any number *x*, \([+\_{((\sigma
\sigma)\sigma)}x]\) is the function which, when applied to any number
*y*, gives the value \([[+\_{((\sigma \sigma)\sigma)}x]y]\),
which is ordinarily abbreviated as \(x + y\). Thus \([+\_{((\sigma
\sigma)\sigma)}x]\) is the function of one argument which adds
*x* to any number. When we think of \(+\_{((\sigma
\sigma)\sigma)}\) as a function of one argument, we see that it maps
any number *x* to the function \([+\_{((\sigma
\sigma)\sigma)}x]\).



More generally, if *f* is a function which maps
*n*-tuples \(\langle w\_{\beta},x\_{\gamma},\ldots
,y\_{\delta},z\_{\tau}\rangle\) of elements of types \(\beta\),
\(\gamma\),..., \(\delta\) ,\(\tau\), respectively, to elements
of type a, we may assign to *f* the type
\(((\ldots((\alpha \tau)\delta)\ldots \gamma)\beta)\). It is customary
to use the convention of association to the left to omit parentheses,
and write this type symbol simply as \((\alpha \tau \delta \ldots
\gamma \beta)\).



A set or property can be represented by a function (often called
*characteristic 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 \(s x\) means that \(s x\) is true, which also expresses
the assertions that *s* maps *x* to truth and that \(x
\in s\). In other words, \(x \in s\) iff \(s x\). We take \({o}\) as
the type symbol denoting the type of truth values, so we may speak of
any function of type \(({o}\alpha)\) as a *set* of elements of
type a. A function of type \((({o}\alpha)\beta)\) is a binary
relation between elements of type b and elements of type a.
For example, if \(\sigma\) is the type of the natural numbers, and
\(<\) is the order relation between natural numbers, \(<\) has
type \(({o}\sigma \sigma)\), and for all natural numbers *x*
and \(y, {<}x y\) (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. Church's type type theory is thus a logic of
functions, and, in this sense, it is in the tradition of the work of
Frege's *Begriffsschrift*. The opposite approach would be
to reduce functions to relations, which was the approach taken by
Whitehead and Russell (1927a) in the *Principia
Mathematica*.



Expressions which denote elements of type a are called
*well-formed formulas (wffs) of type* a. Thus, statements
of type theory are wffs of type \({o}\).



If \(\bA\_{\alpha}\) is a wff of type a in which \(\bu\_{\alpha
\beta}\) is not free, the function (associated with) \(\bu\_{\alpha
\beta}\) such that \(\forall \bv\_{\beta}[\bu\_{\alpha \beta}\bv\_{\beta}
= \bA\_{\alpha}]\) is denoted by \([\lambda \bv\_{\beta}\bA\_{\alpha}]\).
Thus \(\lambda \bv\_{\beta}\) is a variable-binder, like \(\forall
\bv\_{\beta}\) or \(\exists \bv\_{\beta}\) (but with a quite different
meaning, of course); l is known as an *abstraction
operator*. \([\lambda \bv\_{\beta}\bA\_{\alpha}]\) denotes the
function whose value on any argument \(\bv\_{\beta}\) is
\(\bA\_{\alpha}\), where \(\bv\_{\beta}\) may occur free in
\(\bA\_{\alpha}\). For example, \([\lambda n\_{\sigma}[4\cdot
n\_{\sigma}+3]]\) denotes the function whose value on any natural
number *n* is \(4\cdot n+3\). Hence, when we apply this
function to the number 5 we obtain \([\lambda n\_{\sigma}[4\cdot
n\_{\sigma}+3]]5 = 4\cdot 5+3 = 23\).



We use \(\textsf{Sub}(\bB,\bv,\bA)\) as a notation for the result of
substituting \(\bB\) for \(\bv\) in \(\bA\), and
\(\textsf{SubFree}(\bB,\bv,\bA)\) as a notation for the result of
substituting \(\bB\) for all free occurrences of \(\bv\) in \(\bA\).
The process of replacing \([\lambda
\bv\_{\beta}\bA\_{\alpha}]\bB\_{\beta}\) by
\(\textsf{SubFree}(\bB\_{\beta},\bv\_{\beta},\bA\_{\alpha})\) (or
vice-versa) is known as b-*conversion*, which is one form
of l-*conversion*. Of course, when \(\bA\_{{o}}\) is a
wff of type \({o}\), \([\lambda \bv\_{\beta}\bA\_{{o}}]\) denotes the
set of all elements \(\bv\_{\beta}\) (of type \(\beta)\) of which
\(\bA\_{{o}}\) is true; this set may also be denoted by
\(\{\bv\_{\beta}|\bA\_{{o}}\}\). For example, \([\lambda 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 if
it is less than *y*). In familiar set-theoretic notation,



\[[\lambda \bv\_{\beta} \bA\_{{o}}]\bB\_{\beta} = \textsf{SubFree}(\bB\_{\beta},\bv\_{\beta},\bA\_{{o}})\]


would be written

 
\[\bB\_{\beta} \in \{\bv\_{\beta}|\bA\_{{o}}\} \equiv \textsf{SubFree}(\bB\_{\beta},\bv\_{\beta},\bA\_{{o}}).\]


(By the Axiom of Extensionality for truth values, when \(\bC\_{{o}}\)
and \(\bD\_{{o}}\) are of type \({o}, \bC\_{{o}} \equiv \bD\_{{o}}\) is
equivalent to \(\bC\_{{o}} = \bD\_{{o}}\).)



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 \(({o}{o})\). Similarly,
disjunction and conjunction (etc.) are binary functions from truth
values to truth values, so they have type \(({o}{o}{o})\).



The statement \(\forall \bx\_{\alpha}\bA\_{{o}}\) is true iff the set
\([\lambda \bx\_{\alpha}\bA\_{{o}}]\) contains all elements of type
a. A constant \(\Pi\_{{o}({o}\alpha)}\) can be introduced (for
each type symbol \(\alpha)\) to denote a property of sets: a set
\(s\_{{o}\alpha}\) has the property \(\Pi\_{{o}({o}\alpha)}\) iff
\(s\_{{o}\alpha}\) contains all elements of type a. With this
interpretation

 
\[ \forall s\_{{o}\alpha}\left[\Pi\_{{o}({o}\alpha)}s\_{{o}\alpha} \equiv \forall x\_{\alpha}\left[s\_{{o}\alpha}x\_{\alpha}\right]\right] \]


should be true, as well as

 
\[ \Pi\_{{o}({o}\alpha)}[\lambda \bx\_{\alpha}\bA\_{{o}}] \equiv \forall \bx\_{\alpha}[[\lambda \bx\_{\alpha}\bA\_{{o}}]\bx\_{\alpha}] \label{eqPi} \]


for any wff \(\bA\_{{o}}\) and variable \(\bx\_{\alpha}\). Since by
l-conversion we have

 
\[ [\lambda \bx\_{\alpha}\bA\_{{o}}]\bx\_{\alpha} \equiv \bA\_{{o}} \]


this equation can be written more simply as

 
\[ \Pi\_{{o}({o}\alpha)}[\lambda \bx\_{\alpha}\bA\_{{o}}] \equiv \forall \bx\_{\alpha}\bA\_{{o}} \]


Thus, \(\forall \bx\_{\alpha}\) can be defined in terms of
\(\Pi\_{{o}({o}\alpha)}\), and l is the only variable-binder
that is needed.


### 1.2 Formulas (as certain terms)



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. What
we call well-formed formula of type a (\(\text{wff}\_{\alpha}\))
below would in more standard terminology be called *term* of
type a, and then only certain terms, namely those with type
\({o}\), would be called formulas. Anyhow, in this entry we have
decided to stay with Church's original terminology. Another
remark concerns the use of some specific mathematical notation. In
what follows, the entry distinguishes between the symbols \(\imath\),
\(\iota\_{(\alpha({o}\alpha))}\), and \(\atoi\). The first is the
symbol used for the type of individuals; the second is the symbol used
for a logical constant (see
 Section 1.2.1
 below); the third is the symbol used as a variable-binding operator
that represents the definite description "the" (see
 Section 1.3.4).
 The reader should not confuse them and check to see that the browser
is displaying these symbols correctly.


#### 1.2.1 Definitions



*Type symbols* are defined inductively as follows:


* \(\imath\) is a type symbol (denoting the type of individuals).
There may also be additional primitive type symbols which are used in
formalizing disciplines where it is natural to have several sorts of
individuals.
* \({o}\) is a type symbol (denoting the type of truth values).
* If a and b are type symbols, then \((\alpha \beta)\) is
a type symbol (denoting the type of functions from elements of type
b to elements of type a).



The *primitive symbols* are the following:


* Improper symbols: [, ], \(\lambda\)
* For each type symbol a, a denumerable list of
*variables* of type \(\alpha : a\_{\alpha}, b\_{\alpha},
c\_{\alpha}\ldots\)
* Logical constants: \(\nsim\_{({o}{o})}\), \(\lor\_{(({o}{o}){o})}\),
\(\Pi\_{({o}({o}\alpha))}\) and \(\iota\_{(\alpha({o}\alpha))}\) (for
each type symbol a). The types of these constants are indicated
by their subscripts. The symbol \(\nsim\_{({o}{o})}\) denotes negation,
\(\lor\_{(({o}{o}){o})}\) denotes disjunction, and
\(\Pi\_{({o}({o}\alpha))}\) is used in defining the universal
quantifier as discussed above. \(\iota\_{(\alpha({o}\alpha))}\) 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.



A *formula* is a finite sequence of primitive symbols. Certain
formulas are called *well-formed formulas* (*wff*s). We
write \(\textrm{wff}\_{\alpha}\) as an abbreviation for *wff of
type* a, and define this concept inductively as follows:


* A primitive variable or constant of type a is a
wff\(\_{\alpha}\).
* If \(\bA\_{\alpha \beta}\) and \(\bB\_{\beta}\) are wffs of the
indicated types, then \([\bA\_{\alpha \beta}\bB\_{\beta}]\) is a
wff\(\_{\alpha}\).
* If \(\bx\_{\beta}\) is a variable of type b and
\(\bA\_{\alpha}\) is a wff, then \([\lambda \bx\_{\beta}\bA\_{\alpha}]\)
is a wff\(\_{(\alpha \beta)}\).



Note, for example, that by (a) \(\nsim\_{({o}{o})}\) is a
wff\(\_{({o}{o})}\), so by (b) if \(\bA\_{{o}}\) is a wff\(\_{{o}}\),
then \([\nsim\_{({o}{o})}\bA\_{{o}}]\) is a wff\(\_{{o}}\). Usually, the
latter wff will simply be written as \(\nsim \bA\). It is often
convenient to avoid parentheses, brackets and type symbols, and use
conventions for omitting them. For formulas we use the convention of
association to the right, and we may write \(\lor\_{((oo)o)}\bA\_{{o}}
\bB\_{{o}}\) instead of \([[\lor\_{((oo)o)}\bA\_{{o}}] \bB\_{{o}}]\). For
types the corresponding convention is analogous.


##### Abbreviations:


* \(\bA\_{{o}} \lor \bB\_{{o}}\) stands for \(\lor\_{ooo}\bA\_{{o}}
\bB\_{{o}}\).
* \(\bA\_{{o}} \supset \bB\_{{o}}\) stands for
\([\nsim\_{{o}{o}}\bA\_{{o}}] \lor \bB\_{{o}}\).
* \(\forall \bx\_{\alpha}\bA\_{{o}}\) stands for
\(\Pi\_{{o}({o}\alpha)} [\lambda \bx\_{\alpha}\bA\_{{o}}]\).
* Other propositional connectives, and the existential quantifier,
are defined in familiar ways. In particular, 
\[ {\bA\_{{o}} \equiv \bB\_{{o}} \quad \text{stands for} \quad [\bA\_{{o}} \supset \bB\_{{o}}] \land [\bB\_{{o}} \supset \bA\_{{o}}]} \]
* \(\sfQ\_{{o}\alpha \alpha}\) stands for \(\lambda
\)x\(\_{\alpha}\lambda \)y\(\_{\alpha}\forall
f\_{{o}\alpha}{[}f\_{{o}\alpha} x\_{\alpha} \supset
f\_{{o}\alpha}y\_{\alpha}{]}\).
* \(\bA\_{\alpha} = \bB\_{\alpha}\) stands for \(\sfQ\_{{o}\alpha
\alpha}\bA\_{\alpha}\bB\_{\alpha}\).



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.



**Example 1** To express the assertion that
"Napoleon is charismatic" we introduce constants
\(\const{Charismatic}\_{{o}\imath}\) and \(\const{Napoleon}\_{\imath}\),
with the types indicated by their subscripts and the obvious meanings,
and assert the wff

 
\[\const{Charismatic}\_{{o}\imath} \const{Napoleon}\_{\imath}\]


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
\(\const{GreatGeneral}\_{{o}\imath}\) is added to the formal language,
this can be expressed by the wff

 
\[\forall p\_{{o}\imath}[\forall g\_{\imath}{[}\const{GreatGeneral}\_{{o}\imath}g\_{\imath} \supset p\_{{o}\imath}g\_{\imath}] \supset p\_{{o}\imath} \const{Napoleon}\_{\imath}]\]


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

 
\[\forall x\_{\imath}{[}\const{Soldier}\_{{o}\imath}x\_{\imath} \land \const{CommanderOf}\_{\imath\imath}x\_{\imath} = \const{Napoleon}\_{\imath} \supset \const{Admires}\_{{o}\imath\imath}x\_{\imath}\const{Napoleon}\_{\imath}]\]


By l-conversion, this is equivalent to

 
\[[\lambda n\_{\imath}\forall x\_{\imath}{[}\const{Soldier}\_{{o}\imath}x\_{\imath} \land \const{CommanderOf}\_{\imath\imath}x\_{\imath} = n\_{\imath} \supset \const{Admires}\_{{o}\imath\imath}x\_{\imath}n\_{\imath}]]\, \const{Napoleon}\_{\imath}\]


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

 
\[\lambda n\_{\imath}\forall x\_{\imath}{[}\const{Soldier}\_{{o}\imath}x\_{\imath} \land \const{CommanderOf}\_{\imath\imath}x\_{\imath} = n\_{\imath} \supset \const{Admires}\_{{o}\imath\imath}x\_{\imath}n\_{\imath}]\]


**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
\(\const{Hotel}\) and moment \(\const{Start}\), and end it at the
location \(\const{Farm}\) and moment \(\const{Finish}\). Moments will
have type \(\tau\), and locations will have type \(\varrho\). A
*state* will have type \(\sigma\) 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 \((\sigma \tau)\). The exact representation of
states need not concern us, but there will be functions from states to
locations called \(\const{LocationOfSheila}\),
\(\const{LocationOfOstrich}\), and \(\const{LocationOfCheetah}\) which
provide the indicated information. Thus,
\(\const{LocationOfSheila}\_{\varrho \sigma}[p\_{\sigma \tau}t\_{\tau}]\)
will be the location of Sheila according to plan \(p\_{\sigma \tau}\)
at moment \(t\_{\tau}\). The set \(\const{Proposals}\_{{o}(\sigma
\tau)}\) 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 \(\const{Acceptable}\_{{o}(\sigma \tau)}\)
as

 
\[\begin{multline}
\lambda p\_{\sigma \tau} \left[ \begin{aligned}
& \const{LocationOfSheila}\_{\varrho \sigma} [p\_{\sigma \tau}\const{Start}\_{\tau}] = \const{Hotel}\_{\varrho} \,\land\\
 & \const{LocationOfOstrich}\_{\varrho \sigma}[p\_{\sigma \tau} \const{Start}\_{\tau}] = \const{Hotel}\_{\varrho} \,\land\\
 & \const{LocationOfCheetah}\_{\varrho \sigma}[p\_{\sigma \tau} \const{Start}\_{\tau}] = \const{Hotel}\_{\varrho} \,\land\\
 & \const{LocationOfSheila}\_{\varrho \sigma}[p\_{\sigma \tau} \const{Finish}\_{\tau}] = \const{Farm}\_{\varrho} \,\land\\
 & \const{LocationOfOstrich}\_{\varrho \sigma}[p\_{\sigma \tau} \const{Finish}\_{\tau}] = \const{Farm}\_{\varrho} \,\land\\
 & \const{LocationOfCheetah}\_{\varrho \sigma}[p\_{\sigma \tau} \const{Finish}\_{\tau}] = \const{Farm}\_{\varrho} \,\land\\
 & \forall t\_{\tau} \left [ \begin{split}
& \const{Moments}\_{{o}\tau}t\_{\tau} \\
 & \supset \left [ \begin{split}
& \left[ \begin{split}
& \const{LocationOfOstrich}\_{\varrho \sigma}[p\_{\sigma \tau}t\_{\tau}] \\
 & = \const{LocationOfCheetah}\_{\varrho \sigma}[p\_{\sigma \tau}t\_{\tau}] 
\end{split} \right] \\
 & \supset \left[ \begin{split}
& \const{LocationOfSheila}\_{\varrho \sigma}[p\_{\sigma \tau}t\_{\tau}] \\
 & = \const{LocationOfCheetah}\_{\varrho\sigma}[p\_{\sigma\tau}t\_{\tau}] 
\end{split} \right] 
\end{split} \right] 
\end{split} \right] 
\end{aligned} \right] 
\end{multline}\]


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

 
\[\exists p\_{\sigma \tau}[\const{Proposals}\_{{o}(\sigma \tau)}p\_{\sigma \tau} \land \const{Acceptable}\_{{o}(\sigma \tau)}p\_{\sigma \tau}]\]


**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* from 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*.
\([\text{ITERATE+}\_{{o}(\imath\imath)(\imath\imath)}f\_{\imath\imath}g\_{\imath\imath}]\)
means that \(g\_{\imath\imath}\) is an iterate of \(f\_{\imath\imath}\).
\(\text{ITERATE+}\_{{o}(\imath\imath)(\imath\imath)}\) is defined
(inductively) as

 
\[ \lambda f\_{\imath\imath}\lambda g\_{\imath\imath}\forall p\_{{o}(\imath\imath)} \left [p\_{{o}(\imath\imath)}f\_{\imath\imath} \land \forall j\_{\imath\imath} \left [p\_{{o}(\imath\imath)}j\_{\imath\imath} \supset p\_{{o}(\imath\imath)} \left [\lambda x\_{\imath}f\_{\imath\imath} \left [j\_{\imath\imath}x\_{\imath} \right] \right] \right] \supset p\_{{o}(\imath\imath)}g\_{\imath\imath} \right] \]


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

 
\[\begin{aligned}
\forall f\_{\imath\imath} \left [ \begin{split}
\exists g\_{\imath\imath} & \left [ \begin{split}
&\text{ITERATE+}\_{{o}(\imath\imath)(\imath\imath)} f\_{\imath\imath} g\_{\imath\imath} \\
 &{} \land \exists x\_{\imath} \left [ \begin{split}
& g\_{\imath\imath}x\_{\imath} = x\_{\imath} \\
 &{} \land \forall z\_{\imath} \left [g\_{\imath\imath} z\_{\imath} = z\_{\imath} \supset z\_{\imath} = x\_{\imath} \right] 
\end{split} \right] 
\end{split} \right]\\
 & \supset { } \exists y\_{\imath} [f\_{\imath\imath}y\_{\imath} = y\_{\imath}] 
\end{split} \right]. 
\end{aligned}\]


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



**Example 4** An example from philosophy is
Godel's variant of the ontological argument for the
existence of God. This example illustrates two interesting
aspects:


* Church's type theory can be employed as a meta-logic to
concisely embed expressive other logics such as the higher-order modal
logic assumed by Godel. By exploiting the possible world
semantics of this target logic, its syntactic elements are defined in
such a way that the infrastructure of the meta-logic are reused as
much as possible. In this technique, called *shallow semantical
embedding*, the modal operator \(\Box\), for example, is simply
identified with (taken as syntactic sugar for) the
l-formula

 
\[\lambda \varphi\_{{o}\imath} \lambda w\_{\imath} \forall v\_{\imath} [R\_{{o}\imath\imath} w\_{\imath} v\_{\imath} \supset \varphi\_{{o}\imath} v\_{\imath}]\]


where \(R\_{{o}\imath\imath}\) denotes the accessibility relation
associated with \(\Box\) and type \({\imath}\) is identified with
possible worlds. Moreover, since \(\forall x\_{\alpha} [\bA\_{{o}\alpha}
x\_{\alpha}]\) is shorthand in Church's type theory for
\(\Pi\_{{o}({o}\alpha)} [\lambda x\_{\alpha} [\bA\_{{o}\alpha}
x\_{\alpha}]]\), the modal formula

 
\[\Box \forall x \bP x\]


is represented as

 
\[\Box \Pi' [\lambda x\_{\alpha} \lambda w\_{\imath} [\bP\_{{o}\imath\alpha} x\_{\alpha} w\_{\imath}]]\]


where \(\Pi'\) stands for the l-term

 
\[\lambda \Phi\_{{o}\imath\alpha} \lambda w\_{\imath} \forall x\_{\alpha} [\Phi\_{{o}\imath\alpha} x\_{\alpha} w\_{\imath}]\]


and the \(\Box\) gets resolved as described above. The above choice of
\(\Pi'\) realizes a possibilist notion of quantification. By
introducing a binary "existence" predicate in the
metalogic and by utilizing this predicate as an additional guard in
the definition of \(\Pi'\) an actualist notion of quantification can
be obtained. Expressing that an embedded modal formula
\(\varphi\_{{o}\imath}\) is globally valid is captured by the formula
\(\forall x\_{\imath} [\varphi\_{{o}\imath} x\_{\imath}]\). Local
validity (and also actuality) can be modeled as \(\varphi\_{{o}\imath}
n\_{\imath}\), where \(n\_{\imath}\) is a nominal (constant symbol in
the meta-logic) denoting a particular possible world.
* The above technique can be exploited for a natural encoding and
automated assessment of Godel's ontological argument in
higher-order modal logic, which unfolds into formulas in
Church's type theory such that higher-order theorem provers can
be applied. Further details are presented in Section 6 (Logic and
Philosophy) of the SEP entry on
 automated reasoning
 and also in
 Section 5.2;
 moreover, see Benzmuller & Woltzenlogel-Paleo 2014 and
Benzmuller 2019.



**Example 5** Suppose we omit the use of type symbols in
the definitions of wffs. Then we can write the formula \(\lambda
x\nsim[xx]\), which we shall call \(\textrm{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 \([\textrm{R R}]\),
which expresses the assertion that \(\textrm{R}\) is in itself. We can
clearly prove \([\textrm{R R}] \equiv [[\lambda x\nsim [xx]]
\textrm{R}]\), so by l-conversion we can derive \([\textrm{R
R}] \equiv\, \nsim[\textrm{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, \(\textrm{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*
\((\alpha\)-*conversion*). To replace any well-formed part
\(\lambda \bx\_{\beta}\bA\_{\alpha}\) of a wff by \(\lambda \by\_{\beta}
\textsf{Sub}(\by\_{\beta},\bx\_{\beta},\bA\_{\alpha})\), provided that
\(\by\_{\beta}\) does not occur in \(\bA\_{\alpha}\) and \(\bx\_{\beta}\)
is not bound in \(\bA\_{\alpha}\).
2. b-*contraction*. To replace any well-formed part
\([\lambda \bx\_{\alpha}\bB\_{\beta}] \bA\_{\alpha}\) of a wff by
\(\textsf{Sub}(\bA\_{\alpha},\bx\_{\alpha},\bB\_{\beta})\), provided that
the bound variables of \(\bB\_{\beta}\) are distinct both from
\(\bx\_{\alpha}\) and from the free variables of \(\bA\_{\alpha}\).
3. b-*expansion*. To infer \(\bC\) from \(\bD\) if
\(\bD\) can be inferred from \(\bC\) by a single application of
b-contraction.
4. *Substitution*. From \(\bF\_{({o}\alpha)}\bx\_{\alpha}\), to
infer \(\bF\_{({o}\alpha)}\bA\_{\alpha}\), provided that
\(\bx\_{\alpha}\) is not a free variable of \(\bF\_{({o}\alpha)}\).
5. *Modus Ponens*. From \([\bA\_{{o}} \supset \bB\_{{o}}]\) and
\(\bA\_{{o}}\), to infer \(\bB\_{{o}}\).
6. *Generalization*. From \(\bF\_{({o}\alpha)}\bx\_{\alpha}\) to
infer \(\Pi\_{{o}({o}\alpha)}\bF\_{({o}\alpha)}\), provided that
\(\bx\_{\alpha}\) is not a free variable of \(\bF\_{({o}\alpha)}\).


#### 1.3.2 Elementary Type Theory



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

 
\[\begin{align}
[p\_{{o}} \lor p\_{{o}}] & \supset p\_{{o}} \tag{E1}\\
 p\_{{o}} & \supset [p\_{{o}} \lor q\_{{o}}] \tag{E2}\\
 [p\_{{o}} \lor q\_{{o}}] & \supset [q\_{{o}} \lor p\_{{o}}] \tag{E3}\\
 [p\_{{o}} \supset q\_{{o}}] & \supset [[r\_{{o}} \lor p\_{{o}}] \supset [r\_{{o}} \lor q\_{{o}}]] \tag{E4}\\
 \Pi\_{{o}({o}\alpha)}f\_{({o}\alpha)} & \supset f\_{({o}\alpha)}x\_{\alpha} \tag{E\(5^{\alpha}\)} \\
 \forall x\_{\alpha}[p\_{{o}} \lor f\_{({o}\alpha)}x\_{\alpha}] & \supset \left[p\_{{o}} \lor \Pi\_{{o}({o}\alpha)}f\_{({o}\alpha)}\right] \tag{E\(6^{\alpha}\)} 
\end{align}\]


The theorems of elementary type theory are those theorems which can be
derived, using the rules of inference, from Axioms
\((\rE1){-}(\rE6^{\alpha})\) (for all type symbols \(\alpha)\). We shall
sometimes refer to elementary type theory as \(\cT\). It embodies the
logic of propositional connectives, quantifiers, and
l-conversion in the context of type theory.



To illustrate the rules and axioms introduced above, we give a short
and trivial proof in \(\cT\). Following each wff of the proof, we
indicate how it was inferred. (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. The additional proof lines
have been inserted to illustrate some relevant aspects. For the sake
of readability, many brackets have been deleted from the formulas in
this proof. The diligent reader should be able to restore them.)



\[\begin{alignat}{2}
\forall x\_{\imath}\left[p\_{{o}} \lor f\_{{o}\imath}x\_{\imath}\right] \supset\left[p\_{{o}} \lor \Pi\_{{o}({o}\imath)} f\_{{o}\imath}\right] && \text{Axiom \(6^{\imath}\)} \tag\*{1.}\\
 \bigg[\lambda f\_{{o}\imath}\bigg[\forall x\_{\imath}[p\_{{o}} \lor f\_{{o}\imath}x\_{\imath}] \supset \bigg[p\_{{o}} \lor \Pi\_{{o}({o}\imath)}f\_{{o}\imath}\bigg]\bigg]\bigg] f\_{{o}\imath} && \text{b-expansion: 1} \tag\*{2.}\\
 \Pi\_{{o}({o}({o}\imath))}\bigg[\lambda f\_{{o}\imath}\bigg[\forall x\_{\imath}[p\_{{o}} \lor f\_{{o}\imath}x\_{\imath}] \supset \bigg[p\_{{o}} \lor \Pi\_{{o}({o}\imath)}f\_{{o}\imath}\bigg]\bigg]\bigg] && \text{Generalization: 2} \tag\*{3.}\\
 \bigg[\lambda f\_{{o}\imath}\bigg[\forall x\_{\imath}[p\_{{o}}\lor f\_{{o}\imath}x\_{\imath}] \supset \bigg[p\_{{o}} \lor \Pi\_{{o}({o}\imath)}f\_{{o}\imath}\bigg]\bigg]\bigg] [\lambda x\_{\imath}r\_{{o}\imath}x\_{\imath}] && \text{Substitution: 2} \tag\*{4.}\\
 \forall x\_{\imath}[p\_{{o}} \lor [\lambda x\_{\imath}r\_{{o}\imath}x\_{\imath}]x\_{\imath}] \supset \left[p\_{{o}} \lor \Pi\_{{o}({o}\imath)}\left[\lambda x\_{\imath}r\_{{o}\imath}x\_{\imath}\right]\right] && \text{b-contraction: 4} \tag\*{5.}\\
 \forall x\_{\imath}[p\_{{o}} \lor [\lambda y\_{\imath} r\_{{o}\imath} y\_{\imath}] x\_{\imath}] \supset \left[p\_{{o}} \lor \Pi\_{{o}({o}\imath)}\left[\lambda x\_{\imath}r\_{{o}\imath}x\_{\imath}\right]\right] && \text{a-conversion: 5} \tag\*{6.}\\
 \forall x\_{\imath}\left[p\_{{o}} \lor r\_{{o}\imath}x\_{\imath}\right] \supset \left[p\_{{o}} \lor \Pi\_{{o}({o}\imath)}\left[\lambda x\_{\imath}r\_{{o}\imath}x\_{\imath}\right]\right] && \text{b-contraction: 6} \tag\*{7.} 
\end{alignat}\]


Note that line 3 can be written as

 
\[ \forall f\_{{o}\imath} [\forall x\_{\imath} [p\_{{o}} \lor f\_{{o}\imath}x\_{\imath}] \supset [p\_{{o}} \lor [\forall x\_{\imath} f\_{{o}\imath} x\_{\imath}] ]] \tag\*{\(3'.\)} \]


and line 7 can be written as

 
\[ \forall x\_{\imath}[p\_{{o}} \lor r\_{{o}\imath}x\_{\imath}] \supset [p\_{{o}} \lor \forall x\_{\imath}r\_{{o}\imath}x\_{\imath}] \tag\*{\(7'.\)} \]


We have thus derived a well known law of quantification theory. We
illustrate one possible interpretation of the line \(7'\) wff (which is
closely related to Axiom E6) 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 on line \(7'\) if we take the horses to be the elements of type
\(\imath\), interpret \(p\_{{o}}\) to mean "the gate was
closed", and interpret \(r\_{{o}\imath}\) so that
\(r\_{{o}\imath}x\_{\imath}\) asserts "\(x\_{\imath}\) left the
corral". With this interpretation, line \(7'\) says



> 
> 
> If it is true of every horse that the gate was closed or that the
> 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



The axioms of boolean and functional extensionality are the
following:

 
\[\begin{align}
[x\_{{o}} \equiv y\_{{o}}] & \supset x\_{{o}} = y\_{{o}} \tag{\(7^{o}\)} \\
 \forall x\_{\beta}[f\_{\alpha \beta}x\_{\beta} = g\_{\alpha \beta}x\_{\beta}] & \supset f\_{\alpha \beta} = g\_{\alpha \beta}\tag{\(7^{\alpha \beta}\)} 
\end{align}\]


Church did not include Axiom \(7^{{o}}\) 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

 
\[\exists\_1\bx\_{\alpha}\bA\_{{o}}\]


stands for

 
\[[\lambda p\_{{o}\alpha}\exists y\_{\alpha}[p\_{{o}\alpha}y\_{\alpha} \land \forall z\_{\alpha}[p\_{{o}\alpha}z\_{\alpha} \supset z\_{\alpha} = y\_{\alpha}]]]\, [\lambda \bx\_{\alpha}\bA\_{{o}}]\]


For example,

 
\[\exists\_1 x\_{\alpha}P\_{{o}\alpha}x\_{\alpha}\]


stands for

 
\[[\lambda p\_{{o}\alpha}\exists y\_{\alpha}[p\_{{o}\alpha}y\_{\alpha} \land \forall z\_{\alpha}[p\_{{o}\alpha}z\_{\alpha} \supset z\_{\alpha} = y\_{\alpha}]]]\, [\lambda x\_{\alpha}P\_{{o}\alpha}x\_{\alpha}]\]


By l-conversion, this is equivalent to

 
\[\exists y\_{\alpha}[[\lambda x\_{\alpha}P\_{{o}\alpha}x\_{\alpha}]y\_{\alpha} \land \forall z\_{\alpha}[[\lambda x\_{\alpha}P\_{{o}\alpha}x\_{\alpha}] z\_{\alpha} \supset z\_{\alpha} = y\_{\alpha}]]\]


which reduces by l-conversion to

 
\[\exists y\_{\alpha}[P\_{{o}\alpha}y\_{\alpha} \land \forall z\_{\alpha}[P\_{{o}\alpha}z\_{\alpha} \supset z\_{\alpha} = y\_{\alpha}]]\]


This asserts that there is a unique element which has the property
\(P\_{{o}\alpha}\). From this example we can see that in general,
\(\exists\_1\bx\_{\alpha}\bA\_{{o}}\) expresses the assertion that
"there is a unique \(\bx\_{\alpha}\) such that
\(\bA\_{{o}}\)".



When there is a unique such element \(\bx\_{\alpha}\), it is convenient
to have the notation \(\atoi\bx\_{\alpha}\bA\_{{o}}\) to represent the
expression "the \(\bx\_{\alpha}\) such that \(\bA\_{{o}}\)".
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 \(\atoi\bx\_{\alpha}\bA\_{{o}}\)
is defined as \(\iota\_{\alpha({o}\alpha)}[\lambda
\bx\_{\alpha}\bA\_{{o}}]\). Thus, \(\atoi\) behaves like a
variable-binding operator, but it is defined in terms of l with
the aid of the logical constant \(\iota\_{\alpha({o}\alpha)}\). Thus,
l is still the only variable-binding operator that is
needed.



Since \(\bA\_{{o}}\) describes \(\bx\_{\alpha},
\iota\_{\alpha({o}\alpha)}\) is called a *description operator*.
Associated with this notation is the following:


##### Axiom of Descriptions:

 
\[ \exists\_1 x\_{\alpha}[p\_{{o}\alpha}x\_{\alpha}] \supset p\_{{o}\alpha} [\iota\_{\alpha({o}\alpha)}p\_{{o}\alpha}] \tag{\(8^{\alpha}\)} \]


This says that when the set \(p\_{{o}\alpha}\) has a unique member,
then \(\iota\_{\alpha({o}\alpha)}p\_{{o}\alpha}\) is in
\(p\_{{o}\alpha}\), and therefore is that unique member. Thus, this
axiom asserts that \(\iota\_{\alpha({o}\alpha)}\) maps one-element sets
to their unique members.



If from certain hypotheses one can prove

 
\[\exists\_1\bx\_{\alpha}\bA\_{{o}}\]


then by using Axiom \(8^{\alpha}\) one can derive

 
\[[\lambda \bx\_{\alpha}\bA\_{{o}}] [\iota\_{\alpha({o}\alpha)}[\lambda \bx\_{\alpha}\bA\_{{o}}]]\]


which can also be written as

 
\[[\lambda \bx\_{\alpha}\bA\_{{o}}] {[\atoi\bx\_{\alpha}\bA\_{{o}}]}\]


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\_{\varrho}\) and \(\times\_{\varrho \varrho
\varrho}\) to represent the number 1 and the multiplication function,
respectively. (Here \(\varrho\) is the type of real numbers.) To
represent the multiplicative inverse function, we can define the wff
\(\textrm{INV}\_{\varrho \varrho}\) as

 
\[{\lambda z\_{\varrho} \atoi x\_{\varrho} [\times\_{\varrho \varrho \varrho}z\_{\varrho}x\_{\varrho} = 1\_{\varrho}]}\]


Of course, in traditional mathematical notation we would not write the
type symbols, and we would write \(\times\_{\varrho \varrho
\varrho}z\_{\varrho}x\_{\varrho}\) as \(z \times x\) and write
\(\textrm{INV}\_{\varrho \varrho}z\) as \(z^{-1}\). Thus \(z^{-1}\) is
defined to be that *x* such that \(z \times x = 1\). When
*Z* is provably not 0, we will be able to prove \(\exists\_1
x\_{\varrho}[\times\_{\varrho \varrho \varrho} \textrm{Z x}\_{\varrho} =
1\_{\varrho}]\) and \(Z \times 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:

 
\[ \exists x\_{\alpha}p\_{{o}\alpha}x\_{\alpha} \supset p\_{{o}\alpha}[\iota\_{\alpha({o}\alpha)}p\_{{o}\alpha}] \tag{\(9^{\alpha}\)} \]


\((9^{\alpha})\) says that the choice function
\(\iota\_{\alpha({o}\alpha)}\) chooses from every nonempty set
\(p\_{{o}\alpha}\) an element, designated as
\(\iota\_{\alpha({o}\alpha)}p\_{{o}\alpha}\), of that set. When this
form of the Axiom of Choice is included in the list of axioms,
\(\iota\_{\alpha({o}\alpha)}\) is called a selection operator instead
of a description operator, and \(\atoi\bx\_{\alpha} \bA\_{{o}}\) means
"an \(\bx\_{\alpha}\) such that \(\bA\_{{o}}\)" when there
is some such element \(\bx\_{\alpha}\). These selection operators have
the same meaning as Hilbert's \(\epsilon\)-operator (Hilbert
1928). However, we here provide one such operator for each type
a.



It is natural to call \(\atoi\) a definite description operator in
contexts where \(\atoi\bx\_{\alpha}\bA\_{{o}}\) means "the
\(\bx\_{\alpha}\) such that \(\bA\_{{o}}\)", and to call it an
indefinite description operator in contexts where
\(\atoi\bx\_{\alpha}\bA\_{{o}}\) means "an \(\bx\_{\alpha}\) such
that \(\bA\_{{o}}\)".



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:



\[ \exists j\_{\alpha ({o}\alpha)}\forall p\_{{o}\alpha}[\exists x\_{\alpha}p\_{{o}\alpha}x\_{\alpha} \supset p\_{{o}\alpha}[j\_{\alpha({o}\alpha)}p\_{{o}\alpha}]] \tag{\(\text{AC}^{\alpha}\)} \]


Normally when one assumes the Axiom of Choice in type theory, one
assumes it as an axiom schema, and asserts AC\(^{\alpha}\) for each
type symbol a. A similar remark applies to the axioms for
extensionality and description. However, modern proof systems for
Church's type theory, which are, e.g., based on resolution, do
in fact avoid the addition of such axiom schemata for reasons as
further explained in
 Sections 3.4
 and
 4
 below. They work with more constrained, goal-directed proof rules
instead.



Before proceeding, we need to introduce some terminology. \(\cQ\_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 \({o}\) and parentheses.



Yasuhara (1975) defined the relation "\(\ge\)" between
types as the reflexive transitive closure of the minimal relation such
that \((\alpha \beta) \ge \alpha\) and \((\alpha \beta) \ge \beta\).
He established that:


* If \(\alpha \ge \beta\), then \(\cQ\_0 \vdash\) AC\(^{\alpha}
\supset\) AC\(^{\beta}\).
* Given a set *S* of types, none of which is propositional,
there is a model of \(\cQ\_0\) in which AC\(^{\alpha}\) fails if and
only if \(\alpha \ge \beta\) for some b in *S*.



The existence of a choice functions for "higher" types
thus entails the existence of choice functions for "lower"
types, the opposite is generally not the case though.



Buchi (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,
 \(\nsim\_{({o}{o})}, \lor\_{(({o}{o}){o})}\), and the
\(\Pi\_{({o}({o}\alpha))}\)'s were taken as primitive constants,
and the wffs \(\sfQ\_{{o}\alpha \alpha}\) which denote equality
relations at type a were defined in terms of these. We now
present an alternative formulation \(\cQ\_0\) of Church's type
theory in which there are primitive constants \(\sfQ\_{{o}\alpha
\alpha}\) denoting equality, and \(\nsim\_{({o}{o})},
\lor\_{(({o}{o}){o})}\), and the \(\Pi\_{({o}({o}\alpha))}\)'s are
defined in terms of the \(\sfQ\_{{o}\alpha \alpha}\)'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
l 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.



\(\cQ\_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 thus provides an
alternative to the material in the preceding Sections
1.2.1-1.3.4. More details about \(\cQ\_0\) can be found in
Andrews 2002.


#### 1.4.1 Definitions


* Type symbols, improper symbols, and variables of \(\cQ\_0\) are
defined as in
 Section 1.2.1.
* The logical constants of \(\cQ\_0\) are
\(\sfQ\_{(({o}\alpha)\alpha)}\) and \(\iota\_{(\imath({o}\imath))}\)
(for each type symbol a).
* Wffs of \(\cQ\_0\) are defined as in
 Section 1.2.1.


##### Abbreviations:


* \(\bA\_{\alpha} = \bB\_{\alpha}\) stands for \(\sfQ\_{{o}\alpha
\alpha}\bA\_{\alpha}\bB\_{\alpha}\)
* \(\bA\_{{o}} \equiv \bB\_{{o}}\) stands for
\(\sfQ\_{{o}{o}{o}}\)**A\(\_{{o}}\)B**\(\_{{o}}\)
* \(T\_{{o}}\) stands for \(\sfQ\_{{o}{o}{o}} =
\sfQ\_{{o}{o}{o}}\)
* \(F\_{{o}}\) stands for \([\lambda x\_{{o}}T\_{{o}}] = [\lambda
x\_{{o}}x\_{{o}}]\)
* \(\Pi\_{{o}({o}\alpha)}\) stands for
\(\sfQ\_{{o}({o}\alpha)({o}\alpha)}[\lambda x\_{\alpha}T\_{{o}}]\)
* \(\forall \bx\_{\alpha}\bA\) stands for
\(\Pi\_{{o}({o}\alpha)}[\lambda \bx\_{\alpha}\bA]\)
* \(\land\_{{o}{o}{o}}\) stands for \(\lambda x\_{{o}}\lambda
y\_{{o}}[[\lambda g\_{{o}{o}{o}}[g\_{{o}{o}{o}}T\_{{o}}T\_{{o}}]] =
[\lambda g\_{{o}{o}{o}}[g\_{{o}{o}{o}}x\_{{o}}y\_{{o}}]]]\)
* \(\bA\_{{o}} \land \bB\_{{o}}\) stands for \(\land\_{{o}{o}{o}}
\bA\_{{o}} \bB\_{{o}}\)
* \(\nsim\_{{o}{o}}\) stands for \(\sfQ\_{{o}{o}{o}}F\_{{o}}\)



\(T\_{{o}}\) denotes truth. The meaning of \(\Pi\_{{o}({o}\alpha)}\) was
discussed in
 Section 1.1.
 To see that this definition of \(\Pi\_{{o}({o}\alpha)}\) is
appropriate, note that \(\lambda x\_{\alpha}T\) denotes the set of all
elements of type a, and that
\(\Pi\_{{o}({o}\alpha)}s\_{{o}\alpha}\) stands for
\(\sfQ\_{{o}({o}\alpha)({o}\alpha)}[\lambda x\_{\alpha}T]
s\_{{o}\alpha}\), respectively for \([\lambda x\_{\alpha}T] =
s\_{{o}\alpha}\). Therefore \(\Pi\_{{o}({o}\alpha)}s\_{{o}\alpha}\)
asserts that \(s\_{{o}\alpha}\) is the set of all elements of type
a, so \(s\_{{o}\alpha}\) contains all elements of type a.
It can be seen that \(F\_{{o}}\) can also be written as \(\forall
x\_{{o}}x\_{{o}}\), which asserts that everything is true. This is
false, so \(F\_{{o}}\) denotes falsehood. The expression \(\lambda
g\_{{o}{o}{o}}[g\_{{o}{o}{o}}x\_{{o}}y\_{{o}}]\) can be used to represent
the ordered pair \(\langle x\_{{o}},y\_{{o}}\rangle\), and the
conjunction \(x\_{{o}} \land y\_{{o}}\) is true iff \(x\_{{o}}\) and
\(y\_{{o}}\) are both true, i.e., iff \(\langle T\_{{o}},T\_{{o}}\rangle
= \langle x\_{{o}},y\_{{o}}\rangle\). Hence \(x\_{{o}} \land y\_{{o}}\)
can be expressed by the formula \([\lambda
g\_{{o}{o}{o}}[g\_{{o}{o}{o}}T\_{{o}}T\_{{o}}]] = [\lambda
g\_{{o}{o}{o}}[g\_{{o}{o}{o}}x\_{{o}}y\_{{o}}]]\).



Other propositional connectives, such as \(\lor, \supset\), and the
existential quantifier \(\exists\), are easily defined. By using
\(\iota\_{(\imath({o}\imath))}\), one can define description operators
\(\iota\_{\alpha({o}\alpha)}\) for all types a.


#### 1.4.2 Axioms and Rules of Inference



\(\cQ\_0\) has a single rule of inference.



> 
> **Rule R:** From \(\bC\) and \(\bA\_{\alpha} =
> \bB\_{\alpha}\), to infer the result of replacing one occurrence of
> \(\bA\_{\alpha}\) in \(\bC\) by an occurrence of \(\bB\_{\alpha}\),
> provided that the occurrence of \(\bA\_{\alpha}\) in \(\bC\) is not (an
> occurrence of a variable) immediately preceded by l.



The *axioms for \(\cQ\_0\)* are the following:




\[\begin{align}
[g\_{{o}{o}}T\_{{o}} \land g\_{{o}{o}}F\_{{o}}] &= \forall x\_{{o}}[g\_{{o}{o}}x\_{{o}}] \tag{Q1}\\
 [x\_{\alpha} = y\_{\alpha}] & \supset [h\_{{o}\alpha}x\_{\alpha} = h\_{{o}\alpha}y\_{\alpha}] \tag{Q\(2^{\alpha}\)}\\
 [f\_{\alpha \beta} = g\_{\alpha \beta}] & = \forall x\_{\beta}[f\_{\alpha \beta}x\_{\beta} = g\_{\alpha \beta}x\_{\beta}] \tag{Q\(3^{\alpha \beta}\)}\\
 [\lambda \bx\_{\alpha}\bB\_{\beta}]\bA\_{\alpha} & = \textsf{SubFree}(\bA\_{\alpha},\bx\_{\alpha},\bB\_{\beta}), \tag{Q4}\\
 &\quad \text{ provided } \bA\_{\alpha} \text{ is free for } \bx \text{ in } \bB\_{\beta}\\
 \iota\_{\imath({o}\imath)}[\sfQ\_{{o}\imath\imath}y\_{\imath}] &= y\_{\imath} \tag{Q5} 
\end{align}\]
The additional condition in axiom \((\rQ4)\) ensures that the
substitution does not lead to free variables of A being bound in the
result of the substitution.


## 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
Godel's Incompleteness Theorem (Godel 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, which is
often referred to as *general semantics* or *Henkin
semantics*.



A *frame* is a collection \(\{\cD\_{\alpha}\}\_{\alpha}\) of
nonempty domains (sets) \(\cD\_{\alpha}\), one for each type symbol
a, such that \(\cD\_{{o}} = \{\sfT,\sfF\}\) (where \(\sfT\)
represents truth and \(\sfF\) represents falsehood), and \(\cD\_{\alpha
\beta}\) is some collection of functions mapping \(\cD\_{\beta}\) into
\(\cD\_{\alpha}\). The members of \(\cD\_{\imath}\) are called
*individuals*.



An *interpretation* \(\langle \{\cD\_{\alpha}\}\_{\alpha},
\frI\rangle\) consists of a frame and a function \(\frI\) which maps
each constant *C* of type a to an appropriate element of
\(\cD\_{\alpha}\), which is called the *denotation of*
*C*. The logical constants are given their standard
denotations.



An *assignment* of values in the frame
\(\{\cD\_{\alpha}\}\_{\alpha}\) to variables is a function \(\phi\) such
that \(\phi \bx\_{\alpha} \in \cD\_{\alpha}\) for each variable
\(\bx\_{\alpha}\). (Notation: The assignment \(\phi[a/x]\) maps
variable *x* to value *a* and it is identical with
\(\phi\) for all other variable symbols different from
*x*.)



An interpretation \(\cM = \langle \{\cD\_{\alpha}\}\_{\alpha},
\frI\rangle\) is a *general model* (aka *Henkin model*)
iff there is a binary function \(\cV\) such that
\(\cV\_{\phi}\bA\_{\alpha} \in \cD\_{\alpha}\) for each assignment
\(\phi\) and wff \(\bA\_{\alpha}\), and the following conditions are
satisfied for all assignments and all wffs:


* \(\cV\_{\phi}\bx\_{\alpha} = \phi \bx\_{\alpha}\) for each variable
\(\bx\_{\alpha}\).
* \(\cV\_{\phi}A\_{\alpha} = \frI A\_{\alpha}\) if \(A\_{\alpha}\) is a
primitive constant.
* \(\cV\_{\phi}[\bA\_{\alpha \beta}\bB\_{\beta}] =
(\cV\_{\phi}\bA\_{\alpha \beta})(\cV\_{\phi}\bB\_{\beta})\) (the value of
a function \(\cV\_{\phi}\bA\_{\alpha \beta}\) at the argument
\(\cV\_{\phi}\bB\_{\beta})\).
* \(\cV\_{\phi}[\lambda \bx\_{\alpha}\bB\_{\beta}] =\) that function
from \(\cD\_{\alpha}\) into \(\cD\_{\beta}\) whose value for each
argument \(z \in \cD\_{\alpha}\) is \(\cV\_{\psi}\bB\_{\beta}\), where
\(\psi\) is that assignment such that \(\psi \bx\_{\alpha} = z\) and
\(\psi \by\_{\beta} = \phi \by\_{\beta}\) if \(\by\_{\beta} \ne
\bx\_{\alpha}\).



If an interpretation \(\cM\) is a general model, the function \(\cV\)
is uniquely determined. \(\cV\_{\phi}\bA\_{\alpha}\) is called the
*value* of \(\bA\_{\alpha}\) in \(\cM\) with respect to
\(\phi\).



One can easily show that the following statements hold in all general
models \(\cM\) for all assignments \(\phi\) and all wffs \(\bA\) and
\(\bB\):


* \(\cV\_{\phi} T\_{{o}} = \sfT\) and \(\cV\_{\phi} F\_{{o}} =
\sfF\)
* \(\cV\_{\phi} [\nsim\_{{o}{o}} \bA\_{{o}}] = \sfT\) iff \(\cV\_{\phi}
\bA\_{{o}} = \sfF\)
* \(\cV\_{\phi} [ \bA\_{{o}} \lor \bB\_{{o}} ] = \sfT\) iff
\(\cV\_{\phi} \bA\_{{o}} = \sfT\) or \(\cV\_{\phi} \bB\_{{o}} =
\sfT\)
* \(\cV\_{\phi} [ \bA\_{{o}} \land \bB\_{{o}} ] = \sfT\) iff
\(\cV\_{\phi} \bA\_{{o}} = \sfT\) and \(\cV\_{\phi} \bB\_{{o}} =
\sfT\)
* \(\cV\_{\phi} [ \bA\_{{o}} \supset \bB\_{{o}} ] = \sfT\) iff
\(\cV\_{\phi} \bA\_{{o}} = \sfF\) or \(\cV\_{\phi} \bB\_{{o}} =
\sfT\)
* \(\cV\_{\phi} [ \bA\_{{o}} \equiv \bB\_{{o}} ] = \sfT\) iff
\(\cV\_{\phi} \bA\_{{o}} = \cV\_{\phi} \bB\_{{o}}\)
* \(\cV\_{\phi} [\forall \bx\_{\alpha}\bA] = \sfT\) iff
\(\cV\_{\phi[a/x]} \bA= \sfT\) for all \(a \in \cD\_{\alpha}\)
* \(\cV\_{\phi} [\exists \bx\_{\alpha}\bA] = \sfT\) iff there exists
an \(a \in \cD\_{\alpha}\) such that \(\cV\_{\phi[a/x]} \bA= \sfT\)



The semantics of general models is thus as expected. However, there is
a subtlety to note regarding the following condition for arbitrary
types a:


* [equality] \(\cV\_{\phi} [ \bA\_{\alpha} = \bB\_{\alpha} ] = \sfT\)
iff \(\cV\_{\phi} \bA\_{\alpha} = \cV\_{\phi} \bB\_{\alpha}\)



When the definitions of
 Section 1.2.1
 are employed, where equality has been defined in terms of
Leibniz' principle, then this statement is not implied for all
types a. It only holds if we additionally require that the
domains \(\cD\_{{o}\alpha}\) contain all the unit sets of objects of
type a, or, alternatively, that the domains
\(\cD\_{{o}\alpha\alpha}\) contain the respective identity relations on
objects of type a (which entails the former). The need for this
additional requirement, which is not included in the original work of
Henkin (1950), has been demonstrated in Andrews 1972a.



When instead the alternative definitions of
 Section 1.4
 are employed, then this requirement is obviously met due to the
presence of the logical constants \(\sfQ\_{{o}\alpha \alpha}\) in the
signature, which by definition denote the respective identity
relations on the objects of type a and therefore trivially
ensure their existence in each general model \(\cM\). It is therefore
a natural option to always assume primitive equality constants (for
each type a) in a concrete choice of base system for
Church's type theory, just as realized in Andrews' system
\(\cQ\_0\).



An interpretation \(\langle \{\cD\_{\alpha}\}\_{\alpha}, \frI\rangle\)
is a *standard model* iff for all a and \(\beta ,
\cD\_{\alpha \beta}\) is the set of all functions from \(\cD\_{\beta}\)
into \(\cD\_{\alpha}\). Clearly a standard model is a general
model.



We say that a wff \(\bA\) is *valid* in a model \(\cM\) iff
\(\cV\_{\phi}\bA = \sfT\) for every assignment \(\phi\) into \(\cM\). A
model for a set \(\cH\) of wffs is a model in which each wff of
\(\cH\) is valid.



A wff \(\bA\) is *valid in the general* [*standard*]
*sense* iff \(\bA\) 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.



**Completeness and Soundness Theorem (Henkin 1950):** 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 \(\cQ\_0\) is standard (Andrews 2002,
Theorem 5404), but every set of sentences of \(\cQ\_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 \(\cM = \langle \{\cD\_{\alpha}\}\_{\alpha},
\frI\rangle\) in which \(\cD\_{\imath}\) is infinite, and all the
domains \(\cD\_{\alpha}\) are countable. Thus \(\cD\_{\imath}\) and
\(\cD\_{{o}\imath}\) 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 \(\cD\_{\imath}\) 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.,
\(\nsim \exists g\_{{o}\imath\imath}\forall f\_{{o}\imath}\exists
j\_{\imath}[g\_{{o}\imath\imath}j\_{\imath} = f\_{{o}\imath}]\), and
considering what it means in a model. The theorem says that there is
no function \(g \in \cD\_{{o}\imath\imath}\) from \(\cD\_{\imath}\) into
\(\cD\_{{o}\imath}\) which has every set \(f\_{{o}\imath} \in
\cD\_{{o}\imath}\) in its range. The usual interpretation of the
statement is that \(\cD\_{{o}\imath}\) is bigger (in cardinality) than
\(\cD\_{\imath}\). However, what it actually means in this model is
that *h* cannot be in \(\cD\_{{o}\imath\imath}\). Of course,
\(\cM\) must be nonstandard.



While the Axiom of Choice is presumably true in all standard models,
there is a nonstandard model for \(\cQ\_0\) in which AC\(^{\imath}\) is
false (Andrews 1972b). Thus, AC\(^{\imath}\) is not provable in
\(\cQ\_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, and Henkin 1975. Further related work can be found in
Benzmuller et al. 2004, Brown 2004, 2007, and Muskens 2007.


## 3. Metatheory


### 3.1 Lambda-Conversion



The first three rules of inference in
 Section 1.3.1
 are called rules of l-*conversion*. If \(\bD\) and
\(\bE\) are wffs, we write \(\bD \conv \bE\) to indicate that \(\bD\)
can be converted to \(\bE\) by applications of these rules. This is an
equivalence relation between wffs. A wff \(\bD\) is in
b-*normal form* iff it has no well-formed parts of the
form \([[\lambda \bx\_{\alpha}\bB\_{\beta}]\bA\_{\alpha}]\). Every wff is
convertible to one in b-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
b-normal form. (This is called the strong normalization theorem.)
By the Church-Rosser Theorem, this wff in b-normal form is unique
modulo alphabetic changes of bound variables. For each wff \(\bA\) we
denote by \({\downarrow}\bA\) the first wff (in some enumeration) in
b-normal form such that \(\bA \conv {\downarrow} \bA\). Then
\(\bD \conv \bE\) if and only if \({\downarrow} \bD = {\downarrow}
\bE\).



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



> 
> 
> \(\eta\)-*Contraction*. Replace a well-formed part \([\lambda
> \by\_{\beta}[\bB\_{\alpha \beta}\by\_{\beta}]]\) of a wff by
> \(\bB\_{\alpha \beta}\), provided \(\by\_{\beta}\) does not occur free
> in \(\bB\_{\alpha \beta}\).
> 
> 
> 



This rule and its inverse (which is called
\(\eta\)-*Expansion*) are sometimes used as additional rules of
l-conversion. See Church 1941, Stenlund 1972, Barendregt 1984,
and Barendregt et al. 2013 for more information about
l-conversion.



It is worth mentioning (again) that l-abstraction replaces the
need for comprehension axioms in Church's type theory.


### 3.2 Higher-Order Unification



The challenges in higher-order unification are outlined very briefly.
More details on the topic are given in Dowek 2001; its utilization in
higher-order theorem provers is also discussed in Benzmuller
& Miller 2014.



**Definition.** A *higher-order unifier* for a
pair \(\langle \bA,\bB\rangle\) of wffs is a substitution \(\theta\)
for free occurrences of variables such that \(\theta \bA\) and
\(\theta \bB\) have the same b-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).



However, an algorithm has been devised (Huet 1975, Jensen &
Pietrzykowski 1976), called *pre-unification*, which will find
a unifier for a set of pairs of wffs if one exists. The pre-unifiers
computed by Huet's procedure are substitutions that can reduce
the original unification problem to one involving only so called
*flex-flex* unification pairs. Flex-flex pairs have variable
head symbols in both terms to be unified and they are known to always
have a solution. The concrete computation of these solutions can thus
be postponed or omitted. Pre-unification is utilized in all the
resolution based theorem provers mentioned in
 Section 4.



*Pattern unification* refers a small subset of unification
problems, first studied by Miller 1991, whose identification has been
important for the construction of practical systems. In a pattern
unification problem every occurrence of an existentially quantified
variable is applied to a list of arguments that are all distinct
variables bound by either a l-binder or a universal quantifier
in the scope of the existential quantifier. Thus, existentially
quantified variables cannot be applied to general terms but a very
restricted set of bound variables. Pattern unification, like
first-order unification, is decidable and most general unifiers exist
for solvable problems. This is why pattern unification is preferably
employed (when applicable) in some state-of-the-art theorem provers
for Church's type theory.


### 3.3 A Unifying Principle



The *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. The principle
was extended to elementary type theory by Andrews (1971) and to
extensional type theory, that is, Henkin's general semantics
without description or choice, by Benzmuller, Brown and Kohlhase
(2004). We outline these extensions in some more detail below.


#### 3.3.1 Elementary Type Theory



The Unifying Principle was extended to elementary type theory (the
system \(\cT\) of
 Section 1.3.2)
 in Andrews 1971 by applying ideas in Takahashi 1967. This Unifying
Principle for \(\cT\) has been used to establish cut-elimination for
\(\cT\) 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 \(\Gamma\) of finite sets of
wffs\(\_{{o}}\) is an *abstract consistency property* iff for
all finite sets \(\cS\) of wffs\(\_{{o}}\), the following properties
hold (for all wffs **A, B**):


1. If \(\Gamma(\cS)\), then there is no atom \(\bA\) such that \(\bA
\in \cS\) and \([\nsim \bA] \in \cS\).
2. If \(\Gamma(\cS \cup \{\bA\})\), then \(\Gamma(\cS \cup
{\downarrow} \bA\})\).
3. If \(\Gamma(\cS \cup \{\nsim \nsim \bA\})\), then \(\Gamma(\cS
\cup \{\bA\})\).
4. If \(\Gamma(\cS \cup \{\bA \lor \bB\})\), then \(\Gamma(\cS \cup
\{\bA\})\) or \(\Gamma(\cS \cup \{\bB\})\).
5. If \(\Gamma(\cS \cup \{\nsim[\bA \lor \bB]\})\), then \(\Gamma(\cS
\cup \{\nsim \bA,\nsim \bB\})\).
6. If \(\Gamma(\cS \cup \{\Pi\_{{o}({o}\alpha)}\bA\_{{o}\alpha}\})\),
then \(\Gamma(\cS \cup \{\Pi\_{{o}({o}\alpha)}\bA\_{{o}\alpha},
\bA\_{{o}\alpha}\bB\_{\alpha}\})\) for each wff \(\bB\_{\alpha}\).
7. If \(\Gamma(\cS \cup \{\nsim
\Pi\_{{o}({o}\alpha)}\bA\_{{o}\alpha}\})\), then \(\Gamma(\cS \cup
\{\nsim \bA\_{{o}\alpha}\bc\_{\alpha}\})\), for any variable or
parameter \(\bc\_{\alpha}\) which does not occur free in
\(\bA\_{{o}\alpha}\) or any wff in \(\cS\).



Note that *consistency* is an abstract consistency
property.



**Unifying Principle for \(\cT\).** If \(\Gamma\) is an
abstract consistency property and \(\Gamma(\cS)\), then \(\cS\) is
consistent in \(\cT\).



Here is a typical application of the Unifying Principle. Suppose there
is a procedure \(\cM\) which can be used to refute sets of sentences,
and we wish to show it is complete for \(\cT\). For any set of
sentences, let \(\Gamma(\cS)\) mean that \(\cS\) is not refutable by
\(\cM\), and show that \(\Gamma\) is an abstract consistency property.
Now suppose that \(\bA\) is a theorem of \(\cT\). Then \(\{\nsim
\bA\}\) is inconsistent in \(\cT\), so by the Unifying Principle not
\(\Gamma(\{\nsim \bA\})\), so \(\{\nsim \bA\}\) is refutable by
\(\cM\).


#### 3.3.2 Extensional Type Theory



Extensions of the above Unifying principle towards Church's type
theory with general semantics were studied since the mid nineties. A
primary motivation was to support (refutational) completeness
investigations for the proof calculi underlying the emerging
higher-order automated theorem provers (see
 Section 4
 below). The initial interest was on a fragment of Church's type
theory, called *extensional type theory*, that includes the
extensionality axioms, but excludes \(\iota\_{(\alpha({o}\alpha))}\)
and the axioms for it (description and choice were largely neglected
in the automated theorem provers at the time). Analogous to before, a
distinction has been made between extensional type theory with
*defined equality* (as in
 Section 1.2.1,
 where equality is defined via Leibniz' principle) and
extensional type theory with *primitive equality* (e.g., system
\(\cQ\_0\) as in
 Section 1.4,
 or, alternatively, a system based on logical constants
\(\nsim\_{({o}{o})}, \lor\_{(({o}{o}){o})}\), and the
\(\Pi\_{({o}({o}\alpha))}\)'s as in
 Section 1.2.1,
 but with additional primitive logical constants
\(=\_{{o}\alpha\alpha}\) added).



A first attempt towards a Unifying Principle for extensional type
theory with primitive equality is presented in Kohlhase 1993. The
conditions given there, which are still
 incomplete[1],
 were subsequently modified and complemented as follows:


* To obtain a Unifying Principle for extensional type theory with
defined equality, Benzmuller & Kohlhase 1997 added the
following conditions for boolean extensionality, functional
extensionality and saturation to the above conditions 1.-7. for
\(\cT\) (their presentation has been adapted here; for technical
reasons, they also employ a slightly stronger variant for condition 2.
based on b-conversion rather than b-normalization):


	8. If \(\Gamma(\cS \cup \{ \bA\_{{o}} = \bB\_{{o}} \})\), then
	\(\Gamma(\cS \cup \{ \bA\_{{o}}, \bB\_{{o}} \})\) or \(\Gamma(\cS \cup
	\{ \nsim \bA\_{{o}}, \nsim \bB\_{{o}} \})\)
	9. If \(\Gamma(\cS \cup \{ \bA\_{\alpha\beta} = \bB\_{\alpha\beta}
	\})\), then \(\Gamma(\cS \cup \{ \bA\_{\alpha\beta} \bc\_\beta =
	\bB\_{\alpha\beta} \bc\_\beta \})\) for any parameter \(\bc\_{\beta}\)
	which does not occur free in \(\cS\).
	10. \(\Gamma(\cS \cup \{ \bA\_{{o}} \})\) or \(\Gamma(\cS \cup \{ \nsim
	\bA\_{{o}} \})\)
The saturation condition 10. was required to properly establish the
principle. However, since this condition is related to the proof
theoretic notion of cut-elimination, it limits the utility of the
principle in completeness proofs for machine-oriented calculi. The
principle was nevertheless used in Benzmuller & Kohlhase
1998a and Benzmuller 1999a,b to obtain a completeness proof for a
system of extensional higher-order resolution. The principle was also
applied in Kohlhase 1998 to study completeness for a related
extensional higher-order tableau
 calculus,[2]
 in which the extensionality rules for Leibniz equality were adapted
from Benzmuller & Kohlhase 1998a, respectively
Benzmuller 1997.
* Different options for achieving a Unifying Principle for extensional
type theory with primitive equality are presented in Benzmuller
1999a (in this work primitive logical constants
\(=\_{{o}\alpha\alpha}\) were used in addition to \(\nsim\_{({o}{o})},
\lor\_{(({o}{o}){o})}\), and the \(\Pi\_{({o}({o}\alpha))}\)'s;
such a redundant choice of logical constants is not rare in
higher-order theorem provers). One option is to introduce a
reflexivity and substitutivity condition. An alternative is to combine
a reflexivity condition with a condition connecting primitive with
defined equality, so that the substitutivity condition follows. Note
that introducing a defined notion of equality based on the Leibniz
principle is, of course, still possible in this context (defined
equality is denoted in the remainder of this section by \(\doteq\) to
properly distinguish it from primitive equality \(=\)):


	8. Not \(\Gamma(\cS \cup \{ \nsim [\bA\_{\alpha} = \bA\_{\alpha}]
	\})\)
	9. If \(\Gamma(\cS \cup \{ \bA\_{\alpha} = \bA\_{\alpha} \})\), then
	\(\Gamma(\cS \cup \{ \bA\_{\alpha} \doteq \bA\_{\alpha} \})\)
	10. \(\Gamma(\cS \cup \{ \bA\_{{o}} \})\) or \(\Gamma(\cS \cup \{ \nsim
	\bA\_{{o}} \})\)
The saturation condition 10. still has to be added independent of
which option is considered. The principle was applied in
Benzmuller 1999a,b to prove completeness for the extensional
higher-order
 RUE-resolution[3]
 calculus underlying the higher-order automated theorem prover LEO and
its successor LEO-II.
* In Benzmuller et al. 2004 the principle is presented in a very
general way which allows for various possibilities concerning the
treatment of extensionality and equality in the range between
elementary type theory and extensional type theory. The principle is
applied to obtain completeness proofs for an associated range of
natural deduction calculi. The saturation condition is still used in
this work.
* Based on insights from Brown's (2004, 2007) thesis, a solution
for replacing the undesirable saturation condition by two weaker
conditions is presented in Benzmuller, Brown, and Kohlhase 2009;
this work also further studies the relation between saturation and
cut-elimination. The two weaker conditions, termed mating and
decomposition, are easier to demonstrate than saturation in
completeness proofs for machine-oriented calculi. They are (omitting
some type information in the second one and abusing notation):


	1. If \(\Gamma(\cS \cup \{ \nsim \bA\_{{o}}, \bB\_{{o}} \})\) for atoms
	\(\bA\_{{o}}\) and \(\bB\_{{o}}\), then \(\Gamma(\cS \cup \{ \nsim
	[\bA\_{{o}} \doteq \bB\_{{o}}] \})\)
	2. If \(\Gamma(\cS \cup \{ \nsim [h \overline{\bA^n\_{\alpha^n}}
	\doteq h \overline{\bB^n\_{\alpha^n}} ] \})\), where head symbol
	\(h\_{\beta\overline{\alpha^n}}\) is a parameter, then there is an \(i\
	(1 \leq i \leq n)\) such that \(\Gamma(\cS \cup \{ \nsim
	[\bA^i\_{\alpha^i} \doteq \bB^i\_{\alpha^i}] \})\).
The modified principle is applied in Benzmuller et al. 2009 to
show completeness for a sequent calculus for extensional type theory
with defined equality.
* A further extended Unifying Principle for extensional type theory with
primitive equality is presented and used in Backes & Brown 2011 to
prove the completeness of a tableau calculus for type theory which
incorporates the axiom of choice.
* A closely related and further simplified principle has also been
presented and studied in Steen 2018, where it was applied for showing
completeness of the paramodulation calculus that is underlying the
theorem prover Leo-III (Steen & Benzmuller 2018, 2021).


### 3.4 Cut-Elimination and Cut-Simulation



Cut-elimination proofs (see also the SEP entry on
 proof theory)
 for Church's type theory, which are often closely related to
such proofs (Takahashi 1967, 1970; Prawitz 1968; Mints 1999) for other
formulations of type theory, may be found in Andrews 1971, Dowek &
Werner 2003, and Brown 2004. In Benzmuller et al. 2009 it is
shown how certain wffs\(\_{{o}}\), such as axioms of extensionality,
descriptions, choice (see
 Sections 1.3.3
 to
 1.3.5),
 and induction, can be used to justify cuts in cut-free sequent
calculi for elementary type theory. Moreover, the notions of
*cut-simulation* and *cut-strong axioms* are introduced
in this work, and the need for omitting defined equality and for
eliminating *cut-strong axioms* such as extensionality,
description, choice and induction in machine-oriented calculi (e.g.,
by replacing them with more constrained, goal-directed rules) in order
to reduce *cut-simulation* effects are discussed as a major
challenge for higher-order automated theorem proving. In other words,
including cut-strong axioms in a machine-oriented proof calculus for
Church's type theory is essentially as bad as including a cut
rule, since the cut rule can be mimicked by them.


### 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 \(\bA\) is a theorem of elementary type theory if and only if
\(\bA\) has an expansion proof.



In Brown 2004 and 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 \(\cQ\_{0}^1\) obtained by adding to \(\cQ\_0\) the additional
axiom \(\forall x\_{\imath}\forall y\_{\imath}[x\_{\imath}=y\_{\imath}]\)
is decidable.



Although the system \(\cT\) 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 \(\cT\) 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 \(\exists \bx^1 \ldots \exists \bx^n [\bA=\bB]\) is
a theorem of \(\cT\) iff there is a substitution \(\theta\) such that
\(\theta \bA \conv \theta \bB\). In particular, \(\vdash \bA=\bB\) iff
\(\bA \conv \bB\), which solves the decision problem for wffs of the
form \([\bA=\bB]\). Naturally, the circumstance that only trivial
equality formulas are provable in \(\cT\) changes drastically when
axioms of extensionality are added to \(\cT\). \(\vdash \exists
\bx\_{\beta}[\bA=\bB]\) iff there is a wff \(\bE\_{\beta}\) such that
\(\vdash[\lambda \bx\_{\beta}[\bA=\bB]]\bE\_{\beta}\), but the decision
problem for the class of wffs of the form \(\exists
\bx\_{\beta}[\bA=\bB]\) is unsolvable.



A wff of the form \(\forall \bx^1 \ldots \forall \bx^n\bC\), where
\(\bC\) is quantifier-free, is provable in \(\cT\) iff \({\downarrow}
\bC\) is tautologous. On the other hand, the decision problem for wffs
of the form \(\exists \bz\bC\), where \(\bC\) 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
\(\cT\) in prenex normal form defined solely by the structure of the
prefix are those in which no existential quantifiers occur.


## 4. Automation


### 4.1 Machine-Oriented Proof Calculi



The development, respectively improvement, of machine-oriented proof
calculi for Church's type theory has made good progress in
recent years; see, e.g., the references on superposition based calculi
given below. The challenges are obviously much bigger than in
first-order logic. The practically way more expressive nature of the
term-language of Church's type theory causes a larger, bushier
and more difficult to traverse proof search space than in first-order
logic. Moreover, remember that unification, which constitutes a very
important control and filter mechanism in first-order theorem proving,
is undecidable (in general) in type theory; see
 Section 3.2.
 On the positive side, however, there is a chance to find
significantly shorter proofs than in first-order logic. This is well
illustrated with a small, concrete example in Boolos 1987, for which a
fully automated proof seems now in reach (Benzmuller et al.
2023).



Clearly, further progress is needed to further leverage the practical
relevance of existing calculi for Church's type theory and their
implementations (see
 Section 4.3).
 The challenges include


* an appropriate handling of the impredicative nature of
Church's type theory (some form of blind guessing cannot
generally be avoided in a complete proof procedure, but must be
intelligently guided),
* the elimination/reduction of cut-simulation effects (see
 Section 3.4)
 caused by defined equality or cut-strong axioms (e.g.,
extensionality, description, choice, induction) in the search
space,
* the general undecidability of unification, rendering it a rather
problematic filter mechanism for controlling proof search,
* the invention of suitable heuristics for traversing the search
space,
* the provision of suitable term-orderings and their effective
exploitation in term rewriting procedures,
* and efficient data structures in combination with strong technical
support for essential operations such l-conversion,
substitution and rewriting.



It is planned that future editions of this article further elaborate
on machine-oriented proof calculi for Church's type theory. For
the time being, however, we provide only a selection of historical and
more recent references for the interested reader (see also
 Section 5
 below):


* **Sequent calculi:** Schutte 1960; Takahashi
1970; Takeuti 1987; Mints 1999; Brown 2004, 2007; Benzmuller et
al. 2009.
* **Mating method:** Andrews 1981; Bibel 1981; Bishop
1999.
* **Resolution calculi:** Andrews 1971; Huet 1973a;
Jensen & Pietrzykowski 1976; Benzmuller 1997, 1999a;
Benzmuller & Kohlhase 1998a.
* **Tableau method:**
 Kohlhase[4]
 1995, 1998; Brown & Smolka 2010; Backes & Brown 2011.
* **Paramodulation calculi:** Benzmuller 1999a,b;
Steen 2018, Steen & Benzmuller 2018, 2021.
* **Superposition calculi:** Bentkamp et al. 2018,
Bentkamp et al. 2021, Bentkamp et al. 2023a,c
* **Combinator-based superposition calculi:** Bhayat
& Reger 2020


### 4.2 Proof Assistants



Early computer systems for proving theorems of Church's type
theory (or extensions of it) include HOL (Gordon 1988; Gordon &
Melham 1993), TPS (Andrews et al. 1996; Andrews & Brown 2006),
Isabelle (Paulson 1988, 1990), PVS (Owre et al. 1996; Shankar 2001),
IMPS (Farmer et al. 1993), HOL Light (Harrison 1996), OMEGA (Siekmann
et al. 2006), and lClam (Richardson et al. 1998). Prominent
proof assistents that support more powerful dependent type theory
include Coq (Bertot & Casteran 2004) and the recent Lean
system (de Moura & Ullrich 2021). See
 Other Internet References
 section below for links to further info on these and other provers
mentioned later.



Most of the early systems mentioned above focused (at least initially)
on interactive proof. However, the TPS project in particular had been
working since the mid-1980s on the integration of ND-style interactive
proof and automated theorem proving using the mating method, and had
investigated proof transformation techniques between the two. This
research was further intensified in the 1990s, when other projects
investigated various solutions such as proof planning and bridges to
external theorem provers using so-called hammer tools. The hammers
developed at that time were early precursors of todays very successful
hammer tools such as Sledgehammer, HolyHammer and related systems
(Blanchette et al. 2013, Kaliszyk & Urban 2015 and Czaika &
Kaliszyk 2018).



While, triggered by the mentioned dynamics, some first initial
progress was made in the late 80s and during the 90s with regards to
the automation of Church's type theory, the resource investments
and achievements at the time were lacking much behind those seen, for
example, in first-order theorem proving. Good progress was fostered
only later, in particular, through the development of a commonly
supported syntax for Church's type theory, called TPTP THF
(Sutcliffe & Benzmuller 2010, Sutcliffe 2022), and the
inclusion, from 2009 onwards, of a TPTP THF division in the yearly
CASC competitions (kind of world championships for automated theorem
proving; see Sutcliffe 2016 for further details). These competitions,
in combination with further factors, triggered an increasing interest
in the full automation of Church's type theory. Particularly
successful was recently the exploration of equality based theorem
proving using the superposition approach and the adaptation of SMT
techniques to HOL.


### 4.3 Automated Theorem Provers



A selection of theorem provers for Church's type theory is presented.
The focus is on systems that have successfully participated in TPTP
THF CASC competitions in the past, and the order of presentation is
motivated by their first-time CASC participation. The latest editions
of most mentioned systems can be accessed online via the SystemOnTPTP
infrastructure (Sutcliffe 2017). Nearly all mentioned systems produce
verifiable proof certificates in the TPTP TSTP syntax.



The TPS prover (Andrews et al. 1996, Andrews & Brown 2006) can be
used to prove theorems of elementary type theory or extensional type
theory automatically, interactively, or semi-automatically. When
searching for a proof automatically, TPS first searches for an
expansion proof (Miller 1987) or an extensional expansion proof (Brown
2004, 2007) of the theorem. Part of this process involves searching
for acceptable matings (Andrews 1981, Bishop 1999). The behavior of
TPS is controlled by sets of flags, also called modes. A simple
scheduling mechanism is employed in the latest versions of TPS to
sequentially run a about fifty modes for a limited amount of time. TPS
was the winner of the first THF CASC competition in 2009.



The LEO-II prover (Benzmuller et al. 2015) is the successor of
LEO (Benzmuller & Kohlhase 1998b, which was hardwired with
the OMEGA proof assistant (LEO stands for Logical Engine of OMEGA).
The provers are based on the RUE-resolution calculi developed in
Benzmuller 1999a,b. LEO was the first prover to implement
calculus rules for extensionality to avoid cut-simulation effects.
LEO-II inherits and adapts them, and provides additional calculus
rules for description and choice. The prover, which internally
collaborates with first-order provers (preferably E) and SAT solvers,
has pioneered cooperative higher-order/first-order proof automation.
Since the prover is often too weak to find a refutation among the
steadily growing set of clauses on its own, some of the clauses in
LEO-II's search space attain a special status: they are
first-order clauses modulo the application of an appropriate
transformation function. Therefore, LEO-II progressively launches time
limited calls with these clauses to a first-order theorem prover, and
when the first-order prover reports a refutation, LEO-II also
terminates. Parts of these ideas were already implemented in the
predecessor LEO. Communication between LEO-II and the cooperating
first-order theorem provers uses the TPTP language and standards.
LEO-II was the winner of the second THF CASC competition in 2010.



The Satallax prover (Brown 2012) is based on a complete ground tableau
calculus for Church's type theory with choice (Backes &
Brown 2011). An initial tableau branch is formed from the assumptions
of a conjecture and negation of its conclusion. From that point on,
Satallax tries to determine unsatisfiability or satisfiability of this
branch. Satallax progressively generates higher-order formulas and
corresponding propositional clauses. Satallax uses the SAT solver
MiniSat as an engine to test the current set of propositional clauses
for unsatisfiability. If the clauses are unsatisfiable, the original
branch is unsatisfiable. Satallax provides calculus rules for
extensionality, description and choice. If there are no quantifiers at
function types, the generation of higher-order formulas and
corresponding clauses may terminate. In that case, if MiniSat reports
the final set of clauses as satisfiable, then the original set of
higher-order formulas is satisfiable (by a standard model in which all
types are interpreted as finite sets). Satallax was the winner of the
THF CASC competition in 2011 and from 2013 to 2019



The Isabelle/HOL system (Nipkow, Wenzel, & Paulson 2002) has
originally been designed as an interactive prover. However, in order
to ease user interaction several automatic proof tactics have been
added over the years. By appropriately scheduling a subset of these
proof tactics, some of which are quite powerful, Isabelle/HOL has
since about 2011 been turned also into an automatic theorem prover for
TPTP THF (and other TPTP syntax formats), that can be run from a
command shell like other provers. The most powerful proof tactics that
are scheduled by Isabelle/HOL include the Sledgehammer tool
(Blanchette et al. 2013), which invokes a sequence of external
first-order and higher-order theorem provers, the model finder
*Nitpick* (Blanchette & Nipkow 2010), the equational
reasoner *simp*, the untyped tableau prover *blast*, the
simplifier and classical reasoners *auto*, *force*, and
*fast*, and the best-first search procedure *best*. In
contrast to all other automated theorem provers mentioned above, the
TPTP incarnation of Isabelle/HOL does not output proof certificates.
Isabelle/HOL was the winner of the THF CASC competition in 2012.



The agsyHOL prover is based on a generic lazy narrowing proof search
algorithm. Backtracking is employed and a comparably small search
state is maintained. The prover outputs proof terms in sequent style
which can be verified in the Agda system.



coqATP implements (the non-inductive) part of the calculus of
constructions (Bertot & Casteran 2004). The system outputs
proof terms which are accepted as proofs (after the addition of a few
definitions) by the Coq proof assistant. The prover employs axioms for
functional extensionality, choice, and excluded middle. Boolean
extensionality is not supported. In addition to axioms, a small
library of basic lemmas is employed.



The Leo-III prover implements a paramodulation calculus for
Church's type theory (Steen 2018). The system, which is a
descendant of LEO and LEO-II, provides calculus rules for
extensionality, description and choice. The system has put an emphasis
on the implementation of an efficient set of underlying data
structures, on simplification routines and on heuristic rewriting. In
the tradition of its predecessors, Leo-III cooperates with first-order
reasoning tools using translations to many-sorted first-order logic.
The prover accepts every common TPTP syntax dialect and is thus very
widely applicable. Recently, the prover has also been extended to
natively supports almost every normal higher-order modal logic (Steen
et al. 2023).



CVC4, CVC5 and Verit (Barbosa et al. 2019) are SMT-based automated
provers with built-in support for many theories, including linear
arithmetic, arrays, bit vectors, data types, finite sets and strings.
These provers have been extended to support (fragments of) Church's
type theory.



The Zipperposition prover (Bentkamp et al. 2018, Vukmirovic et
al. 2022) focuses on the effective implementation of superposition
calculi for Church's type theory. It comes with Logtk, a supporting
library for manipulating terms, formulas, clauses, etc. in Church's
type theory, and supports relevant extensions such as datatypes,
recursive functions, and arithmetic. Zipperposition was the winner of
the THF CASC competition in 2020, 2021 and 2022.



Vampire (Bhayat & Reger 2020), which has dominated the TPTP
competitions in first-order logic for more than two decades, now also
supports the automation of Church's type theory using a
combinator-based superposition calculus. Vampire was the winner of the
THF CASC competition in 2023.



The theorem prover E (Vukmirovic et al. 2023), another prominent
and leading first-order automated theorem prover, has been extended
for Church's type theory using a variant of the supperposition
approach that is also implemented in Zipperposition.



Lash (Brown and Kaliszyk 2022) is a theorem prover for Church's type
theory created as a fork of Satallax. 



Duper is a superposition-based theorem prover for dependent type
theory, deigned to prove theorems in the proof assistant Lean.



In recent years, there has thus been a significant shift from
first-order to higher-order automated theorem proving.


### 4.4 (Counter-)Model Finding



Support for finding finite models or countermodels for formulas of
Church's type theory was implemented already in the
tableau-based prover HOT (Konrad 1998). Restricted (counter-)model
finding capabilities are also implemented in the provers Satallax,
LEO-II and LEO-III. The most advanced (finite) model finding support
is currently realized in the systems Nitpick, Nunchaku and Refute.
These tools have been integrated with the Isabelle proof assistant.
Nitpick is also available as a standalone tool that accepts TPTP THF
syntax. The systems are particularly valuable for exposing errors and
misconceptions in problem encodings, and for revealing bugs in the THF
theorem provers.


## 5. Applications



In addition to its elegance, Church's type theory also has many
practical advantages. This aspect is emphasised, for example, in the
recent textbook by Farmer (2023), which deals with various relevant
and important further aspects that could not be covered in this
article. Because of its good practical expressiveness, the range of
applications of Church's type theory is very wide, and only a few
examples can be given below (a good source for further information on
practical examples are the proceedings of the conferences on
Interactive Theorem Proving).


### 5.1 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
Typelogical/Categorical Grammar. Further related work on intensional
and higher-order modal logic is presented in Gallin 1975 and Muskens
2006.


### 5.2 Mathematics and Computer Science



Proof assistants based on Church's Type Theory, including
Isabelle/HOL, HOL Light, HOL4, and PVS, have been successfully
utilized in a broad range of application in computer science and
mathematics.



Applications in computer science include the verification of hardware,
software and security protocols. A prominent example is the
L4.verified project in which Isabelle/HOL was used to formally prove
that the seL4 operating system kernel implements an abstract,
mathematical model specifying of what the kernel is supposed to do
(Klein et al. 2018).



In mathematics proof assistants have been applied for the development
of libraries mathematical theories and the verification of challenge
theorems. An early example is the mathematical library that was
developed since the eighties in the TPS project. A exemplary list of
theorems that were proved automatically with TPS is given in Andrews
et al. 1996. A very prominent recent example is Hales Flyspeck in
which HOL Light was employed to develop a formal proof for
Kepler's conjecture (Hales et al. 2017). An example that
strongly exploits automation support in Isabelle/HOL with Sledgehammer
and Nitpick is presented in Benzmuller & Scott 2019. In this
work different axiom systems for category theory were explored and
compared.



A solid overview of past and ongoing formalization projects can be
obtained by consulting appropriate sources such as Isabelle's Archive
of Formal Proofs, the Journal of Formalized Reasoning, or the THF
entries in Sutcliffe's TPTP problem library. Relevant further
information and a discussion of implications and further work can also
be found in Bentkamp et al. 2023b and in Bayer et al. 2024.



Further improving proof automation within these proof
assistants--based on proof hammering tools or on other forms of
prover integration--is relevant for minimizing interaction effort
in future applications.


### 5.3 Computational Metaphysics and Artificial Intelligence



Church's type theory is a classical logic, but topical
applications in philosophy and artificial intelligence often require
expressive non-classical logics. In order to support such applications
with reasoning tools for Church's type theory, the shallow
semantical embedding technique (see also
 Section 1.2.2)
 has been developed that generalizes and extends the ideas underlying
the well known standard translation of modal logics to first-order
logic. The technique was applied for the assessment of modern variants
of the ontological argument with a range of higher-order theorem
provers, including LEO-II, Satallax, Nitpick and Isabelle/HOL. In the
course of experiments, LEO-II detected an inconsistency in the
premises of Godel's argument, while the provers succeeded
in automatically proving Scott's emendation of it and to confirm
the consistency of the emended premises. More details on this work are
presented in a related SEP entry on
 automated reasoning
 (see Section 4.6 on Logic and Philosophy). The semantical embedding
approach has been adapted and further extended for a range of other
non-classical logics and related applications. In philosophy this
includes the encoding and formal assessment of ambitious ethical and
metaphysical theories, and in artificial intelligence this includes
the mechanization of deontic logics and normative reasoning to control
AI systems (Benzmuller et al. 2020) as well as an automatic proof
of the
 muddy children puzzle (see Appendix B of dynamic epistemic logic),
 which is a famous puzzle in epistemic reasoning, respectively dynamic
epistemic reasoning.


### 5.4. Metalogical Studies



Church's type theory is also well suited to support metalogical
studies, including the encoding of other logical formalisms and
formalized soundness and completeness studies (see, e.g.,
Schlichtkrull et al. 2020, Halkjaer et al. 2023, and various
further pointers given in Benzmuller 2019). In particular,
Church's type theory can be studied formally in itself, as shown, for
example, by Kumar et al. (2016), Schlichtkrull (2023), and Diaz
(2023).