\documentclass{article}
\usepackage{amsmath,amstext,amsfonts,amsthm,amssymb,latexsym,xspace}
\renewcommand\baselinestretch{0.95}
\topmargin -0.50in
\oddsidemargin -0.15in
\evensidemargin -0.15in
\textwidth 6.5in
\textheight 9.5in
%%% my math definitions
\def\lnot{\neg}
\def\land{\;\wedge\;}
\def\lor{\;\vee\;}
\def\lthen{\;\rightarrow\;}
\def\liff{\;\leftrightarrow\;}
\def\peq{\Leftrightarrow}
\def\cross{\;\times\;}
%%% my environments
\newtheorem{theorem}{Theorem}[subsection]
\theoremstyle{definition}\newtheorem{definition}[theorem]{Definition}
\theoremstyle{definition}\newtheorem{notation}[theorem]{Notation}
\theoremstyle{definition}\newtheorem{exercise}{Exercise}[subsection]
\theoremstyle{remark}\newtheorem*{answer}{Answer}
\theoremstyle{plain}\newtheorem*{axiom}{}
\theoremstyle{plain}\newtheorem{thm}{Theorem}[subsection]
%%% my numbering alterations
\numberwithin{equation}{subsection}
\newcommand{\lcalc}{\ensuremath{\lambda}-Calculus\xspace}
\newcommand{\Godel}{G\"{o}del\xspace}
\newcommand{\lcA}{\ensuremath{\boldsymbol{A}}\xspace}
\newcommand{\lcB}{\ensuremath{\boldsymbol{B}}\xspace}
\newcommand{\lcC}{\ensuremath{\boldsymbol{C}}\xspace}
\newcommand{\lcD}{\ensuremath{\boldsymbol{D}}\xspace}
\newcommand{\lcE}{\ensuremath{\boldsymbol{E}}\xspace}
\newcommand{\lcF}{\ensuremath{\boldsymbol{F}}\xspace}
\newcommand{\lcG}{\ensuremath{\boldsymbol{G}}\xspace}
\newcommand{\lcH}{\ensuremath{\boldsymbol{H}}\xspace}
\newcommand{\lcI}{\ensuremath{\boldsymbol{I}}\xspace}
\newcommand{\lcJ}{\ensuremath{\boldsymbol{J}}\xspace}
\newcommand{\lcK}{\ensuremath{\boldsymbol{K}}\xspace}
\newcommand{\lcL}{\ensuremath{\boldsymbol{L}}\xspace}
\newcommand{\lcM}{\ensuremath{\boldsymbol{M}}\xspace}
\newcommand{\lcN}{\ensuremath{\boldsymbol{N}}\xspace}
\newcommand{\lcP}{\ensuremath{\boldsymbol{P}}\xspace}
\newcommand{\lcQ}{\ensuremath{\boldsymbol{Q}}\xspace}
\newcommand{\lcR}{\ensuremath{\boldsymbol{R}}\xspace}
\newcommand{\lcS}{\ensuremath{\boldsymbol{S}}\xspace}
\newcommand{\lcT}{\ensuremath{\boldsymbol{T}}\xspace}
\newcommand{\lcW}{\ensuremath{\boldsymbol{W}}\xspace}
\newcommand{\lcX}{\ensuremath{\boldsymbol{X}}\xspace}
\newcommand{\lcY}{\ensuremath{\boldsymbol{Y}}\xspace}
\newcommand{\lcZ}{\ensuremath{\boldsymbol{Z}}\xspace}
\newcommand{\lcfB}{\ensuremath{\mathfrak{B}}\xspace}
\newcommand{\lcfG}{\ensuremath{\mathfrak{G}}\xspace}
\newcommand{\lcfL}{\ensuremath{\mathfrak{L}}\xspace}
\newcommand{\lcfN}{\ensuremath{\mathfrak{N}}\xspace}
\newcommand{\lcfp}{\ensuremath{\mathfrak{p}}\xspace}
\newcommand{\lcfU}{\ensuremath{\mathfrak{U}}\xspace}
\newcommand{\imc}{\ensuremath{\rightarrow}}
\newcommand{\conv}{\ensuremath{\twoheadrightarrow}}
\newcommand{\red}{\ensuremath{\;red\;}}
\title{The Calculi of Lambda-Conversion\\by Alonzo Church\\Annotated Notes and Ramblings of a Tired Student}
\author{Prepared by Ryan Flannery}
\date{}
\setcounter{section}{-1}
\begin{document}
\maketitle
\tableofcontents
\newpage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Chapter 0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Pre-Introduction}
What follows is a brief introduction to set theory,
How does set theory do this? Simple. Consider the following
constructions\ldots
\subsection{Numbers}
In set theory, we posit the existence of the empty set, denoted $\emptyset$,
and use this to build a representation of the natural numbers. $0$ (zero),
is appropriately represented by $\emptyset$, and every natural number $n$ is
the set of all {\em previous} natural numbers. So\ldots
\begin{eqnarray}
\text{Natural Number} & & \text{Set Representation} \\
0_{set} & = & \emptyset \\
1_{set} & = & \{ \emptyset \} \\
2_{set} & = & \{ \emptyset, \{ \emptyset \} \} \\
3_{set} & = & \{ \emptyset, \{ \emptyset \},
\{ \emptyset, \{ \emptyset \} \} \} \\
& \vdots & \\
n_{set} & = & \{ 0_{\text{set}}, 1_{\text{set}}, \ldots,
{n-1}_{\text{set}} \}
\end{eqnarray}
\subsection{Ordered Lists (Tuples)}
TUPLES!
\subsection{Relations}
In set theory, Relations are also represented by sets.
Relations have {\em arity}, that is, the number of things that a relation
{\em relates}. Consider the relation $\le$, which relates two things. Under
this relation, the numbers $4$ and $10$ are related as ``$4\le 10$''. Notice
here that the relation symbol appears between the things it relates (called
{\em infix} notation). For our purposes, let's use {\em prefix} notation,
where the relation symbol ($\le$ in our case) appears before the things it
relates. With this notation, $4\le 10$ becomes $\le(4,10)$.
Notice that the items being related are ordered, and their order cannot be
arbitrarily changed (with $\le$, it's clearly not the case that $\le(10,4)$).
So, for an arbitrary relation $R$, with arity $k$, we can say that the $k$
items $x_1,x_2,\ldots,x_k$ are {\em related by $R$} as $R(x_1,x_2,\ldots,x_k)$.
Notice then that we can use a tuple to represent the ordered list of items
{\em in a} relation, and the relation itself can be repsented simply as the
set of all such tuples.
As an example, we will use the above idea to construct a set-theoretic
representation of $\le$ (which we will call $\le_{set}$), as follows\ldots
\begin{equation}
\le\,=\,\left\{ (a,b)\mid\text{$a$ is less than or equal to $b$} \right\}
\end{equation}
That is, let $\le_{set}$ be the set of all 2-tuples of natural numbers $(x,y)$
such that $x$ is less than or equal to $y$. The set $\le_{set}$ would then
be nothing more than\ldots
\begin{eqnarray}
\le_{set} & = \{ & (0,0), (0,1), (0,2), (0,3), \ldots \\
& & (1,1), (1,2), (1,3), (1,4), \ldots \\
& & (2,2), (2,3), (2,4), (2,5), \ldots \\
& \vdots & \\
& & \}
\end{eqnarray}
Of course, all tuples and numbers would be replaced with their set-theoretic
representations as well.
Any statement of the form $x\le y$ could then be interpretted as the set
membership question $(x,y)\in \le_{set}$, since both $(x,y)$ and $\le_{set}$
are nothing more than sets.
\subsection{Functions}
Similarly, we can represent {\em functions} as sets. An $n$-ary function can
be represented as an $n+1$-ary relation.
Look a the well known binary function $+$ (plus), which is usually written in
the form $a+b=c$. We can {\em represent} this as a ternary relation,
\begin{equation}
+_{set}\,=\,\left\{ (a,b,c) \mid
\text{the sum of $a$ and $b$ is equal to $c$} \right\}
\end{equation}
The set representation of $+$ is then the following set.
\begin{eqnarray}
+_{set} & = \{ & (0,0,0), (0,1,1), (0,2,2), (0,3,3), \ldots \\
& & (1,0,1), (1,1,2), (1,2,3), (1,3,4), \ldots \\
& & (2,0,2), (2,1,3), (2,2,4), (2,3,5), \ldots \\
& \vdots & \\
& & \}
\end{eqnarray}
Any statement of form $x + y = z$ could be replaced simply with
$(x,y,z)\in +_{set}$.
\subsection{Who cares?}
Thus, in set theory, everytime we talk about numbers, ordered lists, relations,
and functions, we're {\em really} talking about sets. {\em Everything is a
set}, and the basic ``thing'' we talk about, and construct more complicated
``things'' from, is a set.
Although this representation maybe easy to work with, it's not necessarily
intuitive, especially when it comes to functions. Alonzo Church, the creator
of Lambda calculus, thought that conceptually, functions are more
like {\em actions}, where given a function $f$ and some input, and the
function performs some action (which is specied in the very definition of $f$)
until an output is produced. Alonzo Church created Lambda calculus as a
system of mathematics that reflects this approach. As an extreme opposite to
set theory, the basic ``thing'' in Lambda calculus {\em is the function}, and
all other things (including numbers, ordered lists, relations, and sets) are
represented through {\em functions}.
This representation of things may seem just as abstract and unintuitive
as the representation used in set theory, but it has a certain appeal when
working with algorithms, where answering
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Chapter 1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
\subsection{Functions in Lambda Calculus}
The underlying concept of Lambda Calculus (from here denoted by \lcalc) is
the {\em function}. Although not a new concept entirely, it is how \lcalc
treats functions that distinguishes it from other formal systems.
\begin{definition}[Function]
A {\em function} is a rule of correspondence by which when anything is
given (as {\em argument}) another thing (the {\em value} of the function
for {\em that} argument) may be obtained. More simply, a function is an
{\em action} that is applied to one thing (the argument) to obtain another
thing (the value). A function need not be applicable to everything; a
function may only make sense for a certain set of arguments, called the
{\em range of arguments}. The set of all values obtained from a applying
all possible arguments to a function is called the {\em range of values}.
\end{definition}
Unlike set theory, where functions are treated as sets of ordered tuples, in
\lcalc functions are treated as {\em actions}, where applying the function
to something (arguments) yields something else (a value). In pure \lcalc,
everything is be treated as a function. Even numbers, as we'll soon see, are
functions.
\begin{notation}
Let $f$ denote a function. Then $(f\alpha)$ denotes the value of $f$ for
the argument $\alpha$.\\
We also adopt the following shorthand: $(f\alpha) = f\alpha$.
\end{notation}
Note that the treatment of functions in \lcalc (as an action) allows a
function to be applied to itself. That is, for a function $f$, there is
nothing preventing $f$ from being in its own range.
Two fundamental function in \lcalc are defined as follows\ldots
\begin{definition}[\lcI, the identity function]
\lcI is defined as follows: $(\lcI x)$ is $x$, whatever $x$ may be.
\end{definition}
\begin{definition}[\lcH]
\lcH is defined as the function that always returns the identity
function. That is, $(\lcH x)$ is \lcI for whatever $x$ may be.
\end{definition}
\subsection{Notions of Equality}
The concept of a function in \lcalc allows the notion of equality between
functions to be defined in two separate manners. The first deals solely
with the result of the action performed by a function and the second deals
with how that action is performed.
\begin{definition}[Extensional Equality]
Two functions, $f$ and $g$, are said to be in {\em extension} if they have
the same range of arguments and for every element $\alpha$ that belongs to
this range, $(f\alpha)$ is the same as $(g\alpha)$.
\end{definition}
Let $f = x + 1$ and $g = (x + 3) - 2$. Clearly, for every possible
numerical argument $\alpha$, $(f\alpha) = (g\alpha)$. Yet the manner in
which $f$ and $g$ reach their value is slightly different. This brings us to
the next notion of equality\ldots
\begin{definition}[Intensional Equality]
Two functions are said to be functions in {\em intension} if they are
extensionally equivalent and identical in the manner by which they produce
some value provided some argument(s).
\end{definition}
\subsection{Functions of Several Variables}
Functions in \lcalc can take more than one argument, however the meaning is
interpreted slightly different from our previous notions of functions. In
\lcalc, a function of $n+1$ arguments is treated as a function of one
argument whose values are functions of (up to) $n$ arguments.
For example, let $f$ be a function of two arguments. Then $((fa)b)$ is how
we would interpret providing two arguments, $a$ and $b$ to $f$.
\begin{notation}
We adopt the following shorthand: $((fa)b) = (fab) = fab$.
\end{notation}
Notice the following: let $f$ denote a function of 3 variables. Then $fabc$
denotes the value of $f$ for the arguments $a$, $b$, and $c$. Given our
interpretation of functions, note that $fa$ is a function whose value is a
function of two variables, $fab$ is a function whose value is a function of
one variable, and $fabc$ denotes an actual value (potentially another function
of any number of arguments). In this respect, we may provide as many
arguments as we wish to any function!
\begin{definition}[\lcK, the constancy function]
\lcK is defined such that $Kxy$ is $x$ for whatever $x$ and $y$ may be.
\end{definition}
Note that $\lcK\lcI\lcI$ is \lcI and $\lcK\lcH\lcI$ is \lcH. More
interestingly, note that $\lcK\lcI$ is \lcH and that $\lcK\lcK$ is, simply,
\lcK.
Next, we define the following functions\ldots
\begin{definition}[\lcT]
$\lcT xf$ is $(fx)$
\end{definition}
\begin{definition}[\lcJ]
$\lcJ fxyz$ is $fx(fzy)$
\end{definition}
\begin{definition}[\lcB, the product function]
$\lcB fgx$ is $f(gx)$
\end{definition}
\begin{definition}[\lcC, the converse function]
$\lcC fxy$ is $(fyx)$
\end{definition}
\begin{definition}[\lcD]
$\lcD x$ is $(xx)$
\end{definition}
\begin{definition}[\lcW]
$\lcW fx$ is $(fxx)$
\end{definition}
\begin{definition}[\lcS]
$\lcS nfx$ is $f(nfx)$ \\
{\em NOTE: This is distinctly different from the function \lcS defined in
Barendregt's text. There, $\lcS fgx$ is $fx(gx)$.}
\end{definition}
\subsection{Abstraction}
\begin{notation}
Let \lcM denote an {\em expression} containing a variable $x$ that is free
(that is, the meaning of \lcM depends upon the value of $x$). Then
$(\lambda x\lcM)$ denotes a {\em function} whose value for some argument
$\alpha$ is denoted by substituting all occurrences of $\alpha$ in \lcM.\\
Notice that if \lcM does not contain the symbol $x$, then the value of
$(\lambda x\lcM)$ is constant and equal to \lcM.\\
Also, although $x$ is free in \lcM, it is {\em bound} in
$(\lambda x\lcM)$ and that $\lambda x$ is an incomplete expression!
$(\lambda x$ has no meaning on its own.
\end{notation}
In the above, note the distinction between an expression and a function. Take
the following two expressions, $\lcM = (x+x)$ and $\lcN = (y+y)$. The
equation $\lcM = \lcN$ then expresses a relation between the numbers denoted
by $x$ and $y$, and its truth depends on determining $x$ and $y$.\\
Now look at $(\lambda x\lcM) = (\lambda y\lcN)$:
\begin{equation} (\lambda x(x+x)) = (\lambda y(y+y)) \end{equation}
This equation denotes something entirely different; it says that the two
functions $(\lambda x\lcM)$ and $(\lambda y\lcN)$ are equivalent (which is
true) and makes no mention of the values of $x$ or $y$.
When we added the $\lambda x$ to the expression \lcM, we created a function.
This operation is called {\em abstraction} and the symbol $\lambda x$ is
called the {\em abstract operator}.
\begin{notation}
The expression $(\lambda x(\lambda y \lcM))$ is abbreviated
$(\lambda xy.\lcM)$ and denotes a function whose value for the argument $x$
is denoted by $(\lambda y\lcM)$.
\end{notation}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Chapter 2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Lambda-Conversion}
\subsection{Primitive Symbols and Formulas}
Now we are ready to lay out the language of \lcalc. It consists of the
following primitive symbols called {\em improper symbols}:
\begin{center} $\lambda$ (the abstraction operator), (, ) \end{center}
and an infinite list of {\em variables} which will use the English alphabet:
\begin{center}
$a, b, c, \ldots , x, y, z, \overline{a}, \overline{b}, \ldots,
\overline{\overline{a}}, \ldots$
\end{center}
\begin{definition}[Formula]
A formula is any finite sequence of primitive symbols.
\end{definition}
\begin{definition}[Well-Formed Formula]
A well-formed formula is any formula where all variables occur either free
or bound, according to the following rules:
\begin{enumerate}
\item A variable $x$ is a well-formed formula and the occurrence of $x$
in this formula (itself) is free.
\item If \lcM and \lcN are well-formed, then $(\lcM\lcN)$ is also
well-formed. Any variables occurring free (or bound) in \lcM or
\lcN are considered free (or bound) in $(\lcM\lcN)$.
\item If \lcM is well-formed and contains the free variable $x$, then
$(\lambda x\lcM)$ is also well-formed and all occurrences of $x$ in
$(\lambda x\lcM)$ are bound.
\end{enumerate}
\end{definition}
\begin{notation}
In \lcalc, bold capital letters
($\boldsymbol{\mathit{M, N, A, B, \ldots}}$) to stand for formulas, and
bold small letters
($\boldsymbol{\mathit{a, b, c, \ldots}}$) to stand for variables.\\
Unless otherwise indicated in a particular case, all formulas are assumed
to be well-formed.
\end{notation}
We now introduce notation that we will use when the concept of substitution
comes in\ldots
\begin{notation}
Let $S^{x}_{\lcN} \lcM|$ denote the formula that results when all
occurrences of $x$ in \lcM are replaced with \lcN.\\
This is equivalent to Barendregt's syntax: $\lcM[x:=\lcN]$. Since
Barendregt's syntax is significantly easier and faster, it shall be used
henceforth in these notes.
\end{notation}
The $\imc$ may be read as ``stands for'' (among other things, as we'll see
later) and is used to expand formulas, replacing some sub-term with the
meaning of that sub-term. For example, the function \lcI defined above is
represented formally by the function $\lambda aa$, so\ldots
\begin{equation} \lcI \imc (\lambda aa) \end{equation}
And, accordingly,
\begin{equation} (\lcI\lcI) \imc ((\lambda aa)(\lambda aa)) \end{equation}
We now make the following definitions:
\begin{definition}\label{LambdaAlgebra}
\begin{eqnarray}
\lbrack\lcM + \lcN\rbrack & \imc & (\lambda a(\lambda b((\lcM a)
((\lcN a)b)))) \\
\lbrack\lcM\times\lcN\rbrack & \imc & (\lambda a(\lcM(\lcN))) \\
\lbrack\lcM^{\lcN}\rbrack & \imc & (\lcN\lcM)
\end{eqnarray}
\end{definition}
\begin{notation}
For convenience, the parentheses will often be omitted for large formulas.
We should keep in mind when replacing the parentheses that grouping in
\lcalc is {\em left-associative}. That is, $\lcM\lcN\lcS$ is really
$((\lcM\lcN)\lcS)$.\\
Similarly for expressions with brackets, $x + y + z$ is really
$[ [ x + y ] + z ]$.
\end{notation}
One bit of confusion that may occur when evaluating expressions in \lcalc
is in formulas of the form $(\lambda x\lcM)$. If we let $\lcM = xyz$, then
we have $(\lambda xxyz)$. This is ambiguous; where does the abstraction
operator stop and the expression begin? To solve this, we use the ``.''.
\begin{notation}
When omitting a set of parentheses or brackets may cause ambiguity, use a
``.'' in place of the left parenthesis or bracket. It is to be
interpreted as follows: replace the ``.'' with a left parentheses and
insert a right parenthesis as far the right as possible. So, for example:
$(\lambda x.\lcM\lcN) \imc (\lambda x(\lcM\lcN))$,
$(\lambda xy.\lcM\lcN) \imc (\lambda x(\lambda y(\lcM\lcN)))$, and
$(\lambda x.\lambda y.\lcM\lcN) \imc (\lambda x(\lambda y(\lcM\lcN)))$
\end{notation}
Now that the formal language of \lcalc has been established, here are the
formal definitions for the functions defined thus far:
\begin{eqnarray}
\lcI & \imc & \lambda a.a \\
\lcH & \imc & \lambda a.I \\
\lcT & \imc & \lambda xf.fx \\
\lcJ & \imc & \lambda fxyz.fx(fzy) \\
\lcB & \imc & \lambda fgx.f(gx) \\
\lcC & \imc & \lambda fxy.fyx \\
\lcD & \imc & \lambda x.xx \\
\lcW & \imc & \lambda fx.fxx \\
\lcS & \imc & \lambda nfx.f(nfx)
\end{eqnarray}
\subsection{Conversion}
We now introduce the fundamental operations on well-formed formulas in
\lcalc: conversion. Although there are many forms of conversion, these are
the three we begin with:
\begin{enumerate}
\renewcommand{\labelenumi}{\Roman{enumi}}
\item Given a formula, we can replace any part \lcM with $\lcM[x:=y]$
as long as $x$ is not a free variable of \lcM and $y$ does not occur
in \lcM. Notice, all we are doing here is changing variable names. \\
This method of conversion is often called {\bf $\alpha$-conversion}.
\item Given a formula, we can replace any part $((\lambda x\lcM)\lcN)$
with $\lcM[x:=\lcN]$ as long as the bound variables of \lcM are
distinct both from $x$ and from the free variables of \lcN.
Application of this rule is called Contraction. \\
This method of conversion is often called {\bf $\beta$-conversion}.
\item Given a formula, we can replace any part $\lcM[x:=\lcN]$ with
$((\lambda x\lcM)\lcN)$ as long as $((\lambda x\lcM)\lcN)$ is
well-formed and the bound variables of \lcN are distinct from both $x$
and the free variables of \lcN. {\em NOTE: where the previous rule
provides a sort of reduction, this rule provides the opposite:
expansion.}
\renewcommand{\labelenumi}{\arabic{enumi}}
\end{enumerate}
\begin{definition}
A {\em part} of a formula is any consecutive well-formed part that does not
immediately follow an occurrence of the symbol $\lambda$.
\end{definition}
Notice, Rule I can convert $ab(\lambda aa)(\lambda aa)$ into
$ab(\lambda bb)(\lambda aa)$, and Rule III can convert $(\lambda aa)$ into
$(\lambda a.(\lambda aa)a)$.
Rules I-III are {\em definite}, in that given any two formulas \lcM and
\lcN, we can determine if \lcN can be derived from \lcM using one of the
rules and, if so, which one.
\begin{definition}[Immediately Convertible]
If \lcM can be converted into \lcN by the application of one of rules
I-III then we say \lcM {\em immediately converts} to \lcN, written
$\lcM\ imc\ \lcN$, or $\lcM\imc\lcN$.
\end{definition}
\begin{definition}[Convertible]
If \lcM can be converted into \lcN by the application of a finite number
of rules I-III then we say \lcM {\em converts} to \lcN, written
$\lcM\ conv\ \lcN$, or $\lcM\conv\lcN$.
\end{definition}
\begin{definition}[Interconvertible]
If $\lcM\conv\lcN$, then we say \lcM and \lcN are interconvertible.
\end{definition}
Notice that conversion (as defined thus far) is transitive, symmetric, and
reflexive (proof omitted).
\begin{definition}[Expansion]
A conversion that contains no applications of Rule II and exactly one
application os Rule III is called expansion.
\end{definition}
\begin{definition}[Reduction]
A conversion that contains no applications of Rule III and exactly one
application os Rule II is called reduction. Further, we say that \lcM
{\em reduces} to \lcN ($\lcM\red\lcN$ for short) if, by a finite number
of reductions, \lcM converts to \lcN.
\end{definition}
\begin{definition}[Normal Form]
A well-formed formula is said to be in normal-form if it contains no part
of the form $((\lambda x\lcM)\lcN)$.
\end{definition}
\begin{definition}[Principle Normal Form]
A well-formed formula is said to be in principle normal-form if it is in
normal form and the bound variables occur in alphabetical ordering from
left to right. Note that any formula in normal form can thus be converted
into principle normal form by a finite number of applications of rule I.
\end{definition}
\subsection{(Selections from) Fundamental Theorems on Well-Formed Formulas and
on the Normal Form}
Below is only a few of the theorems provided in \S7 of Church's text.
\begin{theorem}
If \lcM is well-formed and $\lcM\conv\lcN$ then \lcN is well-formed.
\end{theorem}
\begin{theorem}
If \lcM is well-formed and $\lcM\conv\lcN$ then \lcM and \lcN have
the same free variables.
\end{theorem}
Just as variables occur either free or bound in a formula, we define similar
notions for parts of formula. A well-formed part \lcP of a formula \lcK
is a free occurrence of \lcP in \lcK if every free occurrence of a variable
in \lcP is also a free occurrence of that variable in \lcK. Otherwise,
\lcP is bound in \lcK.
Further, we extend the syntax $\lcM[x:=\lcN]$ to handle this new notion of
free/bound parts.
\begin{notation}
Let $\lcM[\lcN:=\lcP]$ denote the formula that results when all occurrences
of \lcN in \lcM are replaced with \lcP.
\end{notation}
\begin{theorem}
If $\lcM\conv\lcN$ then there is a conversion of \lcM into \lcN in
which no expansion precedes any reduction.
\end{theorem}
\begin{theorem}
If \lcN is a normal form of \lcM, then there is a sequence of
conversions from \lcM into \lcN using only rules I and II (reduction).
\end{theorem}
\begin{theorem}
If \lcM has a normal form, its normal form is unique within applications
of rule I.
\end{theorem}
\begin{theorem}\label{Theorem30}
If \lcM has a normal form, it has a unique principle normal form. Notice
that once a normal form is reached, a finite number of $\alpha$-conversions
will produce a formula in principle normal form.
\end{theorem}
\begin{theorem}
If \lcN is a normal form of \lcM, then there is a number $m$ such that
any sequence of reductions starting from \lcM will lead to \lcN (within
applications of rule I) after at most $m$ reductions. \\
Basically, if \lcN has a normal form then there is an upper bound, $m$,
on the number of reductions taken to obtain the normal form.
\end{theorem}
\begin{theorem}\label{KeyTheorem}
If \lcM has a normal form, every well-formed part of \lcM has a normal
form.
\end{theorem}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Chapter 3
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Lambda-Definability}
\subsection{Lambda-Definability of Functions of Positive Integers}
In \lcalc, everything is a function. Even numbers. The natural numbers
(1, 2, 3, \ldots) are represented in the following fashion:
\begin{definition}[Natural Numbers]
We define the natural numbers as follows:
\begin{eqnarray}
1 & \imc & \lambda ab.ab \\
2 & \imc & \lambda ab.a(ab) \\
3 & \imc & \lambda ab.a(a(ab)) \\
& \vdots & \nonumber
\end{eqnarray}
Notice, any number $x$ can be defined as the function that takes two
arguments, $f$ and $y$, and it applies $f$ $x$-times to $y$.
\end{definition}
To avoid confusion, numbers of multiple digits will have a bar over them to
distinguish them from sequences of single-digit numbers. For example, we
will use $\overline{11}$ to denote eleven and $11$ to denote the function $1$
applied to itself.
\begin{definition}[$\lambda$-Definable]
A function $F$ of $n$ arguments, all of which are natural numbers, is
$\lambda$-definable if there is a formula \lcF such that the following
requirements are met:
\begin{enumerate}
\item If $m_1, m_2, \ldots , m_n, l$ are positive integers and
$Fm_{1}m_{2}\ldots m_{n} = l$, and $\lcM_1, \lcM_2 \ldots
\lcM_n, \lcL$ represent the integers $m_1, m_2, \ldots, m_n, l$
respectively, then $\lcF\lcM_{1}\lcM_{2}\ldots\lcM_{n}\conv\lcL$
\item If the function $F$ has no value for the positive integers
$m_1, m_2, \ldots, m_n$ as arguments, and $\lcM_1, \lcM_2, \ldots
\lcM_n$ represent $m_1, m_2, \ldots, m_n$ respectively, then
$\lcF\lcM_{1}\lcM_{2}\ldots\lcM_{n}$ has no normal form.
\end{enumerate}
\end{definition}
Church then provides the following $\lambda$-definitions for common functions:
\begin{eqnarray}
Successor: & & \lambda abc.b(abc) \\
Addition: & & \lambda ab.a + b \\
Multiplication: & & \lambda ab.a \times b \\
Exponentiation: & & \lambda ab.a^b
\end{eqnarray} Where ``$+$'', ``$\times$'', and exponentiation are to be
interpreted as defined in Definition \ref{LambdaAlgebra}.
For the rest of Church's text, the successor function is abbreviated using
\lcS and is not to be confused with the previous definition for \lcS. How
we are not to confuse the two functions is beyond me, however it seems that
in almost all contexts for the rest of the text, \lcS will mean
``successor''.
\subsection{Ordered Pairs \& Triads and the Predecessor Function}
It is often useful to work with ordered groups of values. To do so in
\lcalc, we introduce the following notation for ordered pairs and triads.
It's easy to see how to extend the syntax for ordered $n$-tuples.
\begin{notation}
\begin{eqnarray}
\lbrack \lcM,\lcN \rbrack & \imc & \lambda a.a\lcM\lcN \\
\lbrack \lcL,\lcM,\lcN \rbrack & \imc & \lambda a.a\lcL\lcM\lcN
\end{eqnarray}
\end{notation}
Church then defines the following functions which extract particular elements
from an ordered pair/triad:
\begin{definition}
For pairs, we have\ldots
\begin{eqnarray}
2_1 & \imc & \lambda a.a(\lambda bc.c\lcI b) \\
2_2 & \imc & \lambda a.a(\lambda bc.b\lcI c)
\end{eqnarray}
For triads, we have\ldots
\begin{eqnarray}
3_1 & \imc & \lambda a.a(\lambda bcd.c\lcI d\lcI b) \\
3_2 & \imc & \lambda a.a(\lambda bcd.b\lcI d\lcI c) \\
3_3 & \imc & \lambda a.a(\lambda bcd.d\lcI c\lcI d)
\end{eqnarray}
\end{definition}
So, for example, $2_1 [\lcM,\lcN]\conv\lcM$, $2_2 [\lcM,\lcN]\conv\lcN$,
$3_1 [\lcL,\lcM,\lcN]\conv\lcL$, $3_2 [\lcL,\lcM,\lcN]\conv\lcM$, and
$3_3 [\lcL,\lcM,\lcN]\conv\lcN$.
The predecessor function is then defined as follows:
\begin{definition}[Predecessor Function]
For any integer $n$ other than $1$, $Pn$ has a value of $n-1$. For $1$,
$P1$ has a value of $1$.
\begin{eqnarray}
\lcP & \imc & \lambda a.3_3 (a(\lambda b[\lcS(3_1 b),\ 3_1 b,\ 3_2 b])
[1,\ 1,\ 1])
\end{eqnarray}
\end{definition}
Using the predecessor function, a form of subtraction can be defined:
\begin{definition}[Subtraction]
For any two integers $a$ and $b$, $a\ \dot{-}\ b$ has a value of $1$ if
$a < b$ and $a - b$ otherwise.
\begin{equation}
\lbrack\lcM\ \dot{-}\ \lcN\rbrack \imc \lcN\lcP\lcM
\end{equation}
\end{definition}
Using the predecessor function, we can then define the typical $min$ and
$max$ functions as follows:
\begin{definition}[Min/Max Functions]
The functions that return the greatest of two positive integers and the
lesser of two positive integers are defined as follows:
\begin{eqnarray}
min & \imc & \lambda ab.\lcS\ \dot{-}\ .Sb\ \dot{-}\ a \\
max & \imc & \lambda ab.[a + b]\ \dot{-}\ min\ ab
\end{eqnarray}
\end{definition}
Later, we'll make use of the following few functions:
\begin{definition}[$Z$ and $Z'$]
To define $Z$ and $Z'$, we first need the following:
\begin{eqnarray}
\lcfL & \imc & \lambda\beta . \beta(\lambda c\beta\lambda d[dPc(\lambda e.e1\lcI)(\lambda fg . fg5)c,\ dPc(\lambda h.h1\lcI5)(\lambda ijk.kij(\lambda l.l1))d]) \\
\lcfU & \imc & \lambda\alpha . \alpha\lcfL[1,\;1]
\end{eqnarray}
Now, we may define $Z$ and $Z'$ as follows:
\begin{eqnarray}
Z & \imc & \lambda\alpha . 2_2 (\lcfU\alpha) \\
Z' & \imc & \lambda\alpha . \lcfU\alpha(\lambda\beta c.b\dot{-}c)
\end{eqnarray}
\end{definition}
Notice the behavior of $Z$ and $Z'$ with integer arguments\ldots
\[\begin{array}{cc}
Z1\conv 1 & Z'1\conv 1 \\
Z2\conv 1 & Z'2\conv 2 \\
Z3\conv 2 & Z'3\conv 1 \\
Z4\conv 1 & Z'4\conv 3 \\
Z5\conv 2 & Z'5\conv 2 \\
Z6\conv 3 & Z'6\conv 1 \\
Z7\conv 1 & Z'7\conv 4
\end{array}\]
In this sense, we can use $Z$ and $Z'$ prime to enumerate the natural
numbers. Indeed, the infinite sequence of ordered pairs:
\begin{equation}
[Z1,\;Z'1],\;[Z2,\;Z'2],\;[Z3,\;Z'3],\ldots
\end{equation}
contains all ordered pairs of positive integers with no repetitions.
The parity function is defined as follows:
\begin{definition}[Parity Function]
The parity of a positive integer is $1$ if the integer is odd and $2$ if it
is even. It is defined by the following function:
\begin{eqnarray}
par & \imc & \lambda a.a(\lambda b.3\ \dot{-}\ b)2
\end{eqnarray}
\end{definition}
\subsection{Propositional Functions}
\begin{definition}[Propositional Function]
Any function whose values are truth values (true / false).
\end{definition}
\begin{definition}[Property]
A propositional function of one variable.
\end{definition}
\begin{definition}[Relation]
A propositional function of two variables.
\end{definition}
In pure \lcalc, we do not have such primitives as ``true'' and ``false''
(all we have are functions). So, to work with propositional functions, we
have the notion of a characteristic function:
\begin{definition}[Characteristic Function]
The characteristic function associated with a propositional function is the
function whose value is $2$ (the $\lambda$-function) when the value of the
propositional function is true, whose value is $1$ when the propositional
function is false, and which has no value otherwise.
\end{definition}
Note that the choice of $2$ and $1$ in the above definition is arbitrary.
A propositional function of natural numbers is said to be $\lambda$-definable
if the associated characteristic function is $\lambda$-definable.
Some examples of $\lambda$-definable characteristic functions follow:
\begin{definition}[Strict Greater-Than and Equality for Natural Numbers]
\begin{eqnarray}
exc & \imc & \lambda ab. min\ 2\ [Sa\ \dot{-}\ b] \\
eq & \imc & \lambda ab.4\ \dot{-}\ .\ exc\ ab + exc\ ba
\end{eqnarray}
\end{definition}
Let $R$ be a $\lambda$-definable propositional function of $n+1$ integer
arguments. In the case that $R$ has a value for every set of arguments, the
function $F$ can be described by saying that $Fx_{1}x_{2}\ldots x_{n}$ is
the least positive integer $y$ such that $Rx_{1}x_{2}\ldots x_{n}y$ holds.
Let \lcfG be defined as follows:
\begin{definition}[\lcfG]
\begin{equation}
\lcfG \imc \lambda n.n(\lambda r.r(\lambda s.s1\lcI\lcI(\lambda
xgt.g1(tx)\lcI x)))(\lambda f.f\lcI 1\lcI\lcI)(\lambda xgt.g(t(\lcS x))
(\lcS x)gt)
\end{equation}
\end{definition}
(Quite a mouthful!) Next, notice the following\ldots
\begin{eqnarray}
\label{G1} \lcfG 1\lcN\lcfG\lcT & \red & \lcfG(\lcT(\lcS\lcN))(\lcS\lcN)\lcfG\lcT \\
\label{G2} \lcfG 2\lcN\lcfG\lcT & \red & \lcN
\end{eqnarray}
{\em NOTE: In the above two equations, \lcS is the successor function.}
Using \lcfG, we can define the function \lcfp as follows:
\begin{definition}[\lcfp, the Kleene \lcfp function]
\begin{equation} \lcfp \imc \lambda tx.\lcfG(tx)x\lcfG t \end{equation}
Note that if \lcN represents a positive integer and $\lcT\lcN$ converts
to either $1$ or $2$ (i.e. \lcT is simply a characteristic function), then
$\lcfp\lcT\lcN\red\lcN$ if $\lcT\lcN\conv 2$ and
$\lcfp\lcT\lcN\conv\lcfp\lcT(\lcS\lcN)$ if $\lcT\lcN\conv 1$. Further,
if $\lcT\lcN$ has no normal form then $\lcfp\lcT\lcN$ has no normal form.
\end{definition}
At first glance, the \lcfG and \lcfp functions seem too much to comprehend. A
closer look at what they do, however, makes them much easier to understand.
The \lcfp function is a ``generic'' version of the two equations in \ref{G1}
and \ref{G2}. That is, for a given characteristic function \lcT and a natural
number \lcN, $\lcfp\lcT\lcN$ will reduce to either equation \ref{G1} or
\ref{G2}, depending on what $\lcT\lcN$ reduces to (remember, \lcT is a
characteristic function, so it always reduces to either 1 or 2). Equation
\ref{G2} always reduces to simply \lcN. Equation \ref{G1}, however (and this
is where it gets interesting) reduces to, essentially, $\lcfp\lcT(\lcN + 1)$!
It effectively increases \lcN and starts over!
The Kleene function, then, provides a convenient way of working with
propositional functions on the natural numbers. Say \lcN represents some
positive integer $n$ and \lcT $\lambda$-defines the characteristic function
associated with some property $T$ of positive integers. $\lcfp\lcT\lcN$ is
then convertible into the formula that represents the least positive $y$, not
less than $n$, such that $\lcT y$ holds (given that such a $y$ exists).
The Kleene function can be used to provide a more intuitive definition for
division and subtraction, which we shall denote by $-$ as opposed to the
previous $\dot{-}$.
\begin{definition}
\begin{eqnarray}
\lbrack\lcM - \lcN\rbrack & \imc & \lcfp(\lambda a.eq\ \lcM\
\lbrack\lcN+a\rbrack)1 \\
\lbrack\lcM\div\lcN\rbrack & \imc & \lcfp(\lambda a.eq\ \lcM\
\lbrack\lcN\times a\rbrack)1
\end{eqnarray}
Note that $x - y$ has no value if $x < y$ and $x \div y$ has no value
unless $x$ is a positive integer multiple of $y$.
\end{definition}
\subsection{Definition by Recursion}
Previously, the {\em composition} of two functions, $(f \circ g)\overline{x}$,
was defined as $f(g\overline{x}))$. Now, the notion of composition is
extended for any number of functions.
\begin{definition}[Composition]
A function $F$ of $n$ positive integer arguments is said to be defined by
composition in terms of functions $G$ and $H_1, H_2, \ldots, H_m$ of
positive integers if $F$ is defined as follows:
\begin{equation}
Fx_1 x_2 \ldots x_n = G(H_1 x_1 x_2 \ldots x_n)
(H_2 x_1 x_2 \ldots x_n) \ldots (H_m x_1 x_2 \ldots x_n)
\end{equation}
Notice that if $n = m = 1$, then we have $Fx = G(Hx)$, which corresponds to
our previous notion of composition for two functions.
\end{definition}
\begin{definition}[Primitive Recursion]
A function $F$ of $n+1$ positive integer arguments is said to be defined by
primitive recursion in terms of functions $G_1$ and $G_2$ of positive
integers if $F$ is defined as follows:
\begin{eqnarray}
Fx_1 x_2 \ldots x_n 1 & = & G_1 x_1 x_2 \ldots x_n \\
Fx_1 x_2 \ldots x_n (y+1) & = & G_2 x_1 x_2 \ldots x_n y (Fx_1 x_2 \ldots x_n y)
\end{eqnarray}
Note that if we allow $n = 0$, then $G_1$ is simply some constant positive
integer $\alpha$.
\end{definition}
Using this notion of Primitive Recursion, the class of all primitive recursive
functions of positive integers can now be defined.
\begin{definition}[Primitive Recursive Functions]
We use the following criteria to define all primitive recursive functions:
\begin{enumerate}
\item Any function $F$ that is equivalent to one of the following 3
functions is primitive recursive:
\begin{enumerate}
\item The function $C$ such that $Cx = 1$ for every positive
integer $x$
\item The successor function of positive integers
\item The function $U_{i}^{n}$, where $n$ and $i$ are any positive
integers and $i \leq n$, such that
$U_{i}^{n} x_1 x_2 \ldots x_n = x_i$ are primitive recursive.
\end{enumerate}
\item If the function $F$ of $n$ arguments is defined by composition
in terms of $G, H_1, \ldots, H_m$, and if $G, H_1, \ldots, H_m$
are primitive recursive, then $F$ is primitive recursive.
\item If the function $F$ of $n+1$ arguments is defined by primitive
recursion in terms of functions $G_1$ and $G_2$, and if $G_1$ and
$G_2$ are primitive recursive, then $F$ is primitive recursive.
\end{enumerate}
\end{definition}
The class of primitive functions includes all of the common numerical
functions, including determining the greatest common divisor, determining
quotient and remainder in integer division, and finding the $x^{th}$ prime
number.
\begin{theorem}
Every primitive recursive function of positive integers is
$\lambda$-definable.
\end{theorem}
Now, we have two methods for defining functions: composition and primitive
recursion. For both, any particular value of a function $F$ (defined by
either method) can be found by a finite number of reductions. By keeping this
requirement, we can extend the notion of recursion in the following fashions.
\begin{definition}[General Recursion]
A function $F$ is generally recursive if it meets the requirement (1) of
the primitive recursive functions and if all defined functions composing
$F$ have a value for every set of integer arguments.
\end{definition}
and\ldots
\begin{definition}[Partial Recursion]
A function $F$ is partially recursive if it only meets the first
requirement of the primitive recursive functions.
\end{definition}
\begin{theorem}
Every partial recursive function of positive integers is
$\lambda$-definable.
\end{theorem}
\begin{theorem}
Every $\lambda$-definable function of positive integers is partially
recursive.
\end{theorem}
Recursion is a powerful notion in \lcalc, as it is elsewhere, and as proven
above the notion of recursion is equivalent to many other notions. Other
equivalent notions are {\em effective calculability}, {\em computability},
and the notion of a {\em finite combinatory process}. Some of these notions
are defined below.
\begin{definition}[Effectively Calculable Function of Positive Integers]
A function $F$ is effectively calculable if there exists a method of
calculating the value of $F$ given any set of positive integer arguments.\\
Note that this definition is equivalent to $\lambda$-definability! It is
simply a more intuitive definition of $\lambda$-definability.
\end{definition}
\begin{definition}[Computable]
A function $F$ is computable (roughly speaking) if it is possible to make
a finite calculating machine capable of computing any required value of
the function (Turing).
\end{definition}
So, what functions aren't recursive? Equivalently, what functions aren't
effectively calculable? An example of such of function follows. If the set
of well-formed formulas of \lcalc is enumerated in a straightforward way, and
if $F$ is the function such that $F$ is $2$ if the $x^{th}$ formula has a
normal form and $1$ if it does not, then $F$ is not $\lambda$-definable.
This leads to the conclusion that the condition of having a normal form is not
sufficient for effective calculability.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Chapter 4
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Combinations \& \Godel Numbers}
\subsection{Combinations}
\begin{definition}[$S$-Combinations]
Let $s$ be any set of well-formed formulas. A formula is called an
$s$-combination if it is defined by the following two rules:
\begin{enumerate}
\item Any formula of the set $s$, and any variable standing alone is an
$s$-combination.
\item If \lcA and \lcB are $s$-combinations, then $\lcA\lcB$ is an
$s$-combination.
\end{enumerate}
The set of all $s$-combinations is called the ``class of $s$-combinations''.
\end{definition}
Church notes that for the cases we are interested in, the formulas of $s$ will
not contain free variables and none will be of the form $\lcA\lcB$. In this
case, any {\em term} of an $s$-combination will be either a free variable or
one of the formulas of $s$.
If $s = \emptyset$, then the $s$-combinations will be call {\em combinations
of variables}.
If $s$ consists of the two formulas \lcI and \lcJ defined as follows:
\begin{eqnarray}
\lcI & \imc & \lambda a.a \\
\lcJ & \imc & \lambda abcd.ab(adc)
\end{eqnarray}
then the $s$-combinations will simply be called {\bf\em combinations}.
{\em NOTE: These definitions of \lcI and \lcJ are the same as presented
earlier}
A function that will prove useful when dealing with combinations is $\tau$,
defined as follows:
\begin{definition}[$\tau$] Let\ldots
\begin{eqnarray} \tau & \imc & \lcJ\lcI\lcI \end{eqnarray}
And notice that $\tau\conv\lambda ab.ba$, or, $\tau\lcA\lcB\conv\lcB\lcA$.
\end{definition}
If \lcM is any combination containing $x$ as a free variable, then we define
an associated combination $\lambda_x \lcM|$, which does not contain $x$
as a free variable, as follows:
\begin{enumerate}
\item $\lambda_x x|$ is $\lcI$
\item If \lcB contains $x$ as a free variable and \lcA does not, then
$\lambda_x \lcA\lcB|$ is
$\lcJ\tau\lambda_x \lcB|(\lcJ\lcI\lcA)$
\item If \lcA contains $x$ as a free variable and \lcB does not, then
$\lambda_x \lcA\lcB|$ is $\lcJ\tau\lcB\lambda_x \lcA|$
\item If both \lcA and \lcB contain $x$ as a free variable, then
$\lambda_x \lcA\lcB|$ is $\lcJ\tau\tau(\lcJ\lcI(\lcJ\tau\tau(\lcJ\tau\lambda_x \lcB|(\lcJ\tau\lambda_x \lcA|\lcJ))))$
\end{enumerate}
The next theorem is easily seen from the construction presented above
\begin{theorem}
If \lcM is a combination containing $x$ as a free variable, then
$\lambda_x \lcM| \conv \lambda x\lcM$.
\end{theorem}
Now, we can define the notion of {\em combinations that belong to a well-
formed formula\ldots}
\begin{definition}[Combinations Belonging to a Well-Formed Formula]
\begin{enumerate}
\item The combination belonging to a variable $x$ is $x$.
\item The combination belonging to $\lcF\lcA$ is $\lcF'\lcA'$, where
$\lcF'$ and $\lcA'$ are the combinations belonging to \lcF and \lcA
respectively.
\item The combination belonging to $\lambda x\lcM$ is $\lambda_x \lcM'|$,
where $\lcM'$ is the combination belonging to \lcM.
\end{enumerate}
\end{definition}
The following theorem is key when dealing with combinations\ldots
\begin{theorem}\label{wff2comboTheorem}
Every well-formed formula is convertible into a combination belonging to it.
\end{theorem}
\begin{theorem}
The combinations belonging to \lcM and the combinations belonging to
\lcN are identical if and only if $\lcM\conv\lcN$ using only Rule (1).
\end{theorem}
\subsection{Primitive Sets of Formulas}
\begin{definition}[Primitive Set]
A set $s$ of well-formed formulas is called a primitive set if the
following conditions are met\ldots
\begin{enumerate}
\item The formulas of $s$ contain no free variables.
\item None of the formulas are of the form $\lcA\lcB$.
\item Every well-formed formula of $s$ is convertible into an
$s$-combination.
\end{enumerate}
\end{definition}
Examples of primitive sets include the set ${\lcI,\lcJ}$,
${\lcB,\lcC,\lcW,\lcI}$, and ${\lcB,\lcT,\lcD,\lcI}$. One way of showing that
a set of formulas, say $s$, is primitive is to express all of the formulas of
another primitive set in terms of only the formulas in $s$.
\begin{definition}[Primitive Independence]
A primitive set of formulas is said to be independent if it ceases to be a
primitive set upon omission of any one of the formulas.
\end{definition}
Notice that any set containing both \lcI and \lcJ is a primitive recursive set
as long as the other formulas in the set meet the above requirements.
\subsection{An Application of the Theory of Combinations}
\begin{theorem}
If $\lcA_1$ and $\lcA_2$ contain no free variables then a formula \lcL can
be found such that $\lcL 1 \conv\lcA_1$ and $\lcL 2 \conv\lcA_2$.
\end{theorem}
This theorem can be generalized into the following through induction\ldots
\begin{theorem}
If $\lcA_1, \lcA_2, \ldots, \lcA_n$ contain no free variables, a formula
\lcL can be found such that $\lcL1\conv\lcA_1$, $\lcL2\conv\lcA_2$,\ldots,
$\lcL\lcN\conv\lcA_n$ (where \lcN is the formula representing the positive
integer $n$).
\end{theorem}
What follows is an example construction of such a formula for $\lcA_1$,\ldots,
$\lcA_5$, such that $\lcQ 1\conv\lcA_1$, $\lcQ 2\conv\lcA_2$,\ldots,
$\lcQ 5\conv\lcA_5$. Define $\lcQ$ as follows:
\begin{eqnarray}
\lcQ & \imc & \lambda i.\lcG_1 [3\dot{-}1](Pi) \\
\lcQ_2 & \imc & \lambda i.\lcG_2 [3\dot{-}1](Pi) \\
\lcQ_3 & \imc & \lambda i.\lcG_3 [3\dot{-}1](Pi)
\end{eqnarray}
Where
\begin{eqnarray}
\lcG_1 & \imc & \lambda n.n(\lambda x.x(\lambda y.y\lcI\lcB_2'))(\lambda z.z\lcI\lcI)\lcB_1' \lcJ \\
\lcG_2 & \imc & \lambda n.n(\lambda x.x(\lambda y.y\lcI\lcB_2''))(\lambda z.z\lcI\lcI)\lcB_1'' \lcJ \\
\lcG_3 & \imc & \lambda n.n(\lambda x.x(\lambda y.y\lcI\lcB_2'''))(\lambda z.z\lcI\lcI)\lcB_1''' \lcJ
\end{eqnarray}
and
\[\begin{array}{ccccc}
\lcB_1'\lcI\imc\lcI & \lcB_1'\lcJ\imc\lcQ_2 & \lcB_2'\lcI\imc\lcI & \lcB_2'\lcJ\imc\lcL_2' & \lcL_2' 1\imc\lcA_1 \\
\lcB_1''\lcI\imc\lcI & \lcB_1''\lcJ\imc\lcQ_3 & \lcB_2''\lcI\imc\lcI & \lcB_2''\lcJ\imc\lcL_2'' & \lcL_2'' 1\imc\lcA_2 \\
\lcB_1'''\lcI\imc\lcI & \lcB_1'''\lcJ\imc\lcL_1''' & \lcB_2'''\lcI\imc\lcI & \lcB_2'''\lcJ\imc\lcL_2''' & \lcL_2''' 1\imc\lcA_3 \\
& \lcL_1'''1\imc\lcA_4 & & \lcL_1'''2\imc\lcA_5 &
\end{array}\]
Now, notice the following:\\
\begin{math}
\lcQ1\imc(\lcG_1 2)1\imc(\lcB_2'\lcJ)1\imc\lcL_2' 1\imc\lcA_1 \\
\lcQ2\imc(\lcG_1 1)1\imc(\lcB_1'\lcJ)1\imc\lcQ_2 1\imc(\lcG_2 2)1\imc(\lcB_2''\lcJ)1\imc\lcL_2'' 1\imc\lcA_2 \\
\lcQ3\imc(\lcG_1 1)2\imc(\lcB_1'\lcJ)2\imc\lcQ_2 2\imc(\lcG_2 1)1\imc(\lcB_1''\lcJ)1\imc\lcQ_3 1\imc(\lcG_3 2)1\imc(\lcB_2'''\lcJ)1\imc\lcL_2''' 1\imc\lcA_3 \\
\lcQ4\imc(\lcG_1 1)3\imc(\lcB_1'\lcJ)3\imc\lcQ_2 3\imc(\lcG_2 1)2\imc(\lcB_1''\lcJ)2\imc\lcQ_3 2\imc(\lcG_3 1)1\imc(\lcB_1'''\lcJ)1\imc\lcL_1''' 1\imc\lcA_4 \\
\lcQ5\imc(\lcG_1 1)4\imc(\lcB_1'\lcJ)4\imc\lcQ_2 4\imc(\lcG_2 1)3\imc(\lcB_1''\lcJ)3\imc\lcQ_3 3\imc(\lcG_3 1)2\imc(\lcB_1'''\lcJ)2\imc\lcL_1''' 2\imc\lcA_5 \\
\end{math}
The notion developed above can be used to create an enumeration of formulas
in \lcalc, as follows\ldots
\begin{theorem}
If $\lcA_1, \lcA_2, \ldots, \lcA_n, \lcF_1, \lcF_2, \ldots, \lcF_m$ contain
no free variables, a formula $\lcE$ can be found which represents an
enumeration of the least set of formulas which contains $\lcA_1, \lcA_2,
\ldots, \lcA_n$ and is closed under each of the operations of the form
$\lcF_\alpha \lcX\lcY$, from the formulas \lcX and \lcY. This enumeration
occurs when every formula in the set is convertible into one of the
formulas in the infinite sequence $\lcE1, \lcE2, \ldots$ {\em and} every
formula in this infinite sequence is convertible into one of the formulas
of the set.
\end{theorem}
\subsection{A Combinatory Equivalent of Conversion}\label{SecCombEquiv}
Until now, any work that has been done with combinations first required us to
convert the combination into a formula of \lcalc, work with it, and then
convert it back into a combination. What we do now is develop a set of
operations that act on combinations and return combinations, thus allowing us
to work only with combinations. Many of these operations mimic similar
operations in \lcalc.
To start with, we define the following\ldots
\begin{definition}[$\gamma$, $\beta$, and $\omega$]
\begin{eqnarray}
\gamma & \imc & J\tau (J\tau)(J\tau) \\
\beta & \imc & \gamma (J\lcI \gamma)(J\lcI) \\
\omega & \imc & \gamma(\gamma(\beta\gamma(\gamma(\beta J\tau)\tau))\tau)
\end{eqnarray}
Notice the following: $\tau\conv\lcT$, $\gamma\conv\lcC$, $\beta\conv\lcB$
and $\omega\conv\lcW$ (where \lcT, \lcC, \lcB, and \lcW were defined
previously).
\end{definition}
Church then lists the 38 operations that may be performed on combinations,
numbered in Roman numerals (note that all of these Roman numerals are
preceded with a leading ``0''). When using these operations on combinations
it must always be cited what operation is being performed.
\begin{notation}[$\vdash$]
When dealing with operations on combinations, we make use of the
``$\vdash$'', and interpret it as follows. For two combinations, $\alpha$
and $\beta$, $\alpha\vdash\beta$ means that $\alpha$ is changed into
$\beta$ by the operation cited.
\end{notation}
The 38 operations (together) that Church lists can be proven equivalent to
$\lambda$-conversion. The difference? The combination operations are much
simpler than rules I, II, and III of \S 6, in the following ways:
\begin{enumerate}
\item The combination operations are one-valued. That is, given the
combination operated on and the particular operation begin performed,
the resulting combination is uniquely determined.
\item The combination operations do not do substitution at arbitrary
places. Rather, the combination operations perform substitution only at
specified places.
\end{enumerate}
\subsection{\Godel Numbers}
\begin{definition}[\Godel number of a combination]
The \Godel number of a combination is defined by induction as follows:
\begin{enumerate}
\item The \Godel number of $I$ is 1
\item The \Godel number of $J$ is 3
\item The \Godel number of the $n^{th}$ variable in alphabetical order is
$2n+5$
\item If $m$ and $n$ are the \Godel numbers of $\lcA$ and $\lcB$
respectively, then the \Godel number of $\lcA\lcB$ is\\
$(m+n)(m+n-1)-2n+2$ {\em NOTE: this is always an even integer!}
\end{enumerate}
\end{definition}
\begin{definition}[\Godel number of a formula]
The \Godel number of a formula is defined to be the \Godel number of the
combination belonging to the formula.
{\em Note: The \Godel number belonging to a combination is thus not
necessarily the same as the \Godel number of the combination itself.}
\end{definition}
The \Godel numbers of two combinations \lcA and \lcB are the same if and only
if \lcA and \lcB are the same. The \Godel numbers belonging to two formulas
\lcA and \lcB are the same if and only if $\lcA\conv\lcB$ using only
$\alpha$-conversion.
\begin{notation}
In the following discussion, subscripts of formulas will be used
extensively, and they are to be interpreted as follows.
Let
\begin{eqnarray}
\alpha_1 & \imc & \lcA\lcB\alpha \\
\alpha_2 & \imc & \lcC\lcD\alpha
\end{eqnarray}
where \lcA, \lcB, \lcC, and \lcD are arbitrary, and the form of $\alpha_1$
and $\alpha_2$ are arbitrary. All that is required is that an $\alpha$
appear in their expansion.\\
We may, then, iterate the use of subscripts, to obtains something such as
\begin{equation}
\alpha_{122}\imc\lcC\lcD(\lcC\lcD(\lcA\lcB\alpha))
\end{equation}
Note that the left-most subscript is the inner-most term, and the right-
most subscript is the outer-most term.
\end{notation}
In using \Godel numbers, we'll make use of a formula ``form'' defined such
that if \lcN represents the \Godel number belonging to formula \lcA, and \lcA
contains no free variables, then form $\lcN\conv\lcA$. To derive this
formula, note the following steps:
\begin{enumerate}
\item Notice that $par \lcN\conv 2$ (meaning \lcN is even) if \lcN
represents the \Godel number of combination having more than one term.
\item If \lcN represents the \Godel number of combination $\lcA\lcB$, then
$\lcZ(\lcH\lcN)$ is convertible into the formula representing the \Godel
number of \lcA, and $\lcZ'(\lcH\lcN)$ is convertible into the formula
representing the \Godel number of \lcB. To simplify, we introduce the
following:
\begin{eqnarray}
\lcN_1 & \imc & \lcZ(\lcH\lcN) \\
\lcN_2 & \imc & \lcZ'(\lcH\lcN)
\end{eqnarray}
\item Using the method described in \S14, we find a formula \lcfB such that:
\begin{eqnarray}
\lcfB 1 & \imc & \lambda x.x12 \\
\lcfB 2 & \imc & \lcI \\
\lcfB 3 & \imc & \lambda x.x12\lcJ
\end{eqnarray}
\item And, using the same method, we find a formula \lcfU such that:
\begin{eqnarray}
\lcfU 1 & \imc & \lcfB \\
\lcfU 2 & \imc & \lambda xy.y(par\ x_1)x_1 y(y(par\ x_2)x_2 y)
\end{eqnarray}
\item Finally, let ``form'' be defined as follows:
\begin{equation} form \imc \lambda n.\lcfU(par\ n)n\lcfU \end{equation}
\item Notice the following:
\begin{eqnarray}
form\ 1 & \imc & \lcI \\
form\ 3 & \imc & \lcJ
\end{eqnarray}
and if \lcN represents and even positive integer\ldots
\begin{equation}
form\ \lcN\imc form\ \lcN_1 (form\ \lcN_2)
\end{equation}
\end{enumerate}
With the formula ``form'' constructed above, then if \lcN represents the
\Godel number for a combination $\lcA'$ belonging to the formula \lcA, we have
\begin{equation} form\ \lcN \conv A' \conv A \end{equation}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Chapter 5
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The Calculi of $\lambda$-\lcK-Conversion and $\lambda$-$\delta$-Conversion}
\subsection{The Calculus of $\lambda$-\lcK-Conversion}
The calculus of $\lambda$-\lcK-conversion is obtained by slightly altering the
calculus of $\lambda$-conversion in the following manner. In \S5, replace the
definition of {\em well-formed formula} with the following:
\begin{definition}[well-formed formula ($\lambda$-\lcK-conversion)]
A well-formed formula is any formula where all variables occur either free
or bound, according to the following rules:
\begin{enumerate}
\item A variable $x$ is a well-formed formula and the occurrence of $x$
in this formula (itself) is free.
\item If \lcM and \lcN are well-formed, then $(\lcM\lcN)$ is also
well-formed. Any variables occurring free (or bound) in \lcM or
\lcN are considered free (or bound) in $(\lcM\lcN)$.
\item If \lcM is well-formed, then $(\lambda x\lcM)$ is also well-formed
and all occurrences of $x$ in $(\lambda x\lcM)$ are bound.
\end{enumerate}
\end{definition}
The {\em only} difference between this definition and the one presented in
\S2.2 is in rule III. The previous definition required $x$ to occur free at
least once in \lcM, and this definition makes no such requirement.
The rules of conversion in $\lambda$-\lcK-conversion are the same as they
appear in \S2.1, except that we must now take into consideration this new
definition of {\em well-formed formula}.
One of the key differences between the calculi of $\lambda$-conversion and
$\lambda$-\lcK-conversion is the possibility of defining the constancy
function (this is not possible in $\lambda$-conversion since $b$, although a
bounded variable, does not occur in the expression):
\begin{definition}[\lcK (the Constancy Function)]
\begin{equation} \lcK\imc\lambda a(\lambda ba) \end{equation}
\end{definition}
Another key advantage in the calculi of $\lambda$-\lcK-conversion is the
existence of the integer zero, defined as follows:
\begin{definition}[0 (Zero)]
\begin{equation} 0\imc\lambda a(\lambda bb) \end{equation}
\end{definition}
Many of the theorems in the calculi of $\lambda$-conversion still hold in
$\lambda$-\lcK-conversion, however a few fail. One key theorem that still
holds, however, is that which asserts the existence of the Kleene \lcfp
function.
Other key similarities are the definitions for the successor function, the
addition and multiplication functions, and the predecessor function. The
existence of the zero integer, however, can be used to greatly simplify the
predecessor function and the Kleene \lcfp function.
\begin{definition}[Predecessor Function]
The following is an example of how we can slightly simplify previously
defined functions by making use of $0$.
\begin{equation}
\lambda a.2_2 (a\lambda b\left[S(2_1 b),\;2_1 b\right])\left[0,\;0\right])
\end{equation}
\end{definition}
Also, the notion of $\lambda$-\lcK-definability is analogous to that of
$\lambda$-definability (as long as we restrict ourselves to the new definition
of well-formed formula).
One serious drawback to the calculi of $\lambda$-\lcK-conversion is that
theorem \ref{KeyTheorem} fails. Without theorem \ref{KeyTheorem}, it is
possible for a formula $\lcF\lcN$ to have a normal form but \lcN not. This
is, as Church states, clearly unreasonable.
\subsection{The Calculus of Restricted $\lambda$-\lcK-Conversion}
In order to avoid the difficulty described above, we can add to Rules II and
III in \S2.2 the additional requirement that \lcN shall be in normal form.
Note that being in normal form is {\em effective}, but having a normal form is
not. Basically, we require up-front that all of the formulas we work with be
in normal form. The resulting calculus is called the {\em calculus of
restricted $\lambda$-\lcK-conversion}.
The benefit of restricted $\lambda$-\lcK-conversion is that it more closely
follows the development of $\lambda$-conversion, allowing many more of the
theorems (specifically theorem \ref{KeyTheorem}) to remain true.
Many of the theorems developed for $\lambda$-conversion have nearly identical
analogues in restricted $\lambda$-\lcK-conversion. Usually, the only
difference is the additional premise that the formulas in question be in
normal form.
\subsection{Transfinite Ordinals}
Previously, the positive integers were defined as functions of functions by
applying one function to another a finite number of times. This method can be
extended to represent the ordinal numbers of the second number class by
allowing them to correspond in the same way to the transfinite powers of a
function, provided that we first fix upon a limiting process relative to which
the transfinite powers are taken.
For example, the ordinal $\omega$ could be represented as the function whose
value for a function $f$ (as an argument) is the function $g$ such that $gx$
is the limit of the sequence $x$, $fx$, $f(fx)$, $f(f(x))$, \ldots.
Accordingly, $\omega+1$ would be $\lambda x.f(\omega fx)$, and so on.
Instead of fixing upon the limiting sequence described above, however, we
could make the representation more general if we let the limiting process be
an additional argument $a$. Using this method, we can construct the following
formulas in the calculi of restricted $\lambda$-\lcK-conversion. The ``o''
subscript is used to distinguish these formulas from previous definitions.
\begin{eqnarray}
0_o & \imc & \lambda a(\lambda b(\lambda cc)) \\
1_o & \imc & \lambda abc.bc \\
2_o & \imc & \lambda abc.b(bc) \\
3_o & \imc & \lambda abc.b(b(bc)) \\
& \vdots & \nonumber\\
\lcS_o & \imc & \lambda dabc.b(dabc) \\
\lcL_o & \imc & \lambda rabc.a(\lambda d.rdabc) \\
\omega_o & \imc & \lambda abc.a(\lambda d.dabc)
\end{eqnarray}
We designate the following:
\begin{itemize}
\item $0_o$ represents the ordinal $0$.
\item If \lcN represents the ordinal $n$, the principal normal form of
$S_o \lcN$ represents the ordinal $n+1$.
\item If \lcR represents the strictly increasing infinite sequence of
ordinals $n_0$, $n_1$, $n_2$, \ldots, in that $\lcR 0_o$, $\lcR 1_o$,
$\lcR 2_o$, \ldots\ are convertible into formulas representing $n_0$,
$n_1$, $n_2$, \ldots, then the principle normal form of $\lcL_o \lcR$
represents the upper limit of this infinite sequence.
{\em NOTE: For a quick example, simply let $\lcR = \lcI$. Then \lcR
represents all natural numbers!}
\end{itemize}
It should be noted that the formula representing a given ordinal of the second
class of numbers is by no means unique. For example, $\omega$ may be
represented not only by $\omega_o$ but also by the principle normal form of
$\lcL_o \lcS_o$ (and many other formulas). Knowing this, formulas
representing ordinals are not to be taken as denoting ordinals but rather as
denoting things that are in many-one correspondences with ordinals.
\begin{definition}[$\lambda$-\lcK-defined]
A function $F$ of ordinal numbers is said to be $\lambda$-\lcK-defined by
a formula \lcF if both of the following requirements are met\ldots
\begin{enumerate}
\item Whenever $Fm=n$ and \lcM represents $m$, the formula
$\lcF\lcM\conv\lcN$ where \lcN represents $n$
\item Whenever an ordinal $m$ is not in the range of $F$ and \lcM
represents $m$, the formula $\lcF\lcM$ has no normal form.
\end{enumerate}
\end{definition}
\subsection{The Calculus of $\lambda$-$\delta$-Conversion}
Now, we develop the calculus of $\lambda$-$\delta$-conversion. This is done
by making the following modifications to the calculus of $\lambda$-conversion:
\begin{enumerate}
\item Add to the list of primitive symbols a symbol $\delta$, which is
neither an improper symbol nor a variable, but is classed with the
variables as a {\em proper symbol}.
\item Add to the rule 1 in the definition of {\em well-formed formula} that
the symbol $\delta$ is a well-formed formula.
\item Introduce the notion of $\delta$-normal form as follows:
\begin{definition}[$\delta$-normal form]
A formula is said to be $\delta$-normal form if it contains no part
of the form $(\lambda x\lcP)\lcQ$ and contains no part of the form
$\delta\lcR\lcS$ with \lcR and \lcS containing no free variables.
\end{definition}
{\em NOTE: Both of the conditions of being in $\delta$-normal form and
that \lcM is not $\alpha$-convertible into \lcN are effective.}
\item Add the following to the rules of conversion:
\begin{enumerate}
\setcounter{enumii}{3}\renewcommand{\labelenumii}{\Roman{enumii}}
\item To replace any part $\delta\lcM\lcN$ of a formula by $1$,
provided that \lcM and \lcN are in $\delta$-normal form and
contain no free variables and \lcM is not $\alpha$-convertible
into \lcN.
\item To replace any part $1$ of a formula by $\delta\lcM\lcN$,
provided that \lcM and \lcN are in $\delta$-normal form and
contain no free variables and \lcM is not $\alpha$-convertible
into \lcN.
\item To replace any part $\delta\lcM\lcM$ of of a formula by $2$,
provided that \lcM is in $\delta$-normal form and contains no
free variables.
\item To replace any part $2$ of a formula by $\delta\lcM\lcM$,
provided that \lcM is in $\delta$-normal form and contains no
free variables.
\renewcommand{\labelenumii}{\arabic{enumii}}
\end{enumerate}
\end{enumerate}
Now, some definition analogous to those for $\lambda$-conversion are made\ldots
\begin{definition}[$\lambda$-$\delta$-conversion]
A $\lambda$-$\delta$-conversion is any finite sequence of applications of
rules I-VII.
\end{definition}
\begin{definition}[$\lambda$-$\delta$-reduction]
A $\lambda$-$\delta$-conversion is called a $\lambda$-$\delta$-reduction
if it contains no application of rule III, V, VII and exactly one
application of the rules II, IV, or VI.
\end{definition}
\begin{definition}[Immediately Reducible]
\lcA is said to be immediately reducible to \lcB if there is a reduction
of \lcA into \lcB.
\end{definition}
\begin{definition}[Reducible]
\lcA is said to be reducible to \lcB if there is a conversion of \lcA into
\lcB which consists of one or more successive reductions.
\end{definition}
One advantage $\lambda$-$\delta$-conversion has over $\lambda$-\lcK-conversion
is that {\em all} of the theorems in the calculi of $\lambda$-conversion also
hold in the calculi of $\lambda$-$\delta$-conversion. This is because the
calculi of $\lambda$-conversion is actually a subset of the calculi of
$\lambda$-$\delta$-conversion.
\begin{definition}[$\lambda$-$\delta$-conversion]
Any finite sequence of Rules I-VII.
\end{definition}
\begin{definition}[$\delta$-normal form]
A formula will be called a $\delta$-normal form of another if it is in
$\delta$-normal form and can be obtained from the other by a finite sequence
of $\lambda$-$\delta$-conversions.
\end{definition}
The calculus of $\lambda$-$\delta$-conversion does have one drawback: it
requires an intensional interpretation of formulas. Take, for example, the
formula $\lambda ab.\delta ab1ab$. This formula corresponds to the same
function as $1$ in extension, however they are not interchangeable (since
$\delta 11\conv 2$ but $\delta 1(\lambda ab.\delta ab1ab)\conv 1$.
Just as we defined the Constancy Function \lcK in the calculus of
$\lambda$-\lcK-conversion, we not introduce a constancy function for
$\lambda$-$\delta$-conversion.
\begin{definition}[$k$ - the Constancy Function]
Define $\kappa$ to be as follows\ldots
\begin{equation}k\imc\lambda ab.\delta bb\lcI a\end{equation}
Then, $k\lcA\lcB\conv\lcA$ if \lcB has a $\delta$-normal form and contains
no free variables, and in that case only.
\end{definition}
The entire theory of $\lambda$-definability of functions of positive
integers carries over into the calculus of $\lambda$-$\delta$-conversion
since the calculus of $\lambda$-conversion is contained in that of
$\lambda$-$\delta$-conversion. All of the theorems of \S4 also hold in the
calculus of $\lambda$-$\delta$-conversion.
The theory of combinations carries over into the calculus of
$\lambda$-$\delta$-conversion as long as we redefine a combination to mean
any $[\lcI,\lcJ,\delta]$-combination. In defining the combination belonging
to a formula, we must also add the rule that the combination belonging to
$\delta$ is $\boldsymbol{\delta}$.
To develop a combinatory equivalent of $\lambda$-$\delta$-conversion, just as
we did in \S\ref{SecCombEquiv}, we must add the following four operations,
where \lcF, \lcA, \lcB, and \lcC are combinations, and \lcA and \lcB belong
to formulas in $\delta$-normal form containing no free variables, and are not
the same. \lcC is the formula which represents the \Godel number \lcA:
{\em Rules omitted. See page 66 of Church's text.}
Using \Godel numbers in $\lambda$-$\delta$-conversion carries over as well,
as long as we add the rule that the \Godel number of $\delta$ is 5.
Accordingly, we add the additional rule that
$\lcfB 5\conv \lambda x.x12\delta$, insuring that $form\ 5\conv\delta$.
It is now possible to define a formula $dncb$ which enumerates the \Godel
numbers of combinations which belong to formulas in $\delta$-normal form
and contain no free variables. {\em NOTE: the construction of $dncb$
follows that of $ncb$.}
In $\lambda$-$\delta$-conversion, it is also possible to define a formula
$met$ that acts as the inverse of the function $form$. That is, if \lcM is
a formula which contains no free variables and has a $\delta$-normal form,
then $met\;\lcM$ is convertible into the formula representing the \Godel
number belonging to the $\delta$-normal form of \lcM. We define $met$ as
follows:
\begin{definition}[$met$]
\begin{equation}
met\imc \lambda x.dncb(\lcfp(\lambda n.\delta(form(dncb\;n))x)1)
\end{equation}
\end{definition}
\subsection{A System of Symbolic Logic}
Now, Church uses the calculus of $\lambda$-$\delta$-conversion to construct
a system of symbolic logic. We retain our use of 2 and 1 to represent truth
and falsehood, respectively (knowing, of course, that these choices are
arbitrary).
This system has only one axiom, the formula $2$ (truth), and seven rules of
inference that correspond to rules I-VII in $\lambda$-$\delta$-conversion.
All provable formulas, or ``theorems'', in this system are the formulas which
can be derived from the formula $2$ by sequences of applications of the rules
of inference.
In this system, the familiar operations of negation, conjunction, and
disjunction may be defined as follows:
\begin{definition}[Negation, Conjunction, \& Disjunction]
Defined respectively, they are:
\begin{eqnarray}
\left[\lnot\lcA\right] & \imc & \pi(\lambda a.a\lcI(\delta 2\lcA))(\lambda a.a\lcI(\delta 1A)) \\
\left[\lcA\land\lcB\right] & \imc & 4\;\dot{-}\;([\lnot\lcA] + [\lnot\lcB]) \\
\left[\lcA\lor\lcB\right] & \imc & \lnot([\lnot\lcA]\land[\lnot\lcB])
\end{eqnarray}
\end{definition}
It follows from these definitions that $\lcA\lor\lcB$ cannot be a theorem
unless either \lcA or \lcB is a theorem, and this situation cannot be altered
by any suitable change in the definitions. Since this property is known to fail
for classical systems of logic such as that of {\em Principia Mathematica}, it
is clear that the present system therefore differs from the classical system
in a direction which may be regarded as finitistic in character.
The propositional function {\em to be a positive integer} is represented in the
system as a formula $N$, defined as follows:
\begin{definition}{$N$}
\begin{equation}N\imc\lambda x.v (met\;x)\end{equation}
\end{definition}
The general relation of equality or identity (in intension) is represented by
$\delta$. An existential quantifier $\Sigma$ is defined as follows:
\begin{definition}[$\iota$ and $\Sigma$]
\begin{equation}
\iota\imc\lambda f.form\left(Z'\left(H\left(dcnvt\;\alpha\left(\lcfp\left(\lambda n.\delta f
\left(form \left(Z\left(H\left(dcnvt\;\alpha n\right)\right)\right)\right)\right)1\right)\right)\right)\right)
\end{equation}
Where $\alpha$ represents the \Godel number belonging to the formula $2$.
Here, $\iota$ acts as a {\em general selection operator}. Given a formula
\lcF, if there is any formula \lcA such that $\lcF\lcA\conv 2$, then
$\iota\lcF$ is one such formula. If \lcF has no such formula, then
$\iota\lcF$ has no normal form.\\
{\em NOTE: The equivalence of two propositional functions \lcF and \lcG
does not necessarily imply the equivalence of $\iota\lcF$ and $\iota\lcG$.}
Now, $\Sigma$ is defined using $\iota\ldots$:
\begin{equation} \Sigma\imc\lambda f.(\iota f) \end{equation}
\end{definition}
Thus, $\Sigma\lcF\conv 2$ if there is a formula \lcA such that
$\lcF\lcA\conv 2$, otherwise $\Sigma\lcF$ has no normal form.
{\em NOTE: the $\iota$ operator can be compared with Hilbert's $\epsilon$
operator and Hilbert and Bernays $\eta$-operator.}
Church notes that interpretation of $\iota$ and $\Sigma$ depends on
identifying formal provability in this system, which can be justified by the
{\em Completeness Property} of $\lambda$-$\delta$-conversion:
\begin{theorem}[Completeness Property]
A formula which is not provable, unless it is convertible into a principal
normal form other than 2 (and hence disprovable), must have no normal form,
and hence be meaningless.
\end{theorem}
For the sake of convenience, we can adopt the following notation\ldots
\begin{notation}
We may abbreviate {\em general selection} and {\em existential
quantification}, respectively, as:
\begin{eqnarray}
\left[\iota x\lcM\right] & \imc & \iota(\lambda x\lcM) \\
\left[\exists x\lcM\right] & \imc & \Sigma(\lambda x\lcM)
\end{eqnarray}
\end{notation}
We might be tempted to introduce a {\em Universal Quantifier} (or simply
an Existential Quantifier with Negation), but as Church notes, there are
difficulties that arise. \Godel showed that any universal quantifier
introduced by definition will have a certain character of incompleteness.
The {\em consistency} of this system of symbolic logic is actually a
corollary of theorem \ref{Theorem30}.
One advantage of using this system of symbolic logic over set theory, is that
certain paradoxes of set theory fail in this system. For some paradoxes,
their failure to transfer into this system of symbolic logic is simply because
the formula leading to the paradox has no normal form. For example, with
Russell's paradox, the formula
\begin{equation} (\lambda x.\lnot(xx))(\lambda x.\lnot(xx))\end{equation}
has no normal form. In other, more complicated paradoxes, their failure to
transfer over may depend on the incompleteness property of quantifiers,
mentioned above.
\end{document}