Completed in 1983, this work culminates nearly half a century of the late Alfred Tarski's foundational studies in logic, mathematics, and the philosophy of science. Written in collaboration with Steven Givant, the book appeals to a very broad audience, and requires only a familiarity with first-order logic. It is of great interest to logicians and mathematicians interested in the foundations of mathematics, but also to philosophers interested in logic, semantics, algebraic logic, or the methodology of the deductive sciences, and to computer scientists interested in developing very simple computer languages rich enough for mathematical and scientific applications. The authors show that set theory and number theory can be developed within the framework of a new, different, and simple equational formalism, closely related to the formalism of the theory of relation algebras. There are no variables, quantifiers, or sentential connectives. Predicates are constructed from two atomic binary predicates (which denote the relations of identity and set-theoretic membership) by repeated applications of four operators that are analogues of the well-known operations of relative product, conversion, Boolean addition, and complementation. All mathematical statements are expressed as equations between predicates. There are ten logical axiom schemata and just one rule of inference: the one of replacing equals by equals, familiar from high school algebra. Though such a simple formalism may appear limited in its powers of expression and proof, this book proves quite the opposite. The authors show that it provides a framework for the formalization of practically all known systems of set theory, and hence for the development of all classical mathematics. The book contains numerous applications of the main results to diverse areas of foundational research: propositional logic; semantics; first-order logics with finitely many variables; definability and axiomatizability questions in set theory, Peano arithmetic, and real number theory; representation and decision problems in the theory of relation algebras; and decision problems in equational logic.
Author(s): Alfred Tarski and Steven Givant
Series: Colloquium Publications Amer Mathematical Soc
Publisher: AMS
Year: 1987
Language: English
Pages: 341
Cover......Page 1
Title Page......Page 2
Copyright Page......Page 3
Table of Contents......Page 4
Explanation of Section Interdependence Diagrams......Page 8
Preface......Page 12
Postscript......Page 20
Acknowledgments......Page 22
1.1 Preliminaries......Page 24
1.2 Symbols and expressions of L......Page 27
1.3 Derivability in L......Page 30
1.4 Semantical notions of L......Page 34
1.5 First-order formalisms......Page 37
1.6 Formalisms and systems......Page 39
2.1 Symbols and expressions of L+......Page 46
2.2 Derivability and semantical notions of L+......Page 48
2.3 The equipollence of L+ and L......Page 50
2.4 The equipollence of a system with an extension......Page 53
2.5 The equipollence of two systems relative to a common extension......Page 64
3.1 Syntactical and semantical notions of Lx......Page 68
3.2 Schemata of equations derivable in Lx......Page 71
3.3 A deduction theorem for Lx......Page 74
3.4 The inequipollence of Lx with L+ and L......Page 76
3.5 The inequipollence of extensions of Lx with L+ and L......Page 79
3.6 Lx-expressibility......Page 85
3.7 The three-variable formalisms L3 and L3+......Page 87
3.8 The equipollence of L3 and L3+......Page 95
3.9 The equipollence of Lx and L3+......Page 99
3.10 Subformalisms of L and L+ with finitely many variables......Page 112
4.1 Conjugated quasiprojections and sentences Qab......Page 118
4.2 Systems of conjugated quasiprojections and systems of predicates Pab......Page 123
4.3 Historical remarks regarding the translation mapping from L+ to Lx......Page 130
4.4 Proof of the main mapping theorem for Lx and L+......Page 133
4.5 The construction of equipollent Q-systems in Lx......Page 147
4.6 The formalizability of systems of set theory in Lx......Page 150
4.7 Problems of expressibility and decidibility in Lx......Page 158
4.8 The undecidability of first-order logics with finitely many variables, and the relative equipollence of L3 with L......Page 163
5.1 One-to-one translation mappings......Page 170
5.2 Reducing the number of primitive notions of Lx: definitionally equivalent variants of Lx......Page 174
5.3 Eliminating the symbol 1 as a primitive notion from systems of set theory in Lx......Page 176
5.4 Eliminating the symbol = as a primitive notion from Lx: the reduced formalism L_1x......Page 181
5.5 Undecidable subsystems of sentential logic......Page 188
6.1 Denotation and truth in Lx......Page 192
6.2 The denotability of first-order definable relations in structures......Page 193
6.3 The Lx-expressibility of certain relativized sentences......Page 197
6.4 The finite axiomatizability of predicative systems of set theory admitting proper classes......Page 200
6.5 The finite axiomatizability of predicative systems of set theory excluding proper classes......Page 210
7.1 Extension of equipollence results to Q-systems in first-order formalisms with just binary relation symbols......Page 214
7.2 Extension of equipollence results to weak Q-systems in arbitrary first-order formalisms......Page 223
7.3 The equipollence of weak Q-systems with finite variable subsystems......Page 231
7.4 Comparison of equipollence results for strong and weak Q-systems......Page 237
7.5 The formalizability of the arithmetic of natural numbers in Lx......Page 238
7.6 The formalizability of Peano arithmetic in Lx, and the definitional equivalence of Peano arithmetic with a system of set theory......Page 245
7.7 The formalizability of the arithmetic of real numbers in Lx......Page 249
7.8 Remarks on first-order formalisms with limited vocabularies......Page 252
8.1 Equational formalisms......Page 254
8.2 Relation Algebras......Page 258
8.3 Representable Relation Algebras......Page 262
8.4 Q-relation algebras......Page 265
8.5 Decision problems for varieties of relation algebras......Page 274
8.6 Decision problems for varieties of groupoids......Page 281
8.7 Historical remarks regarding the decision problems......Page 291
Bibliography......Page 296
Index of Symbols......Page 306
Index of Names......Page 320
Index of Subjects......Page 325
Index of Numbered Items......Page 340
