Church Alonzo (1903–95), American logician, mathematician, and philosopher, known in pure logic for his discovery and application of the Church lambda operator, one of the central ideas of the Church lambda calculus, and for his rigorous formalizations of the theory of types, a higher-order underlying logic originally formulated in a flawed form by Whitehead and Russell. The lambda operator enables direct, unambiguous, symbolic representation of a range of philosophically and mathematically important expressions previously representable only ambiguously or after elaborate paraphrasing. In philosophy, Church advocated rigorous analytic methods based on symbolic logic. His philosophy was characterized by his own version of logicism, the view that mathematics is reducible to logic, and by his unhesitating acceptance of higherorder logics. Higher-order logics, including second-order, are ontologically rich systems that involve quantification of higher-order variables, variables that range over properties, relations, and so on. Higher-order logics were routinely used in foundational work by Frege, Peano, Hilbert, Gödel, Tarski, and others until around World War II, when they suddenly lost favor. In regard to both his logicism and his acceptance of higher-order logics, Church countered trends, increasingly dominant in the third quarter of the twentieth century, against reduction of mathematics to logic and against the so-called ‘ontological excesses’ of higher-order logic. In the 1970s, although admired for his high standards of rigor and for his achievements, Church was regarded as conservative or perhaps even reactionary. Opinions have softened in recent years. On the computational and epistemological sides of logic Church made two major contributions. He was the first to articulate the now widely accepted principle known as Church’s thesis, that every effectively calculable arithmetic function is recursive. At first highly controversial, this principle connects intuitive, epistemic, extrinsic, and operational aspects of arithmetic with its formal, ontic, intrinsic, and abstract aspects. Church’s thesis sets a purely arithmetic outer limit on what is computationally achievable. Church’s further work on Hilbert’s ‘decision problem’ led to the discovery and proof of Church’s theorem – basically that there is no computational procedure for determining, of a finite-premised first-order argument, whether it is valid or invalid. This result contrasts sharply with the previously known result that the computational truth-table method suffices to determine the validity of a finite-premised truthfunctional argument. Church’s thesis at once highlights the vast difference between propositional logic and first-order logic and sets an outer limit on what is achievable by ‘automated reasoning.’ Church’s mathematical and philosophical writings are influenced by Frege, especially by Frege’s semantic distinction between sense and reference, his emphasis on purely syntactical treatment of proof, and his doctrine that sentences denote (are names of) their truth-values. See also CHURCH’S THESIS, COMPUTABILITY, FORMALIZATION , HILBERT, HILBERT ‘ S PRO – GRAM , LOGICISM , RECURSIVE FUNCTION THE – ORY, SECOND – ORDER LOGIC , TRUTH TABLE , TYPE THEORY. J.Cor.