H. P. Grice, "Churchianum implicatum"

CHURCHIANUM IMPLICATUM -- Church, Alonzo (1903–95) American mathematical logician, born in Washington, DC, Professor at Princeton and UCLA. In mathematical logic, Church’s theorem proved the undecidability of first-order logic, and Church’s thesis linked the notion of effective computation to recursiveness. Church argued for realism regarding abstract objects and contributed to the theory of probability as well as playing a major role in the development of mathematical logic. His works include Introduction to Mathematical Logic, vol. 1 (1956). Church’s theorem, see Church’s thesis Church’s thesis Logic “That the notion of an effectively calculable function of positive integers should be identified with that of a recursive function . . .” This thesis was proposed by the American mathematical logician Alonzo Church in 1935. It combines Gödel’s notion of recursiveness with the notion of computability. A function is computable if and only if it is recursive and Turing-computable. Since this thesis is closely related to the concept of Turing-computability, it is sometimes called the Church–Turing thesis. The notion of effective computability in Church’s thesis is an intuitive rather than proven notion. For this reason, Church’s thesis is a thesis rather than a theorem. There is, however, Church’s theorem, proved by Church in 1936, which states that there is no decision procedure for determining whether an arbitrary formula of predicate calculus is a theorem of the calculus. It is a negative solution to the decision problem. Church’s thesis serves as one of the premises of Church’s theorem. “Church’s thesis, if true, guarantees that a Turing machine can compute any ‘effective’ procedure.” Baker, Saving Belief