The Decision Problem for Logic of Predicates and Operations

The article consists of two chapters. In the first part of the first chapter, the author rediscovers well-partial-orderings and well-quasi-orderings, which he calls tight partial orders and tight quasi orders, and develops a theory of such orderings. (In this connection, it may be appropriate to point out Joseph B. Kruskal’s article “The theory of well-quasi-ordering: A frequently discoverred concept” in J. Comb. Theory A, vol. 13 (1972), 297-305.) To understand the idea behind the term “tight”, think of a boot: you cannot move your foot far down or sidewise — only up. This is similar to tight partial orders where infinite sequences have no infinite descending subsequences, no infinite antichains, but always have infinite ascending subsequences.

In the second part of the first chapter, the author applies the theory of tight orders to prove a classifiability theorem for prefix-vocabulary classes of first-order logic. The main part of the classifiability theorem is that the partial order of prefix-vocabulary classes (ordered by inclusion) is tight. But there is an additional useful part of the classifiability theorem, about the form of the minimal classes outside a downward closed collection, e.g. the minimal classes that are undecidable in one way or another.

In the second chapter, the author completes the decision problem for (the prefix-vocabulary fragments of) pure logic of predicates and functions, though the treatment of the most difficult decidable class is deferred to 18 (opens in new tab). In particular, the classes [∀²,(0,1),(1)] and [∀²,(1),(0,1)] are proved to be conservative reduction classes. (This abstract is written in January 2006.)