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

, & (eds.)
Cham, Switzerland: Springer Verlag (2020)
  Copy   BIBTEX

Abstract

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.

Categories

Add categories

Keywords

Reprint years

ISBN(s)

3030302288   9783030302283   9783030302290   3030302318

DOI

10.1007/978-3-030-30229-0
View all bargains

Buy this book

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,322

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Chapters

Well Quasi-orders and the Functional Interpretation

The purpose of this article is to study the role of Gödel’s functional interpretation in the extraction of programs from proofs in well quasi-order theory. The main focus is on the interpretation of Nash–Williams’ famous minimal bad sequence construction, and the exploration of a number of much broa... see more

The Reverse Mathematics of wqos and bqos

In this paper we survey wqo and bqo theory from the reverse mathematics perspective. We consider both elementary results and more advanced theorems. The classification from the reverse mathematics viewpoint of both kinds of results provides interesting challenges, and we cover also recent advances o... see more

Recent Progress on Well-Quasi-ordering Graphs

Graphs are arguably the first objects studied in the field of well-quasi-ordering. Giant successes in research on well-quasi-ordering graphs and fruitful extensions of them have been obtained since Vázsonyi proposed the conjecture about well-quasi-ordering trees by the topological minor relation in ... see more

Upper Bounds on the Graph Minor Theorem

Lower bounds on the proof-theoretic strength of the graph minor theorem were found over 30 years ago by Friedman, Robertson and Seymour , but upper bounds have always been elusive. We present recently found upper bounds on the graph minor theorem and other theorems appearing in the Graph Minors seri... see more

Well Quasi-orderings and Roots of Polynomials in a Hahn Field

Let G be a divisible ordered Abelian group, and let K be a field. The Hahn fieldK) is a field of formal power series, with terms corresponding to elements in a well ordered subset of G and the coefficients coming from K. Ideas going back to Newton show that if K is either algebraically closed of cha... see more

Strong WQO Tree Theorems

Ordinal labeled finite trees are well-quasi-ordered by homeomorphic embeddability with sound gap-conditions. Such strong generalizations of Harvey Friedman’s tree theorem on trees whose vertices are labeled by bounded natural numbers are provable in second-order arithmetic \documentclass[12pt]{minim... see more

The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings

Elegant and general algorithms for handling upwards-closed and downwards-closed subsets of WQOs can be developed using the filter-based and ideal-based representation for these sets. These algorithms can be built in a generic or parameterized way, in parallel with the way complex WQOs are obtained b... see more

On Ordinal Invariants in Well Quasi Orders and Finite Antichain Orders

We investigate the ordinal invariants height, length, and width of well quasi orders , with particular emphasis on width, an invariant of interest for the larger class of orders with finite antichain condition . We show that the width in the class of FAC orders is completely determined by the width ... see more

Well, Better and In-Between

Starting from well-quasi-orders , we motivate step by step the introduction of the complicated notion of better-quasi-order . We then discuss the equivalence between the two main approaches to defining bqo and state several essential results of bqo theory. After recalling the rôle played by the idea... see more

Well-Partial Orderings and their Maximal Order Types

Combinatorial theorists have for some time been showing that certain partial orderings are well-partial-orderings . De Jongh and Parikh showed that w.p.o.’s are just those well-founded partial orderings which can be extended to a well-ordering of maximal order type; we call the ordinal thus obtained... see more

A Mechanized Proof of Higman’s Lemma by Open Induction

I present a short, mechanically checked Isabelle/HOL formalization of Higman’s lemma by open induction.

A Combinatorial Bound for a Restricted Form of the Termination Theorem

We present a combinatorial bound for the H-bounded version of the Termination Theorem. As a consequence we improve the result by Solovay and Ketonen on the relationship between the Paris–Harrington Theorem and the Fast Growing Hierarchy.

Well-Quasi Orders and Hierarchy Theory

We discuss some applications of WQOs to several fields were hierarchies and reducibilities are the principal classification tools, notably to Descriptive Set Theory, Computability theory and Automata Theory. While the classical hierarchies of sets usually degenerate to structures very close to ordin... see more

Similar books and articles

Languages, machines, and classical computation.Luis M. Augusto - 2021 - London, UK: College Publications.
Languages, Meta-languages and METATEM, A Discussion Paper.Howard Barringer, Graham Gough, Derek Brough, Dov Gabbay & Ian Hodkinson - 1996 - Logic Journal of the IGPL 4 (2):255-272.
A mathematical theory of truth and an application to the regress problem.S. Heikkilä - forthcoming - Nonlinear Studies 22 (2).
Logic and computation: interactive proof with Cambridge LCF.Lawrence C. Paulson - 1987 - New York: Cambridge University Press.
Computability, complexity, logic.Egon Börger - 1989 - New York, N.Y., U.S.A.: Elsevier Science Pub. Co..
Automata for Epistemic Temporal Logic with Synchronous Communication.Swarup Mohalik & R. Ramanujam - 2010 - Journal of Logic, Language and Information 19 (4):451-484.
Corrado Böhm and Wolf Gross. Introduction to the CUCH. Automata theory, edited by E. R. Caianiello, Academic Press, New York and London1966, pp. 35–65. Reprinted in Pubblicazioni dell'Istituto Nazionale per le Applicazioni del Calcolo, ser. 11 no. 669, Rome 1966. - C. Böhm. The CUCH as a formal and description language. Formal language description languages for computer programming, Proceedings of the IFIP Working Conference on Formal Language Description Languages, edited by T. B. SteelJr., North-Holland Publishing Company, Amsterdam1966, pp. 179–197. [REVIEW]Jonathan P. Seldin - 1975 - Journal of Symbolic Logic 40 (1):81-83.
On Relation Between Linear Temporal Logic and Quantum Finite Automata.Amandeep Singh Bhatia & Ajay Kumar - 2020 - Journal of Logic, Language and Information 29 (2):109-120.
A Poor Concept Script.Hartley Slater - 2004 - Australasian Journal of Logic 2:44-55.
Elements of the Theory of Computation.Harry R. Lewis & Christos H. Papadimitriou - 1984 - Journal of Symbolic Logic 49 (3):989-990.
Three Conceptions of Formal Logic.Thom Paul - 2010 - Vivarium 48 (1-2):228-242.
A Note on the Relation Between Formal and Informal Proof.Jörgen Sjögren - 2010 - Acta Analytica 25 (4):447-458.
Descriptive complexity theories.Joerg Flum - 2003 - Theoria 18 (1):47-58.
Remarks on the Theory of Quasi-sets.Steven French & Décio Krause - 2010 - Studia Logica 95 (1-2):101 - 124.
forall x: An introduction to formal logic.P. D. Magnus - 2005 - Victoria, BC, Canada: State University of New York Oer Services.

Analytics

Added to PP
2020-04-10

Downloads
11 (#1,105,752)

6 months
5 (#652,053)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Peter Schuster
University of Leeds

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references