Well-Quasi Orders in Computation, Logic, Language and Reasoning: A Unifying Concept of Proof Theory, Automata Theory, Formal Languages and Descriptive Set Theory (Trends in Logic)

Description

This book bridges the gaps between logic, mathematics and computer science by delving into the theory of well-quasi orders, also known as wqos. This highly active branch of combinatorics is deeply rooted in and between many fields of mathematics and logic, including proof theory, commutative algebra, braid groups, graph theory, analytic combinatorics, theory of relations, reverse mathematics and subrecursive hierarchies. As a unifying concept for slick finiteness or termination proofs, wqos have been rediscovered in diverse contexts, and proven to be extremely useful in computer science.  The book introduces readers to the many facets of, and recent developments in, wqos through chapters contributed by scholars from various fields. As such, it offers a valuable asset for logicians, mathematicians and computer scientists, as well as scholars and students. Preface Contents Editors and Contributors Well, Better and In-Between 1 Well Is Not Good Enough 2 Super-Sequences Versus Multi-sequences 2.1 The Ordinal Rank 2.2 Sub-fronts 2.3 A Ramsey Property for Fronts: Nash-Williams's Theorem 2.4 Continuous Definition: Multi-sequences 3 Well, Here Is Better! 3.1 Two Equivalent Definitions 3.2 First Examples and Finite Stability 3.3 The Real Deal: Infinite Stability 4 In-Between: An Intractable Diversity of Inconspicuous Orders 5 Classes of Bqos Definable by Forbidden Pattern 5.1 Interval Orders 5.2 More Classes of Better-Quasi-orders via Forbidden Patterns References On Ordinal Invariants in Well Quasi Orders and Finite Antichain Orders 1 Introduction 2 Background and Basic Results 2.1 Posets and Quasi-orders 2.2 Rankings and Well-Founded Trees 2.3 Residual Characterisation 2.4 Games for WQO Invariants 2.5 Cardinal Invariants 2.6 WPOs as a Basis for FAC Posets 3 Characterisations of Ordinal Invariants 3.1 Height and Maximal Chains 3.2 Maximal Order Types and Linearisations 3.3 Maximal Order Types and Height of Downwards-Closed Sets 3.4 Width and Antichain Rank 3.5 Relationship Between Width, Height and Maximal Order Type 4 Computing the Invariants of Common WQOs 4.1 Lexicographic Sums 4.2 Disjoint Sums 4.3 Direct Products 4.4 Cartesian Products 4.5 Finite Multisets, Sequences, and Trees 4.6 Infinite Products and Rado's Structure 5 Concluding Remarks References The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings 1 Introduction 2 Well-Quasi-orderings, Ideals, and Some Motivations 2.1 Two Motivating Examples 2.2 What About Downwards-Closed Subsets? 2.3 Well-Quasi-orders 2.4 Canonical Prime Decompositions of Closed Subsets 2.5 Filter Decompositions and Ideal Decompositions 3 Ideally Effective WQOs 3.1 Some First Ideally Effective WQOs 4 Constructing Ideally Effective WQOs 4.1 Ideally Effective WQO Constructors 4.2 Sums of WQOs 4.3 Products of WQOs and Dickson's Lemma 4.4 Sequence Extensions of WQOs and Higman's Lemma 4.5 Finitary Powersets 5 More Constructions on Ideally Effective WQOs 5.1 Order Extension 5.2 Quotienting Under a Compatible Equivalence 5.3 Induced WQOs 6 Towards a Richer Theory of Ideally Effective WQOs 6.1 A Minimal Definition 6.2 On Alternative Effectiveness Assumptions 6.3 On Computational Complexity 7 Concluding Remarks References Strong WQO Tree Theorems 1 Introduction 2 Labeling Trees with Ordinals 2.1 Basic Notations 2.2 Vertex-Labeled Trees 2.3 Edge-Labeled Trees 2.4 Complex Edge-Labeled Trees 2.5 Main Propositions 3 Proof of Proposition C. Part 1 3.1 Basic Definitions and Notations 3.2 Basic Observations 4 Proof of Proposition C. Part 2 4.1 Proof of Theorem 18. Part 1 (Construction) 4.2 Proof of Theorem 18. Part 2 (Soundness) 4.3 Formalization 5 Proof of Proposition D References Well Quasi-orderings and Roots of Polynomials in a Hahn Field 1 Introduction 2 Hahn Fields 3 Well Quasi-orderings and Hahn Fields 3.1 Background on Well Quasi-orderings 3.2 Sums and Products 4 Roots of Polynomials 4.1 Support of a Root 4.2 Lengths of Roots 5 More on Our Original Motivation 5.1 Integer Parts and the Work of Mourgues and Ressayre 5.2 Bounds on Lengths of Elements of Special Subfields 5.3 Complexity References Upper Bounds on the Graph Minor Theorem 1 Introduction 2 Well-Quasi-ordering Theorems of the Graph Minors Series 3 Bar Induction in the Graph Minors Series 4 Possible Lower Bound Improvements References Recent Progress on Well-Quasi-ordering Graphs 1 Introduction 2 Topological Minors 2.1 Directed Graphs 3 Minors 3.1 Directed Minors 3.2 Induced Minors 3.3 Vertex-Minors and Pivot-Minors 4 Immersions 4.1 Directed Graphs 5 Subgraphs 5.1 Subdigraphs 5.2 Induced Subgraphs 5.3 Rao-Containments References The Reverse Mathematics of wqos and bqos 1 Reverse Mathematics 2 Characterizations and Basic Properties of wqos 3 Characterizations and Basic Properties of bqos 4 Minimality Arguments 5 Structural Results 6 Major Theorems About wqos and bqos 7 A Topological Version of wqos References Well Quasi-orders and the Functional Interpretation 1 Introduction 1.1 Proof Interpretations and Well Quasi-Orders: A Brief History 1.2 The Origins and Purpose of This Chapter 2 Well Quasi-orders and Zorn's Lemma 2.1 The Minimal Bad Sequence Construction and Zorn's Lemma 2.2 Zorn's Lemma as an Axiom 3 A Formal Proof of Higman's Lemma 3.1 The Logical System 3.2 The Formal Proof 4 Gödel's Functional Interpretation 4.1 The Basics 4.2 The Programming Language 4.3 The Interpretation 4.4 The Meaning of the Interpretation 5 Interpreting the Proof of WQOseq(=B) 5.1 The Law of Excluded-Middle for Σ02 Formulas 5.2 Interpreting (forallx)(b)(foralln)(kn)(xk=b) 5.3 Simplifying the Realizing Term 5.4 The Final Step 5.5 Summary 6 The Functional Interpretation of ZLlex—Part 1 6.1 A Rough Idea 6.2 Learning Procedures 7 Recursion over rhdlex in the Continuous Functionals 7.1 The Problem with Recursion over rhdlex 7.2 The Continuous Functionals and Berger's Open Recursor 7.3 The Explicitly Controlled Open Recursor 8 The Functional Interpretation of ZLlex—Part 2 9 Interpreting the Proof of WQO(=B,ast) 10 Conclusion References Well-Quasi Orders and Hierarchy Theory 1 Introduction 2 Preliminaries 2.1 Ordinals 2.2 Partial Orders and Quasiorders 2.3 Topological Spaces 2.4 Classical Hierarchies in Quasi-Polish Spaces 2.5 Wadge Hierarchy 3 Well and Better Quasiorders 3.1 Well Quasiorders 3.2 Better Quasiorders 3.3 Computable Well Partial Orders 3.4 Definability and Decidability Issues 4 Wadge-Like Reducibilities in Quasi-Polish Spaces 4.1 Wadge-Like Reducibilities in the Baire Space 4.2 Wadge Reducibility of k-Partitions in the Baire Space 4.3 Wadge Reducibility in Quasi-Polish Spaces 4.4 Weak Homeomorphisms Between Quasi-Polish Spaces 4.5 Weak Reducibilities in Quasi-Polish Spaces 5 Other Reducibilities and Hierarchies 5.1 Borel Reducibility of Borel Equivalence Relations 5.2 Continuous Reducibility of Borel Equivalence Relations 5.3 Hierarchies and Reducibilities of Functions 5.4 Definability and Decidability Issues 6 Hierarchies in Quasi-Polish Spaces 6.1 Hierarchies of Sets 6.2 Hierarchies of k-Partitions 6.3 Hierarchies of Sets in Quasi-Polish Spaces 6.4 Hierarchies of k-Partitions in Quasi-Polish Spaces 7 Hierarchies in Computability Theory 7.1 Preliminaries 7.2 Difference Hierarchies of Sets and k-Partitions 7.3 Fine Hierarchies of Sets and k-Partitions 7.4 Natural Degrees 8 Hierarchies in Automata Theory 8.1 Preliminaries 8.2 Well Quasiorders and Regular Languages 8.3 Hierarchies of Regular Languages 8.4 Hierarchies of ω-Regular Languages and k-Partitions 9 Conclusion References A Combinatorial Bound for a Restricted Form of the Termination Theorem 1 Introduction 2 Background Material 2.1 Fast Growing Hierarchy 2.2 Paris–Harrington Theorem 2.3 Restricted Forms of the Termination Theorem 2.4 Erdős' Trees 3 Main Result 3.1 Proof of the Two-Relations Case 3.2 Proof of the (k+1)-Relations Case 3.3 Complexity 4 Conclusion References A Mechanized Proof of Higman's Lemma by Open Induction 1 Introduction 2 Preliminaries 3 From Minimal Counterexamples to Open Induction 4 Setting the Stage: An Open Property and an Appropriate Order 5 The Proof via Open Induction 6 Conclusions and Future Work References Well-Partial Orderings and their Maximal Order Types 1 Introduction 2 Preliminaries 2.1 Well-Quasi-Orderings – Definitions and Results 2.2 Sequences and Trees Over a q.o. Set 2.3 Systems of Notations for Ordinals 3 The Maximal Order Types of Some Well-Quasi-Ordered Sets of Sequences and Trees 3.1 The Set of all leqslant n-Branching Finite Structured Trees with Labels in a w.q.o. Set 3.2 The Set of All Finite Structured Trees with Labels in a w.q.o. Set 3.3 Finitary Sequences of Elements of a w.q.o. Set 4 Applications of the Results in Sect. 3 4.1 Monotonic Increasing Ordinal Functions 4.2 X-Monotonic Increasing Ordinal Functions 4.3 Possible Connections with Proof Theory References