Higher Order Logic

Daniel Leivant

Contents

1 Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2
2 The expressive power of second order Logic : : : : : : : : : : : 3
2.1 The language of second order logic : : : : : : : : : : : : : 3
2.2 Expressing size : : : : : : : : : : : : : : : : : : : : : : : : 4
2.3 Defining data types : : : : : : : : : : : : : : : : : : : : : 6
2.4 Describing processes : : : : : : : : : : : : : : : : : : : : : 8
2.5 Expressing convergence using second order

validity : : : : : : : : : : : : : : : : : : : : : : : : : 9
2.6 Truth definitions: the analytical hierarchy : : : : : : : : 10
2.7 Inductive definitions : : : : : : : : : : : : : : : : : : : : : 13
3 Canonical semantics of higher order logic : : : : : : : : : : : : 15
3.1 Tarskian semantics of second order logic : : : : : : : : : 15
3.2 Function and relation formulations : : : : : : : : : : : : 15
3.3 Normal forms : : : : : : : : : : : : : : : : : : : : : : : : 16
3.4 Finite order logic : : : : : : : : : : : : : : : : : : : : : : 17
3.5 Functional types : : : : : : : : : : : : : : : : : : : : : : : 18
3.6 Formulas as higher order functions : : : : : : : : : : : : : 19
3.7 Truth definitions revisited : : : : : : : : : : : : : : : : : 20
4 Proof theory : : : : : : : : : : : : : : : : : : : : : : : : : : : : 22
4.1 Basic formalisms : : : : : : : : : : : : : : : : : : : : : : : 22
4.2 Additional set existence principles : : : : : : : : : : : : : 24
4.3 Constructive finite order logics : : : : : : : : : : : : : : : 26
4.4 Normalization and the subformula property : : : : : : : 27
5 Ontology : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 29
5.1 The gulf between first order and second order logic : : : 29

5.2 Lindstrom's and Quine's tests : : : : : : : : : : : : : : : 31
5.3 Slipping from first to second order logic : : : : : : : : : : 33
5.4 Higher order logic as mathematics: Henkin's

semantics : : : : : : : : : : : : : : : : : : : : : : : : 34
5.5 Henkin completeness for full finite order logic : : : : : : 37
5.6 Finite order logic as a second order theory : : : : : : : : 39
6 Restricted higher order logic : : : : : : : : : : : : : : : : : : : 40
6.1 Restricted expressiveness 1: Monadic second order logic : 41