Some Theorems on Omitting Types, With Applications to Model Completeness, Amalgamation, and Related Properties

AbstractUniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.

Download Full-text

ON THE MODEL THEORY OF THE LOGARITHMIC FUNCTION IN COMPACT LIE GROUPS

Journal of Algebra and Its Applications ◽

10.1142/s0219498813500552 ◽

2013 ◽

Vol 12 (08) ◽

pp. 1350055

Author(s):

SONIA L'INNOCENTE ◽

FRANÇOISE POINT ◽

CARLO TOFFALORI

Keyword(s):

Lie Groups ◽

Lie Group ◽

Model Theory ◽

Effective Model ◽

Logarithmic Function ◽

Compact Lie Groups ◽

Model Completeness ◽

Schanuel's Conjecture ◽

Logarithm Function ◽

Natural Expansion

Given a compact linear Lie group G, we form a natural expansion of the theory of the reals where G and the graph of a logarithm function on G live. We prove its effective model-completeness and decidability modulo a suitable variant of Schanuel's Conjecture.

Download Full-text

Model completions and omitting types

Journal of Symbolic Logic ◽

10.2307/2275856 ◽

1995 ◽

Vol 60 (2) ◽

pp. 654-672 ◽

Cited By ~ 2

Author(s):

Terrence Millar

Keyword(s):

Partial Order ◽

Omitting Types

AbstractUniversal theories with model completions are characterized. A new omitting types theorem is proved. These two results are used to prove the existence of a universal ℵ0-categorical partial order with an interesting embedding property. Other aspects of these results also are considered.

Download Full-text

Model completeness of some metric completions of absolutely free algebras

Algebra Universalis ◽

10.1007/bf02483872 ◽

1981 ◽

Vol 12 (1) ◽

pp. 137-144

Author(s):

Jan Mycielski ◽

Paul Perlmutter

Keyword(s):

Free Algebras ◽

Model Completeness

Download Full-text

Omitting types in -minimal theories

Journal of Symbolic Logic ◽

10.2307/2273943 ◽

1986 ◽

Vol 51 (1) ◽

pp. 63-74 ◽

Cited By ~ 10

Author(s):

David Marker

Keyword(s):

Finite Union ◽

Structure Theory ◽

Real Closed Fields ◽

Minimal Theory ◽

Order Language ◽

Closed Fields ◽

Hanf Number ◽

Definable Sets ◽

Omitting Types ◽

Binary Relation Symbol

Let L be a first order language containing a binary relation symbol <.Definition. Suppose ℳ is an L-structure and < is a total ordering of the domain of ℳ. ℳ is ordered minimal (-minimal) if and only if any parametrically definable X ⊆ ℳ can be represented as a finite union of points and intervals with endpoints in ℳ.In any ordered structure every finite union of points and intervals is definable. Thus the -minimal structures are the ones with no unnecessary definable sets. If T is a complete L-theory we say that T is strongly (-minimal if and only if every model of T is -minimal.The theory of real closed fields is the canonical example of a strongly -minimal theory. Strongly -minimal theories were introduced (in a less general guise which we discuss in §6) by van den Dries in [1]. Extending van den Dries' work, Pillay and Steinhorn (see [3], [4] and [2]) developed an extensive structure theory for definable sets in strongly -minimal theories, generalizing the results for real closed fields. They also established several striking analogies between strongly -minimal theories and ω-stable theories (most notably the existence and uniqueness of prime models). In this paper we will examine the construction of models of strongly -minimal theories emphasizing the problems involved in realizing and omitting types. Among other things we will prove that the Hanf number for omitting types for a strongly -minimal theory T is at most (2∣T∣)+, and characterize the strongly -minimal theories with models order isomorphic to (R, <).

Download Full-text

Omitting types in logic of metric structures

Journal of Mathematical Logic ◽

10.1142/s021906131850006x ◽

2018 ◽

Vol 18 (02) ◽

pp. 1850006 ◽

Cited By ~ 3

Author(s):

Ilijas Farah ◽

Menachem Magidor

Keyword(s):

Complete Theory ◽

Simple Test ◽

Finite Sets ◽

Complete Type ◽

Metric Structures ◽

Omitting Types ◽

Theory Formula

This paper is about omitting types in logic of metric structures introduced by Ben Yaacov, Berenstein, Henson and Usvyatsov. While a complete type is omissible in some model of a countable complete theory if and only if it is not principal, this is not true for the incomplete types by a result of Ben Yaacov. We prove that there is no simple test for determining whether a type is omissible in a model of a theory [Formula: see text] in a countable language. More precisely, we find a theory in a countable language such that the set of types omissible in some of its models is a complete [Formula: see text] set and a complete theory in a countable language such that the set of types omissible in some of its models is a complete [Formula: see text] set. Two more unexpected examples are given: (i) a complete theory [Formula: see text] and a countable set of types such that each of its finite sets is jointly omissible in a model of [Formula: see text], but the whole set is not and (ii) a complete theory and two types that are separately omissible, but not jointly omissible, in its models.

Download Full-text