Books in Mathematical logic and foundations

Logic from Russell to Church

1st Edition
Volume 5
May 26, 2009
Dov M. Gabbay + 1 more
English
Hardback
9 7 8 0 4 4 4 5 1 6 2 0 6
eBook
9 7 8 0 0 8 0 8 8 5 4 7 6

This volume is number five in the 11-volume Handbook of the History of Logic. It covers the first 50 years of the development of mathematical logic in the 20th century, and concentrates on the achievements of the great names of the period--Russell, Post, Gödel, Tarski, Church, and the like. This was the period in which mathematical logic gave mature expression to its four main parts: set theory, model theory, proof theory and recursion theory. Collectively, this work ranks as one of the greatest achievements of our intellectual history. Written by leading researchers in the field, both this volume and the Handbook as a whole are definitive reference tools for senior undergraduates, graduate students and researchers in the history of logic, the history of philosophy, and any discipline, such as mathematics, computer science, and artificial intelligence, for whom the historical background of his or her work is a salient consideration.

Mathematical Analysis and Proof

2nd Edition
April 30, 2009
David S G Stirling
English
eBook
9 7 8 0 8 5 7 0 9 9 3 4 1

This fundamental and straightforward text addresses a weakness observed among present-day students, namely a lack of familiarity with formal proof. Beginning with the idea of mathematical proof and the need for it, associated technical and logical skills are developed with care and then brought to bear on the core material of analysis in such a lucid presentation that the development reads naturally and in a straightforward progression. Retaining the core text, the second edition has additional worked examples which users have indicated a need for, in addition to more emphasis on how analysis can be used to tell the accuracy of the approximations to the quantities of interest which arise in analytical limits.

The Many Valued and Nonmonotonic Turn in Logic

1st Edition
Volume 8
July 6, 2007
Dov M. Gabbay + 1 more
English
eBook
9 7 8 0 0 8 0 5 4 9 3 9 2

The present volume of the Handbook of the History of Logic brings together two of the most important developments in 20th century non-classical logic. These are many-valuedness and non-monotonicity. On the one approach, in deference to vagueness, temporal or quantum indeterminacy or reference-failure, sentences that are classically non-bivalent are allowed as inputs and outputs to consequence relations. Many-valued, dialetheic, fuzzy and quantum logics are, among other things, principled attempts to regulate the flow-through of sentences that are neither true nor false. On the second, or non-monotonic, approach, constraints are placed on inputs (and sometimes on outputs) of a classical consequence relation, with a view to producing a notion of consequence that serves in a more realistic way the requirements of real-life inference. Many-valued logics produce an interesting problem. Non-bivalent inputs produce classically valid consequence statements, for any choice of outputs. A major task of many-valued logics of all stripes is to fashion an appropriately non-classical relation of consequence.The chief preoccupation of non-monotonic (and default) logicians is how to constrain inputs and outputs of the consequence relation. In what is called “left non-monotonicity”, it is forbidden to add new sentences to the inputs of true consequence-statemen... The restriction takes notice of the fact that new information will sometimes override an antecedently (and reasonably) derived consequence. In what is called “right non-monotonicity”, limitations are imposed on outputs of the consequence relation. Most notably, perhaps, is the requirement that the rule of or-introduction not be given free sway on outputs. Also prominent is the effort of paraconsistent logicians, both preservationist and dialetheic, to limit the outputs of inconsistent inputs, which in classical contexts are wholly unconstrained.In some instances, our two themes coincide. Dialetheic logics are a case in point. Dialetheic logics allow certain selected sentences to have, as a third truth value, the classical values of truth and falsity together. So such logics also admit classically inconsistent inputs. A central task is to construct a right non-monotonic consequence relation that allows for these many-valued, and inconsistent, inputs.The Many Valued and Non-Monotonic Turn in Logic is an indispensable research tool for anyone interested in the development of logic, including researchers, graduate and senior undergraduate students in logic, history of logic, mathematics, history of mathematics, computer science, AI, linguistics, cognitive science, argumentation theory, and the history of ideas.

Lectures on the Curry-Howard Isomorphism

1st Edition
Volume 149
July 4, 2006
Morten Heine Sørensen + 1 more
English
Hardback
9 7 8 0 4 4 4 5 2 0 7 7 7
eBook
9 7 8 0 0 8 0 4 7 8 9 2 0

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance,minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc.The isomorphism has many aspects, even at the syntactic level:formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to term reduction, etc.But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transformsproofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq).This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic.Key features- The Curry-Howard Isomorphism treated as common theme- Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics- Thorough study of the connection between calculi and logics- Elaborate study of classical logics and control operators- Account of dialogue games for classical and intuitionistic logic- Theoretical foundations of computer-assisted reasoning

Infinite Words

1st Edition
Volume 141
February 12, 2004
Dominique Perrin + 1 more
English
Hardback
9 7 8 0 1 2 5 3 2 1 1 1 2
eBook
9 7 8 0 0 8 0 5 2 5 6 4 8

Infinite Words is an important theory in both Mathematics and Computer Sciences. Many new developments have been made in the field, encouraged by its application to problems in computer science. Infinite Words is the first manual devoted to this topic.Infinite Words explores all aspects of the theory, including Automata, Semigroups, Topology, Games, Logic, Bi-infinite Words, Infinite Trees and Finite Words. The book also looks at the early pioneering work of Büchi, McNaughton and Schützenberger.

Relation Algebras by Games

1st Edition
Volume 147
July 1, 2002
Robin Hirsch + 1 more
English
eBook
9 7 8 0 0 8 0 5 4 0 4 5 0

Relation algebras are algebras arising from the study of binary relations.They form a part of the field of algebraic logic, and have applications in proof theory, modal logic, and computer science. This research text uses combinatorial games to study the fundamental notion of representations of relation algebras. Games allow an intuitive and appealing approach to the subject, and permit substantial advances to be made. The book contains many new results and proofs not published elsewhere. It should be invaluable to graduate students and researchers interested in relation algebras and games.After an introduction describing the authors' perspective on the material, the text proper has six parts. The lengthy first part is devoted to background material, including the formal definitions of relation algebras, cylindric algebras, their basic properties, and some connections between them. Examples are given. Part 1 ends with a short survey of other work beyond the scope of the book. In part 2, games are introduced, and used to axiomatise various classes of algebras. Part 3 discusses approximations to representability, using bases, relation algebra reducts, and relativised representations. Part 4 presents some constructions of relation algebras, including Monk algebras and the 'rainbow construction', and uses them to show that various classes of representable algebras are non-finitely axiomatisable or even non-elementary. Part 5 shows that the representability problem for finite relation algebras is undecidable, and then in contrast proves some finite base property results. Part 6 contains a condensed summary of the book, and a list of problems. There are more than 400 exercises.The book is generally self-contained on relation algebras and on games, and introductory text is scattered throughout. Some familiarity with elementary aspects of first-order logic and set theory is assumed, though many of the definitions are given. Chapter 2 introduces the necessary universal algebra and model theory, and more specific model-theoretic ideas are explained as they arise.

Theory of Relations

1st Edition
Volume 145
December 15, 2000
R. Fraisse
English
Hardback
9 7 8 0 4 4 4 5 0 5 4 2 2
eBook
9 7 8 0 0 8 0 5 1 9 1 1 1

Relation theory originates with Hausdorff (Mengenlehre 1914) and Sierpinski (Nombres transfinis, 1928) with the study of order types, specially among chains = total orders = linear orders. One of its first important problems was partially solved by Dushnik, Miller 1940 who, starting from the chain of reals, obtained an infinite strictly decreasing sequence of chains (of continuum power) with respect to embeddability. In 1948 I conjectured that every strictly decreasing sequence of denumerable chains is finite. This was affirmatively proved by Laver (1968), in the more general case of denumerable unions of scattered chains (ie: which do not embed the chain Q of rationals), by using the barrier and the better orderin gof Nash-Williams (1965 to 68).Another important problem is the extension to posets of classical properties of chains. For instance one easily sees that a chain A is scattered if the chain of inclusion of its initial intervals is itself scattered (6.1.4). Let us again define a scattered poset A by the non-embedding of Q in A. We say that A is finitely free if every antichain restriction of A is finite (antichain = set of mutually incomparable elements of the base). In 1969 Bonnet and Pouzet proved that a poset A is finitely free and scattered iff the ordering of inclusion of initial intervals of A is scattered. In 1981 Pouzet proved the equivalence with the a priori stronger condition that A is topologically scattered: (see 6.7.4; a more general result is due to Mislove 1984); ie: every non-empty set of initial intervals contains an isolated elements for the simple convergence topology.In chapter 9 we begin the general theory of relations, with the notions of local isomorphism, free interpretability and free operator (9.1 to 9.3), which is the relationist version of a free logical formula. This is generalized by the back-and-forth notions in 10.10: the (k,p)-operator is the relationist version of the elementary formula (first order formula with equality).Chapter 12 connects relation theory with permutations: theorem of the increasing number of orbits (Livingstone, Wagner in 12.4). Also in this chapter homogeneity is introduced, then more deeply studied in the Appendix written by Norbert Saucer.Chapter 13 connects relation theory with finite permutation groups; the main notions and results are due to Frasnay. Also mention the extension to relations of adjacent elements, by Hodges, Lachlan, Shelah who by this mean give an exact calculus of the reduction threshold.The book covers almost all present knowledge in Relation Theory, from origins (Hausdorff 1914, Sierpinski 1928) to classical results (Frasnay 1965, Laver 1968, Pouzet 1981) until recent important publications (Abraham, Bonnet 1999).All results are exposed in axiomatic set theory. This allows us, for each statement, to specify if it is proved only from ZF axioms of choice, the continuum hypothesis or only the ultrafilter axiom or the axiom of dependent choice, for instance.

From Peirce to Skolem

1st Edition
Volume 4
November 22, 2000
Geraldine Brady
English
eBook
9 7 8 0 0 8 0 5 3 2 0 2 8

This book is an account of the important influence on the development of mathematical logic of Charles S. Peirce and his student O.H. Mitchell, through the work of Ernst Schröder, Leopold Löwenheim, and Thoralf Skolem. As far as we know, this book is the first work delineating this line of influence on modern mathematical logic.