*Photo from Burge & Enderton 2019,
reproduced with permission from the editor.*

# Alonzo Church

*First published Thu Oct 21, 2021; substantive revision Thu Feb 24, 2022*

Alonzo Church (1903–1995) was a renowned mathematical logician,
philosophical logician, philosopher, teacher and editor. He was one of
the founders of the discipline of mathematical logic as it developed
after Cantor, Frege and Russell. He was also one of the principal
founders of the *Association for Symbolic Logic* and the
*Journal of Symbolic Logic*. The list of his students,
mathematical and philosophical, is striking as it contains the names
of renowned logicians and philosophers. In this article, we focus
primarily on Church’s philosophical contributions. (For an
account of his life and academic history see the Introduction to
*The Collected Works of Alonzo Church* (2019).) However, we
also discuss his mathematical results when it is desirable to do so in
order to pursue a philosophical issue. In Church’s case, the
distinction between philosopher and formal logician/mathematician is
not entirely correct, since *all* of his work (except for the
occasional paper on some purely mathematical subject) concerns logical
issues in one way or another.

Church brought both the general outlook and the specific distinctions
of formal logic to bear on philosophy in a distinctive way by applying
his “logistic method” to the philosophical topics he
discussed. Conversely, he also wove certain aspects of his philosophy
into the fabric of formal, mathematical logic as he presented it. The
result was a formidable combination of philosophical vision and
focused argumentation. For Church, the logistic method (or
formalization) was not only necessary to obtain additional
clarification beyond informal discussion and to make meta-mathematical
investigations possible; it was also the ideal method for dealing with
philosophical problems in epistemology, metaphysics and philosophy of
language. It was Church’s view that one who does not aspire to
this ideal falls short. However, he also recognized that formalization
is not always appropriate. He did not demand that the natural sciences
be formalized and even provided an informal philosophical discussion
of semantics in the introductory chapter of his *Introduction to
Mathematical Logic* (1956a). The theories and arguments discussed
in this article describe and illustrate Church’s logistic
method.

In the following, we often use the notational conventions that Church
adopted from *Principia Mathematica* (Whitehead & Russell
1910; hereafter PM). When we do so, these conventions are explained
and sometimes compared with modern notation.

- 1. Computability and Church’s Thesis
- 2. Philosophy of Logic
- 3. Applications of the Logistic Method
- 4. Paradox
- 5. Foundations of Mathematics
- 6. Metaphysics
- Bibliography
- Academic Tools
- Other Internet Resources
- Related Entries

- List of Supplements
- A. Church on Computability (for §1)
- B. Early Philosophy of Logic and Metaphysics (for §2)
- C. Applications of the Logistic Method (for §3)
- D. The λ-Calculus and Type Theory (for §§3, 4, 5)
- E. Philosophy of Language (for §§3, 4)
- F. Paradox and Comparison with Tarski (for §4)

## 1. Computability and Church’s Thesis

### 1.1 Church’s Seminal Paper

Church was the first to devise a formalism—the
λ-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 Gödel 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 Gödel (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 λ-definability) and he argued that each of these methods results in functions that are already recursive (and λ-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 λ-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, Gödel expressed a strong preference for Turing’s analysis and there are good reasons for Gödel’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 λ-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 λ-definability may serve as a precise counterpart of intuitive computability (Kleene 1981). Kleene also describes the difficulty of giving λ-definitions of certain basic number theoretic functions—particularly the predecessor function—given the particular way Church gives λ-expressions standing for integers (1981: 56; these λ-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 λ-definability and recursiveness (Kleene [1936] gives a more detailed proof). Gödel complained of exactly this:

He [Gödel] 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)

Gödel 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: §9). It seems that a counterpart of Turing’s compelling analysis has yet to be given for the case of λ-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 λ-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 Gödel 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 λ-definable and hence recursive. (B) is the striking fact that the various mathematically precise counterparts of computability—λ-definability, recursiveness, Turing computability and others of the period due to Gödel 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 λ-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 Gödel 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

- the behavior of the computor is completely determined by the symbols observed and the computor’s state of mind;
- that there is a finite bound on the number of symbols observed at any one time;
- that only a finite number of states of mind are involved at any one time (a condition that Gödel [1972] disputed); and
- 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 Gödel 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: §00). 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: §00)

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: §07)

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: §07)

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: §07)

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: §29 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: §07)

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 Gödel’s incompleteness theorems (see §5.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:

Sis empirically verifiable iffSlogically entailsA1,A2…,

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

Sisdirectlyverifiable iff eitherSis an observation sentence or elseS, perhaps in conjunction with other observation sentencesA,B,C,…, logically implies an observation sentence that is not implied byA,B,C….

In addition:

Sisindirectlyverifiable if and only ifS, perhaps in conjunction with other sentencesP,Q,R,… logically implies a directly verifiable sentenceDthat is not implied byP,Q,R,…. Furthermore, these sentencesP,Q,Rare 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
§3.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 Gödel (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: §04), 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: §04): 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 §6.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. Salmón 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.
§3.3
and
§6.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: §01). 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; Salmón 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 λ-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,
“Hesperus_{0}”—“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 Salmón (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 §4.4 and §5). 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:

- He gives an elegant formulation of RTT as a straightforward complication of STT. (See supplement D. We adopt the definitions and notations used there.)
- 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.
- 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. - 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\). - 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.
- 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”:

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

(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

which replaces
***,
when level indicators are supplied, defines an infinite list of het
predicates, “het^{2}”,
“het^{3}”, …, 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:

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:

- Assume for
*reductio*that \(K(p \hdot \neg Kp)\). - Then \(Kp \hdot K\neg Kp\), assuming \(K(q \hdot r)\) implies \(Kq \hdot Kr\), for arbitrary \(q\) and \(r\).
- \(\neg Kp\), assuming \(Kq\) implies \(q\), for arbitrary \(q\).
- Hence, \(Kp \hdot \neg Kp\) by logic.
- 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) λ-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 λ-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 λ-calculus—is, however, consistent in the sense that not all equations between λ 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 λ-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 Gödel (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 λ-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 λ 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
§3)
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
§5.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 Gödel’s Theorems and the Continuum Problem

Church was acutely conscious of the effect on the question of foundations of Gödel’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 λ-calculus escapes Gödel’s first incompleteness theorem, this is only in virtue of its lack of provability strength, and so:

The sense in which it escapes the Gödel 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
§2).
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
Gödel’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 Gödel 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 Salmón (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 Gödel, 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: §4)

Frege’s position, according to Church, is that “*there
are* two such things as truth and falsehood” (1956a:
§4). 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.
§5.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. §3.3 and §6.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
§3.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
§3.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.

## Bibliography

### Primary Sources

- [BE] Burge, Tyler and Herbert Enderton (eds), 2019,
*The Collected Works of Alonzo Church*, Cambridge, MA: MIT Press.

Church’s papers are located at the Princeton University Library

- 1927, “Alternatives to Zermelo’s Assumption”,
*Transactions of the American Mathematical Society*, 29(1): 178–208. Reprinted in BE: 19–42. doi:10.2307/1989285 - 1928a, “On the Law of Excluded Middle”,
*Bulletin of the American Mathematical Society*, 34(1): 75–79. Reprinted in BE: 43–45. doi:10.1090/S0002-9904-1928-04516-0 - 1928b, “Review of
*Principia Mathematica*, by Alfred North Whitehead and Bertrand Russell”,*Bulletin of the American Mathematical Society*, 34(2): 237–241. Reprinted in BE: 46–48. doi:10.1090/S0002-9904-1928-04525-1 - 1932, “A Set of Postulates for the Foundation of
Logic”,
*The Annals of Mathematics*, 33(2): 346–366. Reprinted in BE: 51–67. doi:10.2307/1968337 - 1933, “A Set of Postulates For the Foundation of Logic
(2)”,
*The Annals of Mathematics*, 34(4): 839–864. Reprinted in BE: 68–87. doi:10.2307/1968702 - 1934, “The Richard Paradox”,
*The American Mathematical Monthly*, 41(6): 356–361. Reprinted in BE: 94–98. doi:10.1080/00029890.1934.11987569 - 1935a, “A Proof of Freedom from Contradiction”,
*Proceedings of the National Academy of Sciences*, 21(5): 275–281. Reprinted in BE: 99–104. doi:10.1073/pnas.21.5.275 - 1935b, “Review of
*A System of Logistic*, by W. V. O. Quine”,*Bulletin of the American Mathematical Society*, 41(9): 598–604. Reprinted in BE: 105–109. doi:10.1090/S0002-9904-1935-06146-4 - 1935c, “An Unsolvable Problem of Elementary Number Theory:
Preliminary Report”,
*Bulletin of the AMS*, 41(5): 332–333. Reprinted in BE: 110. doi:10.1090/S0002-9904-1935-06097-5 - 1935d, “Letter to Kleene”. Printed in BE: 1000. November 15, 1935.
- 1935e, “Letter to Bernays”. Printed in BE: 995–997. July 15, 1935.
- 1936a, “An Unsolvable Problem of Elementary Number
Theory”,
*American Journal of Mathematics*, 58(2): 345–363. Reprinted in BE: 111–125. doi:10.2307/2371045 - 1936b, “A Note on the Entscheidungsproblem”,
*Journal of Symbolic Logic*, 1(1): 40–41. Reprinted in BE: 126–129. doi:10.2307/2269326 - 1937a, “Review of ‘On Computable Numbers, with an
Application to the Entscheidungsproblem’, by A. M.
Turing”,
*Journal of Symbolic Logic*, 2(1): 42–43. Reprinted in BE: 934. doi:10.1017/S002248120003958X - 1937b, “Review of ‘Finite Combinatory
Processes—Formulation 1’, by Emil L. Post”,
*Journal of Symbolic Logic*, 2(1): 43. doi:10.1017/S0022481200039591 - 1937c, “Review of ‘The Logic of Quantum
Mechanics’, by Garrett Birkhoff and John von Neumann”,
*Journal of Symbolic Logic*, 2(1): 44–45. doi:10.1017/S0022481200039633 - 1938, “The Constructive Second Number Class”,
*Bulletin of the American Mathematical Society*, 44: 224–232. Reprinted in BE: 148–154. - 1939a, “Review of
*Foundations of Logic and Mathematics*, by Rudolf Carnap”,*Bulletin of the American Mathematical Society*, 45(11): 821–822. Reprinted in BE: 161–162. doi:10.1090/S0002-9904-1939-07085-7 - 1939b, “The Present Situation in the Foundations of
Mathematics”, in
*Philosophie mathématique*, by F. Gonseth, (Actualités scientifiques et industrielles 837), Paris: Hermann et Cie, pp. 67–72. Reprinted in BE: 155–160. - 1939c, “Review of ‘A Logistical Approach to the
Ontological Problem’., by W. V. O. Quine”,
*Journal of Symbolic Logic*, 4(4): 170. Reprinted in BE: 937–938. doi:10.2307/2268739 - 1940, “A Formulation of the Simple Theory of Types”,
*Journal of Symbolic Logic*, 5(2): 56–68. Reprinted in BE: 171–183. doi:10.2307/2266170 - 1941,
*The Calculi of Lambda Conversion*(Annals of Mathematics Studies 6), Princeton, NJ: Princeton University Press. Reprinted in BE: 201–255. - 1943a, “Carnap’s
*Introduction to Semantics*(1942)”,*The Philosophical Review*, 52(3): 298–304. Reprinted in BE: 259–264. doi:10.2307/2180923 - 1943b/1968, “Review of ‘Notes on Existence and
Necessity’, by W. V. O. Quine”,
*Journal of Symbolic Logic*, 8(2): 45–47. Postscript, 1968, originally published in 1973,*Semántica filosófica*, Thomas Moro Simpson (ed.). Reprinted with postscript in BE: 942–948. doi:10.2307/2267994 - 1943c, “Correspondence with W. V. Quine”. Printed in BE: 1074–1090.
- 1944a, “Review of
*Formalization of Logic*, by Rudolf Carnap”,*The Philosophical Review*, 53(5): 493. Reprinted in BE: 265–269. doi:10.2307/2181359 - 1944b,
*Introduction to Mathematical Logic, Part I*, (Annals of Mathematics Studies, 13), Princeton, NJ: Princeton University Press. Revised and enlarged in Church 1956a. - 1945a, “Review of ‘Logic without Ontology’, by
Ernest Nagel”,
*Journal of Symbolic Logic*, 10(1): 16–18; reprinted in BE: 951–953. doi:10.2307/2267202 - 1945b, “Referee Reports on Fitch’s ‘A Definition of Value’ ”, in J. Salerno (ed.) 2009, 13–20.
- 1946a, “Review of ‘A Note on the Paradox of
Analysis’, by Morton G. White; ‘The Paradox of Analysis
Again: A Reply’, by Max Black; ‘Analysis and Identity: A
Rejoinder’, by Morton G. White; ‘How Can Analysis Be
Informative?’ by Max Black”,
*Journal of Symbolic Logic*, 11(4): 132–133. Reprinted in BE: 956–957. doi:10.2307/2268327 - 1946b, “A Formulation of the Logic of Sense and
Denotation”, Abstract from the Eighth Meeting of the Association
for Symbolic Logic,
*Journal of Symbolic Logic*, 11(1): 31. Reprinted in BE: 270–272. doi:10.2307/2269172 - 1949a, “Review of
*Language, Truth and Logic*, by Alfred Jules Ayer”,*Journal of Symbolic Logic*, 14(1): 52–53. Reprinted in BE: 963–964. doi:10.2307/2268980 - 1949b, “Grelling’s Antinomy for the System of
*A Formulation of the Simple Theory of Types*”, previously unpublished manuscript. Printed in BE: 276–278. - 1950a, “On Carnap’s Analysis of Statements of
Assertion and Belief”,
*Analysis*, 10(5): 97–99. Reprinted in BE: 279–281. doi:10.1093/analys/10.5.97 - 1950b, “Letter to Carnap”. Printed in BE: 1063–1064. July 11, 1950.
- 1950c, “Review of ‘Modern Logic and the Synthetic A
Priori’, by Irving M. Copi”,
*Journal of Symbolic Logic*, 15(3): 221. doi:10.2307/2266825 - 1951a, “A Formulation of the Logic of Sense and
Denotation”, in
*Structure, Method and Meaning: Essays in Honor of Henry M. Sheffer*, Paul Henley, H. M. Kallen, and S. K. Langer (eds), New York: The Liberal Arts Press, pp. 3–24. Reprinted in BE: 292–306. - 1951b, “The Need for Abstract Entities in Semantic
Analysis”,
*Proceedings of the American Academy of Arts and Sciences*, 80(1): 100–112. Reprinted as “Intensional Semantics” in BE: 282–291. doi:10.2307/20023640 - 1952, “Review of ‘Introduction’ by A. G. N.
Flew; ‘Systematically Misleading Expressions’ by Gilbert
Ryle; and ‘Verifiability’ by Friedrich Waismann in
*Essays on Logic and Language*”,*Journal of Symbolic Logic*, 17(4): 284–285. Reprinted in BE: 966–968. doi:10.2307/2266640 - 1954, “Intensional Isomorphism and Identity of
Belief”,
*Philosophical Studies*, 5(5): 65–73. Reprinted in BE: 349–355. doi:10.1007/BF02221771 - 1956a,
*Introduction to Mathematical Logic, Volume I,*, Princeton, NJ: Princeton University Press. Revised and enlarged version of 1944b; the second volume was never published. Reprinted in BE: 372–425. - 1956b, “Propositions and Sentences”, in
*The Problem of Universals: A Symposium*, I.M. Bochenski, Alonzo Church, and Nelson Goodman, Notre Dame, IN: University of Notre Dame Press pp. 1–12. Reprinted in BE: 356–361. - 1956–72, Articles from
*Encyclopedia Britannica*. Reprinted in BE: 692–746. - 1958a, “Ontological Commitment”,
*The Journal of Philosophy*, 55(23): 1008–1014. Reprinted in BE: 356–361. doi:10.2307/2021909 - 1958b, “Misogyny and Ontological Commitment”. Printed in BE: 443–447.
- 1959, Articles from
*the Dictionary of Philosophy*, D. D. Runes (ed.), New York: Philosophical Library. Reprinted in BE: 448–530. - 1960, “Application of Recursive Arithmetic to the Problem of
Circuit Synthesis”, in
*Summaries of Talks Presented at the Summer Institute for Symbolic Logic, CornellUniversity*, 1957, 2nd ed., Princeton, NJ: Communications Research Division, Institute for Defense Analyses, pp. 3–50. - 1962a, “Logic, Arithmetic, and Automata”,
*Proceedings of the International Congress of Mathematicians, 1962*, volume 1, pp. 23–35. - 1962b, “Mathematics and Logic”,
*Logic, Methodology and Philosophy of Science: Proceedings of the 1960 International Congress*, Ernest Nagel, Patrick Suppes, and Alfred Tarski (eds), Stanford, CA: Stanford University Press, pp. 181–186. Reprinted in BE: 608–612. - 1965, “Review of ‘Existential Import Revisited’
by Karel Lambert”,
*Journal of Symbolic Logic*, 30(1): 103–104. - 1966, “Paul J. Cohen and the Continuum Problem”,
*Proceedings of the International Congress of Mathematicians 1966*, volume 1, pp. 15–20. Reprinted in BE: 675–679. - 1968/1972/1976, “Partial Outline of
*Introduction to Mathematical Logic*Chapter VIII”, unpublished manuscripts, printed BE: 889–927. - 1973a, “On Scheffler’s Approach to Indirect
Quotation”, in
*Sobre el análisis del discurso indirecto propuesto por Scheffler, Semántica filosófica: Problemas y discusiones*, Thomas Moro Simpson (ed.), Siglo XXI Argentina Editores S.A., Buenos Aires, pp. 363–369. Reprint in BE: 747–750. - 1973b, “Outline of a Revised Formulation of the Logic of
Sense and Denotation (Part I)”,
*Noûs*, 7(1): 24–33. Reprinted in BE: 751–772. doi:10.2307/2216181 - 1974a, “Outline of a Revised Formulation of the Logic of
Sense and Denotation (Part II)”,
*Noûs*, 8(2): 135–156. Reprinted in BE: 751–772. doi:10.2307/2214782 - 1974b, “Russellian Simple Type Theory”,
*Proceedings and Addresses of the American Philosophical Association*, 47: 21–33. Reprinted in BE: 773–783. doi:10.2307/3129899 - 1974c, “Set Theory with a Universal Set”,
*Proceedings of the Tarski Symposium in American Mathematical Society: Proceedings of Symposia in Pure Mathematics*, volume 25: 297–308. Reprinted in BE: 784–793. doi:10.1090/pspum/025/0369069 - 1975, “Review of ‘Realism as a Philosophy of
Mathematics’ by Stephen F. Barker in
*Foundations of mathematics, Symposium papers commemorating the sixtieth birthday of Kurt Godel*”,*Journal of Symbolic Logic*, 40: 593. Reprinted in BE: 983-984. - 1976, “Comparison of Russell’s Resolution of the
Semantical Antinomies with That of Tarski”,
*Journal of Symbolic Logic*, 41(4): 747–760. Reprinted in BE: 794–806. doi:10.2307/2272393 - 1979, “How Far Can Frege’s Intensional Logic be Reproduced Within Russell’s Theory of Descriptions”, previously unpublished abstract of a lecture. Printed in BE: 807–808.
- 1982, “A Remark Concerning Quine’s Paradox About
Modality”,
*Una Observacion respecto a la Paradoja de Quine sobre la Modalidad*, special issue of*Análisis Filosófico*, 2(1/2): 25–32. Reprinted in BE: 809–814. - 1984, “Russell’s Theory of Identity of
Propositions”,
*Philosophia Naturalis*, 21(2/4): 513–522. Reprinted in BE: 815–821. - 1989, “Intensionality and the Paradox of the Name Relation”, in Almog, Perry, and Wettstein 1989: 151–165. Reprinted in BE: 834–844.
- 1993, “A Revised Formulation of the Logic of Sense and
Denotation. Alternative (1)”,
*Noûs*, 27(2): 141–157. Reprinted in BE: 845–859. doi:10.2307/2215752 - 1995a, “Grelling’s Antinomy”, printed BE: 929–931.
- 1995b, “Corrections and Minor Comments Affecting
Heyting’s
*Intuitionism,*Edition of 1976”. Printed in BE: 932–933. - 1995c, “A Theory of the Meaning of Names”, in
*The Heritage of Kazimierz Ajdukiewicz*, Vito Sinisi and Jan Woleński (eds), Amsterdam: Rodopi, 69–74. Reprinted in BE: 859–863. - n.d., “Resolution of Berry’s Antinomy by Ramified Type Theory”, printed in BE: 928.
- Church, Alonzo and J. B. Rosser, 1936, “Some Properties of
Conversion”,
*Transactions of the American Mathematical Society*, 39(3): 472–482. Reprinted in BE: 130–138. doi:10.1090/S0002-9947-1936-1501858-0

### Secondary Sources

- Ajdukiewicz, Kazimierz, 1960, “A Method of Eliminating
Intensional Sentences and Sentential Formulae”:, in
*Atti Del XII Congresso Internazionale Di Filosofia*, Sansoni Editore, 5:17–24. doi:10.5840/wcp1219605242 - –––, 1967, “Intensional
Expressions”,
*Studia Logica*, 20: 63–86. doi:10.1007/BF02340029 - Almog, Joseph and Paolo Leonardi (eds.), 2009,
*The Philosophy of David Kaplan*, Oxford: Oxford University Press. doi:10.1093/acprof:oso/9780195367881.001.0001 - Almog, Joseph, John Perry, and Howard Wettstein (eds), 1989,
*Themes from Kaplan*, New York: Oxford University Press. - Anderson, C. Anthony, 1980, “Some New Axioms for the Logic
of Sense and Denotation: Alternative (0)”,
*Noûs*, 14(2): 217–234. doi:10.2307/2214862 - –––, 1983, “The Paradox of the
Knower”,
*The Journal of Philosophy*, 80(6): 338–355. doi:10.2307/2026335 - –––, 1986, “Some Difficulties Concerning
Russellian Intensional Logic”,
*Noûs*, 20(1): 35–43. doi:10.2307/2215278 - –––, 1987, “Semantical Antinomies in the
Logic of Sense and Denotation”,
*Notre Dame Journal of Formal Logic*, 28(1): 99–114. doi:10.1305/ndjfl/1093636849 - –––, 1998, “Alonzo Church’s
Contributions to Philosophy and Intensional Logic”,
*Bulletin of Symbolic Logic*, 4(2): 129–171. doi:10.2307/421020 - –––, 2001, “Alternative (1*): A Criterion of Identity for Intensional Entities”, in Anderson and Zelëny 2001: 395–427. doi:10.1007/978-94-010-0526-5_19
- Anderson, C. Anthony and Michael Zelëny (eds.), 2001,
*Logic, Meaning and Computation: Essays in Memory of Alonzo Church*, Dordrecht: Kluwer. doi:10.1007/978-94-010-0526-5 - Anderson, Alan Ross, Ruth Barcan Marcus, and R. M. Martin (eds.),
1975,
*The Logical Enterprise*, New Haven, CT: Yale University Press. - Andrews, P.B., 1986,
*Introduction to Mathematical Logic and Type Theory: To Truth Through Proof*, Orlando, FL: Academic Press. - Ayer, A.J., 1936 [1952],
*Language, Truth and Logic*, London: V. Gollancz. Reprinted New York: Dover Publications, 1952. - Azzouni, Jody, 2004,
*Deflating Existential Consequence: A Case for Nominalism*, New York: Oxford University Press. doi:10.1093/0195159888.001.0001 - –––, 2010,
*Talking About Nothing: Numbers, Hallucinations and Fictions*, New York: Oxford University Press. doi:10.1093/acprof:oso/9780199738946.001.0001 - Bealer, George, 1982,
*Quality and Concept*, Oxford: Clarendon Press. doi:10.1093/acprof:oso/9780198244288.001.0001 - Bernays, Paul, 1961, “Zur Rolle der Sprache in
erkenntnistheoretischer Hinsicht”,
*Synthese*, 13(3): 185–200. Translated as “On the Role of Language from An Epistemological Point of View” by Dirk Schlimm with revisions by Steve Awodey, Bernays Project, Text No. 25, no date. doi:10.1007/BF00489883 [Translation of Bernays 1961 available online] - Boolos, George S., John P. Burgess, and Richard C. Jeffrey, 2007,
*Computability and Logic*, fifth edition, Cambridge: Cambridge University Press. First edition by George Boolos and Richard Jeffrey, 1974. doi:10.1017/CBO9780511804076 - Burge, Tyler, 1978, “Belief and Synonymy”,
*The Journal of Philosophy*, 75(3): 119–138. doi:10.2307/2025424 - –––, 2005a,
*Truth, Thought, Reason: Essays on Frege*, Oxford: Clarendon Press. doi:10.1093/acprof:oso/9780199278534.001.0001 - –––, 2005b, “Introduction”, in Burge 2005a: 1–68.
- –––, 2005c, “Postscript to
*Frege and the Hierarchy*”, in Burge 2005a: 167–210. - –––, 2007, “Postscript to ‘Belief
*De Re*’”, in his*Foundations of Mind*, Oxford: Clarendon Press, 65–81. - –––, 2009, “Five Theses on De Re States and Attitudes”, in Almog and Leonardi 2009: 246–316. doi:10.1093/acprof:oso/9780195367881.003.0015
- –––, 2019, “Alonzo Church: Life and Work”, in BE: xx–xxiv.
- Burgess, John P., 2001, “Nominalist Paraphrase and Ontological Commitment”, in Anderson and Zelëny 2001: 429–443. doi:10.1007/978-94-010-0526-5_20
- Button, Tim and Sean Walsh, 2018,
*Philosophy and Model Theory*, Oxford: Oxford University Press. doi:10.1093/oso/9780198790396.001.0001 - Carnap, Rudolf, 1939,
*Foundations of Logic and Mathematics*, (International Encyclopedia of Unified Science, vol. 1, no. 3), Chicago, IL: University of Chicago Press. - –––, 1942,
*Introduction to Semantics*, Cambridge, MA: Harvard University Press. - –––, 1947,
*Meaning and Necessity: A Study in Semantics and Modal Logic*, Chicago, IL: University of Chicago Press. - –––, 1964, “Replies and Systematic
Expositions”, in
*The Philosophy of Rudolph Carnap*, Paul Arthur Schilpp (ed.), Illinois: La Salle. - Carroll, Lewis, 1895, “What the Tortoise Said to
Achilles”,
*Mind*, 4(14): 278–280. doi:10.1093/mind/IV.14.278 - Copi, Irving, 1971,
*The Theory of Logical Types*, London: Routledge and Kegan Paul. - Craig, William, 1953, “On Axiomatizability within a
System”,
*Journal of Symbolic Logic*, 18(1): 30–32. doi:10.2307/2266324 - Davidson, Donald, 1965, “Theories of Meaning and Learnable
Languages”, in
*Proceedings of the International Congress for Logic, Methodology, and Philosophy of Science*, Yehoshua Bar-Hillel (ed.), Dordrecht: North-Holland, 3–17. - Davis, Martin, 1958,
*Computability and Unsolvability*, New York: McGraw Hill. - ––– (ed.), 1965,
*The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions*, Hewlett, NY: Raven Press. - –––, 1982, “Why Gödel Didn’t
Have Church’s Thesis”,
*Information and Control*, 54(1–2): 3–24. doi:10.1016/S0019-9958(82)91226-8 - Deutsch, Harry, 2008, “Review of
*The Nature and Structure of Content*, by Jeffrey C. King”, Notre Dame Philosophical Reviews, 2008.05.24. [Deutsch 2008 available online] - –––, 2014, “Resolution of Some Paradoxes
of Propositions”,
*Analysis*, 74(1): 26–34. doi:10.1093/analys/ant089 - –––, 2019, “Propositional Paradox”,
in
*The Routledge Handbook of Propositions*, Chris Tillman (ed.), Taylor and Francis. - Farmer, William M., 2008, “The Seven Virtues of Simple Type
Theory”,
*Journal of Applied Logic*, 6(3): 267–286. doi:10.1016/j.jal.2007.11.001 - Feferman, Sol, 1995, “Ordinal logic”,
*The Cambridge Dictionary of Philosophy*, Cambridge: Cambridge University Press, 550–551. - Fitch, Frederick, 1963, “A Logical Analysis of Some Value
Concepts”,
*Journal of Symbolic Logic*, 28(2): 135–142; reprinted in J. Salerno (ed.) 2009, 21–28. - Fitting, Melvin and Richard L. Mendelsohn, 1998,
*First-Order Modal Logic*, Dordrecht: Kluwer. doi:10.1007/978-94-011-5292-1 - Frege, Gottlob, 1884 [1953],
*Die Grundlagen der Arithmetik: eine logisch mathematische Untersuchung über den Begriff der Zahl*, Breslau: W. Koebner. Translated as*The Foundations of Arithmetic.*, J. L. Austin (trans.), New York: Harper, 1950; second edition, 1953. - –––, 1891, “Funktion und Begriff”, (Vortrag, gehalten in der Sitzung vom 9. Januar 1891 der Jenaischen Gesellschaft für Medizin und Naturwissenschaft), Jena: Hermann Pohle. Translated as “On Function and Concept” in Frege 1997: 130–148.
- –––, 1892a, “Über Sinn und
Bedeutung”,
*Zeitschrift für Philosophie und philosophische Kritik*, 100: 25–50. Translated as “On Sense and Reference” in Frege 1997: 151–171. - –––, 1892b, “Über Begriff und
Gegenstand”,
*Vierteljahrsschrift für wissenschaftliche Philosophie*, 16: 192–205. Translated as “On Concept and Object” in Frege 1997: 181–193. - –––, 1997,
*The Frege Reader*, Michael Beaney (ed.), Oxford: Blackwell Publishers. - Gaifman, Haim, 2006, “Naming and Diagonalization, from
Cantor to Gödel to Kleene”,
*Logic Journal of IGPL*, 14(5): 709–728. doi:10.1093/jigpal/jzl006 - Gandy, Robin, 1980, “Church’s Thesis and Principles
for Mechanisms”, in
*The Kleene Symposium*, Jon Barwise, H. Jerome Keisler, and Kenneth Kunen (eds.), (Studies in Logic and the Foundations of Mathematics 101), Amsterdam: North-Holland, 123–148. doi:10.1016/S0049-237X(08)71257-6 - –––, 1992, “The Confluence of Ideas in
1936”, in
*The Universal Turing Machine: A Half-Century Survey*, Rolf Herken (ed.), Oxford: Oxford University Press, 55–111. - Gödel, Kurt, 1931 [1986], “Über formal
unentscheidbare Sätze der
*Principia mathematica*und verwandter Systeme I (1931)”,*Monatshefte für Mathematik und Physik*, 38: 173–198. Reprinted and translated as “On Formally Undecidable Propositions of*Principia Mathematica*and Related Systems I” in Gödel CW I: 144–195. doi:10.1007/BF01700692 (1931) - –––, 1944 [1951], “Russell’s
Mathematical Logic”, in
*The Philosophy of Bertrand Russell*(Library of Living Philosophers), Paul Arthur Schilpp (ed.), New York: Tudor. Third edition, 1951, pp. 123–153. - –––, 1972, “Remark 3 (1972a): A Philosophical Error in Turing’s Work”. Printed in Gödel CW II: 306.
- –––, [CW I] 1986,
*Collected Works, Volume I: Publications 1929–1936*, Sol Feferman (editor-in-chief), New York: Oxford University Press. - –––, [CW II] 1989,
*Collected Works, Volume II: Publications 1938–1974*, Sol Feferman (editor-in-chief), New York: Oxford University Press. - Goodman, Jeremy, 2017, “Reality Is Not Structured”,
*Analysis*, 77(1): 43–53. doi:10.1093/analys/anw002 - Heim, Irene and Angelika Kratzer, 1998,
*Semantics in Generative Grammar*, (Blackwell Textbooks in Linguistics 13), Malden, MA: Blackwell. - Henkin, Leon, 1950, “Completeness in the Theory of
Types”,
*Journal of Symbolic Logic*, 15(2): 81–91. doi:10.2307/2266967 - Hilbert, David, 1926 [1967], “Über das
Unendliche”,
*Mathematische Annalen*, 95: 161–190; presented to the Westphalian Mathematical Society 4 June 1925. Translated as “On the Infinite”, Stefan Bauer-Mengelberg (trans.), in*From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931*, Jean van Heijenoort (ed.), Cambridge, MA: Harvard University Press, 1967, pp. 367–392. doi:10.1007/BF01206605 (German) - Hilbert, David and W. Ackerman, 1928 [1950],
*Grundzuge der theoretischen Logik*, Berlin: J. Springer. Translated as*Principles of Mathematical Logic*, Lewis M. Hammond, George G. Leckie, and F. Steinhardt (trans), New York: Chelsea Publishing Company. - Hilbert, David and Bernays, Paul, 1934 [1968],
*Grundlagen der Mathematik I*,*Die Grundlehren der mathematischen Wissenschaften*, 40, 2nd edition, Berlin: J. Springer. - Hindley, J. Roger and Jonathan P. Seldin, 2008,
*Lambda-Calculus and Combinators: An Introduction*, second edition, Cambridge: Cambridge University Press. doi:10.1017/CBO9780511809835 - Hudak, Paul, 1989, “Conception, Evolution, and Application
of Functional Programming Languages”,
*ACM Computing Surveys*, 21(3): 359–411. doi:10.1145/72551.72554 - Kaplan, David, 1964,
*Foundations of Intensional Logic*, Ph.D. Thesis, University of California, Los Angeles. - –––, 1975a, “Significance and
Analyticity”, in
*Rudolf Carnap, Logical Empiricist*, Jaakko Hintikka (ed.), Boston: Dordecht Reidel, pp. 87–94. - –––, 1975b, “How to Russell a
Frege-Church”,
*The Journal of Philosophy*, 72(19): 716–729. doi:10.2307/2024635 - –––, 1989, “Demonstratives”, in Almog, Perry, and Wettstein 1989: 481–564.
- –––, 2005, “Reading ‘On
Denoting’ on Its Centenary”,
*Mind*, 114(456): 933–1003. doi:10.1093/mind/fzi933 - Kemeny, John George, 1949,
*Type-theory vs. Set-theory*, Ph.D. Thesis, Princeton University. - Kleene, Stephen C., 1936, “General Recursive Functions of
Natural Numbers”,
*Mathematische Annalen*, 112: 727–742. doi:10.1007/BF01565439 - –––, 1938, “On Notations for Ordinal
Numbers”,
*The Journal of Symbolic Logic*, 3(4): 150–155. - –––, 1952,
*Introduction to Metamathematics*, New York: Van Nostrand. - –––, 1981, “Origins of Recursive Function
Theory”,
*Annals of the History of Computing*, 3(1): 52–67. doi:10.1109/MAHC.1981.10004 - Kleene, Stephen C. and J. B. Rosser, 1935, “The
Inconsistency of Certain Formal Logics”,
*The Annals of Mathematics*, 36(3): 630–636. doi:10.2307/1968646 - Klement, Kevin C., 2002,
*Frege and the Logic of Sense and Reference*, New York: Routledge. - Kreisel, Georg, 1987, “Church’s Thesis and the Ideal
of Informal Rigour”,
*Notre Dame Journal of Formal Logic*, 28(4): 499–519. doi:10.1305/ndjfl/1093637646 - Kripke, Saul A., 1979, “A Puzzle about Belief”, in Margalit 1979: 239–283. doi:10.1007/978-1-4020-4104-4_20
- –––, 2005, “Russell’s Notion of
Scope*”,
*Mind*, 114(456): 1005–1037. doi:10.1093/mind/fzi1005 - –––, 2008 [2011a], “Frege’s Theory
of Sense and Reference: Some Exegetical Notes”,
*Theoria*, 74(3): 181–218. Reprinted in Kripke 2011c: ch. 9, pp. 254–291. doi:10.1111/j.1755-2567.2008.00018.x - –––, 2011b, “A Puzzle about Time and Thought”, in Kripke 2011c: ch. 13, pp. 273–380.
- –––, 2011c,
*Philosophical Troubles: Collected Papers, Volume 1*, Oxford: Oxford University Press. doi:10.1093/acprof:oso/9780199730155.001.0001 - –––, 2013, “The Church-Turing
‘Thesis’ as a Special Corollary of Gödel’s
Completeness Theorem”, in
*Computability: Turing, Gödel, Church, and Beyond*, Jack Copeland, Carl Posy, and Oron Shagrir (eds), Cambridge, MA: MIT Press, pp. 77–104. - –––, 2014, “The Road to Gödel”,
in
*Naming, Necessity, and More: Explorations in the Philosophical Work of Saul Kripke*, Jonathan Berg (ed.), London: Palgrave Macmillan UK, 223–241. doi:10.1057/9781137400932_11 - Linsky, Bernard, 2009, “Logical Types in Some Arguments about Knowability and Belief”, in J. Salerno (ed.) 2009, 263–282.
- Margalit, Avishai (ed.), 1979,
*Meaning and Use: Papers Presented at the Second Jerusalem Philosophical Encounter April 1976*, (Synthese Language Library 3), Dordrecht: Springer Netherlands. doi:10.1007/978-1-4020-4104-4 - Martin, Robert L., 1984,
*Recent Essays on Truth and the Liar Paradox*, Oxford: Clarendon Press. - Mates, Benson, 1950, “Synonymity”, in
*University of California Publications in Philosophy*, volume 25, Berkeley, CA: University of California Press, pp. 201–266. - Mendelson, Elliott, 1990, “Second Thoughts about
Church’s Thesis and Mathematical Proofs”,
*The Journal of Philosophy*, 87(5): 225–233. doi:10.2307/2026831 - Montague, Richard, 1962, “Syntactical Treatments of
Modality, with Corollaries on Reflexion Principles and Finite
Axiomatizability”, in
*Proceedings of a Colloquium on Modal and Many-valued Logics, Helsinki, 23–26 August, 1962*,*Acta philosophica Fennica*, 16: 153–167. - –––, 1969, “On the Nature of Certain
Philosophical Entities”:,
*The Monist*, 53(2): 159–194. doi:10.5840/monist19695327 - –––, 1970a, “Universal Grammar”,
*Theoria*, 36: 373-398. - –––, 1970, “Pragmatics and Intensional
Logic”,
*Synthese*, 22(1–2): 68–94. doi:10.1007/BF00413599 - Myhill, John R., 1953, “Symposium: On the Ontological
Significance of the Löwenheim-Skolem Theorem II”, in
*Academic Freedom, Logic, and Religion*, Morton White (ed.), Philadelphia, PA: University of Pennsylvania Press, 57–70. doi:10.9783/9781512808520-002 - –––, 1958, “Problems Arising in the
Formalization of Intensional Logic”,
*Logique et Analyse*, new series 1(2): 74–83. - –––, 1975, “Levels of Implication”, in Anderson et al. 1975: 1979–185.
- –––, 1979, “A Refutation of An Unjustified
Attack on the Axiom of Reducibility”,
*Bertrand Russell Memorial Volume*, George W. Roberts (ed.), New York: Humanities Press. pp. 81–90. - Padró, Romina, 2015,
*What the Tortoise Said to Kripke: the Adoption Problem and the Epistemology of Logic*, Ph.D. Thesis, City University of New York. - Parsons, Charles, 1982, “Intensional Logic in Extensional
Language”,
*Journal of Symbolic Logic*, 47(2): 289–328. doi:10.2307/2273143 - –––, 1987, “Developing Arithmetic in Set
Theory without Infinity: Some Historical Remarks”,
*History and Philosophy of Logic*, 8(2): 201–213. doi:10.1080/01445348708837116 - –––, 2007,
*Mathematical Thought and Its Objects*, Cambridge: Cambridge University Press. doi:10.1017/CBO9780511498534 - Parsons, Terence, 1986, “Why Frege Should Not Have Said
‘The Concept
*Horse*Is Not a Concept’”,*History of Philosophy Quarterly*, 3(4): 449–465. - –––, 2001, “The Logic of Sense and Denotation: Extensions and Applications”, in Anderson and Zelëny 2001: 507–543. doi:10.1007/978-94-010-0526-5_25
- Partee, Barbara H., Alice ter Meulen, and Robert E. Wall, 1990,
*Mathematical Methods in Linguistics*, (Studies in Linguistics and Philosophy 30), Dordrecht: Kluwer. doi:10.1007/978-94-009-2213-6 - Peacocke, Christopher, 2008,
*Truly Understood*, Oxford: Oxford University Press. doi:10.1093/acprof:oso/9780199239443.001.0001 - Plotkin, Gordon D., 1993, “Set-Theoretical and Other
Elementary Models of the λ-Calculus”,
*Theoretical Computer Science*, 121(1–2): 351–409. doi:10.1016/0304-3975(93)90094-A - Poincaré, Jules H., 1906, “Mathematcs and Logic
III”, translated by Halsted, G. & Ewald, W. In Ewald (ed.),
1996,
*From Kant to Hilbert: A Sourcebook in the Foundations of Mathematics*(2 volumes), Oxford: Clarendon Press. - Post, Emil L., 1936, “Finite Combinatory
Processes—Formulation”,
*Journal of Symbolic Logic*, 1(3): 103–105. doi:10.2307/2269031 - Putnam, Hilary, 1954, “Synonymity, and the Analysis of
Belief Sentences”,
*Analysis*, 14(5): 114–122. doi:10.1093/analys/14.5.114 - Quine, Willard V., 1939, ‘A Logistical Approach to the
Ontological Problem’,
*Journal of Symbolic Logic*, 4(4): 170. - –––, 1943, “Notes on Existence and
Necessity”,
*The Journal of Philosophy*, 40(5): 113–127. doi:10.2307/2017458 - Rogers, Hartley, 1967,
*Theory of Recursive Functions and Effective Computability*, New York: McGraw-Hill. - Rosser, Barkley, 1939, “An Informal Exposition of Proofs of
Gödel’s Theorems and Church’s Theorem”,
*Journal of Symbolic Logic*, 4(2): 53–60. doi:10.2307/2269059 - Russell, Betrand, 1903,
*The Principles of Mathematics*, Cambridge: Cambridge University Press. - –––, 1905, “On Denoting”,
*Mind*, 14(4): 479–493. doi:10.1093/mind/XIV.4.479 - –––, 1908, “Mathematical Logic as Based on
the Theory of Types”,
*American Journal of Mathematics*, Jul., 30(3): 222-262. - Salerno, Joe (ed.), 2009,
*New Essays on the Knowability Paradox*, Oxford: Oxford University Press. - Salmón, Nathan, 1986, “Reflexivity”,
*Notre Dame Journal of Formal Logic*, 27(3): 401–429. doi:10.1305/ndjfl/1093636683 - –––, 1993, “A Problem in the Frege-Church
Theory of Sense and Denotation”,
*Noûs*, 27(2): 158–166. doi:10.2307/2215753 - –––, 2001, “The Very Possibility of Language”, in Anderson and Zelëny 2001: 573–595. doi:10.1007/978-94-010-0526-5_27
- –––, 2006, “A Theory of Bondage”,
*Philosophical Review*, 115(4): 415–448. doi:10.1215/00318108-2006-009 - –––, 2010, “Lambda in Sentences with
Designators: An Ode to Complex Predication”,
*The Journal of Philosophy*, 107(9): 445–468. doi:10.5840/jphil2010107930 - –––, 2020, “On What Exists”, in
*Quine, Structure, and Ontology*, Frederique Janssen-Lauret (ed.), Oxford: Oxford University Press, 200–229. doi:10.1093/oso/9780198864288.003.0010 - Scott, Dana, and Strachey, Christopher, 1971, “Toward a
Mathematical Semantics for Computer Languages”,
*Proceedings of the Symposium on Computers and Automata, Microwave Research Institute Symposia Series*, 21, Polytechnic Institute of Brooklyn. - Shapiro, Stewart, 1991,
*Foundations without Foundationalism: The Case for Second-Order Logic*, Oxford: Clarendon Press. - –––, 2001, “The ‘Triumph’ of First-Order Languages”, in Anderson and Zelëny 2001: 219–259. doi:10.1007/978-94-010-0526-5_10
- Scheffler, Israel, 1954, “An Inscriptional Approach to
Indirect Quotation”,
*Analysis*, 14(4): 83–90. doi:10.1093/analys/14.4.83 - Shoenfield , Joseph R., 1967,
*Mathematical Logic*, Reading, MA: Addison-Wesley. - –––, 1993,
*Recursion Theory*(Lecture Notes in Logic, 1), Berlin/New York: Springer Verlag. - Sieg, Wilfried, 1997, “Step by Recursive Step:
Church’s Analysis of Effective Calculability”,
*Bulletin of Symbolic Logic*, 3(2): 154–180. doi:10.2307/421012 - Smullyan, Arthur Francis, 1947, “Review of ‘The
Problem of Interpreting Modal Logic’, by W. V. Quine”,
*The Journal of Symbolic Logic*, 12(4): 139–141. doi:10.2307/2266498 - –––, 1948, “Modality and
Description”,
*Journal of Symbolic Logic*, 13(1): 31–37. doi:10.2307/2268137 - Soames, Scott, 1987, “Direct Reference, Propositional
Attitudes, and Semantic Content”,
*Philosophical Topics*, 15(1): 47–87. doi:10.5840/philtopics198715112 - –––, 2010,
*What is Meaning?*, Princeton, NJ: Princeton University Press. - Tarski, Alfred, 1936 [1941],
*O logice matematycznej i metodzie dedukcyjnej*(Bibljoteczka matematyczna 3–5), Lwów and Warsaw: Ksiażnica-Atlas. German translation*Einfuhrung in die mathe- matische Logik und in die Methodologie der Mathematik*, Vienna: Julius Springer. Translated from the German as*Introduction to Logic and to the Methodology of Deductive Science*, with additions, Olaf Helmer (trans.), Oxford: Oxford University Press, 1941. - Taylor, Barry and A.P. Hazen, 1992, “Flexibly Structured
Predication”,
*Logique et Analyse*, 35(139/140): 375–393. - Turing, Alan M., 1936 [1965], “On Computable Numbers, with
an Application to the Entscheidungsproblem”,
*Proceedings of the London Mathematical Society*, series 2, 42(1): 230–265. Reprinted in Davis 1965: 115–153. doi:10.1112/plms/s2-42.1.230 - –––, (1939) “Systems of Logic Based on
Ordinals”,
*Proceedings of the London Mathematical Society*2: 161–228. - Uzquiano, Gabriel, 2015, “A Neglected Resolution of
Russell’s Paradox of Propositions”,
*The Review of Symbolic Logic*, 8(2): 328–344. doi:10.1017/S1755020315000106 - [PM] Whitehead, Alfred North and Bertrand Russell, 1910
[1925–1927],
*Principia Mathematica*, vol. I, Cambridge: Cambridge University Press. Second edition 1925–1927.

## Academic Tools

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

## Other Internet Resources

### Acknowledgments

The authors are grateful to C. Anthony Anderson, Allen Hazen, Hasen Khudairi, Gary Ostertag, Nathan Salmón and to those who participated in the Santa Barbarians Discussion Group in 2020. We are also grateful to the referees for their comments on an earlier version.