## 1. Computability and Church's Thesis


### 1.1 Church's Seminal Paper



Church was the first to devise a formalism--the
l-calculus--within which it was possible to define a class
of functions that coincide, arguably, with the intuitively computable
functions--those that can be evaluated by means of an algorithm,
i.e., a computer program. He also provided, again arguably, the first
example of a particular significant function that is *not*
computable. (Other examples, due independently to Kleene (1936) and
Turing (1936) followed quickly.) He did this by constructing a
function that is provably not recursive in the sense defined slightly
earlier by Godel and Herbrand. He then appealed to the assumption
that *any intuitively computable function is recursive* to
conclude that the function in question is not computable--in
Church's terminology it is not *effectively calculable*.
(We will continue to use the terms "computable" and
"intuitively computable" rather than "effectively
calculable" since they are more readily understood by
non-specialists.) Given the nature of this function, this meant that a
certain problem of elementary number theory is unsolvable: there is no
way it could be solved by algorithmic means. It also implied a
negative solution to the *Entscheidungsproblem* first
enunciated by Hilbert and Ackerman (1928): the problem whether there
is a decision procedure for first order logic. The italicized
assumption later came to be known as "Church's
thesis" (Kleene 1952).



The paper in which this result is presented, entitled "An
Unsolvable Problem of Elementary Number Theory" (1936a), is a
great classic of logic and computability theory, but it has been
somewhat overshadowed by the almost contemporaneous and brilliant
paper by Turing (1936), as well as the earlier remarkable
incompleteness theorems of Godel (1931). In this section,
Church's paper takes center stage.



Section 7 of Church's paper contains the first explicit
formulation of Church's thesis (apart from a preliminary
statement in 1935c):



> 
> 
> We now define the notion, already discussed, of an effectively
> calculable function of positive integers by identifying it with the
> notion of a recursive function of positive integers (or of a
> lambda-definable function of positive integers). This definition is
> thought to be justified by the considerations which follow, so far as
> positive justification can ever be obtained for the selection of a
> formal definition to correspond to an intuitive notion. (1936a [BE:
> 119])
> 
> 
> 



Church goes on to consider two natural ways one might seek to expand
the notion of computability beyond that of recursiveness (or
l-definability) and he argued that each of these methods
results in functions that are already recursive (and
l-definable) and so concludes:



> 
> 
> Thus it is shown that no more general definition of effective
> calculability than that proposed above can be obtained by either of
> two methods which naturally suggest themselves (1) by defining a
> function to be effectively calculable if there exists an algorithm for
> the calculation of its values (2) by defining a function \(F\) (of one
> positive integer) to be effectively calculable if, for every positive
> integer \(m\), there exists a positive integer \(n\) such that \(F(m)
> = n\) is a provable theorem. (1936a [BE: 121])
> 
> 
> 



Kleene (1952: 222-223) discusses these two classic arguments for
Church's thesis. (See
 supplement A.2
 for further details.)


### 1.2 What is Church's Thesis?



Church's thesis is the first of the following two propositions,
but the second plays an important role in discussions of the first. We
use the term "CT" for the conjunction of the two:



CT1
Every intuitively computable function is recursive
CT2
Every recursive function is intuitively computable.


CT might be formulated in terms of l-definability or Turing
computability or a number of other distinct mathematical conditions
known to be extensionally equivalent to recursiveness. Despite these
equivalences, the differences are significant. On several occasions,
Godel expressed a strong preference for Turing's analysis
and there are good reasons for Godel's preference. These
are amply detailed elsewhere (see the entry on the
 Church-Turing thesis
 as well as Davis 1965). Church himself thought that Turing's
analysis was superior to his:



> 
> 
> computability by a Turing machine ... has the advantage of making
> the identification with effectiveness in the ordinary (not explicitly
> defined) sense evident immediately. (Church 1937a [BE: 934])
> 
> 
> 



The identification of l-definability with intuitive
computability was certainly not "evident immediately". In
fact, Church's student, Stephen Cole Kleene, reports that it
only gradually dawned on Church, Rosser (J. Barkley Rosser, also
Church's student), and himself that l-definability may
serve as a precise counterpart of intuitive computability (Kleene
1981). Kleene also describes the difficulty of giving
l-definitions of certain basic number theoretic
functions--particularly the predecessor function--given the
particular way Church gives l-expressions standing for integers
(1981: 56; these l-expressions are described in
 supplement D).
 But the fundamental difficulty with
 CT1
 as Church (1936a) enunciates it is that it is given as a definition
without any accompanying justification other than a brief sketch of a
proof of the extensional equivalence of l-definability and
recursiveness (Kleene [1936] gives a more detailed proof). Godel
complained of exactly this:



> 
> 
> He [Godel] insisted ... that it was "thoroughly
> unsatisfactory" to define the effectively calculable functions
> to be some particular class without first showing that "the
> generally accepted properties" of the notion of effective
> calculability necessarily lead to this class. (Davis 1982:12)
> 
> 
> 



Godel eventually held up Turing's analysis as a better
model of computation precisely because Turing justifies the
identification of intuitive computation with Turing machine
computation on the basis of a detailed analysis of what a human
computer, equipped with paper and pencil, must actually do (Turing
1936: SS9). It seems that a counterpart of Turing's
compelling analysis has yet to be given for the case of
l-computation. It should be emphasized, however, that
Church's main aim was not to defend an analysis of computability
but rather to set the stage for a proof that a particular number
theoretic combinatorial problem is not solvable. So long as
computation is defined as a finite process, cardinality considerations
imply that non-computable functions must exist, and Church wished to
demonstrate that his combinatorial problem was one of these.



For most of its life, Church's view--that
 CT1
 is not subject to mathematical proof, or any sort of mathematical
treatment at all--has prevailed. But some such as Shoenfield,
(and Church himself), have observed that
 CT2
 is subject to intuitive proof *despite* the lack of a
mathematically precise definition of "computable"
(Shoenfield 1967: 120). Shoenfield's view of CT2 has been
seconded by Kripke. All that is needed, Kripke says, is "just a
direct argument" (2013). Moreover, Kripke and others (e.g.,
Mendelson 1990) have challenged the received view that CT1 is not
amenable to mathematical treatment. Accordingly, the discussion of CT1
divides into two parts: The first part is the evidence usually adduced
for CT1 on the assumption that it is a definition or hypothesis not
amenable to proof; and the second part is the evidence derived from
recent attempts to support CT1 by mathematical arguments. The first
sort of evidence we may term "external" and the second
"internal". The emphasis in what follows is on
Church's role in these developments.


### 1.3 The Role of CT1



In Church's terms, the decision problem for a logistic system is
the problem of finding



> 
> 
> an effective procedure, a *decision procedure*, by which, for
> an arbitrary wff of the system, it is possible to determine whether or
> not it is a theorem (and if it is a theorem, to obtain a proof of it).
> (1956a: 273)
> 
> 
> 



In a footnote, Church remarked that from a classical point of view,
the parenthetical condition is not required, but is in "the
direction of" intuitionism, which he described as
"radical", but the proviso nonetheless was, in subsequent
parts of his 1956a, always included. But such a determination must be
made on the basis of a precise counterpart of the concept of an
effective procedure, such as a recursive or l-definable
procedure. In case there is a positive result,
 CT2
 allows one to infer that a computable (effective) procedure exists;
and if the result is negative,
 CT1
 allows the inference to its non-existence. This has been the role of
CT in computability theory and the development of logic. A
particularly telling example is Church's negative solution to
the *Entscheidungsproblem*--the decision problem for first
order logic, now known as "Church's theorem"
(1936b). It was felt that a positive solution would render mathematics
completely mechanical at least in principle. Every mathematical
problem could in principle be solved by an algorithm. On the other
hand, the shape of a negative solution was a mystery. It is reported
that von Neumann declared that "We have no clue how to prove
it" (Gandy 1988: 62). Church's result rendered a negative
solution conceivable and gave some hope that the solution to
mathematical problems would continue to require human ingenuity. In
any case, appeals to CT1 have sometimes been viewed as part of the
*proofs* giving the solutions to decision problems and
sometimes not, depending on the required degree of formalization. To
prove, for example, that some axiomatic theory is undecidable is to
prove that its set of theorems is not recursive (or not Turing
computable, etc.) and the appeal to CT1 often comes after the strictly
mathematical work. However, it has not been common to suggest that one
or other of the precise counterparts of intuitive computability should
actually *replace* it; and although Godel comes close to
such a view (in the case of Turing computability), this is not the
standard view. Other reductions of intuitive notions to mathematical
terms have often been viewed as replacements (cf. Mendelson 1990); but
there has been resistance to this view in the case of Church's
thesis, for otherwise logicians should long ago have ceased to speak
of intuitive computability (effective calculability).



However, significant developments in computability theory often take
the form of informal mathematics, as with the rest of mathematics. An
informal method of computation is given, where it is clear that it
could be replaced by a formal one although such a demonstration might
be thought to be unnecessary or cumbersome. To give a simple example:
Proofs of Craig's theorem that any recursively enumerable set of
formulas is recursively axiomatizable often take the form of an
informal argument that the set of Craig-axioms is decidable; and then
 CT1
 is applied to conclude that it is recursive (cf. Craig 1953). Rogers
(1967) gives many examples of the role of informal mathematics in
conjunction with CT1 in computability theory. In fact, Rogers'
classic text uses informal mathematics together with Church's
thesis in its positive (non-contrapositive) form to develop recursive
function theory as a whole. By contrast, Davis (1958) gives a fully
formal account and so uses CT1 mainly in its contrapositive form, or,
equivalently, in its positive form but resting on a *reductio*
assumption. A third role of CT1 has been to motivate the proofs that
certain basic sets and relations are recursive. For example,
membership in the set of formulas of a standard formalized language is
intuitively computable. Hence by CT1 it must be recursive, but a proof
that it is recursive can be surprisingly complex (see Boolos et al.
2007: Ch. 15).


### 1.4 The External Evidence



The classic account of the external evidence for
 CT1
 is by Kleene (1952: 318-323). Kleene organizes the evidence
under four headings:



(A)
Heuristic evidence,
(B)
Equivalence of diverse formulations,
(C)
Turing's concept of a Turing machine, and
(D)
Symbolic logics and symbolic algorithms.


(A) is the fact that large families of functions had been shown to be
l-definable and hence recursive. (B) is the striking fact that
the various mathematically precise counterparts of
computability--l-definability, recursiveness, Turing
computability and others of the period due to Godel and
Post--despite being technically quite different from one
another--turn out to lead to the same class of functions. (Not
everyone is impressed by this "confluence" of definitions;
cf. Kreisel 1987.) As for (C), Kleene observes that Turing's
analysis constitutes a direct attempt to give a mathematical account
of the actions of a human computor and thus differs from the other
analyses (in terms of recursiveness and l-definability), which
"arose differently". He remarks that Turing's
identification of intuitive computability with computability by a
(Turing) machine constitutes an "independent statement of
Church's thesis". For this reason
 CT1
 has come to be known as the Church-Turing Thesis. Both Church (1937b)
and Kleene (1952) also note that Post (1936) independently gives an
analysis very similar to Turing's. Perhaps, then, CT1 should
properly be known as the Church-Turing-Post-Thesis.



Kleene's (D) consists of the two arguments mentioned earlier by
Church (1936a: section 7). The first argument is that the notion of
computation by means of an algorithm does not lead outside the class
of recursive functions (cf. Shoenfield [1967: 120] for an argument of
the same sort). The second of these concerns the relation between
recursive functions and formal systems of "symbolic
logic". Church argues that in any such system whose set of
theorems is recursively enumerable, if \(f\) is a unary
("singulary" is Church's term) function of positive
integers and if it is true that

 
\[\tag{\*} f(m) = n,\]


for integers \(m\) and \(n\), then (in essence) \((\*)\) is provable in
the system; and if \((\*)\) is false, then it is not provable in the
system, then \(f\) is recursive. See
 supplement A.2
 for a more detailed discussion of this controversial
argument--controversial because Church simply *assumes*
that the set of axioms and rules of a symbolic logic must be
recursive, and this has seemed to some to beg the question of the
truth of
 CT1
 and thus to constitute a "stumbling block" to the
acceptance of Church's argument (Sieg 1997).


### 1.5 The Internal Evidence



Mendelson challenged the view that
 CT1
 is not subject to mathematical treatment by citing cases in which an
intuitive concept has literally been *replaced* by a
corresponding mathematically precise one. It is not a mere
*thesis* that the limit concept, for example, is given by the
familiar epsilon-delta definition. The definition replaces the
intuitive concept (Mendelson 1990). Others have gone further, arguing
that computability may be taken as a primitive concept subject to an
axiomatic treatment, as Godel had once suggested (according to
Church's letter to Kleene, 1935d [BE: 1000]). Sieg proposes an
axiomatization based on Turing's analysis of a person who
computes ("a computor"). In section 9 of his (1936),
Turing argues (argument I) that the Turing machine is a good model of
a computor, who, as such, is subject to certain constraints such as
that


1. the behavior of the computor is completely determined by the
symbols observed and the computor's state of mind;
2. that there is a finite bound on the number of symbols observed at
any one time;
3. that only a finite number of states of mind are involved at any
one time (a condition that Godel [1972] disputed); and
4. that each newly observed symbol is within finitely many steps of
earlier ones.



Sieg, building on work of Gandy, formulates axioms corresponding to
such conditions and claims that these constitute an axiomatization of
computability (Gandy 1988; Sieg 1997).



In a recent paper (2013), Kripke argues that
 CT
 may be regarded as a "special corollary" of the
completeness theorem for first order logic. Kripke's argument is
reminiscent of one given earlier by Kreisel (1987) concerning, not CT,
but rather the relation between informal validity, on the one hand,
and formal validity and provability on the other. It is useful to
consider Kreisel's argument first and Kripke's afterwards
(some details of the following are not Kreisel's):



Let \(TA\), \(VA\), and \(DA\) mean respectively that \(A\) is a first
order translation of an informal argument that is intuitively valid
"in virtue of form alone", that \(A\) is valid according
to the standard model theoretic definition of validity for first order
logic, and that \(A\) is derivable in a first order formal system of
deduction, \(D\), that is sound and complete in the usual sense. Then
informally, we have that \(DA\) implies \(TA\). If an argument is
formally derivable, we regard it as valid in virtue of its form alone.
At least that is often taught to students. And also \(TA\) implies
\(VA\)--something also taught to students. By completeness,
\(VA\) implies \(DA\). And so it follows that \(TA\)--an informal
notion--is equivalent to \(DA\), a formal notion, for the case of
first order logic. (It might be assumed in addition that any
intuitively valid argument is formalizable in a first order language,
but Kreisel does not assume this.)



Now, Kripke summarizes his argument as follows:



> 
> 
> Suppose one has any valid argument whose steps can be stated in a
> first-order language. It is an immediate consequence of the Godel
> completeness theorem for first-order logic with identity that the
> premises of the argument can be formalized in any conventional formal
> system of first-order logic. Granted that the proof relation of such a
> system is recursive (computable), it immediately follows in the
> special case where one is computing a function (say, in the language
> of arithmetic) that the function must be recursive (Turing
> computable). (2013: 81)
> 
> 
> 



Kripke assumes "Hilbert's thesis":



> 
> 
> namely that the steps of any mathematical argument can be given in a
> language based on first order logic (with identity)
> 
> 
> 



and he assumes that the proof relation is recursive and hence that the
provability relation is semirecursive. Thus, the argument runs as
follows: (1) Let \(A\) be a valid mathematical argument that is a
calculation, "where one is computing a function (say, in the
language of arithmetic)". Then, (2) by Hilbert's thesis,
the steps of \(A\) can be stated in a first order language (and so the
premises and conclusion of \(A\) can be stated in such a language).
But then (3) by the completeness theorem, there is a formal derivation
of the conclusion of \(A\)--the final result of the
calculation--from its premises, and so (4) "it immediately
follows" that the function representing the calculation is
recursive. This is a proof of Church's thesis, assuming
Hilbert's, and, as Kripke mentions, it might therefore be viewed
alternatively as a reduction of Church's thesis to
Hilbert's.



The similarity to Kreisel's argument is clear: Define \(C(A)\)
to mean that \(A\) is a is correct mathematical calculation; then by
Hilbert's thesis, \(C(A)\) implies \(V(A)\) and by completeness
\(C(A)\) implies \(D(A)\). Moreover, apart from the appeal to the
completeness theorem, Kripke's argument is essentially the same
as the Church-Kleene argument mentioned earlier and discussed in
 supplement A.1:



> 
> 
> It is because of these considerations that I take myself to be
> reviving somewhat neglected arguments already given by Church, and
> especially Turing. (Kripke 2013: 81)
> 
> 
> 



One important consequence of Kripke's argument, in particular,
is that as he observes, there is--and has been from the
beginning--a characterization of computable functions in terms of
first order provability that is fully equivalent to the others (2013:
82).


## 2. Philosophy of Logic



In this section we describe how Church's wove certain
philosophical doctrines about logic into the fabric of formal,
mathematical logic as he presented it in (Church 1956a, 1959, 1962b,
1956-72). Church's early philosophy of logic is described
in
 supplement B.


### 2.1 Philosophy of Logic and the Logistic Method



In Church's philosophy of logic, the phenomenon of deductive
reasoning is assumed to be "already known, from experience with
particular instances of it" and the stated goal of logic is to
provide a theory of such reasoning



> 
> 
> plus whatever is required in object language or metalanguage for the
> adequacy, generality, and simplicity of the theory. (1962b [BE:
> 608])
> 
> 
> 



This attitude required Church to accept not only first order logic but
also the logic of second and higher orders, so that he could study
logic in all its generality. It was not enough to accept, for example,
"\((x) F(x) \supset F(y)\)", because there are infinitely
many sentences of this form requiring one to also accept
"\((F)(y) \hdot (x) F(x) \supset F(y)\)" "by
generalization from infinitely many analytic sentences of the
appropriate form" (1962b [BE: 608]). (Note Church's
notational convention that a dot placed before a connective or (as
above) a quantifier brackets a proposition.)



Another consideration Church offered in favor of second order logic
was the more pragmatic one that a greater understanding of
mathematical theories could be obtained by comparing their
formulations in first and second order languages (1956a: chapter V).
(Discussion of this topic is beyond the scope of this entry; but see
Myhill (1953), Shapiro (1991, 2001), Button and Walsh (2018) and the
citations therein. See also the entries on
 model theory,
 second and higher order logic, and
 Skolem's Paradox.)



Church's philosophy of logic was shaped not only on the one hand
by a belief in the generality of logic but also on the other by the
need to avoid the paradoxes to be discussed in
 section 4.
 In order to avoid the paradoxes to which Frege's position lead,
Church was forced to work primarily within a type-theoretic
framework--the logic of second, third and higher orders up to and
including *w*--with different kinds of variables, with
different restricted domains of individuals, classes, relations, etc.
(Church's type theory is described in
 supplement D.)
 Moreover, as we will now see, Church departed even further from Frege
and Russell by presenting these ideas in terms of conventional model
theory.



The purpose of formal logic, in Church's view, was first and
foremost to study the *form* of correct deductive reasoning in
abstraction from its subject matter (1956a: SS00). For Church,
deductive reasoning operates on propositions, and so the study of such
reasoning is the study of the logical form of propositions--which
Church distinguished from their "content" or
"matter" (ibid)--via the study of the logical forms
of sentences that express them (ibid; cf. 1959 [BE: 475]). This way of
studying logical form invoked what Church called the "logistic
method" (1956a). This required him to distinguish between
informal languages and formalized languages, because



> 
> 
> the natural languages, including English, have been evolved over a
> long period of history to serve practical purposes of facility of
> communication, and these are not always compatible with soundness and
> precision of logical analysis... To adopt a particular language
> thus involves adopting a particular theory or system of logical
> analysis. (1956a: SS00)
> 
> 
> 



In order to adopt a formal language, one first devises what Church
calls "a particular theory or system" (1956a [BE: 373]),
which is a syntactic theory. This specifies the *primitive
symbols* and *formation rules* for building *the
well-formed expressions (the wffs)* of the theory, as well as what
are the *axioms* and *inference rules.* The
*theorems* are the wffs that occur at the end of
*proofs*, which are themselves specified as finite sequences of
wffs that are either axioms or inferable from prior wffs in the
sequence according to the inference rules. In order for this theory to
serve as a *language*, it must be provided with semantic rules
that assign *designata* (or denotations) to the names of the
theory, as well as *values* to expressions containing free
occurrences of variables.



The logical forms of sentences are the ways that sentences are built
up from the logical particles. From this perspective, to say that a
wff B is a *logical consequence* of a set of wffs \(\Sigma\) is
to say that the logical forms of B and the wffs in \(\Sigma\) are so
related that if the wffs in \(\Sigma\) are true, so is B. Moreover,
since logical form is sufficient to ensure this, for any argument of
*the same logical form*, if the premises are true, so is the
conclusion. This leads to the now familiar idea that



> 
> 
> the proof of a theorem (of the object language) shall make no
> reference to or use of any interpretation, but shall proceed purely by
> the rules of the logistic system. (1956a: SS07)
> 
> 
> 



Church gave three reasons for this requirement. First, it adheres to
extant standards of mathematical rigor. Secondly, reasoning purely by
the rules of the logistic system is safer than reasoning about any
interpretation one may wish to adopt, because--as is discussed in
2.2--the object language is set up using an informal
meta-language that is "so elementary and restricted that its
essential reliability can hardly be doubted if mathematics is to be
possible at all" (1956a [BE: 415]). Finally, it allows one to
draw a precise distinction between form and content:



Returning to B and \(\Sigma\), if the former is a logical consequence
of the latter, then, if we do *not* reinterpret the logical
particles but *do* reinterpret the nonlogical vocabulary by
associating it with different rules, then it will still be the case
that if all the wffs in \(\Sigma\) are true, so is B. In this way, we
can isolate the form of a proposition by studying the corresponding
sentence and reinterpreting its non-logical vocabulary.



This, of course, is the now conventional model-theoretic treatment of
logical consequence originally due to Tarski (1937 [1941]) and
extended to the logic of higher orders by Church's student Leon
Henkin (1950), which is presented in Church (1956a). (For more on
Henkin's contribution, see the entries on
 second and higher order logic
 and on
 Church's type theory.)
 It should be noted that Church, in addition to working in classical
model theory with restricted universes that can be accommodated in ZF
set theory, was also willing to allow the existence of a universal set
(1974c). Further, he not only distinguished between sharply between
model theoretic interpretations and intended interpretations (1956a),
but also argued that giving a particular model theoretic
interpretation of a formal language was not sufficient for describing
its logic. In particular, he argued that giving a formal language
containing empty names (like 'Pegasus') an interpretation
with inner and outer domains that invalidates Existential
Generalization (as well as, presumably, Universal Instantiation) was
not sufficient for describing the logic of that language (1965).


### 2.2 Adopting a Formalized Language



Central to the logistic method is the process of adopting a formalized
language. This process takes place in an informal meta-language (such
as a fragment of English) that



> 
> 
> deals with matters of everyday human experience, going beyond such
> matters only in that no finite upper limit is imposed on the number of
> objects that may be involved in any particular case, or on the time
> that may be required for their manipulation according to instructions.
> (1956a: SS07)
> 
> 
> 



Included in Church's description of the process of adopting a
formalized language is that one first specifies the primitive symbols
and formation rules, which together with the axioms and inference
rules constitute *the primitive basis* of the logistic system
(which will become a language once semantical rules are added). The
description of this process assumes that the person who undergoes it
has a stock of information about language and the world, the ability
to understand definitions (such as the definition of "primitive
symbol") as well as the ability to understand and follow
instructions. Church also provided a rational reconstruction of how we
learn our first language and suggested that this method could, in
principle, be used to learn a formalized language rather than a
natural language as a first language:



> 
> 
> Some part of the language must first be learned approximately by the
> method of example and imitation; then this imprecisely known part of
> the language is applied in order to state rules of the language (and
> perhaps to correct initial misconceptions); then the known part of the
> language may be extended by further learning by example and imitation,
> and so on in alternate steps, until some precision in knowledge of the
> language is reached. There is no reason in principle why a first
> language, learned in this way, should not be one of the formalized
> languages of this book, instead of one of the natural languages.
> (1956a: SS07)
> 
> 
> 



This assumes that the person who undergoes this process can not only
state rules but also apply them, so it assumes that such a person can
reason as well as imitate behavior. In this way, it resembles,
somewhat, Church's earlier philosophy of logic in which he
distinguished between *intuitive* logic and *formal*
logic and maintained that intuitive logic cannot be learned and is a
precondition of reasoning in formal logic. (Church's early
philosophy of logic is described in
 supplement B.)
 One reason for the absence of the locution "intuitive
logic" from Church's mature philosophy might be that he
wanted to avoid the impression that there is some essential difference
between what should take place in an informal meta-language and what
should take place in a formalized object language. In fact, he was
adamant that basic deductive reasoning should not *have to*
take place in an informal meta-language. Rather, once the object
language has been set up it



> 
> 
> shall be an independent language capable, without continued support
> and supplementation from the meta-language, of expressing those things
> for which it was designed. (1956a: fn. 121)
> 
> 
> 



The idea is that a person who can already reason as well as use an
informal meta-language to set up the object language can come to
reason with greater rigor and to a greater extent in the object
language. At which point, having pulled herself up by her bootstraps,
she should no longer have any need for an informal meta-language. (Of
course, a meta-language is still needed to prove certain meta-theorems
about the object language such as its consistency.)


### 2.3 Logic and Communication



When one is setting up a logistic system, the well-formed expressions,
axioms and rules of inference must all be specified
*effectively* in order that there can be an effective test of
whether a purported proof is really a proof. Intuitively, the
requirement is that one can test--by looking at the symbols and
following a fixed set of instructions for performing concrete
operations with symbols--whether a given finite sequence of
symbols is a wff, or whether a given finite sequence of wffs is a
proof of the last wff in the sequence. In the absence of such a
method.



> 
> 
> a proof would not necessarily carry conviction, the proposer of a
> proof could fairly be asked to give a proof that it was a
> proof--in short the formal analysis of what constitutes a proof
> (in the sense of a cogent demonstration) would be incomplete (1959
> [BE: 477-8]).
> 
> 
> 



The philosophy underlying Church's position is that mathematical
proof and logical analysis--as well as other attempts at precise
reasoning--should be *public* and *communicable*.
Just as one should be able to convince an interlocutor that a
mathematical proof is really a proof, so one should be able to
convince her that an argument more generally is cogent, which will
also require convincing her that meaningful assertions have been made.
Further, these questions should be addressed *by the object
language in which one is speaking* (although one will often have
to look beyond the language to convince an interlocutor that
one's assertions are true):



> 
> 
> But without the requirements of effectiveness, it might happen that
> someone confronted with a proof of a theorem (and admitting the axioms
> and rules of inference) might nevertheless continue to doubt the
> theorem, because of doubt that the alleged proof actually is a
> proof.... the proposer of the proof might be fairly asked to give
> supplementary proof that it is a proof--and for the purposes of
> deductive logic, this supplementary proof ought then to be treated as
> part of the whole proof, and included with it when the process of
> proof is formalized by the logistic method. (1956-71 [BE:
> 703])
> 
> 
> 



For example, while there may be advantages to using the deduction
theorem as a primitive rule of inference, there is also reason to
avoid doing so, i.e., to obviate the need for supplementary proof
(1956a: SS29 and fn. 181).



For Church, it is constitutive of a language that it provides the
foregoing connection between reasoning and communication:



> 
> 
> For, however indefinite or imprecisely fixed the common idea of a
> language may be, it is at least fundamental to it that a language
> shall serve the purpose of communication. And to the extent that
> requirements of effectiveness fail, the purpose of communication is
> defeated. (1956a: SS07)
> 
> 
> 
> To say that an assertion has been made if there is a meaning evades
> the issue unless an effective criterion is provided for the presence
> of meaning. An understanding of the language, however reached, must
> include effective ability to recognize meaningfulness (in some
> appropriate sense), and in the purely formal aspect of the language,
> the logistic system, this appears as an effective criterion of
> well-formedness. (1956a: fn. 120)
> 
> 
> 



In short, an assertion can be recognized as meaningful only if there
is an effective method for determining whether it is meaningful;
Church's logistic method provides such a method by way of
well-formedness. Further, since communication and conviction are at
issue (as well as mere judgments of meaningfulness), one must also be
able to tell *which* propositions have been asserted and, in
particular, which ones have been proved.



However, some critics have questioned the cogency of Church's
philosophical arguments for his requirement of effectiveness (Anderson
1998). Moreover, it should be noted that logical consequence is not in
general an effective notion. By Church's Theorem (1936a), there
is no effective test for deciding the validity or provability of the
wffs of first order logic or of logics of any higher order (as Church
himself notes; 1956-71 [BE: 703]). Further, as Church was
acutely aware, there is a price to be paid for communicating and
verifying proofs in a formalized language that meets the requirement
of effectiveness. If the formalized language is sufficiently
expressive, it will be subject to Godel's incompleteness
theorems (see
 SS5.4).



It should also be noted that the question what exactly is an effective
procedure spurred Church's work on effective calculability and
the decision problem (see
 section 1).
 It is also motivated some of his other technical work such as his
work on constructive ordinals (1938).



In addition to the requirement of effectiveness, Church also demands
that proofs should be constructive. However, in later years his
attitude became more ecumenical. See (1936b: fn. 10 added 1971 [BE:
128]).


## 3. Applications of the Logistic Method



Church used the logistic method to apply the general outlook and
specific distinctions of formal logic to problems in philosophy. In
this section we describe five such applications.


### 3.1 Against Logical Empiricism



Church was never a member of the Vienna Circle and neither were Kleene
nor Rosser (an ocean separated them from Vienna); nor did they show
particular sympathy for the Circle and its aims. Church was, however,
appreciative of the work of Carnap in particular (cf. Church's
[1939a] review of Carnap's *Foundations of Logic and
Mathematics* [1939]). But commenting on Carnap's
Circle-inspired view that the sole task of philosophy is semantical
analysis, Church remarked that this "represents an extreme
view" (1943a). Church adds that, nonetheless, the importance of
semantical investigations to philosophy should not be
underestimated.



Thus, Church was among those logicians and philosophers who did
*not* subscribe to the Circle's approach to the question
of meaning. This, of course, is not to deny that the Circle was a
powerful force in the development of analytic philosophy (see the
entry on
 logical empiricism).
 But Church and many of his students did not participate in the
Circle.



The logical empiricists tried to explicate the notion of empirical
verification in terms of logical entailment. We begin with their
second attempt, an explication known as "weak
verifiability", which (like its predecessor, "strong
verifiability") was framed in terms of logical entailment or
logical deducibility:



> 
> 
> *S* is empirically verifiable iff *S* logically entails
> *A*1, *A*2...,
> 
> 
> 



(perhaps with the help of additional premises). More specifically, the
form A. J. Ayer initially gave to this idea was as follows:



> 
> 
> It is the mark of a genuine factual proposition...that some
> experiential [observation] propositions can be deduced from it in
> conjunction with certain other premises without being deducible from
> these other premises alone (1936 [1952: 38-39]).
> 
> 
> 



For example, from "This is a swan" together with
"All swans are white" we can deduce "This is
white" although the latter cannot be deduced from "All
swans are white" alone. Thus, "All swans are white"
counts as meaningful.



But this is obviously unacceptable and (as with its predecessor) it is
properties of logical entailment that cause the problem. To borrow
Ayer's own example (given in the second edition of his 1936
[1952]), from "The Absolute is lazy" together with
"If the Absolute is lazy, then this is white", it follows
that "This is white", and this does not follow from the
conditional premise alone. Hence, contrary to every bone in the
logical empiricist's body, "The Absolute is lazy" is
meaningful. The argument can be redeployed to show that any sentence
whatsoever is meaningful.



In the second edition of *Language, Truth, and Logic*, Ayer
attempted to remedy this problem. In a review, Church (1949a) roundly
refuted Ayer's proposal. This rebuttal sent verificationism and
logical empiricism itself into a tailspin. Carnap tried to rescue
these doctrines by adopting an approach not based directly on logical
entailment but this effort was refuted by Kaplan (1975a). Despite
these difficulties, there is currently an intense revival of interest
in the question of the empirical structure and content of scientific
theories and in Carnap's work in particular (see the entry on
 Rudolph Carnap).



Ayer's revised criterion of empirical verification is as
follows:



> 
> 
> *S* is *directly* verifiable iff either *S* is an
> observation sentence or else *S*, perhaps in conjunction with
> other observation sentences *A*, *B*,
> *C*,..., logically implies an observation sentence that is
> not implied by *A*, *B*, *C*....
> 
> 
> 



In addition:



> 
> 
> *S* is *indirectly* verifiable if and only if
> *S*, perhaps in conjunction with other sentences *P*,
> *Q*, *R*,... logically implies a directly
> verifiable sentence *D* that is not implied by *P*,
> *Q*, *R*,.... Furthermore, these sentences
> *P*, *Q*, *R* are each either analytic or
> directly verifiable.
> 
> 
> 



In sum:



> 
> 
> A sentence is meaningful if and only if it is directly or indirectly
> verifiable, or else analytic.
> 
> 
> 



Church argues as follows: Let \(O1,\) \(O2,\) and \(O3\) be
independent observation sentences (no one of them entails any other),
and suppose \(S\) is any sentence whatsoever--it might be
"The Nothing Nots". Church shows that Ayer's
definition entails that either \(S\) or its negation "It is not
the case that the Nothing Nots", is meaningful. For consider the
disjunctive sentence




\[ R: (\nsim O1 \cdot O2) \lor (O3 \cdot \nsim S) \]




\(R\) together with \(O1\) entails the observation sentence \(O3\) and
hence \(R\) is directly verifiable. Also, \(S\) and \(R\) entail
\(O2\). This means that \(S\) is indirectly verifiable,
*unless* \(R\) alone entails \(O2\). But if \(R\) alone entails
\(O2,\) then its right hand disjunct alone entails \(O2,\) and hence
\(\nsim S\) is directly verifiable. So either \(S\) or \(\nsim S\) is
meaningful and therefore many sentences that Ayer would reject as
meaningless are meaningful according to his definitions.



It is worth mentioning that the foregoing argument may *seem*
to depend crucially on a somewhat contested feature of classical
propositional logic. The argument appeals to the principle that if \(A
\lor B\) logically entails \(C\), then \(B\) alone logically entails
\(C\). But this in turn rests on the principle that \(B\) alone
logically entails \(A \lor B\), for any \(A\), and this principle is
rejected by so-called containment logics (for which see
 SS3.1 of the entry on connexive logic).
 However, it is possible to revise Church's argument so that it
is compatible with containment-logical principles. So in fact
Church's argument is not in this way beholden to classical
logic.


### 3.2 The Slingshot Argument



In Frege's logical system, declarative sentences stand for
(*bedeuten*) truth values, which are two distinct abstract
objects in Frege's ontology. Thus Frege treated such sentences
as a special kind of name. But others, Carnap in particular, viewed
sentences as standing for propositions. In response, Church gave an
argument, directly traceable to Frege, that the denotations of
sentences are indeed their truth values, and so cannot be propositions
as Carnap supposed. (While we prefer "designate" we will
follow Church and use "denote" in this section.) This
argument has become known as "the Slingshot", invoking the
slaying of Goliath by David, for its ability to refute looming
hypotheses such as that sentences are correlated directly with facts
or propositions.



Church argued that sentences *must* stand for truth values, for
if sentences stood for propositions, there would only be two
propositions. A similar argument that all true sentences stand for the
same thing (and that all false sentences stand for a distinct thing)
was suggested by Godel (1944; for an extended discussion of truth
values, the slingshot, and generalized truth values see the entry on
 truth values).
 Here we focus exclusively on Church's review, and his related
commentary in (1956a: SS04), which constitute the *locus
classicus* of the Slingshot argument.



Here is a simple, ingenious, logic-notation-free version of the
argument given by Church (1956a: SS04): Assume first that
sentences do denote something or other. Now consider the following
list of sentences:



(1)
Sir Walter Scott is the author of Waverley
(2)
Sir Walter Scott is Sir Walter Scott
(3)
Sir Walter Scott is the man who wrote twenty-nine Waverley novels
altogether
(4)
The number such that Sir Walter Scott is the man who wrote that
many Waverley novels is twenty-nine.
(5)
The number of counties in Utah is twenty-nine.


Church argued that (1) and (5), which seem totally unrelated in
meaning, must denote the same thing, namely, their truth value (since
that is all they have in common). The only additional assumptions
Church works with are the following two:



(A)
Co-denoting names or definite descriptions are
interchangeable.

(B)
Synonymous sentences (or, Church remarks, nearly synonymous
sentences such as (3) and (4)) have the same denotation.


Assumption (A) allows that an occurrence of a name or a definite
description N in a sentence S may be replaced by a name or description
M that denotes the same thing without altering the denotation of S.
Thus, (2) comes from (1) by (A). (But it is not clear what role, if
any, (2) plays in the argument.) (3) comes from (1) by (A); (4) comes
from (3) by (B); and (5) comes from (4) by (A). A similar argument can
be used to show that all false sentences denote the same thing. A
further conclusion, important to Church, is that if, as this argument
seems to demonstrate, (1) and (5) denote the same thing, this cannot
be the propositions expressed by each, since those are clearly
different. (For further discussion see
 supplement C.1
 as well as the supplement to the entry on
 truth values.)


### 3.3 The Translation Argument



Consider the sentences



(1)
Seneca said that man is a rational animal
(2)
Columbus believed that the world is round.


A natural analysis of such sentences is that they express a relation
between Seneca or Columbus and the propositions that man is a rational
animal or that the world is round, where such propositions are
objective abstract entities that are the ultimate vehicles of truth
and meaning. But there has been--and no doubt always will
be--skepticism about the existence of such entities and this has
motivated the view that sentences such as (1) and (2) express
relations between agents and sentence types or even particular
inscriptions (or other tokens) of sentences of a particular language,
where sentences are assumed to be more concrete than propositions.
While this assumption of concreteness seems highly questionable in the
case of sentence types, Carnap and others nevertheless vigorously
pursued the project of analyzing (1) and (2) in terms that relate
agents to such types. (The theory that saying and believing are
relations to particular physical tokens is obviously implausible.
Contrary to what it predicts, the destruction of such tokens would not
have voided Seneca's belief.) In response, Church deployed his
translation argument (CTA) that if we limit our ontology to sentence
types, then our semantic theory will not be able to provide a true
analysis of sentences like (1) and (2). (This is a crucial part of
Church's broader argument that no philosophical theory that is
both true and humanly understandable can do without propositions. We
return to the rest of the argument in
 SS6.3.)



CTA--as formulated in Church's (1950a)--is
specifically directed at Carnap's (1947) analysis of sentences
like (1) and (2), which in turn appeals to a particular notion of
synonymy. However, since Church has shown that Carnap's notion
of synonymy is incorrect (via an argument described in
 supplement E),
 we can safely omit the details of Carnap's notion for present
purposes and speak simply in terms of synonymy. Now, according to
Carnap's analysis, (2) is synonymous with



(3)
Columbus was disposed to an affirmative response to the English
sentence "the world is round".


This is presumed true in virtue of Columbus' disposition to
affirm, say, "*El mundo es redondo*" or a
synonymous sentence in some other language (such as the English
sentence "The earth is round").



Church suggested that the reader translate (2) and (3) into German
making sure that, among other things, "that the world is
round" as it occurs in (2) is translated as "*dass die
welt rund ist*", whereas "the world is round" as
it occurs in (3) is translated as "the world is round".
The difference is that the sentence "the world is round"
is *mentioned* in (3), whereas it is *used* in (2);
moreover, (3) does not mention the German sentence "*die welt
rund ist*", only the English sentence "the world is
round" and so a proper translation of (2)--one that
preserves meaning (and not merely "the main
point")--will mention the latter not the former. So, the
translations are:



(4)
*Columbus glaubte, dass die Welt rund ist*
(5)
*Columbus war bereit, den englischen Satze* "The
world is round" *zu bejahen*.


(Notice that if we replace "The world is round" in (5) by
its German translation, the result is clearly false, since the German
translation is not a sentence of English.)



Church concluded this version of CTA by noting that (4) and (5) are
clearly not synonymous, since they convey different information to a
German speaker who does not speak English. Church concluded that,
therefore, (2) and (3) are not synonymous (1951a [BE: 294]). Church
assumed, plausibly, that synonymy is an equivalence
relation--reflexive, symmetric, and transitive. Hence, the basic
structure of CTA is as follows: Assume that (2) and (3) are
synonymous. Then (4) and (5) are synonymous. But (4) and (5) are not
synonymous, and so neither are (2) and (3), and therefore (3) cannot
serve as an analysis of (2).



However, Church argued that translation is not needed to establish
that (2) and (3) are not synonymous, and he gave another argument that
does not appeal to translation:



> 
> 
> It is not possible to infer [(2)] as a consequence of [(3)], on
> logical grounds alone--but only by making use of an item of
> factual information not contained in [(3)], namely, that "the
> earth is round" means in English that the earth is round. (1950a
> [BE: 280])
> 
> 
> 



The point is that it is only a contingent fact about the English
language that the particular sequence of symbols and associated sounds
"the earth is round" mean in English that the earth is
round. (Compare Church's summary of his argument where he says
that it is designed to "dispel any remnants of an illusion that
there is something in some way necessary or transparent about the
connection between a word or sentence and its meaning, whereas, of
course, this connection is entirely artificial and arbitrary"
(1951a [BE: 294]).) Moreover, this additional factual information is
needed to infer (2) from (3). For example, the language might have
developed in such a way that "round" and
"square" were interchanged, so that to say "the
earth is square" in this version of English is to say that the
earth is round. Note that the following would nonetheless be true in
this new version of English:



> 
> 
> "the earth is square" means that the earth is square,
> 
> 
> 



where the latter *used* occurrence of "the earth is
square" is a pronouncement of the new version of English, not
the familiar one. This shows that the aforementioned factual
information is needed to infer (2) from (3), since otherwise the
expression "the earth is round" need not represent
Columbus' belief. This argument that CTA does not essentially
involve translation is worth a closer look, since Church himself
describes the argument as expressing "the main point" he
is trying make via CTA:



> 
> 
> The main point is that [(3)] is inadequate as an analysis of [(2)]
> because it conveys less information than [(2)] does. (1950b [BE:
> 1061]; cf. Salmon 2001)
> 
> 
> 



The information conveyed by (2) but not (3) is:



(6)
"The earth is round" means in English that the earth
is round.


Church claims that this is "an item of factual information not
contained in [(3)]", and it was Church's view that the
word "English" as commonly used contains "reference
to matters of pragmatics" (1950b [BE: 1060]). By this he meant
that the word "English" means something like, as Church
puts it, "the language that was current in the United States,
Canada and Great Britain in 1949 AD", since it allows that
English is an evolving rather than a fixed system (1950). If so, it
seems clear that the information given by [(2)] is not contained in
[(3)] and that translation is not required to establish this.



However, in a further twist, Carnap responds that
"English" as \(he\) intends it means something like
"the unique language having such and such semantical
rules" and he brings this to Church's attention in his
letter (1950b [BE: 1063]), thus challenging Church's claim that
(5) is an item of factual information not contained in (3) but needed
to infer (2) from (3). Church recognizes the threat:



> 
> 
> The objection would then be less immediate that [(2)] is not a logical
> consequence of [(3)] and it is possible that it would disappear.
> (1950a [BE: 280])
> 
> 
> 



The point is that if English is defined to be the unique language with
such and such semantical rules and (5) is one such rule, then it looks
as though (2) *would* be a logical consequence of (3), so
interpreted.



In the last paragraph of (1950a), Church briefly states two arguments
that he obviously views as cementing the falsehood of Carnap's
analysis, even if English is taken to be the language with such and
such fixed semantical rules. He first observes that if Carnap's
proposal is discussed in German rather than English, then it will not
be synonymous with the English version! The one version involves an
English sentence while the other a German sentence. Church's
assumption appears to be that a correct analysis of (2) should be
language independent. Next, he observes that even if (3) logically
entails (2), a person might not see the entailment, and so not draw
the inference, leading her to believe (3) and yet not believe (2). Is
Church's assumption here that if (3) were a correct analysis of
(2), then understanding and believing it should entail understanding
and believing (2)? If so, this would conflict with Church's own
way of dealing with the Paradox of Analysis. Moreover, there is
arguably an outright inconsistency between Church's solution to
this paradox and his solution to the Mates puzzle, which we discuss in
 supplement C.
 Church's criticism of Carnap's notion of synonymy is
discussed in
 supplement E.


### 3.4 The Paradox of Analysis



Church's brief remarks on the paradox of analysis focus
exclusively on the sentence



(1)
A brother is a male sibling.


(While this is an example of a trivial analysis, its triviality does
not affect the cogency of Church's discussion.) Church renders
(1) as



(2)
\(b = \textit{ms}\)


which he thinks of as an expression "of the Boolean algebra of
classes--or better, of class concepts" (1946a [BE: 956]).
According to this proposal, the concept of a brother is a kind of
"product" of the concepts of a male and a sibling. (Of
course, this ignores the relational nature of both sides of the
equation. For example, the only siblings relevant to the definition
are the brother's siblings; other siblings are ignored, and so
the analysis is incomplete. But we shall nonetheless stick to
Church's formulation.) The problem as Church sees it is
this:



> 
> 
> If \(b\) and \(\textit{ms}\) are the same concept, then it must be
> possible to introduce either in place of the other without alteration
> of meaning--indeed this is clearly the intention, or part of the
> intention, of any analysis in the sense of Moore. Hence in particular
> the analysis \(b = \textit{ms}\) must not be different from \(b = b\)
> or \(\textit{ms} = \textit{ms}\). This would seem to reduce analysis
> to something trivial and uninformative. But it is evident
> otherwise--especially from cases in which, though a concept is in
> some sense known, its analysis presents difficulty--that analysis
> is not always trivial. (1946a [BE: 956])
> 
> 
> 



Church argues that the paradox is a special case of what is now known
as "Frege's Puzzle". It is unclear how a statement
of the form \(a = b\) can be both true and informative; for if it is
true, then it would seem to say the same thing as \(a = a\), since
this is the result of substituting \(a\) for \(b\) in \(a = b\).
Moreover, Church views (2) as a special case of an informative
identity statement, with the difference that (2)--unlike a
statement of the form \(a = a\) that asserts the identity of
objects--asserts the identity of concepts or senses. That is,
Church takes "brother" and "male sibling" to
designate concepts in the context of (2), rather than classes, since
(2) is meant to be an analysis. Further, while "brother"
and "male sibling" designate the same concept, viz.
*brother* or *male sibling*, they may nevertheless
differ in sense (that is, though they designate the same concept the
express, they *express* different concepts as senses); and this
is what explains how (2) can be informative and how the proposition
expressed by (2) can differ from that expressed by the trivial \(b =
b\) or \(\textit{ms} = \textit{ms}\).



The power of Church's proposal may not yet be apparent due to
the triviality of the sample analysis. Recall Church's remark
that there are cases of analyses (or hoped for analyses) where



> 
> 
> though a concept is in some sense known, its analysis presents
> difficulty--that analysis is not always trivial. (1946a [BE:
> 956])
> 
> 
> 



In philosophy the correct analysis of the concept of knowledge has
proved to be profoundly elusive. In mathematics, the analysis of the
concept of the limit of a function was a triumph, as was the analysis
of the concept of an effectively calculable (computable) function.
Church would view these as cases where *analysans* and
*analysandum* designate the same concept but express radically
different senses; and this does seem exactly right. Some, however,
have thought that Church's way of dealing with the paradox of
analysis and his way of dealing with Mates' problem are
incompatible. This is discussed in
 supplement C.2.


### 3.5 The Logic of Sense and Denotation



Church's (1943a) review of Carnap's *Introduction to
Semantics* (1942) constitutes an important early step in the
application of the logistic method to the subject of semantics (see
also Church 1943c, 1951b, 1952, 1956a). Like Frege, Church believed
that the *Sinn* or sense of an expression is an
*objective*--i.e., mind-and-language
independent--abstract entity (cf.
 SS3.3
 and
 SS6.3)
 and that senses are needed in semantics for their power to explain
the informative nature of identity statements containing
co-designating names, as well as to explain the failure of the
substitutivity of co-designating names in intensional contexts (1943a;
1956a: SS01). Moreover, Church also shared Frege's highly
controversial view that in addition to assigning senses to expressions
in scientific language, one should also assign them to expressions in
natural language. (See
 supplement E
 for discussion.)



However, given that senses and propositions are objective, one might
wonder whether theorizing about them via the logistic method should
*really* proceed *indirectly*, via the study of
intensional semantic theories of possible languages (again, see
 supplement E),
 or whether the logistic method should instead study senses
*directly* by theorizing about how these entities are related
to one another and to the *designata* that they determine.
Church himself distinguishes these two approaches and claims that if a
theory could be formulated in a satisfactory way using the direct
method, then "it should be a comparatively simple matter to
devise a language with the desired sort of semantics" (1979 [BE:
807]). He pursued this direct approach in his papers on the *Logic
of Sense and Denotation* or "LSD" (1946b, 1951a,
1973b, 1974a, 1993).



The fundamental difference between the intensional semantic approach
to language and the direct LSD approach to senses can be seen from the
following. Church's view that the sense assigned to a name by a
semantic theory is *univocal* raises the question of
*which* sense to assign to "Hesperus". Further,
names can occur not only in *customary* contexts like



(1)
Hesperus is a planet


but also in *indirect* contexts such as:



(2)
Hammurabi believes that (1).


Which sense do we assign to "Hesperus" in (2)? From the
perspective of a Fregean semantic theory, this question has the
following answer. First, we distinguish the expression
"Hesperus" from an *occurrence* of it in a
non-customary syntactic position such as in (2). Secondly, we assign a
non-customary sense to its occurrence in (2) so that this occurrence
expresses not the customary sense of "Hesperus" (say,
*the first planet visible in the evening*) but its indirect
sense. Thirdly, we claim that this indirect sense determines the
expression's customary sense as the designatum of the
non-customary occurrence (cf. Frege 1892a; Salmon 1993).
However, such subtleties will require us to complicate the background
logic. In this case, we have to prohibit the application of Leibniz
law to indirect contexts; this is because names with the same
customary designatum but *different* customary senses cannot be
substituted *salva veritate* within contexts where they
designate their customary senses. For example, (2) can be true while
(2\*) is false:



(2\*)
Hammurabi believes that Phosphorus is a planet.


From the perspective of LSD, these complications pertaining to
indirect contexts can be avoided by replacing the occurrence of
"Hesperus" in (2) with a new name; and likewise for all
other occurrences that *would* be assigned a non-customary
*designatum* were we still working in a semantic theory. For
example, we can replace the customary occurrence of
"Hesperus" in (1) with a constant "\(a\_0\)"
and replace the non-customary occurrence of "Hesperus" in
(2) with "\(a\_1\)". This raises the question of the
relationship between these constants.



LSD was originally formulated in a simply typed l-calculus (of
the kind described in
 supplement D),
 which allows the subject matter of the theory to be sorted into
various type hierarchies. Individuals (like Hesperus) are of type
\(\iota\_0\). Senses (which Church calls "concepts") that
determine individuals--i.e., "individual
concepts"--are of type \(\iota\_1\) etc. In another
hierarchy, truth values are of type \(o\_0\), concepts of truth
values--i.e., propositions--are of type \(o\_1\), concepts of
propositions--i.e., "propositional
concepts"--are of type \(o\_2\) etc. (Individuals are
designated by constants, truth values are designated by sentences
while propositions are designated by complex names corresponding to
"that"-clauses.) In addition to typed hierarchies of
concepts of individuals and concepts of truth values, there is also a
hierarchy of functions and concepts of functions; for any types
\(\alpha\_k\) and \(\beta\_k\), there exists a type
\(\ulcorner\)(\(\alpha\_k\) \(\beta\_k )\urcorner\) of functions from
entities of \(\beta\_k\) to entities of type \(\alpha\_k\).



In this framework, "\(a\_0\)" designates an individual of
type \(\iota\_0\) and expresses an individual concept of type
\(\iota\_1\). Further, "\(a\_1\)" designates this individual
concept in virtue of expressing a concept of type \(\iota\_2\) of the
individual concept. However, and crucially, in LSD this concept of
type \(\iota\_2\) is *not* the Fregean indirect sense of
"\(a\_0\)"; rather, it is a distinct semantic primitive
that is assigned to "\(a\_1\)" only. How, then, are these
concepts related?



Church tells us that there is a relation \(\Delta\) that holds between
concepts of each type within a hierarchy and the entities of the type
immediately below it, for example between a concept of type
\(\iota\_2\) and another concept of \(\iota\_1\). But something more
needs to be said to illuminate the nature of this relationship. This
is because although it helps to increase the numerical value of a
subscript in order to remove ambiguity from our notation and indicate
a corresponding increase in type, *this provides little or no
insight into the relationships among the concepts themselves*,
which are neither related by the numerical successor relation, nor
dependent for their existence and identity on the notation for them.
Moreover, expressing concepts may require adding new expressions to
the language, so not everything can be expressed using a fixed
vocabulary like the numerals.



This bring us to an objection, which arises from the fact that
intensional contexts can be iterated:



(1)
Hesperus is a planet
(2)
Hammurabi believes that (1)
(3)
Monica said that (2)
 
*Ad infinitum.*


Replacing such constructions with the corresponding ones in LSD
requires an infinity of independent names,
"Hesperus0"--"Hesperus*n*",
corresponding to the occurrences of "Hesperus" in (1),
(2), (3), etc. If these names named an infinity of primitive and
independent concepts, Church's proposal would be subject to the
objection that a language for which LSD was a semantic theory could
not be learned (Davidson 1965). To meet this objection, something more
needs to be said about the nature of the relation \(\Delta\). The
issue is discussed in
 supplement E,
 as are Church's numerous other achievements in the philosophy
of language.



A more formidable problem is that John Myhill was able to derive a
version of the so-called "Russell-Myhill paradox (RM)"
within Church's initial formulation of LSD (see Myhill 1958). In
response, Church reformulated LSD by ramifying the relation \(\Delta\)
(1973-4). In response, Anderson (1987) showed that the source of
the inconsistency of LSD lay in its axioms. We turn to the subject of
antinomy and paradox and their impact on Church's work in the
next section.



Before we do so, it should be noted that LSD had some influence on the
development of intensional logic. Both Kaplan (1964) and Montague
(1969, 1970b) built on Church's work, combining type theory with
Carnap's (1947) notion of an intension as a function from worlds
to extensions. However, to the extent that Kaplan and Montague favored
Carnap's notion of an intension they disagreed with Church
himself, who rejected this notion and treated senses along the same
lines as Frege (again, see
 supplement E).
 Anderson (1980, 1987, 2001), Klement (2002), T. Parsons (2001) and
Salmon (2010) follow Frege and Church more closely. Bealer
(1982) also responded to Church. (See also the entry on
 intensional logic.)


## 4. Paradox


### 4.1 Antinomy in Church's Work



Church's work was dogged by what he termed
"antinomies", which he distinguished from paradoxes in
that the former result in outright contradiction whereas the latter
give rise only to unacceptable conclusions. (Quine's paradox
discussed in
 supplement C
 is an example of a paradox that is not an antinomy.) His early
attempt at providing foundations for mathematics turned out to be
susceptible to Russell's antinomy (Church 1932) and
Richard's antinomy (Church 1933). (Hereafter we use
"paradox" rather than "antinomy" since that is
the current usage; but bear in mind that there are then two kinds of
paradox.) His later attempts to formulate LSD gave rise to the
Russell-Myhill paradox and Anderson's (1987) paradox, which
drove Church to turn to Ramified Type Theory (or "RTT") as
a solution (see below
 SS4.4
 and
 SS5).
 In addition Church was convinced that Simple Type Theory (or
"STT", see
 supplement D)
 supplemented with a semantical predicate is threatened by the
semantical paradoxes and in particular by the Grelling-Nelson paradox
(the "heterological" paradox), hereafter
"Grelling's paradox" or GP. Church had an intense
desire to show first how GP may be derived in STT so supplemented,
secondly, how RTT resolves the problem, third, that adding the axioms
of reducibility does not restore the paradox and in fact leads to an
important definability result concerning RTT with reducibility, and
finally, fourth, that the resolution of GP by means of RTT does not
differ significantly from a Tarskian resolution in terms of the
distinction between object and metalanguage.


### 4.2 Grelling's Paradox



This paradox is usually--and was originally--formulated as
pertaining to adjectives expressing properties that are or are not
true of the adjective (the word) itself. For example,
"short" is short, whereas "red" is not red.
Those adjectives that have the properties they express are termed
"autological" and those that don't are termed
"heterological". The problem arises with the question: Is
"heterological" heterological or not? And the answer is
that it is if and only if it's not. But the paradox is better
formulated in terms of the extensions, in general, of any sort of
predicate--adjective, common noun, or verb phrase. Some
predicates belong to their own extensions and some do not. The problem
arises if it supposed that there is a
predicate--"heterological"--whose extension
consists of exactly those predicates that do not belong to their own
extensions, since then "heterological" belongs to its
extension if and only if it does not.



Viewed in this way, the reasoning of the paradox is in direct
violation of Cantor's theorem. The latter theorem is usually
thought of as the principle that the cardinality of the power set of a
set is greater than that of the set; and applied to an infinite set,
this leads to the sequence of ever larger infinite cardinal numbers.
But in its most basic form--from which the result about
cardinality follows as a corollary--Cantor's theorem is the
following set theoretical principle:



Cantor's Lemma (CL)
  

Let \(f\) be a function with domain \(A\) and range \(B\). Then the
set: \(D\_{f} = \{x \in A: x \not\in f(x)\}\) is not in \(B\).



*Proof*. If \(D\_f\) is in \(B\), then there is some \(y\) in
\(A\) such that \(f(y) = D\_f\). It now follows that \(y\) is in
\(D\_f\) iff it's not. Contradiction. Note that when \(A = B\)
and \(f\) is the identity map defined on \(A\), the result is (a form
of) the theorem asserting that the set of non-self-membered sets does
not exist.



It's worth mentioning, firstly, that this principle underlies
diagonal argumentation in general (cf. Gaifman 2006). Even venerable
examples such as Post's informal argument that there is a
recursively enumerable set of positive integers whose complement is
not recursively enumerable, rely in essence on
 CL
 (Davis 1965: 312). A slight variant of CL is frequently found in the
literature on undecidability (cf. Shoenfield 1967: 131). Secondly, the
proof of CL only relies on minimal set-theoretic resources. Of
course, the famous corollary of CL about cardinality relies
on the power set axiom. But the theorem that there can be no
one-one function from a set onto its power set is otherwise a direct
consequence of CL. In this case, \(D\_f\) must be in \(B\), since it
belongs to the power set of \(A\), and the conclusion must be that
\(f\) does not exist. Third, Grelling's paradox as well as
Berry's paradox can be used as a basis for alternative proofs of
the first incompleteness theorem (Boolos et al. 2007; Kripke 2014).
Lastly, a somewhat more general form of CL pertaining to relations in
general--not just to functions--, which is now accepted as a
version of Cantor's Theorem, was already noticed by Russell
(1903). Whereas CL is essentially a principle of first order logic,
the relational version is second order in nature.



To say that \(D\_f\) is not an element of \(B\), where \(B\) is the
range of \(f\), is to say that there is no element \(x\) of \(A\) such
that \(f(x) = D\_f\). Applied to predicates and their extensions,
 CL
 implies that for any function \(g\) mapping *some* predicates
\(A\) to their extensions, there is a predicate
"heterological\(\_g\)" whose extension is \(D\_g\) although
this predicate cannot be in the domain of \(g\). However, assuming
that there is a function, \(h\), mapping *every* predicate to
its extension, there can be no predicate, heterological\(\_h\), *at
all*, whose extension is \(D\_h\). From a Tarskian point of view,
heterological\(\_h\), must be a predicate of the metalanguage. From
Church's point of view, there are a multiplicity of
heterological predicates analogous to, but not the same as, the
heterological\(\_g\) predicates, distinguished by their types and
orders in the ramified hierarchy. CL is exploited in the next
section.


### 4.3 Comparing Russell and Tarski



In an important paper but one still not widely discussed in print,
"A Comparison of Russell's Resolution of the Semantical
Antinomies with that of Tarski" (1976), reprinted with some
additions and corrections in Martin (1984) and *The Collected
Works* (2019), Church does the following:


1. He gives an elegant formulation of RTT as a straightforward
complication of STT. (See
 supplement D.
 We adopt the definitions and notations used there.)
2. He shows how Grelling's paradox, GP, may be derived within
STT with the addition of a semantical predicate Val in the object
language interpreting "forms" (wffs containing free
variables) and governed by appropriate postulates.
3. He shows how RTT resolves GP and how it answers the question
whether "heterological" is heterological or not. Depending
on its level, it sometimes is and sometimes is not; but the assignment
of levels is not *ad hoc*. It emerges as a product of RTT along
with the axioms about Val.
4. He defines languages \(L\_1,\) \(L\_2,\)..., \(L\_{n +
1},\)..., \(L\_w = L,\) in terms of the *r*-types and Val,
where \(L\_{n + 1}\) is a semantical metalanguage for \(L\_n\).
5. He shows how analogues of Tarski's definitions of
satisfaction and truth and Tarski's theorem are obtained for the
languages \(L\_n\) and concludes that Russell's resolution of GP
is a special case of Tarski's.
6. He formulates the axioms of reducibility which are needed to
restore the impredicative definitions required for classical
mathematics. He then shows that reducibility does not, at least not in
any obvious way, reinstate GP. However, the system with Val and
reducibility does prove certain results about definability and
nameability of propositional functions.


### 4.4 The Derivation and Dissolution of GP



In the following, we focus on Church's Russellian resolution of
GP and leave aside most of the remaining issues. In this we are aided
by a simplified account of the matter prepared by Church (1995a). The
simplification does not omit anything essential to the argument of
Church (1976) regarding GP specifically. It is clear that a main
concern of Church was to communicate once and for all Russell's
resolution of the semantic paradoxes to a wider audience.



Church's *r*-typed Val predicate is rather clumsy, but it
is required for the generalizations in (1976) to accomplish all the
goals listed above. In the simplified account, however, Val is
replaced by a denotation predicate \(D(v, F)\), where \(v\) is a word,
understood to be an individual, and \(F\) is a propositional function
of any *r*-type. \(D(v, F)\) is read "\(v\) denotes
\(F\)". Church remarks that



> 
> 
> We shall make use only of the case that the second argument of \(D\)
> is a singulary functional variable or singulary functional constant of
> lowest type, so fixing the type of \(D\). (1995a [BE: 929])
> 
> 
> 



The *r*-type of \(D\) is then \((i (i))/1\), for the purposes
of the following.



Church first shows how GP may be derived within STT using certain
principles concerning \(D\), the first of which is a principle of
"univocacy":




\[\tag{\*} D(v,F) \supset\_{v F} \hdot D(v,G) \supset\_{G} \hdot F(x) \equiv\_{x} G(x).\]



(Note the following notational conventions. Firstly, a connective can
take a variable as subscript: that variable becomes a universal
quantifier whose scope is precisely that of the connective. Secondly,
a dot placed before a connective brackets a proposition. The stars are
also Church's notation.) Church decides to avoid the stronger
axiom asserting that \(D\) is functional due to complications
concerning identity in the ramified theory, but the effect is the
same. The
 axiom \*
 guarantees a weaker form of functionality: It is a function from
words as individuals to extensions of propositional functions,
assuming the axiom of extensionality for such extensions. Next Church
invokes an informally stated principle that he describes as
"reasonable":



\*\*
Whenever an individual or a propositional function has been
determined in some unique way, it is permissible to extend the
language by introducing a constant (a word) which denotes it.


On this basis, he says, the constant "het" may be
introduced together with an axiom defining it implicitly:




\[\tag\*{\*\*\*} \het(w) \equiv\_{w} (\exists F) \hdot D(w, F) \cdot \nsim F(w).\]



(Note the difference between the dot placed before the connective and
the conjunction sign itself.) By a simple deduction from the three
starred principles and basic logic, Church derives both \(\het(v)\)
and \(\nsim \het(v)\). Church's deduction closely resembles one
given by Copi (1971), who attributes it to Ramsey. (See
 supplement F.)



Church clearly thinks that the starred principles are
"reasonable" and that the only problem is that they make
use of an impredicative definition, namely,
 \*\*\*,
 and that when the starred principles are suitably ramified, the
problem can be solved in the manner Russell (1908) foresaw and
implemented, if imperfectly (PM). He remarks that




\[\tag\*{\*\*\*\*} \het^{m+1} (w) \equiv\_{w} (\exists F^{1/m}) \hdot D(w,F) \cdot \nsim F(w)\]



which replaces
 \*\*\*,
 when level indicators are supplied, defines an infinite list of het
predicates, "het2",
"het3", ..., and the two other starred
principles are also to be supplied with level indicators. Church now
gives what appears to be a hastily composed list of inferences with
annotations but no comment. However, Church in effect here proves the
analogues of theorems (6) and (7) of (1976), with \(D\) in place of
Val. These are:

 
\[\tag{\(6'\)} \left[D^{m +1} (v, G^{1/m+1}) \hdot G(x) \equiv\_{x} \het^{m+1} (x)\right] \supset \nsim \het^{n+1} (v), \textrm{ if } m \ge n \]
 
\[ \tag{\(7'\)} \left[D^{m +1} (v, G^{1/m+1}) \hdot G(x) \equiv\_{x} \het^{m+1} (x)\right] \supset \het^{n+1} (v), \textrm{ if } m \lt n. \]


To derive these, Church assumes that:




\[\tag{5} \het^{n+1} (v) \supset \het^{m+1} (v), \text{ if } m \ge n.\]




(5) is a theorem of (1976).



Note that, as in the case of Val, the level \(m+1\) of \(D^{m+1}\) is
determined entirely by the level of its second argument place. (5) is
needed as a lemma in the proofs of (\(6'\)) and (\(7'\)). In (1995a)
Church appeals to (5) without comment, perhaps assuming implicitly the
\(D\)-analogue of axiom (4) of (1976) reflecting that the types of the
semantical predicates are cumulative--as are the types of (1976)
in general. It is also worth noting that in the background is an
*r*-typed version of the
 principle \*\*
 asserting that at any level \(m\) there is a word \(v\) denoting a
property having the same extension as \(\het^m\). (Compare theorem (8)
of (1976).)



In this scheme, the question whether the word
"heterological" is heterological becomes the question
whether a word \(v\) denoting that property, or rather a word with
same extension, is heterological; and the answer is that it depends on
the level of the property \(\het^{m+1}\).



At levels equal to or less than \(m+1\), \(\het(v)\) is false; that
is, \(v\) is autological. At levels greater than \(m+1\), v is
heterological; this, according to (\(6'\)) and (\(7'\)). There is,
therefore, no *one* property of heterologicality such that it
is possible to ask whether a word for it is heterological or not; and
this blocks GP.



Church's point of view is that the semantical primitives and
principles, including
 \*\*,
 that were added to STT to obtain GP are all "reasonable".
The only thing missing is ramification. This is in essence why Church
thought that RTT provides the framework for the solution to the
semantical paradoxes. (For more details see
 supplement F.)



In an undated typescript newly published in *The Collected
Works* (n.d., [BE: 928]), Church formulates conditions required
for the derivation of the Berry paradox within STT and indicates how
it is resolved in RTT. He uses Val to formulate a condition giving the
"Berry number" of a formula. His formulation is quite
similar to that found in Boolos et al. [2007: 228). But in this short
note he does not give a derivation of the paradox within STT.


### 4.5 The Russell-Myhill Paradox



In a later paper, Church turns his attention to a paradox that Russell
formulates in Appendix B of *Principles of Mathematics* (1903).
Once again, Church's aim is first to show how this contradiction
arises in STT, and then to appeal to RTT as a means of solving the
problem. This time, however, STT is not supplemented directly by any
overt semantic principles concerning denotation or predication, but
only by a predicate for identity of propositions and axioms supporting
Russell's view as of 1903, that if a pair of propositions differ
by a constituent, then they are different propositions. For example,
if \(X\) and \(Y\) are distinct classes of propositions, then the
propositions expressed by "Every proposition in \(X\) is
true" differs from that expressed by "Every proposition in
\(Y\) is true". Given this principle--call it
"Structure"--if such propositions are correlated with
the classes they mention, then it is possible to diagonalize and
obtain a contradiction. For let \(W\) be the class of propositions
that are not in the classes with which they are correlated, and
consider the proposition expressed by "Every proposition in
\(W\) is true". Then this proposition is in \(W\) if and only if
it's not. (Note that this argument involves yet another
violation of
 CL,
 since in effect it defines a function \(f\) from propositions to sets
of them, and then assumes that \(D\_f\) is in the range of \(f\). )
Church gives a careful proof theoretical analysis of this argument
showing exactly what formal principles must be assumed for it to be
formally derivable. (See
 supplement F
 for a sketch of some details.)



In a certain form, this contradiction actually rose up to bite Church
himself, because Myhill (1958) was able to derive a version of it
within Church's initial formulation of LSD. Thus it has come to
be called "the Russell-Myhill paradox (RM)". In fact, RM
can be deployed to prove the inconsistency of popular accounts of
propositions such as that of Soames (1987, 2010; see Deutsch 2008,
2014, 2019). Recently, however, higher order versions of RM have
enjoyed attention from philosophers seeking to draw metaphysical
morals (Goodman 2017; Uzquiano 2015). These writers see the
contradiction as a proof that Russell's Structure principle is
false. But neither Russell nor Church saw it that way. Russell left
the problem open and Church turned to RTT for a resolution.


### 4.6 The Knowability Paradox



In the course of writing a referee's report on a paper submitted
to the *Journal of Symbolic Logic* by Frederick Fitch, Church
gives the following inspired argument:



> 
> Then it may plausibly be maintained that if \(a\) is not omniscient,
> there is always a true proposition which it is empirically impossible
> for \(a\) to know at time \(t\). For let \(k\) be a true proposition
> which is unknown to \(a\) at time \(t\), and let \(k'\) be the
> proposition that \(k\) is true but unknown to \(a\) at time \(t\).
> Then \(k'\) is true. But it would seem that if \(a\) knows \(k'\) at
> time \(t\), then \(a\) must know \(k\) at time \(t\), and must also
> know that he does not know \(k\) at time \(t\) ... this is a
> contradiction. (1945b [Salerno (ed.) 2009: 14])
> 



It follows that it is impossible for \(a\) to know \(k'\) at time
\(t\). A generalization of this argument appears to show that if there
are true propositions that are not known to be true, then there are
true propositions that cannot be known--that are unknowable.
Contrapositively, if every true proposition can be known, then every
true proposition is known--which is clearly absurd.



The generalization--which Church does not formulate and which was
first formulated by Fitch (1963)--has become known as "The
Knowability Paradox" or "Fitch's Paradox" and
it has been the subject of a great deal of wide-ranging commentary
collected in Salerno's (2009). Fitch's argument may be
formulated as follows:


1. Assume for *reductio* that \(K(p \hdot \neg Kp)\).
2. Then \(Kp \hdot K\neg Kp\), assuming \(K(q \hdot r)\) implies \(Kq
\hdot Kr\), for arbitrary \(q\) and \(r\).
3. \(\neg Kp\), assuming \(Kq\) implies \(q\), for arbitrary
\(q\).
4. Hence, \(Kp \hdot \neg Kp\) by logic.
5. Therefore, \(K(p \hdot \neg Kp)\) cannot possibly be true, and
therefore, \(p \hdot \neg Kp\) is unknowable.



Fitch, in his (1963), does not state the argument 1--5, but
instead notes that the proof of his generalized conclusion is
"similar" to Church's argument. Surprisingly, Church
does not comment on the incompatibility of a Fitch-style
generalization with the logical positivist doctrine that any
meaningful and true proposition is in principle verifiable and hence
knowable. The contemporary revival of Fitch's argument, however,
is almost entirely devoted to this issue and, more generally, to the
consequences of Fitch's argument for widely held views committed
to the principle that there are no unknowable truths.



Church remarks in effect that step 2, the distribution of \(K\) over a
conjunction, is an instance of the doubtful principle that the logical
consequences of a known proposition are also known. He also notes that
there are "fools" who would believe a conjunction and yet
not believe its conjuncts. But could there be such foolishness as to
count a conjunction as *known* and yet not count its conjuncts
as such? Most find this highly implausible. Finally, Church suggests
that his argument runs afoul of type restrictions. Linsky, in his
(2009), gives a lucid account of the application of Church's
1976 version of RTT to the knowability paradox. See also the entry on
Fitch's Paradox of Knowability.


## 5. Foundations of Mathematics



Church was primarily concerned with providing a foundational system
that meets two basic conditions: (1) it avoids the paradoxes, and (2)
it is adequate for extant mathematics. These two conditions will be
the main focus of this section.


### 5.1 Attempts at Type-Free Foundations



Later in his career, Church looked to RTT to meet conditions (1) and
(2); but in his early forays into foundations he was quite dismissive
of RTT:



> 
> 
> Rather than adopt the method of Russell for avoiding the paradoxes of
> mathematical logic, or that of Zermelo, both of which appear somewhat
> artificial, we introduce for this purpose, as we have said, a certain
> restriction on the law of excluded middle. (1932 [BE: 52])
> 
> 
> 



It turned out that despite this restriction a form of Russell's
paradox is derivable in the system of 1932. Nevertheless, it was here
that Church first formulated the (untyped) l-calculus as a mere
part of the whole system. This part turned out to be of great
importance for the theory of computation, formal semantics and for the
foundations of mathematics in general. So much for inconsistency! (See
 supplement D
 for a description of the l-calculus).



In the second paper (Church 1933), the problem about Russell's
paradox was corrected. But Kleene and Rosser (1935) established that
both systems--those of Church 1932 and 1933--as well as
related early systems of combinatory logic fell prey to
Richard's paradox. The mere part--the pure untyped
l-calculus--is, however, consistent in the sense that not
all equations between l terms are derivable. This follows from
an early result due to Church himself and Rosser (1936)--the
Church-Rosser theorem (see the entry on the
 lambda calculus
 for discussion). Significant mathematical models for the
l-calculus were developed later (Scott and Strachey 1971;
Plotkin 1993; see Hindley & Seldin 2008: ch. 16). Church also
proved the consistency of a variant of the system of (1933) by
elementary means (1934), thus escaping, as he hoped, the
incompleteness theorems of Godel (1931). But this system was too
weak to satisfy requirement (2), and Church abandoned the system. (A
type-free system with a similar motivation was proposed later by
Myhill 1975.) It is remarkable that in his failed struggle to produce
a consistent, type-free foundational system, Church nevertheless
introduced ideas that have profoundly affected the development of
logic.


### 5.2 Type-theoretic vs. Set-theoretic Foundations



In 1940 Church turned away from a type-free approach and published a
version of STT that incorporated l-abstraction (see
 supplement D).
 Although Church had developed what became the most useful and famous
version of STT (1940), he thought that it was not enough to meet
condition (1), since he thought that STT when augmented with a
semantical predicate was vulnerable to the semantical paradoxes such
as the Epimenides and Grelling's paradox (cf.
 section 4
 above). To avoid these he thought it necessary to appeal to RTT (with
reducibility).



Regarding condition (2), STT with axioms of infinity and choice
permits the full development of classical number theory and analysis.
Church (1959 [BE: 493]) notes that STT with an axiom of infinity and
Zermelo set theory (Z) are of "comparable" provability
strength but that Z is slightly stronger. (Indeed, the first detailed
proof that Z is stronger than STT with infinity is given in a thesis
written under Church's supervision by Kemeny (1949). It is now
known that STT with an axiom of infinity is equi-consistent with and
has as much provability strength as *bounded* Zermelo set
theory (see Farmer 2008 and the citations therein). Moreover,
Church's STT has turned out to be an important tool in the
investigation of automated reasoning and proof verification in
computer science. The typed system with l is particularly well
suited for the use and development of programming languages and
paradigms (such as Haskell and Functional Programming [Hudak 1989]).
Thus, Church succeeded in providing a type theoretical alternative to
set theory as a foundation for mathematics. (It's also worth
mentioning that through his work on finite automata, Church
contributed in yet another fundamental way to computer science [1960,
1962a].)



However, for the most part, at this point, Church focused on the
development of intensional logic in the form of LSD (see
 SS3)
 and on condition (1)--viz. the problem of *semantical*
paradox. In his 1976, his aim is clearly to communicate the resolution
via RTT of the semantical paradoxes:



> 
> 
> To avoid impredicativity the essential restriction is that
> quantification over any domain (type) must not be allowed to add new
> members to the domain, as it is held that adding new members changes
> the meaning of quantification over the domain in such a way that a
> vicious circle results. (1976 [BE: 794]).
> 
> 
> 



Given the rest of 1976, it is natural to view Church as defending
Russell's diagnosis of the paradoxes. (This contrasts with
Church's early view that RTT embodies an "ad hoc"
resolution; see the quotes at the beginning of this section.)
Church's final position seems to have been, then, that both RTT
and Russell's rationale for it are correct.



As for the axioms of reducibility, Church's view was that the
axioms only reinstate impredicativity for extensional notions and that
*intensional notions remain unaffected*: "Thus the
rejection of impredicative definition is annulled in extensional but
not in intensional matters". In this way, RTT with the axioms of
reducibility permits the full development of classical number theory
and analysis and blocks the semantical paradoxes. This is a view
shared by Kripke (2011b) and Myhill (1979).



Church's published remarks on set theory are scattered,
relatively brief and stop short of full endorsement. However, his
overall attitude towards set theory was accepting and conciliatory,
although he was skeptical of some of its axioms, including separation
and choice. His doctoral dissertation (under Veblen) was on
"Alternatives to Zermelo's Assumption"
(1927)--namely, the axiom of choice. He viewed Zermelo's
axiomatization of set theory as "transferring" the
concepts of class and class membership from the "(unformalized)
logical level" to the "(formalized) mathematical
level", but viewed the improvements due to von Neumann, Fraenkel
and Skolem as bringing it continually closer to (formalized) logic, so
that



> 
> 
> it is now possible to formulate the theory as a system of symbolic
> logic in the same sense as the system of *Principia*. (1939b
> [BE: 156])
> 
> 
> 



These improvements brought with them an emphasis on formalization
(such as Skolem's isolation of first order logic) and that was
for Church a sign that logic was being done; although he no doubt
modified his view as the distinction between logic and proper theory
became pronounced. Later on, Church himself contributed again to set
theory. His paper on set theory with a universal set shows great
ingenuity in the analysis of a route to a consistent set theory
(consistent relative to ZF) with a universal set (1974c). But he did
not think that set theory could handle intensional notions, despite
the success of set theoretic model theory for modal logic. For a
treatment of intensional notions he continued to look to RTT.


### 5.3 Logicism and Intuitionism



Church (1962b) distinguished sharply between which systems provide
foundations for "the whole of presently extant
mathematics" and which ones provide "an economical
basis" for particular branches such as arithmetic.
Church's view was that while the study of logicism had led to
the discovery of type theory and so to the discovery of adequate
foundations for the whole of extant mathematics (see
 SS5.2),
 it did *not* succeed in putting arithmetic on the most
economical basis possible (for reasons explained, in
 supplement D
 on TT). Moreover:



> 
> 
> A more satisfactorily economical basis for elementary arithmetic is
> provided either by one of the standard formulations of first-order
> arithmetic employing primitive notations special to arithmetic and
> special arithmetic postulates, or by a weak set theory which is
> adequate for the treatments of finite sets but omits all the standard
> set-theoretic axioms that are not needed for this purpose (including
> the axiom of infinity). (1962b [BE: 611])
> 
> 
> 



For example, elementary arithmetic can be represented in the universe
of hereditarily finite sets (HF), without the axiom of infinity (for
discussion and history see C. Parsons 1987, 2007).



As for intuitionism, early on Church rejected Brouwer's view
that in mathematics the truth of a proposition is identical with the
possibility of proving the proposition, because



> 
> 
> it seems more in accord with our usual ideas to think of truth as a
> property of a proposition independent of our ability to prove it.
> (1928a [BE: 44])
> 
> 
> 



But he welcomed Heyting's formalization of intuitionism as
providing needed clarification. Later in a discussion of
intuitionistic objections to logicism, he pointed out that
Heyting's work was a concession to the method of logistic
characteristic of logic, and hence in tension with Brouwer's
view that mathematics is prior to logic (1962b [BE: 611]). The point
is a powerful one. Even those seeking to replace, for example,
Kripke's proof within classical logic of the completeness of
intuitionistic propositional calculus, with an intuitionistically
acceptable argument, have had to use the logistic method in their
investigation.


### 5.4. The Significance of Godel's Theorems and the Continuum Problem



Church was acutely conscious of the effect on the question of
foundations of Godel's incompleteness theorems. His early
attitude was that they were "unpleasant" results to be
circumvented, if at all possible (1934). His work in this direction is
related to Alan Turing's work on "ordinal logics" in
his Princeton doctoral thesis completed under Church's direction
(see Turing's [1939] paper and Feferman [1995]). Turing's
idea, encouraged by Church, was to extend an incomplete system by
adding to it the sentences unprovable in it and iterating this
operation into the transfinite. However, the iteration must be
effective and involve only ordinals that are constructive in the sense
defined and studied earlier by Church (1938) and Kleene (1938). This
idea is still being investigated today.



Church also noted that while the pure l-calculus escapes
Godel's first incompleteness theorem, this is only in
virtue of its lack of provability strength, and so:



> 
> 
> The sense in which it escapes the Godel theorem is not
> significant from the point of view of logic as a foundation of
> mathematics. (1984 [BE: 829])
> 
> 
> 



On the other hand, he also noted that for any sufficiently strong
formalized language, such as STT with the axiom of infinity,



> 
> 
> no proof of consistency... is known, except by methods involving
> assumptions so strong as to destroy any major significance. (1959 [BE:
> 488])
> 
> 
> 



Moreover, he was aware that the incompleteness theorems are a price
that has to be paid for communicating and verifying proofs in a
sufficiently strong formalized language that *also* meets his
requirement of effectiveness (discussed in
 SS2).
 The theorems, their significance for Hilbert's program, their
relation to effectiveness, and their relation to Tarski's work
are discussed in some detail in chapter VIII of Church's
textbook on mathematical logic (1968/1972/1976; printed in BE). Here
Church also acknowledged the value of Gentzen's and
Godel's consistency proofs, but apparently did not think
their significance was "major". A finitary consistency
proof in the sense of Hilbert was desirable but impossible.



Elsewhere, Church comments that:



> 
> 
> The feeling that there is an absolute realm of sets, somehow
> determined in spite of the non-existence of a complete axiomatic
> characterization, receives more of a blow from the solution (better,
> the unsolving) of the continuum problem than from the famous
> Godel incompleteness theorems. It is not a question of
> realism... versus either conceptualism or nominalism, but if one
> chooses realism, whether there can be a "genetic" realism
> without axiomatic specification. (1966 [BE: 677]).
> 
> 
> 



While Church may have wished to postulate an absolute realm of sets,
just as he postulated such a realm of senses, in neither case was he
happy to affirm the existence of such entities without first
formulating an axiomatic theory of them and then evaluating it for
truth (see
 section 6).
 The independence from the axioms of ZFC of a natural set-theoretic
question like that of the cardinality of the continuum showed that
Church's strictures could not be met without the discovery of
another axiom. Absent this discovery, Church hesitated to postulate an
absolute realm of sets and even noted the possibility of set-theoretic
relativism: that there could be "rival set theories" and
that sets "have their reality only relative to and within a
certain theory" (1966 [BE: 677]).


## 6. Metaphysics


### 6.1 Metaphysics and the Logistic Method



Church's mature view was that discussion of metaphysical
doctrines is only worthwhile if they can be reformulated and developed
using the logistic method. For example, he thought that the question
of the legitimacy of the distinction between form and matter should be
investigated by setting up a formal language, which is used to isolate
the form of a proposition as well as of the corresponding sentence, so
that one can reinterpret its non-logical vocabulary and study what is
common under various reinterpretations: "this may be considered
a more precise formulation of the traditional distinction between form
and matter" (1956a [BE: 372-3 and 379]; 1956-72 [BE:
697]; 1959 [BE: 415, 475]).



Another question that receives such a reformulation is that of the
existence of abstract entities, which, according to Church, are
"postulated" as ontological commitments of a true sentence
or theory that has been developed in accordance with the strictures of
the logistic method. The basic idea is that theory \(T\) is
ontologically committed to entities of kind \(K\) if the truth of
\(T\) implies that there are \(K\)s (1958a). Moreover, as Church
clarified later, "theory" was intended to encompass not
only formal theories but also



> 
> 
> systems of notions which arose long before scientific method came to
> be consciously used and which have therefore become embedded matters
> of "common sense" in the natural languages (1951b, fn.
> Added 1971 [BE: 287]).
> 
> 
> 



This would suggest that numbers were postulated when notations for
them first entered human culture--long before the advent of
modern science and the discovery of the logistic method. (For an
example of how natural numbers have become embedded in natural
language, see the discussion of "descendant" in
 supplement D.)
 Presumably, however, according to the logistic method, such notations
must ultimately be included in a formalized object language to which
the criterion of ontological commitment is then applied. Further,
given this commitment:



> 
> 
> If [the philosopher] maintains, for example, that numbers do not exist
> but nevertheless asserts, or is persuaded to admit, "1729 is the
> sum of two cubes in more than one way", he is, at least
> *prima facie*, involved in contradiction, because by naming the
> number 1729 and attributing a property to it he seems to be committed
> to the existence of at least this one number. (1958a [BE: 438])
> 
> 
> 



More generally,



> 
> 
> those philosophers who speak of "existence",
> "reality", and the like are to be understood as meaning
> the existential quantifier, and are to be condemned as inconsistent if
> on this basis inconsistency appears in their writings. The
> justification is that no other reasonable meaning of
> "existence" has ever been provided (which would fit into
> contexts of the kind that were quoted), and the burden of providing
> such a second meaning of "existence" rests on those whose
> writings or whose philosophical views require it. (1958a [BE:
> 442]).
> 
> 
> 



Recently, Jody Azzouni (2004, 2010) has attempted to shoulder this
burden. For discussion of nominalism and Church's criterion see
Church (1958a,b), Burgess (2001) as well as Salmon (2020).


### 6.2 Church's Modest Realism



Church was at pains to distinguish his preferred brand of realism from
Platonism (1973a [BE: 748]). Moreover, he was also clear that his
realism was not



> 
> 
> even the extreme realism of Frege and Godel, but rather only in
> opposition to the claim of superior reality for physical or
> spatio-temporal entities. (1951b, fn. Added 1971 [BE: 287])
> 
> 
> 



To show the contrast with Frege, Church stated that while his own view
is that the two truth values are "postulated":



> 
> 
> To Frege, as a thoroughgoing Platonic realist, our use of the word
> "postulate" here would not be acceptable. (1956a:
> SS4)
> 
> 
> 



Frege's position, according to Church, is that "*there
are* two such things as truth and falsehood" (1956a:
SS4). Of course, it also follows from Church's semantic
theory together with his criterion of ontological commitment that
*there are* two such things as truth and falsehood. What, then,
is the disagreement with Frege? It appears to be that because Church
postulated the two truth values relative to a logistic theory, and
because he did not claim to have demonstrated conclusively the truth
of one such theory, he still saw room for consideration of competing
logistic theories, and so competing ontologies, which do not postulate
truth values as objects (cf. 1966).



Nevertheless, according to Church, theories that are effectively
specifiable (cf. 2.3) can be communicated, inspected, compared with
each other and with observational data--as well as evaluated for
truth by other rational, checkable procedures. So there is no
*principled* reason (other than Church's Theorem) why,
after rational debate has come to an end, we could not assert the
truth of our theory and postulate the existence of its ontological
commitments with near certainty. (Of course, in some cases the theory
may be underdetermined by the data; and in the case of set theory
there may be genuine theory relativity; cf.
 SS5.4.)



Returning to Church's "opposition to the claim of superior
reality for physical or spatio-temporal entities", his reason
was that spatio-temporal entities are, like abstract entities,
postulated ontological commitments of theories. For this reason,
terminology for spatio-temporal entities does *not*
"belong to the vocabulary in which the observational data are
stated;" rather they are theoretical constructs the terminology
for which "belongs to a theoretical language" (1951b, fn.
Added 1971 [BE: 287]; cf. 1975 [BE: 983-4].)



Complementary to Church's "opposition to the claim of
superior reality for spatio-temporal entities" was his view that
abstract entities--assuming they exist--are no more remote
from causal explanations than are spatio-temporal ones. To Carnap, who
claimed that abstracts entities may be avoided in causal explanations
of phenomena (1963), Church responded by claiming



> 
> 
> the cause of an event is never a physical object or even another event
> but a total situation, in the description of which many entities, both
> abstract and concrete, must in general be mentioned (1951b, fn. Added
> 1971 [BE: 287]).
> 
> 
> 



Moreover, Church added that if we assume that the objects of
linguistic understanding and (other) propositional attitudes are
propositions (cf.
 SS3.3
 and
 SS6.3),
 then propositions are also an essential part of any adequate causal
explanation of behavior.



Given all this, it is not surprising that Church did not see a
*special* problem about our epistemological access to concepts
and propositions:



> 
> 
> But the preference of (say) seeing over understanding as a method of
> observation seems to me capricious. For just as an opaque body may be
> seen, so a concept may be understood or grasped. And the parallel
> between the two cases is indeed rather close. In both cases the
> observation is not direct but through intermediaries--light, lens
> of eye or optical instrument, and retina in the case of visible body,
> linguistic expressions in the case of the concept. And in both cases
> there are or may be tenable theories according to which the entity in
> question, opaque body or concept, is not assumed, but only those
> things which would otherwise be called its effects. (1951b [BE:
> 287])
> 
> 
> 



It should be emphasized that Church's realism about propositions
is not supposed to follow from their role in causal explanations but
from his view that no logistic theory that is both true and humanly
understandable can do without them. It is to this that we now
turn.


### 6.3 Realism about Propositions



The notion of *proposition* that Church argued must be
postulated by semantics is the "abstract notion":



> 
> 
> independent alike of any particular expression in words and of any
> particular psychological act of judgment or conception--not the
> particular declarative sentence, but the content or meaning which is
> common to the sentence and its translation into another
> language--not the particular judgment, but the objective content
> of the judgment, which is capable of being the common property of
> many. (1956-72 [BE: 742])
> 
> 
> 



Church credited Leibniz with an important argument that goes some way
to establishing the need for this notion in semantics. The argument,
as reported by Church (1956b), is as follows:



Truth cannot attach to actual particular thoughts
(*cogitationes*) or particular acts of judgment, since what is
thought or judged by no one may nevertheless be true. Perhaps, then,
truth attaches to things (*res*) rather than particular
thoughts. However, falsehood cannot attach to things, only to
thoughts. In which case, if truth attaches to things and falsehood
attaches to thoughts, then we cannot say that the same subject might
be true or false. Leibniz's way out, as reported by Church, is
that truth and falsehood attach to *possible thoughts*. This is
the notion that Church considered an important step towards the
abstract notion of a proposition.



Church (1956b) noted that instead of making the final step from
possible thoughts to propositions, we might claim that truth and
falsehood attach to *possible sentences* of some
language--those that the syntactical rules of the language allow
as well formed. He added that this move won't serve the
nominalist like Goodman--who denies propositions because they are
abstract--since the move also invokes abstract types. Further,
and for the reasons discussed in
 SS3.3,
 if we abandon nominalism but continue to limit our ontology to
possible sentences, then our semantic theory will provide a false
analysis of attributions of assertion and belief.



Church (1956b) also considered rejecting the first line of argument
and insisting that truth and falsehood *do* attach only to
actual particular thoughts or sentences. In that case, he argued, we
would be limited to those things that we could actually think or say
in a reasonable amount of time. In which case, there would no longer
be a distinction between statements that are unproved because of human
limitations and those that are *unprovable* as a matter of
mathematical necessity.



Moreover, Church pointed out that those who are willing to accept
these limitations must, at the very best, face an excessively
complicated theory of syntax and semantics (one that, for example,
would have to be formulated without the notion of an infinite
sequence):



> 
> 
> Indeed the justification would seem to be basically the same for
> extended physical objects in macrophysical theory and for ideal
> sentences in logical syntax: both are postulated entities--some
> may prefer to say inferred entities--without which the theory
> would be intolerably complex if not impossible. (1956b [BE:
> 359-60])
> 
> 
> 



Returning to Leibniz's dialogue, Church pointed out that it
contained an important assumption about logical form (which Church
accepted): that there is some *thing*--whether a thought
or another kind of thing--that is the logical subject of
attributions of truth and falsehood as well as the logical object of
attributions of assertion and belief, including attributions
containing bound variables such as "there is something that
Church asserts and Goodman denies". Church was scathingly
critical of those (like Goodman) who denied this assumption without
also providing, in sufficient detail, their own corresponding analyses
of attributions of assertion and belief. Church (1956b; 1973) noted
that Scheffler (1954) was almost alone in offering such an analysis
and defended the assumption by submitting Scheffler's proposal
to extensive criticism. Especially puzzling to Church was
Scheffler's willingness to admit that there is a philosophical
problem about the existence of physical objects while also insisting,
without argument, that there is a problem about the existence of
propositions and sentence types that is different in kind.



In sum, Church's argument for the existence of propositions is
as follows. (1) Actual thought or sentence tokens, as well as possible
sentences, are insufficient for semantics to be a true and humanly
understandable theory. Rather, (2) propositions are also needed.
Further, by Church's criterion of ontological commitment, (3) if
entities of kind \(K\) are entailed by a true theory, then there exist
entities of kind \(K\). So, (4) there exist propositions. Church
(1952, 1958a) chides Ayer and Ryle for not taking this last step, that
is for inadvertently committing themselves to propositions while
talking about propositional attitudes but denying their existence
while talking explicitly about propositions as theoretical
commitments.



Regarding the second premise, it remains to be shown that we need to
take the step from the notion of a *possible
thought*--which is abstracted from the notion of a possible
mind that is capable of error and so of thinking something
false--to the notion of an abstract proposition. Church
attributed the discovery of the latter notion to both Bolzano and
Frege (Church 1943a; 1956a,b). However, Church did not endorse
Bolzano's arguments so much as his conclusion. (For the
argument, see
 SS3.3 of the entry on Bolzano.)
 And as for Frege, Church simply reiterated his remarks about the
objectivity, mind and language independence, and publicity of
*Gedanke*, without telling us exactly why possible thoughts are
not also objective, mind-and-language-independent, abstract and
public. Perhaps the issue is that the existence of possible thoughts
depends on the existence of possible minds, whereas propositions, such
as *that two and two are four*, do not depend on the existence
of possible minds, since, intuitively, they would be true if there
were no minds at all. Arguably, then, the notion of an abstract
proposition must be postulated by and so is an ontological commitment
of a theory that can explain the foregoing intuition.