The Classical Decision Problem

Cover ......Page 1
Preface to the Series ......Page 6
Preface ......Page 8
Table of contents ......Page 10
1.1 The Original Problem ......Page 14
1.2 The Transformation of the Classical Decision Problem ......Page 18
1.3 What Is and What Isn’t in this Book ......Page 21
Part I. Undecidable Classes ......Page 28
2. Reductions ......Page 30
2.1.1 The Church-Turing Theorem and Reduction Classes ......Page 31
2.1.2 Trakhtenbrot’s Theorem and Conservative Reductions ......Page 46
2.1.3 Inseparability and Model Complexity ......Page 51
2.2 Logic and Complexity ......Page 56
2.2.1 Propositional Satisfiability ......Page 57
2.2.2 The Spectrum Problem and Fagin’s Theorem ......Page 61
2.2.3 Capturing Complexity Classes ......Page 70
2.2.4 A Decidable Prefix-Vocabulary Class ......Page 79
2.3.1 The Problem ......Page 83
2.3.2 Well Partially Ordered Sets ......Page 84
2.3.3 The Well Quasi Ordering of Prefix Sets ......Page 87
2.3.4 The Well Quasi Ordering of Arity Sequences ......Page 90
2.3.5 The Classifiability of Prefix-Vocabulary Sets ......Page 91
2.4 Historical Remarks ......Page 94
3. Undecidable Standard Classes for Pure Predicate Logic ......Page 98
3.1.1 Domino Problems ......Page 100
3.1.2 Formalization of Domino Problems by [AEA,(0,w)]-Formulae ......Page 104
3.1.3 Graph Interpretation of [AEA,(0,w)]-Formulae ......Page 111
3.1.4 The Remaining Cases without E* ......Page 122
3.2 Existential Interpretation for [AAAE*,(0,1)] ......Page 128
3.3.1 The Proof Strategy ......Page 137
3.3.2 Reduction to Diagonal-Freeness ......Page 143
3.3.3 Reduction to Shift-Reduced Form ......Page 144
3.3.4 Reduction to Fi-Elimination Form ......Page 148
3.3.5 Elimination of Monadic Fi ......Page 150
3.3.6 The Kostyrko-Genenz and Suranyi Classes ......Page 156
3.4 Historical Remarks ......Page 159
4. Undecidable Standard Classes with Functions or Equality ......Page 162
4.1 Classes with Functions and Equality ......Page 163
4.2 Classes with Functions but without Equality ......Page 172
4.3 Classes with Equality but without Functions: the Goldfarb Classes ......Page 174
4.3.1 Formalization of Natural Numbers in [AAE*,(w,w),(0)]= ......Page 176
4.3.2 Using Only One Existential Quantifier ......Page 184
4.3.3 Encoding the Non-Auxiliary Binary Predicates ......Page 191
4.3.4 Encoding the Auxiliary Binary Predicates of NUM* ......Page 199
4.4 Historical Remarks ......Page 201
5. Other Undecidable Cases ......Page 202
5.1.1 Krom Prefix Classes without Functions or Equality ......Page 203
5.1.2 Krom Prefix Classes with Functions or Equality ......Page 211
5.2 Few Atomic Subformulae ......Page 216
5.2.1 Few Function and Equality Free Atoms ......Page 218
5.2.2 Few Equalities and Inequalities ......Page 223
5.2.3 Horn Clause Programs With One Krom Rule ......Page 229
5.3 Undecidable Logics with Two Variables ......Page 232
5.3.1 First-Order Logic with the Choice Operator ......Page 233
5.3.2 Two-Variable Logic with Cardinality Comparison ......Page 236
5.4 Conjunctions of Prefix-Vocabulary Classes ......Page 240
5.4.2 Another Classifiability Theorem ......Page 241
5.4.3 Some Results and Open Problems ......Page 242
5.5 Historical Remarks ......Page 246
Part II. Decidable Classes and Their Complexity ......Page 250
6. Standard Classes with the Finite Model Property ......Page 252
6.1.1 Domino Problems Revisited ......Page 255
6.1.2 Succinct Descriptions of Inputs ......Page 260
6.2.1 Monadic Formulae ......Page 262
6.2.2 The Bernays-Schonfinkel-Ramsey Class ......Page 270
6.2.3 The Godel-Kalmar-Schiitte Class: a Probabilistic Proof ......Page 274
6.3 Formulae with One A ......Page 283
6.3.1 A Satisfiability Test for [E*AE*, all, all] ......Page 284
6.3.2 The Ackermann Class ......Page 294
6.3.3 The Ackermann Class with Equality ......Page 298
6.4.1 The Relational Classes in P, NP and Co-NP ......Page 303
6.4.2 Fragments of the Theory of One Unary Function ......Page 308
6.4.3 Other Functional Classes ......Page 317
6.5 Finite Model Property vs. Infinity Axioms ......Page 319
6.6 Historical Remarks ......Page 323
7. Monadic Theories and Decidable Standard Classes with Infinity Axioms ......Page 328
7.1.1 Monadic Theories ......Page 329
7.1.2 Automata on Infinite Words and the Monadic Theory of One Successor ......Page 331
7.1.3 Tree Automata, Rabin’s Theorem and Forgetful Determinacy ......Page 336
7.1.4 The Forgetful Determinacy Theorem for Graph Games ......Page 342
7.2 The Monadic Second-Order Theory of One Unary Function ......Page 350
7.2.1 Decidability Results for One Unary Function ......Page 351
7.2.2 The Theory of One Unary Function is not Elementary Recursive ......Page 354
7.3.1 Algebras with One Unary Operation ......Page 358
7.3.2 Canonic Sentences ......Page 361
7.3.3 Terminology and Notation ......Page 364
7.3.4 1-Satisfiability ......Page 367
7.3.5 2-Satisfiability ......Page 370
7.3.6 Refinements ......Page 372
7.3.7 Villages ......Page 373
7.3.8 Contraction ......Page 378
7.3.9 Towns ......Page 382
7.3.10  The Final Reduction ......Page 383
7.4 Historical Remarks ......Page 387
8.1 First-Order Logic with Two Variables ......Page 390
8.2.1 Unification ......Page 395
8.2.2 Herbrand Formulae ......Page 400
8.2.3 Positive First-Order Logic ......Page 401
8.3.1 The Chain Criterion ......Page 403
8.3.2 The Aanderaa-Lewis Class ......Page 406
8.3.3 The Maslov Class ......Page 413
8.4 Historical Remarks ......Page 417
A.1 Introduction ......Page 420
A.2 The Origin Constrained Domino Problem ......Page 421
A.3 Robinson’s Aperiodic Tile Set ......Page 423
A.4 The Unconstrained Domino Problem ......Page 427
A.5 The Periodic Problem and the Inseparability Result ......Page 432
Annotated Bibliography ......Page 434
Index ......Page 490