Certifying Proofs in the First-Order Theory of Rewriting

The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present , a reincarnation of the decision tool with certifiable output, and the formally verified certifier .

DECIDABILITY FOR THEORIES OF MODULES OVER VALUATION DOMAINS

Extending work of Puninski, Puninskaya and Toffalori in [5], we show that if V is an effectively given valuation domain then the theory of all V-modules is decidable if and only if there exists an algorithm which, given a, b ε V, answers whether a ε rad(bV). This was conjectured in [5] for valuation domains with dense value group, where it was proved for valuation domains with dense archimedean value group. The only ingredient missing from [5] to extend the result to valuation domains with dense value group or infinite residue field is an algorithm which decides inclusion for finite unions of Ziegler open sets. We go on to give an example of a valuation domain with infinite Krull dimension, which has decidable theory of modules with respect to one effective presentation and undecidable theory of modules with respect to another. We show that for this to occur infinite Krull dimension is necessary.

Classifying model-theoretic properties

In 2004 Csima, Hirschfeldt, Knight, and Soare [1] showed that a set A ≤T 0′ is nonlow2 if and only if A is prime bounding, i.e., for every complete atomic decidable theory T, there is a prime model computable in A. The authors presented nine seemingly unrelated predicates of a set A, and showed that they are equivalent for sets. Some of these predicates, such as prime bounding, and others involving equivalence structures and abelian p-groups come from model theory, while others involving meeting dense sets in trees and escaping a given function come from pure computability theory.As predicates of A, the original nine properties are equivalent for sets; however, they are not equivalent in general. This article examines the (degree-theoretic) relationship between the nine properties. We show that the nine properties fall into three classes, each of which consists of several equivalent properties. We also investigate the relationship between the three classes, by determining whether or not any of the predicates in one class implies a predicate in another class.

The degree spectra of homogeneous models

Much previous study has been done on the degree spectra of prime models of a complete atomic decidable theory. Here we study the analogous questions for homogeneous models. We say a countable model has a d-basis if the types realized in are all computable and the Turing degree d can list -indices for all types realized in . We say has a d-decidable copy if there exists a model ≅ such that the elementary diagram of is d-computable. Goncharov, Millar, and Peretyat'kin independently showed there exists a homogeneous with a 0-basis but no decidable copy.We prove that any homogeneous with a 0′-basis has a low decidable copy. This implies Csima's analogous result for prime models. In the case where all types of the theory T are computable and is a homogeneous model with a 0-basis, we show has copies decidable in every nonzero degree. A degree d is 0-homogeneous bounding if any automorphically nontrivial homogeneous with a 0-basis has a d-decidable copy. We show that the nonlow2 degrees are 0-homogeneous bounding.

Complexity, decidability and completeness

We give resource bounded versions of the Completeness Theorem for propositional and predicate logic. For example, it is well known that every computable consistent propositional theory has a computable complete consistent extension. We show that, when length is measured relative to the binary representation of natural numbers and formulas, every polynomial time decidable propositional theory has an exponential time (EXPTIME) complete consistent extension whereas there is a nondeterministic polynomial time (NP) decidable theory which has no polynomial time complete consistent extension when length is measured relative to the binary representation of natural numbers and formulas. It is well known that a propositional theory is axiomatizable (respectively decidable) if and only if it may be represented as the set of infinite paths through a computable tree (respectively a computable tree with no dead ends). We show that any polynomial time decidable theory may be represented as the set of paths through a polynomial time decidable tree. On the other hand, the statement that every polynomial time decidable tree represents the set of complete consistent extensions of some theory which is polynomial time decidable, relative to the tally representation of natural numbers and formulas, is equivalent to P = NP. For predicate logic, we develop a complexity theoretic version of the Henkin construction to prove a complexity theoretic version of the Completeness Theorem. Our results imply that that any polynomial space decidable theory Δ possesses a polynomial space computable model which is exponential space decidable and thus Δ has an exponential space complete consistent extension. Similar results are obtained for other notions of complexity.

Elimination theory for addition and the frobenius map in polynomial rings

We develop an elimination theory for addition and the Frobenius map over rings of polynomials. As a consequence we show that if F is a countable, recursive and perfect field of positive characteristic p, with decidable theory, then the structure of addition, the Frobenius map x → xp and the property ‘x ∈ F1, over the ring of polynomials F[T], has a decidable theory.

Degree spectra of prime models

We consider the Turing degrees of prime models of complete decidable theories. In particular we show that every complete decidable atomic theory has a prime model whose elementary diagram is low. We combine the construction used in the proof with other constructions to show that complete decidable atomic theories have low prime models with added properties.If we have a complete decidable atomic theory with all types of the theory computable, we show that for every degree d with 0 < d < 0', there is a prime model with elementary diagram of degree d. Indeed, this is a corollary of the fact that if T is a complete decidable theory and L is a computable set of c.e. partial types of T, then for any degree d > 0, T has a d-decidable model omitting the nonprincipal types listed by L.