Logic, Induction and SetsThis is an introduction to logic and the axiomatization of set theory from a unique standpoint. Philosophical considerations, which are often ignored or treated casually, are here given careful consideration, and furthermore the author places the notion of inductively defined sets (recursive datatypes) at the center of his exposition resulting in a treatment of well established topics that is fresh and insightful. The presentation is engaging, but always great care is taken to illustrate difficult points. Understanding is also aided by the inclusion of many exercises. Little previous knowledge of logic is required of the reader, and only a background of standard undergraduate mathematics is assumed. |
Contents
Definitions and notations | 5 |
11 Structures | 6 |
12 Intension and extension | 7 |
13 Notation for sets and relations | 9 |
14 Order | 11 |
15 Products | 17 |
16 Logical connectives | 20 |
Recursive datatypes | 23 |
571 Further applications of ultraproducts | 120 |
58 Exercises on compactness and ultraproducts | 121 |
Computable functions | 123 |
61 Primitive recursive functions | 125 |
611 Primitive recursive predicates and relations | 126 |
62 𝝁recursion | 129 |
63 Machines | 132 |
631 The 𝝁recursive functions are precisely those computed by register machines | 134 |
213 Generalise from IN | 24 |
214 Wellfounded induction | 25 |
215 Sensitivity to set existence | 39 |
217 Proofs | 43 |
221 Propositional languages | 47 |
223 Intersectionclosed properties and Horn formulae | 49 |
224 Do all wellfounded structures arise from rectypes? | 51 |
Partially ordered sets | 52 |
312 Witts theorem | 54 |
313 Exercises on fixed points | 55 |
32 Continuity | 56 |
321 Exercises on lattices and posets | 60 |
33 Zorns lemma | 61 |
331 Exercises on Zorns lemma | 62 |
341 Filters | 63 |
342 Atomic and atomless boolean algebras | 66 |
35 Antimonotonic functions | 67 |
36 Exercises | 69 |
Prepositional calculus | 70 |
41 Semantic and syntactic entailment | 74 |
the Hilbert approach | 75 |
412 No founders many rules | 79 |
413 Sequent calculus | 81 |
42 The completeness theorem | 85 |
421 Lindenbaum algebras | 89 |
423 Nonmonotonic reasoning | 92 |
43 Exercises on propositional logic | 93 |
Predicate calculus | 94 |
52 The language of predicate logic | 95 |
53 Formalising predicate logic | 101 |
532 Predicate calculus in the natural deduction style | 102 |
54 Semantics | 103 |
541 Truth and satisfaction | 104 |
55 Completeness of the predicate calculus | 109 |
551 Applications of completeness | 111 |
56 Back and forth | 112 |
561 Exercises on backandforth constructions | 114 |
57 Ultraproducts and Loss theorem | 115 |
632 A universal register machine | 135 |
64 The undecidablity of the halting problem | 140 |
641 Rices theorem | 141 |
65 Relative computability | 143 |
Ordinals | 147 |
71 Ordinals as a rectype | 148 |
711 Operations on ordinals | 149 |
712 Cantors normal form theorem | 151 |
72 Ordinals from wellorderings | 152 |
721 Cardinals pertaining to ordinals | 159 |
722 Exercises | 160 |
73 Rank | 161 |
Set theory | 167 |
81 Models of set theory | 168 |
82 The paradoxes | 170 |
83 Axioms for set theory with the axiom of foundation | 173 |
84 Zermelo set theory | 175 |
replacement collection and limitation of size | 177 |
851 Mostowski | 181 |
862 Von Neumann ordinals | 182 |
863 Collection | 183 |
864 Reflection | 185 |
87 Some elementary cardinal arithmetic | 189 |
871 Cardinal arithmetic with the axiom of choice | 195 |
88 Independence proofs | 197 |
881 Replacement | 198 |
882 Power set | 199 |
883 Independence of the axiom of infinity | 200 |
885 Foundation | 201 |
886 Choice | 203 |
89 The axiom of choice | 205 |
891 AC and constructive reasoning | 206 |
892 The consistency of the axiom of choice? | 207 |
Answers to selected questions | 210 |
231 | |
233 | |
Other editions - View all
Common terms and phrases
antimonotone arbitrary arity atomic axiom of choice axiom scheme axiomatisable bijection binary relation boolean algebra Cantor's cardinal carrier set closed cofinality cofinite complete lattice completeness theorem computable function concept construction constructors contains deduction defined definition element engendering relation example EXERCISE extensional filter first-order fixed point formalise formula function f give graph infer infinite injection isomorphic language least lexicographic mathematics means Miniexercise natural numbers nonempty nontrivial normal form theorem notation ordered pairs ordinals P₁ paradox partial order poset power set predicate calculus predicate letter primitive recursive function proof propositional logic prove quantifiers R-predecessors rectype Recursive datatypes register machine semantics semidecidable set sense sequent set theory structural induction subset succ Suppose TC(x things total computable total order transitive closure true ultrafilter ultraproducts valuation variables well-founded relation well-founded sets well-ordering Zorn's lemma