Omitting types algebraically and more about amalgamation for modal cylindric algebras

AbstractWe give a novel application of algebraic logic to first order logic. A new, flexible construction is presented for representable but not completely representable atomic relation and cylindric algebras of dimension n (for finite n > 2) with the additional property that they are one-generated and the set of all n by n atomic matrices forms a cylindric basis. We use this construction to show that the classical Henkin-Orey omitting types theorem fails for the finite variable fragments of first order logic as long as the number of variables available is > 2 and we have a binary relation symbol in our language. We also prove a stronger result to the effect that there is no finite upper bound for the extra variables needed in the witness formulas. This result further emphasizes the ongoing interplay between algebraic logic and first order logic.

Download Full-text

Algebraic Logic, Where Does it Stand Today?

Bulletin of Symbolic Logic ◽

10.2178/bsl/1130335206 ◽

2005 ◽

Vol 11 (4) ◽

pp. 465-516 ◽

Cited By ~ 28

Author(s):

Tarek Sayed Ahmed

Keyword(s):

Proof Theory ◽

Algebraic Logic ◽

Theory Model ◽

Historical Background ◽

Relation Algebras ◽

Cylindric Algebras ◽

Open Problems ◽

The Subject ◽

Omitting Types ◽

Modern Perspective

AbstractThis is a survey article on algebraic logic. It gives a historical background leading up to a modern perspective. Central problems in algebraic logic (like the representation problem) are discussed in connection to other branches of logic, like modal logic, proof theory, model-theoretic forcing, finite combinatorics, and Gödel's incompleteness results. We focus on cylindric algebras. Relation algebras and polyadic algebras are mostly covered only insofar as they relate to cylindric algebras, and even there we have not told the whole story. We relate the algebraic notion of neat embeddings (a notion special to cylindric algebras) to the metalogical ones of provability, interpolation and omitting types in variants of first logic. Another novelty that occurs here is relating the algebraic notion of atom-canonicity for a class of boolean algebras with operators to the metalogical one of omitting types for the corresponding logic. A hitherto unpublished application of algebraic logic to omitting types of first order logic is given. Proofs are included when they serve to illustrate certain concepts. Several open problems are posed. We have tried as much as possible to avoid exploring territory already explored in the survey articles of Monk [93] and Németi [97] in the subject.

Download Full-text

A completeness theorem for higher order logics

Journal of Symbolic Logic ◽

10.2307/2586575 ◽

2000 ◽

Vol 65 (2) ◽

pp. 857-884 ◽

Cited By ~ 9

Author(s):

Gábor Sági

Keyword(s):

Set Theory ◽

Representation Theorem ◽

Completeness Theorem ◽

Higher Order ◽

Algebraic Solution ◽

Algebraic Proof ◽

Relation Algebras ◽

Cylindric Algebras ◽

Strong Representation ◽

Algebraic Counterpart

AbstractHere we investigate the classes of representable directed cylindric algebras of dimension α introduced by Németi [12]. can be seen in two different ways: first, as an algebraic counterpart of higher order logics and second, as a cylindric algebraic analogue of Quasi-Projective Relation Algebras. We will give a new, “purely cylindric algebraic” proof for the following theorems of Németi: (i) is a finitely axiomatizable variety whenever α ≥ 3 is finite and (ii) one can obtain a strong representation theorem for if one chooses an appropriate (non-well-founded) set theory as foundation of mathematics. These results provide a purely cylindric algebraic solution for the Finitization Problem (in the sense of [11]) in some non-well-founded set theories.

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

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