Atom canonicity and first order definability in classes of algebras of relations

2020 ◽  
Vol 57 (3) ◽  
pp. 321-371
Author(s):  
Tarek Sayed Ahmed
Keyword(s):  
Proof Theory ◽  
Blow Up ◽  
Algebraic Logic ◽  
Boolean Algebras ◽  
First Order ◽  
Dense Subalgebra ◽  
Algebras Of Relations ◽  
Omitting Types ◽  
First Order Definability ◽  
Algebraic Counterpart

AbstractFix 2 < n < ω and let CAn denote the class of cyindric algebras of dimension n. Roughly CAn is the algebraic counterpart of the proof theory of first order logic restricted to the first n variables which we denote by Ln. The variety RCAn of representable CAns reflects algebraically the semantics of Ln. Members of RCAn are concrete algebras consisting of genuine n-ary relations, with set theoretic operations induced by the nature of relations, such as projections referred to as cylindrifications. Although CAn has a finite equational axiomatization, RCAn is not finitely axiomatizable, and it generally exhibits wild, often unpredictable and unruly behavior. This makes the theory of CAn substantially richer than that of Boolean algebras, just as much as Lω,ω is richer than propositional logic. We show using a so-called blow up and blur construction that several varieties (in fact infinitely many) containing and including the variety RCAn are not atom-canonical. A variety V of Boolean algebras with operators is atom canonical, if whenever 𝔄 is atomic, then its Dedekind-MacNeille completion, sometimes referred to as its minimal completion, is also in V. From our hitherto obtained algebraic results we show, employing the powerful machinery of algebraic logic, that the celebrated Henkin-Orey omitting types theorem, which is one of the classical first (historically) cornerstones of model theory of Lω,ω, fails dramatically for Ln even if we allow certain generalized models that are only locallly clasfsical. It is also shown that any class K such that , where CRCAn is the class of completely representable CAns, and Sc denotes the operation of forming dense (complete) subalgebras, is not elementary. Finally, we show that any class K such that is not elementary, where Sd denotes the operation of forming dense subalgebra.

Relation algebra reducts of cylindric algebras and an application to proof theory

2002 ◽  
Vol 67 (1) ◽  
pp. 197-213 ◽  
Author(s):  
Robin Hirsch ◽  
Ian Hodkinson ◽  
Roger D. Maddux
Keyword(s):  
Proof Theory ◽  
Predicate Logic ◽  
Algebraic Logic ◽  
Relation Algebra ◽  
Relation Algebras ◽  
Cylindric Algebras ◽  
First Order ◽  
Order Language ◽  
Binary Relation Symbol ◽  
Made In

AbstractWe confirm a conjecture, about neat embeddings of cylindric algebras, made in 1969 by J. D. Monk, and a later conjecture by Maddux about relation algebras obtained from cylindric algebras. These results in algebraic logic have the following consequence for predicate logic: for every finite cardinal α ≥ 3 there is a logically valid sentence X, in a first-order language ℒ with equality and exactly one nonlogical binary relation symbol E, such that X contains only 3 variables (each of which may occur arbitrarily many times), X has a proof containing exactly α + 1 variables, but X has no proof containing only α variables. This solves a problem posed by Tarski and Givant in 1987.

scholarly journals Omitting types in fragments and extensions of first order logic

2021 ◽  
Author(s):  
Tarek Sayed Ahmed
Keyword(s):  
Algebraic Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Negative Results ◽  
Omitting Types

Fix \(2 < n < \omega\). Let \(L_n\) denote first order logic restricted to the first $n$ variables. Using the machinery of algebraic logic, positive and negative results on omitting types are obtained for \(L_n\) and for infinitary variants and extensions of \(L_{\omega, \omega}\).

Copeland algebras

1972 ◽  
Vol 37 (4) ◽  
pp. 646-656 ◽  
Author(s):  
Daniel B. Demaree
Keyword(s):  
Predicate Logic ◽  
Algebraic Logic ◽  
Boolean Algebras ◽  
Primary Concern ◽  
Cylindric Algebras ◽  
First Order ◽  
Polyadic Algebras ◽  
Algebraic Setting ◽  
Finite Set ◽  
Natural Way

It is well known that the laws of logic governing the sentence connectives—“and”, “or”, “not”, etc.—can be expressed by means of equations in the theory of Boolean algebras. The task of providing a similar algebraic setting for the full first-order predicate logic is the primary concern of algebraic logicians. The best-known efforts in this direction are the polyadic algebras of Halmos (cf. [2]) and the cylindric algebras of Tarski (cf. [3]), both of which may be described as Boolean algebras with infinitely many additional operations. In particular, there is a primitive operator, cκ, corresponding to each quantification, ∃υκ. In this paper we explore a version of algebraic logic conceived by A. H. Copeland, Sr., and described in [1], which has this advantage: All operators are generated from a finite set of primitive operations.Following the theory of cylindric algebras, we introduce, in the natural way, the classes of Copeland set algebras (SCpA), representable Copeland algebras (RCpA), and Copeland algebras of formulas. Playing a central role in the discussion is the set, Γ, of all equations holding in every set algebra. The reason for this is that the operations in a set algebra reflect the notion of satisfaction of a formula in a model, and hence an equation expresses the fact that two formulas are satisfied by the same sequences of objects in the model. Thus to say that an equation holds in every set algebra is to assert that a certain pair of formulas are logically equivalent.

Omitting types for finite variable fragments and complete representations of algebras

2008 ◽  
Vol 73 (1) ◽  
pp. 65-89 ◽  
Author(s):  
Hajnal Andréka ◽  
István Németi ◽  
Tarek Sayed Ahmed
Keyword(s):  
Algebraic Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Cylindric Algebras ◽  
First Order ◽  
Complete Representations ◽  
Atomic Relation ◽  
Representations Of Algebras ◽  
Omitting Types ◽  
Binary Relation Symbol

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.

Algebraic Logic, Where Does it Stand Today?

2005 ◽  
Vol 11 (4) ◽  
pp. 465-516 ◽  
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.

On the elementary equivalence of automorphism groups of Boolean algebras; downward Skolem Löwenheim theorems and compactness of related quantifiers

1980 ◽  
Vol 45 (2) ◽  
pp. 265-283 ◽  
Author(s):  
Matatyahu Rubin ◽  
Saharon Shelah
Keyword(s):  
Boolean Algebra ◽  
Automorphism Groups ◽  
Order Logic ◽  
Boolean Algebras ◽  
First Order Logic ◽  
Elementary Equivalence ◽  
First Order ◽  
Finite Models ◽  
Countably Compact

AbstractTheorem 1. (◊ℵ1,) If B is an infinite Boolean algebra (BA), then there is B1, such that ∣ Aut (B1) ≤∣B1∣ = ℵ1 and 〈B1, Aut (B1)〉 ≡ 〈B, Aut(B)〉.Theorem 2. (◊ℵ1) There is a countably compact logic stronger than first-order logic even on finite models.This partially answers a question of H. Friedman. These theorems appear in §§1 and 2.Theorem 3. (a) (◊ℵ1) If B is an atomic ℵ-saturated infinite BA, Ψ Є Lω1ω and 〈B, Aut (B)〉 ⊨Ψ then there is B1, Such that ∣Aut(B1)∣ ≤ ∣B1∣ =ℵ1, and 〈B1, Aut(B1)〉⊨Ψ. In particular if B is 1-homogeneous so is B1. (b) (a) holds for B = P(ω) even if we assume only CH.

scholarly journals On an interpretation of second order quantification in first order intuitionistic propositional logic

1992 ◽  
Vol 57 (1) ◽  
pp. 33-52 ◽  
Author(s):  
Andrew M. Pitts
Keyword(s):  
Propositional Logic ◽  
Heyting Algebra ◽  
Propositional Calculus ◽  
Interpolation Theorem ◽  
Second Order ◽  
Heyting Algebras ◽  
Intuitionistic Propositional Logic ◽  
First Order ◽  
Intuitionistic Propositional Calculus ◽  
Algebraic Counterpart

AbstractWe prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, ϕ, built up from propositional variables (p, q, r, …) and falsity (⊥) using conjunction (∧), disjunction (∨) and implication (→). Write ⊢ϕ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula ϕ there exists a formula Apϕ (effectively computable from ϕ), containing only variables not equal to p which occur in ϕ, and such that for all formulas ψ not involving p, ⊢ψ → Apϕ if and only if ⊢ψ → ϕ. Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions.An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra.

Uniqueness, definability and interpolation

1988 ◽  
Vol 53 (2) ◽  
pp. 554-570 ◽  
Author(s):  
Kosta Došen ◽  
Peter Schroeder-Heister
Keyword(s):  
Proof Theory ◽  
Interpolation Theorem ◽  
Order Logic ◽  
First Order Logic ◽  
General Notion ◽  
Structural Part ◽  
First Order ◽  
First Case ◽  
Additional Constant ◽  
Special Case

This paper is meant to be a comment on Beth's definability theorem. In it we shall make the following points.Implicit definability as mentioned in Beth's theorem for first-order logic is a special case of a more general notion of uniqueness. If α is a nonlogical constant, Tα a set of sentences, α* an additional constant of the same syntactical category as α and Tα, a copy of Tα with α* instead of α, then for implicit definability of α in Tα one has, in the case of predicate constants, to derive α(x1,…,xn) ↔ α*(x1,…,xn) from Tα ∪ Tα*, and similarly for constants of other syntactical categories. For uniqueness one considers sets of schemata Sα and derivability from instances of Sα ∪ Sα* in the language with both α and α*, thus allowing mixing of α and α* not only in logical axioms and rules, but also in nonlogical assumptions. In the first case, but not necessarily in the second one, explicit definability follows. It is crucial for Beth's theorem that mixing of α and α* is allowed only inside logic, not outside. This topic will be treated in §1.Let the structural part of logic be understood roughly in the sense of Gentzen-style proof theory, i.e. as comprising only those rules which do not specifically involve logical constants. If we restrict mixing of α and α* to the structural part of logic which we shall specify precisely, we obtain a different notion of implicit definability for which we can demonstrate a general definability theorem, where a is not confined to the syntactical categories of nonlogical expressions of first-order logic. This definability theorem is a consequence of an equally general interpolation theorem. This topic will be treated in §§2, 3, and 4.

Sign in / Sign up

Export Citation Format

Share Document