Mathematical Logic. An Introduction Summer 2006 by P eter Koepke

Table of contents Table of contents

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1

1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2

1.1 1.2 1.3 1.4 1.5

A simple proof . . . . Formal proofs . . . . . Syntax and semantics Set theory . . . . . . . Circularity . . . . . . .

. . . . .

. . . . .

. . . . .

. . . . .

2 3 3 4 4

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4

3 Symbols and words . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7

4 Induction and recursion on calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9

2 Set theoretic preliminaries

5 Terms and formulas

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

6 Structures and models

10

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

11

7 The satisfaction relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

13

8 Logical implication and propositional connectives

. . . . . . . . . . . . . . . . . . . .

15

9 Substitution and quantification rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

16

1 0 A sequent calculus

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

20

1 1 Derivable sequent rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

21

11.1 11.2 11.3 11.4

Auxiliary rules . . . . . . . . . . . . . . . . . . . Introduction and elimination of ∨ , ∧ , Manipulations of antecedents . . . . . . . . Examples of formal proofs . . . . . . . . . .

1 2 C onsistency

. . . .

21 22 24 24

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

25

1 3 Term models and H enkin sets

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

26

1 4 C onstructing H enkin sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .