Franz Baader and Ralf K¨usters
Nonstandard Inferences in Description Logics:
The Story So Far . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2
2. Description Logics and Standard Inferences . . . . . . . . . . . . . . . . . . .6
3. Nonstandard Inferences—Motivation and Definitions . . . . . . . . 11
3.1. Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12
3.2. Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
3.3. Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .21
4. A Structural Characterization of Subsumption . . . . . . . . . . . . . . 23
4.1. Getting started — The characterization for EL . . . . . . . . . . 24
4.2. Extending the characterization to ALE . . . . . . . . . . . . . . . . . .27
4.3. Characterization of subsumption for other DLs . . . . . . . . . . 31
5. The Least Common Subsumer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5.1. The LCS for EL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5.2. The LCS for ALE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .34
5.3. The LCS for other DLs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6. The Most Specific Concept . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .36
6.1. Existence and approximation of the MSC . . . . . . . . . . . . . . . 36
6.2. The most specific concept in the presence of cyclic
TBoxes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .44
7. Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
7.1. The minimal rewriting decision problem . . . . . . . . . . . . . . . . .45
7.2. The minimal rewriting computation problem . . . . . . . . . . . . 46
xxiv Content
7.3. Approximation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .52
8. Matching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
8.1. Deciding matching problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
8.2. Solutions of matching problems . . . . . . . . . . . . . . . . . . . . . . . . . 55
8.3. Computing matchers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
8.4. Matching in other DLs and extensions of matching . . . . . . 64
9. Conclusion and Future Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . 64
10. References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
Lev Beklemishev and Albert Visser
Problems in the Logic of Provability . . . . . . . . . . . . . . . . . . . . . . . . . 77
1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
2. Informal Concepts of Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .81
2.1. Formal and informal provability and
the problem of equivalence of proofs . . . . . . . . . . . . . . . . . . . . . . . 81
2.2. Strengthening Hilbert’s thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
2.3. Coordinate-free proof theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
3. Basics of Provability Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
4.Provability Logic for Intuitionistic Arithmetic . . . . . . . . . . . . . . . . 93
4.1. Propositional logics of arithmetical theories . . . . . . . . . . . . . 94
4.2. Admissible rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
4.3. The provability logic of HA and related theories . . . . . . . . 100
5. Provability Logic and Bounded Arithmetic . . . . . . . . . . . . . . . . . 102
6. Classification of Bimodal Provability Logics . . . . . . . . . . . . . . . . 106
7. Magari Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
8. Interpretability Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
9. Graded Provability Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
10. List of Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
Johan van Benthem
Open Problems in Logical Dynamics . . . . . . . . . . . . . . . . . . . . . . . .137
Content xxv
1. Logical Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
2. Standard Epistemic Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
2.1. Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
2.2. Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .141
2.3. Basic model theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142
2.4. Axiomatics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143
2.5. Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143
2.6. Open problems, even here . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .144
3. Public Announcement: Epistemic Logic Dynamified . . . . . . . . 144
3.1. World elimination: the system PAL . . . . . . . . . . . . . . . . . . . .145
3.2. What are the real update laws? . . . . . . . . . . . . . . . . . . . . . . . .150
3.3. Model theory of learning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
3.4. Communication and planning . . . . . . . . . . . . . . . . . . . . . . . . . . 155
3.5. Group knowledge . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156
4. Dynamic Epistemic Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157
4.1. Information from arbitrary events: product update . . . . .158
4.2. Update evolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160
4.3. Questions of language design . . . . . . . . . . . . . . . . . . . . . . . . . . .162
4.4. Extensions of empirical coverage . . . . . . . . . . . . . . . . . . . . . . . 163
5. Background in Standard Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164
5.1. Modal logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
5.2. First-order logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .166
5.3. Fixed-point logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .168
6. From Information Update to Belief Revision . . . . . . . . . . . . . . . 170
6.1. From knowledge to belief . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .170
6.2. Dynamic doxastic logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .171
6.3. Better-known theories of belief revision . . . . . . . . . . . . . . . . .175
6.4. Probabilistic update . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
7. Temporal Epistemic logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
7.1. Broader temporal perspectives on update . . . . . . . . . . . . . . 178
7.2. Knowledge and ignorance over time . . . . . . . . . . . . . . . . . . . . 179
7.3. Representation of update logics . . . . . . . . . . . . . . . . . . . . . . . . 181
7.4. Connections with other parts of mathematics . . . . . . . . . . 183
8. Game Logics and Game Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
9. Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .185
References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186
xxvi Content
S Barry Cooper
Computability and Emergence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .193
1. An Emergent World around Us . . . . . . . . . . . . . . . . . . . . . . . . . . . . 194
2. Descriptions, Algorithms, and the Breakdown
of Inductive Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .195
3. Ontology and Mathematical Structure . . . . . . . . . . . . . . . . . . . . . .202
4. Where does It All Start? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .204
5. Towards a Model Based on Algorithmic Content . . . . . . . . . . . 209
6. Levels of Reality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 214
7. Algorithmic Content Revisited . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
8. What Is to Be Done? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224
References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228
John N Crossley
Samsara† . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .233
1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234
1.1. The structure of the paper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234
2. An Example of a Process . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .235
3. What Logics Do We Need? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 236
3.1. Extracting constructions from proofs . . . . . . . . . . . . . . . . . . .242
3.2. The Lambda Calculus and the Curry–Howard
correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .243
3.3. Proofs as types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 245
3.4. Strong normalization and program extraction . . . . . . . . . . 248
3.5. Beyond traditional logic in program extraction . . . . . . . . . 250
3.6. Proofs from programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .256
3.7. Programs then proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257
4. What are Logical Systems and What Should They Be? . . . . .258
4.1. Higher order logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .259
4.2. A note on set theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 261
4.3. Computation and proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 262
† The endless cycle of death and rebirth to which life in the material world is
bound. (OED)
Content xxvii
5. The Nature of Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 262
5.1. The question of scale and the role of technology . . . . . . . . 263
5.2. Foundations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 268
6. Final Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 269
References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 270
Wilfrid Hodges
Two Doors to Open . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 277
1. Logic and Cognitive Science . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .279
1.1. Spatial intuition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 281
1.2. Kurt G¨odel and the choice of representation . . . . . . . . . . . .285
1.3. A sample cognitive description of reasoning . . . . . . . . . . . . 293
1.4. Frege versus Peirce: comparison of representations . . . . . 298
2. Medieval Arabic Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .300
References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 313
Lawrence S Moss
Applied Logic: A Manifesto . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 317
1. What is Applied Logic? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .317
2. Mathematics and Logic, but Different from
Mathematical Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 319
2.1. Mathematical Logic and Mathematics . . . . . . . . . . . . . . . . . .320
2.2. Where applied logic differs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 322
2.3. Applied mathematics is good mathematics . . . . . . . . . . . . . 324
2.4. Applied logic is applied mathematics . . . . . . . . . . . . . . . . . . . 325
3. Applied Philosophical Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .326
3.1. Applied philosophical logic = theoretical AI . . . . . . . . . . . .328
4. What Does Computer Science Have to Do with It? . . . . . . . . .328
4.1. Logic is the calculus of computer science . . . . . . . . . . . . . . . 329
4.2. Computer science motivates logic . . . . . . . . . . . . . . . . . . . . . . 330
4.3. Going beyond the traditional boundaries of logic . . . . . . . 331
5. Other Case Studies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 332
5.1. Neural networks and non-monotonic logic . . . . . . . . . . . . . . 332
xxviii Content
5.2. Dynamic epistemic logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 333
5.3. Linguistics, logic, and mathematics . . . . . . . . . . . . . . . . . . . . .335
5.4. But is it dead? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 339
6. Being as catholic as Possible . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 341
References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 343
Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 345