This short book, geared towards undergraduate students of computer science and mathematics, is specifically designed for a first course in mathematical logic. A proof of Gödel's completeness theorem and its main consequences is given using Robinson's completeness theorem and Gödel's compactness theorem for propositional logic. The reader will familiarize himself with many basic ideas and artifacts of mathematical logic: a non-ambiguous syntax, logical equivalence and consequence relation, the Davis-Putnam procedure, Tarski semantics, Herbrand models, the axioms of identity, Skolem normal forms, nonstandard models and, interestingly enough, proofs and refutations viewed as graphic objects. The mathematical prerequisites are minimal: the book is accessible to anybody having some familiarity with proofs by induction. Many exercises on the relationship between natural language and formal proofs make the book also interesting to a wide range of students of philosophy and linguistics.
Author(s): Daniele Mundici
Series: UNITEXT / La Matematica per il 3+2
Publisher: Springer
Year: 2012
Language: English
Pages: 143
Cover......Page 1
Title Page......Page 4
Copyright Page......Page 5
Preface......Page 6
Symbols and Expressions......Page 8
Contents......Page 10
Part I Propositional Logic......Page 14
1 Introduction......Page 16
2.1 Syntax......Page 20
2.3 Logical consequence and logical equivalence......Page 21
Exercises......Page 22
3.1 Clauses and formulas as finite sets......Page 26
3.2 Resolution......Page 27
3.3 Davis-Putnam procedure 䐀倀倀......Page 29
Exercises......Page 30
4.1 Statement and proof......Page 32
4.2 Refutation......Page 35
Exercises......Page 36
5.1 Krom clauses......Page 40
5.2 Horn clauses......Page 41
Exercises......Page 42
6.1 Preparatory material......Page 44
6.2 Statement and proof......Page 45
Exercises......Page 46
7.1 Formulas......Page 48
7.2 Unambiguity of the syntax......Page 49
Exercises......Page 52
8.1 Assignment, logical consequence, logical equivalence......Page 54
Connectives......Page 55
Assignment, logical consequence, logical equivalence......Page 56
9.1 Some logical equivalences......Page 60
9.2 Propositional logic and the logic of clauses......Page 61
Exercises......Page 63
10 Recap: Expressivity and Efficiency......Page 66
Part II Predicate Logic......Page 68
11.1 Introduction......Page 70
Exercises......Page 72
12.1 Elements of the syntax......Page 76
12.2 Formalisation in clauses......Page 77
12.3 Substitution of terms for variables......Page 78
12.4 Herbrand universe......Page 79
12.5 Refutation......Page 80
Exercises......Page 82
13.1 Tarski semantics: types and models......Page 84
13.2 Tarski semantics: clauses......Page 86
13.3 Instantiation, resolution and its correctness......Page 87
Exercises......Page 88
14.1 Introduction......Page 92
14.2 Completeness and compactness......Page 93
14.3 Comments on the Completeness Theorem......Page 95
Refutational Method......Page 96
Satisfiability/Unsatisfiability......Page 99
15.1 Introduction......Page 102
15.2 Axiomatisation of the equality......Page 103
Exercises......Page 105
16.1 Introduction......Page 108
16.2 Transformation of formulas in PNF......Page 110
16.3 Skolemisation......Page 112
16.4 Completeness, compactness and nonstandard models......Page 114
Transformation into clauses......Page 116
Logical consequence......Page 118
Logical consequence, models and natural language......Page 122
17 Final Remarks......Page 130
Index......Page 134
