Mathematical Logic - Department Mathematik
Mathematical Logic
Helmut Schwichtenberg
Mathematisches Institut der Universit?at Mu?nchen Wintersemester 2003/2004
Contents
Chapter 1. Logic
1
1. Formal Languages
2
2. Natural Deduction
4
3. Normalization
11
4. Normalization including Permutative Conversions
20
5. Notes
31
Chapter 2. Models
33
1. Structures for Classical Logic
33
2. Beth-Structures for Minimal Logic
35
3. Completeness of Minimal and Intuitionistic Logic
39
4. Completeness of Classical Logic
42
5. Uncountable Languages
44
6. Basics of Model Theory
48
7. Notes
54
Chapter 3. Computability
55
1. Register Machines
55
2. Elementary Functions
58
3. The Normal Form Theorem
64
4. Recursive Definitions
69
Chapter 4. G?odel's Theorems
73
1. G?odel Numbers
73
2. Undefinability of the Notion of Truth
77
3. The Notion of Truth in Formal Theories
79
4. Undecidability and Incompleteness
81
5. Representability
83
6. Unprovability of Consistency
87
7. Notes
90
Chapter 5. Set Theory
91
1. Cumulative Type Structures
91
2. Axiomatic Set Theory
92
3. Recursion, Induction, Ordinals
96
4. Cardinals
116
5. The Axiom of Choice
120
6. Ordinal Arithmetic
126
7. Normal Functions
133
8. Notes
138
Chapter 6. Proof Theory
139
i
ii
CONTENTS
1. Ordinals Below 0
139
2. Provability of Initial Cases of TI
141
3. Normalization with the Omega Rule
145
4. Unprovable Initial Cases of Transfinite Induction
149
Bibliography
157
Index
159
CHAPTER 1
Logic
The main subject of Mathematical Logic is mathematical proof. In this introductory chapter we deal with the basics of formalizing such proofs. The system we pick for the representation of proofs is Gentzen's natural deduction, from [8]. Our reasons for this choice are twofold. First, as the name says this is a natural notion of formal proof, which means that the way proofs are represented corresponds very much to the way a careful mathematician writing out all details of an argument would go anyway. Second, formal proofs in natural deduction are closely related (via the so-called CurryHoward correspondence) to terms in typed lambda calculus. This provides us not only with a compact notation for logical derivations (which otherwise tend to become somewhat unmanagable tree-like structures), but also opens up a route to applying the computational techniques which underpin lambda calculus.
Apart from classical logic we will also deal with more constructive logics: minimal and intuitionistic logic. This will reveal some interesting aspects of proofs, e.g. that it is possible und useful to distinguish beween existential proofs that actually construct witnessing objects, and others that don't. As an example, consider the following proposition.
There are irrational numbers a, b such that ab is rational.
This can Case
be 2pro2viesdraastifoonlalolw. sC, bhyoocsaeseas.=
2
and
b
=
2.
Then a, b are
irrational Case
an2db2yisasisruramtpiotnioanl.
ab is rational. Choose a =
22
and
b
=
2.
Then by
assumption a, b are irrational and
ab =
22
2
=
2 2 =2
is
rational. As long
as
we
have
not
decided
whether
22
is
rational,
we
do
not
know which numbers a, b we must take. Hence we have an example of an
existence proof which does not provide an instance.
An essential point for Mathematical Logic is to fix a formal language to
be used. We take implication and the universal quantifier as basic. Then
the logic rules correspond to lambda calculus. The additional connectives ,
, and are defined via axiom schemes. These axiom schemes will later
be seen as special cases of introduction and elimination rules for inductive
definitions.
1
2
1. LOGIC
1. Formal Languages
1.1. Terms and Formulas. Let a countable infinite set { vi | i N } of variables be given; they will be denoted by x, y, z. A first order language L then is determined by its signature, which is to mean the following.
? For every natural number n 0 a (possible empty) set of n-ary relation symbols (also called predicate symbols). 0-ary relation symbols are called propositional symbols. (read "falsum") is required as a fixed propositional symbol. The language will not, unless stated otherwise, contain = as a primitive.
? For every natural number n 0 a (possible empty) set of n-ary function symbols. 0-ary function symbols are called constants.
We assume that all these sets of variables, relation and function symbols are disjoint.
For instance the language LG of group theory is determined by the signature consisting of the following relation and function symbols: the group operation (a binary function symbol), the unit e (a constant), the inverse operation -1 (a unary function symbol) and finally equality = (a binary relation symbol).
L-terms are inductively defined as follows.
? Every variable is an L-term. ? Every constant of L is an L-term. ? If t1, . . . , tn are L-terms and f is an n-ary function symbol of L
with n 1, then f (t1, . . . , tn) is an L-term.
From L-terms one constructs L-prime formulas, also called atomic formulas of L: If t1, . . . , tn are terms and R is an n-ary relation symbol of L, then R(t1, . . . , tn) is an L-prime formula.
L-formulas are inductively defined from L-prime formulas by
? Every L-prime formula is an L-formula. ? If A and B are L-formulas, then so are (A B) ("if A, then B"),
(A B) ("A and B") and (A B) ("A or B"). ? If A is an L-formula and x is a variable, then xA ("for all x, A
holds") and xA ("there is an x such that A") are L-formulas.
Negation, classical disjunction, and the classical existential quantifier are defined by
?A := A , A cl B := ?A ?B , clxA := ?x?A.
Usually we fix a language L, and speak of terms and formulas instead of L-terms and L-formulas. We use
r, s, t
for terms,
x, y, z c
for variables, for constants,
P, Q, R for relation symbols,
f, g, h
for function symbols,
A, B, C, D for formulas.
................
................
In order to avoid copyright disputes, this page is only a partial summary.
To fulfill the demand for quickly locating and searching documents.
It is intelligent file search solution for home and business.