Indiscernibles and decidable models

1983 ◽  
Vol 48 (1) ◽  
pp. 21-32 ◽  
Author(s):  
H. A. Kierstead ◽  
J. B. Remmel
Keyword(s):  
Order Theory ◽  
Stable Theory ◽  
Categorical Theory ◽  
Large Classes ◽  
Decidable Theory ◽  
First Order Theory ◽  
Decidable Model ◽  
Decidable Theories ◽  
Basic Facts ◽  
Infinite Set

Ehrenfeucht and Mostowski [3] introduced the notion of indiscernibles and proved that every first order theory has a model with an infinite set of order indiscernibles. Since their work, techniques involving indiscernibles have proved to be extremely useful for constructing models with various specialized properties. In this paper and in a sequel [5], we investigate the effective content of Ehrenfeucht's and Mostowski's result. In this paper we consider the question of which decidable theories have decidable models with infinite recursive sets of indiscernibles. In §1, using some basic facts from stability theory, we show that certain large classes of decidable theories have decidable models with infinite recursive sets of indiscernibles. For example, we show that every ω-stable decidable theory and every stable theory which possesses a certain strong decidability property called ∃Q-decidability have such models. In §2 we construct several examples of decidable theories which have no decidable models with infinite recursive sets of indiscernibles. These examples show that our hypothesis for our positive results in §1 are necessary. Finally in §3 we give two applications of our results. First as an easy application of our results in §1, we show that every ω-stable decidable theory has uncountable models which realize only recursive types. Also our counterexamples in §2 allow us to answer negatively two questions of Baldwin and Kueker [1] concerning the effectiveness of their elimination of Ramsey quantifiers for certain theories.In [5], we show that in general the problem of finding an infinite set of indiscernibles in a decidable model is recursively equivalent to finding a path through a recursive infinite branching tree. Similarly, we show that the problem of finding an co-type of a set of indiscernibles in a decidable ω-categorical theory is recursively equivalent to finding a path through a highly recursive finitely branching tree.

Theories with recursive models

1979 ◽  
Vol 44 (1) ◽  
pp. 59-76 ◽  
Author(s):  
Manuel Lerman ◽  
James H. Schmerl
Keyword(s):  
Existential Quantifier ◽  
Categorical Theory ◽  
Recursive Model ◽  
Recursive Models ◽  
Decidable Theory ◽  
Decidable Model

A structure is recursive if the set of quantifier-free sentences in the complete diagram ⊿() of is recursive. It has been known for some time that every decidable theory has a recursive model. In fact, every decidable theory has a decidable model (that is a model such that ⊿() is recursive). In this paper we find other conditions which imply that a theory have a recursive model.In §1 we study the relation between an ℵ0-categorical theory T having a recursive model and the complexity of the quantificational hierarchy of that theory. We let ∃0 denote the set of quantifier-free sentences, and let ∃n÷1 denote the set of sentences beginning with an existential quantifier and having n alternations of quantifiers. (∀n is defined analogously.) Then we show that if T is an arithmetical ℵ0-categorical theory such that T ⋂ ∃n÷2 is Σn÷10 for each n < ω, then T has a recursive model. We show that this is a best possible result by giving an example of a ⊿n÷20 ℵ0-categorical theory T such that T ⋂ ∃n÷1 is recursive yet T has no recursive model.In §2 we consider the theory of trees. Ershov [1] had proved that every Σ10 theory of trees has a recursive model. We show this to be best possible by giving an example of a ⊿20 theory of trees which has no recursive model.

Categoricity and the natural numbers

2018 ◽  
Author(s):  
Tim Button ◽  
Sean Walsh
Keyword(s):  
Order Theory ◽  
Second Order ◽  
Order Logic ◽  
Natural Numbers ◽  
Categorical Theory ◽  
First Order Theory ◽  
Standard Models ◽  
Skolem Theorem ◽  
Infinite Model ◽  
Second Order Logic

This chapter focuses on modelists who want to pin down the isomorphism type of the natural numbers. This aim immediately runs into two technical barriers: the Compactness Theorem and the Löwenheim-Skolem Theorem (the latter is proven in the appendix to this chapter). These results show that no first-order theory with an infinite model can be categorical; all such theories have non-standard models. Other logics, such as second-order logic with its full semantics, are not so expressively limited. Indeed, Dedekind's Categoricity Theorem tells us that all full models of the Peano axioms are isomorphic. However, it is a subtle philosophical question, whether one is entitled to invoke the full semantics for second-order logic — there are at least four distinct attitudes which one can adopt to these categoricity result — but moderate modelists are unable to invoke the full semantics, or indeed any other logic with a categorical theory of arithmetic.

Countable homogeneous relational structures and ℵ0-categorical theories

1972 ◽  
Vol 37 (3) ◽  
pp. 494-500 ◽  
Author(s):  
C. Ward Henson
Keyword(s):  
Order Theory ◽  
Linear Ordering ◽  
Categorical Theory ◽  
Symmetric Relation ◽  
First Order ◽  
Relational Structures ◽  
First Order Theory ◽  
Partial Orderings ◽  
Homogeneous Structures ◽  
Binary Relation Symbol

A relational structure of cardinality ℵ0 is called homogeneous by Fraissé [1] if each isomorphism between finite substructures of can be extended to an automorphism of . In §1 of this paper it is shown that there are isomorphism types of such structures for the first order language L0 with a single (binary) relation symbol, answering a question raised by Fraissé. In fact, as is shown in §2, a family of nonisomorphic homogeneous structures for L0 can be constructed, each member of which satisfies the following conditions (where U is the homogeneous, ℵ0-universal graph, the structure of which is considered in [4]):(i) The relation R of is asymmetric (R ∩ R−1 = ∅);(ii) If A is the domain of and S is the symmetric relation R ∪ R−1, then (A, S) is isomorphic to U. That is, each may be regarded as the result of assigning a unique direction to each edge of the graph U.Let T0 be the first order theory of all homogeneous structures for L0 which have cardinality ℵ0. In §3 (which can be read independently of §2) it is shown that T0 has complete extensions (in L0), each of which is ℵ0-categorical. Moreover, among the complete extensions of T0 are theories of arbitrary (preassigned) degree of unsolvability. In particular, there exists an undecidable, ℵ0-categorieal theory in L0, which answers a question raised by Grzegorczyk [2], [3].It follows from Theorem 6 of [3] that there are ℵ0-categorical theories of partial orderings which have arbitrarily high degrees of unsolvability. This is in sharp contrast to the situation for linear orderings, which were the motivation for Fraissé's early work. Indeed, as is shown in [10], every ℵ0-categorical theory of a linear ordering is finitely axiomatizable. (W. Glassmire [12] has independently shown the existence of theories in L0 which are all ℵ0-categorical, and C. Ash [13] has independently shown that such theories exist with arbitrary degree of unsolvability.)

scholarly journals Certifying Proofs in the First-Order Theory of Rewriting

2021 ◽  
pp. 127-144
Author(s):  
Fabian Mitterwallner ◽  
Alexander Lochmann ◽  
Aart Middeldorp ◽  
Bertram Felgenhauer
Keyword(s):  
Decision Procedure ◽  
Order Theory ◽  
Proof Assistant ◽  
Tree Automata ◽  
Decision Tool ◽  
Rewrite Systems ◽  
First Order ◽  
Decidable Theory ◽  
First Order Theory ◽  
Isabelle Proof Assistant

AbstractThe 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 .

Models of countable theories

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Order Theory ◽  
Cardinal Function ◽  
First Order ◽  
First Order Theory ◽  
Free Variables ◽  
Basic Facts ◽  
Small Models

We define and study types of a complete first-order theory T. This concept allows us to refine our analysis of Mod(T). If T has few types, then Mod(T) contains a uniquely defined smallest model that can be elementarily embedded into any structure of Mod(T). We investigate the various properties of these small models in Section 6.3. In Section 6.4, we consider the “big” models of Mod(T). For any theory, the number of types is related to the number of models of the theory. For any cardinal κ, I(T, κ) denotes the number of models in Mod(T) of size κ. We prove two basic facts regarding this cardinal function. In Section 6.5, we show that if T has many types, then I(T, κ) takes on its maximal possible value of 2κ for each infinite κ. In Section 6.6, we prove Vaught’s theorem stating that I(T, ℵ0) cannot equal 2. All formulas are first-order formulas. All theories are sets of first-order sentences. For any structure M, we conveniently refer to an n-tuple of elements from the underlying set of M as an “n-tuple of M.” The notion of a type extends the notion of a theory to include formulas and not just sentences. Whereas theories describe structures, types describe elements within a structure. Definition 6.1 Let M be a ν-structure and let ā = (a1, . . . , an) be an n-tuple of M. The type of ā in M, denoted tpM(ā), is the set of all ν-formulas φ having free variables among x1, . . . , xn that hold in M when each xi in is replaced by ai. More concisely, but less precisely: If ā is an n-tuple, then each formula in tpM(ā) contains at most n free variables but may contain fewer. In particular, the type of an n-tuple contains sentences. For any structure M and tuple ā of M, tpM(ā) contains Th(M) as a subset. The set tpM(ā) provides the complete first-order description of the tuple ā and how it sits in M.

Prime models and almost decidability

1986 ◽  
Vol 51 (2) ◽  
pp. 412-420 ◽  
Author(s):  
Terrence Millar
Keyword(s):  
Order Theory ◽  
The Other ◽  
Prime Model ◽  
First Order ◽  
Decidable Theory ◽  
Complete Extension ◽  
First Order Theory ◽  
Additional Constant ◽  
Open Question ◽  
Countable Models

This paper introduces and investigates a notion that approximates decidability with respect to countable structures. The paper demonstrates that there exists a decidable first order theory with a prime model that is not almost decidable. On the other hand it is proved that if a decidable complete first order theory has only countably many complete types, then it has a prime model that is almost decidable. It is not true that every decidable complete theory with only countably many complete types has a decidable prime model. It is not known whether a complete decidable theory with only countably many countable models up to isomorphism must have a decidable prime model. In [1] a weaker result was proven—if every complete extension, in finitely many additional constant symbols, of a theory T fails to have a decidable prime model, then T has 2ω nonisomorphic countable models. The corresponding statement for saturated models is false, even if all the complete types are recursive, as was shown in [2]. This paper investigates a variation of the open question via a different notion of effectiveness—almost decidable.A tree Tr will be a subset of ω<ω that is closed under predecessor. For elements f, g in ω<ω ∪ ωω, ƒ ⊲ g iffdf ∀i < lh(ƒ)[ƒ(i) = g(i)].

Degree spectra of prime models

2004 ◽  
Vol 69 (2) ◽  
pp. 430-442 ◽  
Author(s):  
Barbara F. Csima
Keyword(s):  
Turing Degrees ◽  
Prime Model ◽  
Atomic Theory ◽  
Computable Set ◽  
Decidable Theory ◽  
Degree Spectra ◽  
Decidable Model ◽  
Decidable Theories

Abstract.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.

Sign in / Sign up

Export Citation Format

Share Document