Nonfinitizability of classes of representable cylindric algebras

1969 ◽  
Vol 34 (3) ◽  
pp. 331-343 ◽  
Author(s):  
J. Donald Monk
Keyword(s):  
Predicate Logic ◽  
Infinite Dimension ◽  
Fundamental Result ◽  
Cylindric Algebra ◽  
Cylindric Algebras ◽  
Locally Finite ◽  
First Order ◽  
Alfred Tarski ◽  
Sentential Logic ◽  
Algebraic Counterpart

Cylindric algebras were introduced by Alfred Tarski about 1952 to provide an algebraic analysis of (first-order) predicate logic. With each cylindric algebra one can, in fact, associate a certain, in general infinitary, predicate logic; for locally finite cylindric algebras of infinite dimension the associated predicate logics are finitary. As with Boolean algebras and sentential logic, the algebraic counterpart of completeness is representability. Tarski proved the fundamental result that every locally finite cylindric algebra of infinite dimension is representable.

Cylindric algebras with terms

1990 ◽  
Vol 55 (2) ◽  
pp. 854-866 ◽  
Author(s):  
Norman Feldman
Keyword(s):  
Predicate Logic ◽  
Equivalence Classes ◽  
Cylindric Algebra ◽  
Cylindric Algebras ◽  
First Order ◽  
Order Language ◽  
First Order Predicate Logic

In this paper we discuss cylindric algebras with terms. The setting is two—sorted algebras—one sort for terms and one for Boolean elements. As with cylindric algebras, a cylindric algebra with terms has its roots in first order predicate logic [HMT1].Let Σ be a set of sentences in a first order language with terms, equality and variables u0,u1,u2, …, Define a relation ≡Σ on Fm, the set of formulas, by φ ≡Σθ if and only if Σ ⊢ φ ↔ θ, and on Tm, the set of terms, by τ ≡Σσ if and only if Σ ⊢ τ ≈ σ. The operations +, ·, cκ, 0, 1 are defined as usual on equivalence classes. Define , where is σ with τ substituted for all occurrences of uκ. That the operation *κ, for κ < α, is well defined follows from the first order axioms of equality. Let vκ = [uκ]. To establish the link between terms and Booleans, define operations oκ as follows: , where φ' is a variant of φ such that uκ is free for τ in φ′ and is φ′ with τ substituted for all free occurrences of uκ in φ′. From the first order axioms it follows that oκ, for κ < α, is well defined. Finally, instead of diagonal elements, we define a Boolean-valued operation on terms as follows: [τ] e [σ] = [τ ≈ σ].

STONE SPACE OF CYLINDRIC ALGEBRAS AND TOPOLOGICAL MODEL SPACES

2016 ◽  
Vol 81 (3) ◽  
pp. 1069-1086
Author(s):  
CHARLES C. PINTER
Keyword(s):  
Boolean Algebra ◽  
Model Theory ◽  
Representation Theorem ◽  
Stone Space ◽  
Equivalence Relations ◽  
Cylindric Algebra ◽  
Cylindric Algebras ◽  
Locally Finite ◽  
Abstract Model Theory ◽  
Image Position

AbstractThe Stone representation theorem was a milestone for the understanding of Boolean algebras. From Stone’s theorem, every Boolean algebra is representable as a field of sets with a topological structure. By means of this, the structural elements of any Boolean algebra, as well as the relations between them, are represented geometrically and can be clearly visualized. It is no different for cylindric algebras: Suppose that ${\frak A}$ is a cylindric algebra and ${\cal S}$ is the Stone space of its Boolean part. (Among the elements of the Boolean part are the diagonal elements.) It is known that with nothing more than a family of equivalence relations on ${\cal S}$ to represent quantifiers, ${\cal S}$ represents the full cylindric structure just as the Stone space alone represents the Boolean structure. ${\cal S}$ with this structure is called a cylindric space.Many assertions about cylindric algebras can be stated in terms of elementary topological properties of ${\cal S}$. Moreover, points of ${\cal S}$ may be construed as models, and on that construal ${\cal S}$ is called a model space. Certain relations between points on this space turn out to be morphisms between models, and the space of models with these relations hints at the possibility of an “abstract” model theory. With these ideas, a point-set version of model theory is proposed, in the spirit of pointless topology or category theory, in which the central insight is to treat the semantic objects (models) homologously with the corresponding syntactic objects so they reside together in the same space.It is shown that there is a new, purely algebraic way of introducing constants in cylindric algebras, leading to a simplified proof of the representation theorem for locally finite cylindric algebras. Simple rich algebras emerge as homomorphic images of cylindric algebras. The topological version of this theorem is especially interesting: The Stone space of every locally finite cylindric algebra ${\frak A}$ can be partitioned into subspaces which are the Stone spaces of all the simple rich homomorphic images of ${\frak A}$. Each of these images completely determines a model of ${\frak A}$, and all denumerable models of ${\frak A}$ appear in this representation.The Stone space ${\cal S}$ of every cylindric algebra can likewise be partitioned into closed sets which are duals of all the types in ${\frak A}$. This fact yields new insights into miscellaneous results in the model theory of saturated models.

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.

Nonfinitizability of classes of representable polyadic algebras

1969 ◽  
Vol 34 (3) ◽  
pp. 344-352 ◽  
Author(s):  
James S. Johnson
Keyword(s):  
Predicate Logic ◽  
Free Algebras ◽  
Cylindric Algebra ◽  
Cylindric Algebras ◽  
Polyadic Algebras

The notion of polyadic algebra was introduced by Halmos to reflect algebraically the predicate logic without equality. Later Halmos enriched the study with the introduction of the notion of equality. These algebras are very closely related to the cylindric algebras of Tarski. The notion of diagonal free cylindric algebra predates that of cylindric algebra and is also due to Tarski. The theory of diagonal free algebras forms an important fragment of the theories of polyadic and cylindric algebras.

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.

The equational theory of CA3 is undecidable

1980 ◽  
Vol 45 (2) ◽  
pp. 311-316 ◽  
Author(s):  
Roger Maddux
Keyword(s):  
Equational Theory ◽  
Cylindric Algebra ◽  
Relation Algebras ◽  
Cylindric Algebras ◽  
3 Dimensional ◽  
First Order ◽  
Equational Theories ◽  
Order Language ◽  
Theoretic Proof

There is no algorithm for determining whether or not an equation is true in every 3-dimensional cylindric algebra. This theorem completes the solution to the problem of finding those values of α and β for which the equational theories of CAα and RCAβ are undecidable. (CAα and RCAβ are the classes of α-dimensional cylindric algebras and representable β-dimensional cylindric algebras. See [4] for definitions.) This problem was considered in [3]. It was known that RCA0 = CA0 and RCA1 = CA1 and that the equational theories of these classes are decidable. Tarski had shown that the equational theory of relation algebras is undecidable and, by utilizing connections between relation algebras and cylindric algebras, had also shown that the equational theories of CAα and RCAβ are undecidable whenever 4 ≤ α and 3 ≤ β. (Tarski's argument also applies to some varieties K ⊆ RCAβ with 3 ≤ β and to any variety K such that RCAα ⊆ K ⊆ CAα and 4 ≤ α.)Thus the only cases left open in 1961 were CA2, RCA2 and CA3. Shortly there-after Henkin proved, in one of Tarski's seminars at Berkeley, that the equational theory of CA2 is decidable, and Scott proved that the set of valid sentences in a first-order language with only two variables is recursive [11]. (For a more model-theoretic proof of Scott's theorem see [9].) Scott's result is equivalent to the decidability of the equational theory of RCA2, so the only case left open was CA3.

A completeness theorem for higher order logics

2000 ◽  
Vol 65 (2) ◽  
pp. 857-884 ◽  
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.

Syllogism and quantification

1962 ◽  
Vol 27 (1) ◽  
pp. 58-72 ◽  
Author(s):  
Timothy Smiley
Keyword(s):  
Predicate Logic ◽  
Modern Logic ◽  
First Order ◽  
First Order Predicate Logic

Anyone who reads Aristotle, knowing something about modern logic and nothing about its history, must ask himself why the syllogistic cannot be translated as it stands into the logic of quantification. It is now more than twenty years since the invention of the requisite framework, the logic of many-sorted quantification.In the familiar first-order predicate logic generality is expressed by means of variables and quantifiers, and each interpretation of the system is based upon the choice of some class over which the variables may range, the only restriction placed on this ‘domain of individuals’ being that it should not be empty.

Some logical and syntactical observations concerning the first-order dependent type system λP

1999 ◽  
Vol 9 (4) ◽  
pp. 335-359 ◽  
Author(s):  
HERMAN GEUVERS ◽  
ERIK BARENDSEN
Keyword(s):  
Predicate Logic ◽  
Type System ◽  
Logical Framework ◽  
First Order ◽  
Logical Derivation ◽  
Dependent Type ◽  
First Order Predicate Logic

We look at two different ways of interpreting logic in the dependent type system λP. The first is by a direct formulas-as-types interpretation à la Howard where the logical derivation rules are mapped to derivation rules in the type system. The second is by viewing λP as a Logical Framework, following Harper et al. (1987) and Harper et al. (1993). The type system is then used as the meta-language in which various logics can be coded.We give a (brief) overview of known (syntactical) results about λP. Then we discuss two issues in some more detail. The first is the completeness of the formulas-as-types embedding of minimal first-order predicate logic into λP. This is a remarkably complicated issue, a first proof of which appeared in Geuvers (1993), following ideas in Barendsen and Geuvers (1989) and Swaen (1989). The second issue is the minimality of λP as a logical framework. We will show that some of the rules are actually superfluous (even though they contribute nicely to the generality of the presentation of λP).At the same time we will attempt to provide a gentle introduction to λP and its various aspects and we will try to use little inside knowledge.

Sign in / Sign up

Export Citation Format

Share Document