Logic, Meaning and Computation: Essays in Memory of Alonzo Church

ISBN-13: 9781402001413 / Angielski / Twarda / 2002 / 627 str.

C. Anthony Anderson; Michael Zelc+ny; Michael Zelkny

Opis

Alonzo Church was undeniably one ofthe intellectual giants of theTwenti eth Century . These articles are dedicated to his memory and illustrate the tremendous importance his ideas have had in logic, mathematics, comput er science and philosophy . Discussions of some of thesevarious contributions have appeared in The Bulletin of Symbolic Logic, and th e interested reader is invited to seek details there . Here we justtry to give somegener al sense of the scope, depth, and value of his work. Church is perhaps best known for the theorem, appropriately called " C h u r c h ' s Theorem," that there is no decision procedure forthelogical valid ity of formulas first-order of logic . A d ecision proce dure forthat part of logic would have come near to fulfilling Leibniz's dream of a calculus that could be mechanically used tosettle logical disputes . It was not to . be It could not be . What Church proved precisely is that there is no lambda-definable function that can i n every case providethe right answer, ' y e s ' or ' n o', tothe question of whether or not any arbitrarily given formula is valid .

Spis treści

Preface; C.A. Anderson, M. Zelëny. Remembering Alonzo Church; D. Kaplan, T. Burge. Part I: Logic. Logic, truth and number: The elementary genesis of arithmetic; P. Apostoli. Second-order logic; J. Corcoran. A representation of relation algebras using Routley-Meyer frames; J.M. Dunn. Church's set theory with a universal set; Th. Forster. Axioms of infinity in Church's type theory; R.O. Gandy. Logical objects; E.L. Keenan. The lambda calculus and adjoint functors; S.M. Lane. Atomic Boolean algebras and classical propositional logic; G.J. Massey. Improved decision procedures for pure relevant logic; R.K. Meyer. The `triumph' of first-order languages; S. Shapiro. Equivalence relations and groups; R. Smullyan. Part II: Computation. Discriminating coded lambda terms; H. Barendregt. lambda-calculus as a foundation for mathematics; K. Grue. Peano's lambda calculus: The functional abstraction implicit in arithmetic; D. Leivant. The undecidability of lambda-definability; R. Loader. A construction of the provable wellorderings of the theory of species; P. Martin-Löf. Semantics for first and higher order realizability; C. Mclarty. Language and equality theory in logic programming; J.C. Shepherdson. Part III: Philosophy, Meaning, and Intensional Logic. Alternative (1*): A criterion of identity for intensional entities; C.A. Anderson. Nominalist paraphrase and ontological commitment; J.P. Burgess. Peace, justice and computation: Leibniz' program and the moral and political significance of Church's theorem; M. Detlefsen. Tarski's theorem and NFU; M.R. Holmes. Church's theorem and randomness; G. Mar. Russellian type theory andsemantical paradoxes; E. Martino. The logic of sense and denotation: Extensions and applications; T. Parsons. Analysis, synonymy and sense; M. Richard. The very possibility of language; N. Salmon. Index.