Modal Quantifiers [PhD Thesis]

This is a PhD Thesis written under supervision of Prof.dr. J. F. A. K. van Benthem. 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