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 [σ] = [τ ≈ σ].

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.

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.

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.

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.

First order predicate logic

1986 ◽  
pp. 155-183
Author(s):  
Igor Aleksander ◽  
Henri Farreny ◽  
Malik Ghallab
Keyword(s):  
Predicate Logic ◽  
First Order ◽  
First Order Predicate Logic

A Test of a Two-Stage Model of the Evaluation of Hypotheses from Quantified First-Order Predicate Logic in Information Use Tasks

1992 ◽  
Vol 71 (3_suppl) ◽  
pp. 1091-1104 ◽  
Author(s):  
Peter E. Langford ◽  
Robert Hunting
Keyword(s):  
Predicate Logic ◽  
Information Use ◽  
Stage Model ◽  
Two Stage ◽  
First Order ◽  
Alternative Hypotheses ◽  
Age Range ◽  
Hypothesis Evaluation ◽  
Universe Of Discourse ◽  
First Order Predicate Logic

480 adolescents and young adults between the ages of 12 and 29 years participated in an experiment in which they were asked to evaluate hypotheses from quantified first-order predicate logic specifying that certain classes of event were necessarily, possibly, or certainly not included within a universe of discourse. Results were used to test a two-stage model of performance on hypothesis evaluation tasks that originated in work on the evaluation of conditionals. The two-stage model, unlike others available, successfully predicted the range of patterns of reply observed. In dealing with very simple hypotheses subjects in this age range tended not to make use of alternative hypotheses unless these were explicitly or implicitly suggested to them by the task. This tells against complexity of hypothesis as an explanation of the reluctance to use alternative hypotheses in evaluating standard conditionals.

Sign in / Sign up

Export Citation Format

Share Document