Modal Quantifiers [PhD Thesis]

1 Introduction 3
1.1 Generalized quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.1.1 Generalized quantifiers and modal operators. (How modal
quantifiers could have been invented) . . . . . . . . . . . . . . 5
1.1.2 Dependence relation between objects . . . . . . . . . . . . . . 5
1.2 Proof-theoreticmotivation . . . . . . . . . . . . . . . . . . . . . . . . 6
1.2.1 Sequent calculus with indexed variables . . . . . . . . . . . . . 6
1.2.2 Generalized quantification as substructural logic . . . . . . . . 7
1.3 Assignments and cylindrifications . . . . . . . . . . . . . . . . . . . . 8
1.4 Composite variables in programming languages . . . . . . . . . . . . 9
1.5 Overview of the thesis . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2 Various logics of modal quantifiers 13
2.1 Structured dependence models . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Hilbert-style axiomatization . . . . . . . . . . . . . . . . . . . . . . . 15
2.3 Obtaining stronger logics . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.3.1 In the direction of generalized quantifiers . . . . . . . . . . . . 22
2.3.2 Circular dependencies, or assignments . . . . . . . . . . . . . . 23
2.4 Crsn-models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.5 The weakest logic above Crs and dependence models . . . . . . . . . 29
2.6 Restricted fragments of predicate logic . . . . . . . . . . . . . . . . . 31
2.7 Tableaux for Crs and Crs+ . . . . . . . . . . . . . . . . . . . . . . . 33
2.8 When there are few relevant variables . . . . . . . . . . . . . . . . . . 36
3 Minimal logic of dependence models 39
3.1 Language and models. Informal discussion . . . . . . . . . . . . . . . 39
3.2 Axiomatics and Completeness . . . . . . . . . . . . . . . . . . . . . . 41
3.3 Preservation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
3.4 Tableaux. Decidability . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.4.1 Tableaux for theminimal logic . . . . . . . . . . . . . . . . . . 47
3.4.2 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
3.4.3 Tableaux for extensions of theminimal logic . . . . . . . . . . 54
3.5 Sequent calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.6 Interpolation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
3.7 Using graphs instead of indexed variables . . . . . . . . . . . . . . . . 67
4 Correspondence and Completeness for Generalized Quantifiers 69
4.1 Frame Correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . 70
4.1.1 Sahlqvist theoremfor frames . . . . . . . . . . . . . . . . . . . 71
4.1.2 Limitative Results . . . . . . . . . . . . . . . . . . . . . . . . 75
4.2 Correspondence for completeness . . . . . . . . . . . . . . . . . . . . 78
4.2.1 Sahlqvist theoremfor completeness . . . . . . . . . . . . . . . 79
4.2.2 Non-existence of correspondents for completeness . . . . . . . 90
4.2.3 Other truth definitions . . . . . . . . . . . . . . . . . . . . . . 93
4.2.4 Undecidability of the correspondence problem . . . . . . . . . 94
5 Binary quantifiers 95
5.1 Semantics and axiomatizations . . . . . . . . . . . . . . . . . . . . . . 96
5.1.1 Minimal logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
5.1.2 Definability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
5.1.3 Other truth definitions. Correspondence. . . . . . . . . . . . 99
5.2 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
5.2.1 Propositional conditional logic . . . . . . . . . . . . . . . . . . 104
5.2.2 Predicate conditional logic . . . . . . . . . . . . . . . . . . . . 105
5.3 Defeasible reasoning for Bin . . . . . . . . . . . . . . . . . . . . . . . 110
5.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
Samenvatting 115
Bibliography 117
Index 121