Theory of pure equality

Last updated February 02, 2024

In mathematical logic the theory of pure equality is a first-order theory. It has a signature consisting of only the equality relation symbol, and includes no non-logical axioms at all.^[1]

This theory is consistent but incomplete, as a non-empty set with the usual equality relation provides an interpretation making certain sentences true. It is an example of a decidable theory and is a fragment of more expressive decidable theories, including monadic class of first-order logic (which also admits unary predicates and is, via Skolem normal form, related^[2] to set constraints in program analysis) and monadic second-order theory of a pure set (which additionally permits quantification over predicates and whose signature extends to monadic second-order logic of k successors^[3]).

Historical significance

The theory of pure equality was proven to be decidable by Leopold Löwenheim in 1915.

If an additional axiom is added saying that there are exactly m objects for a fixed natural number m, or an axiom scheme is added saying that there are infinitely many objects, then the resulting theory is complete.

Definition as FOL theory

The pure theory of equality contains formulas of first-order logic with equality, where the only predicate symbol is equality itself and there are no function symbols.

Consequently, the only form of an atomic formula is $x=y$ where $x,y$ are (possibly identical) variables. Syntactically more complex formulas can be built as usual in first-order logic using propositional connectives such as $\land ,\lor ,\lnot$ and quantifiers $\forall ,\exists$ .

A first-order structure with equality interpreting such formulas is just a set with the equality relation on its elements. Isomorphic structures with such signature are thus sets of the same cardinality. Cardinality thus uniquely determines whether a sentence is true in the structure.

Example

The following formula:

\forall x,y,z.\ (z=x\lor z=y)

is true when the set interpreting the formula has at most two elements.

Expressive power

This theory can express the fact that the domain of interpretation has at least $k$ elements for a constant $k$ using the formula that we will denote $D_{k}$ for a constant $k$ :

\exists x_{1},\ldots ,x_{k}.\ \bigwedge _{1\leq i<j\leq k}x_{i}\neq x_{j}

Using negation, it can then express that the domain has more than $k$ elements. More generally, it can constrain the domain to have a given finite set of finite cardinalities.

Definition of the theory

In terms of models, pure theory of equality can be defined as set of those first-order sentences that are true for all (non-empty) sets, regardless of their cardinality. For example, the following is a valid formula in the pure theory of equality:

(\forall x,y,z.\ (z=x\lor z=y))\lor (\exists p,q,r.\ p\neq q\land p\neq r\land q\neq r)

By completeness of first-order logic, all valid formulas are provable using axioms of first-order logic and the equality axioms (see also equational logic).

Decidability

Decidability can be shown by establishing that every sentence can be shown equivalent to a propositional combination of formulas about the cardinality of the domain.^[4]

To obtain quantifier elimination, one can expand the signature of the language while preserving the definable relations (a technique that works more generally for monadic second-order formulas). Another approach to establish decidability is to use Ehrenfeucht–Fraïssé games.

Related Research Articles

In mathematics and computer science, the Entscheidungsproblem is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "yes" or "no" according to whether the statement is universally valid, i.e., valid in every structure.

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

In mathematical logic, model theory is the study of the relationship between formal theories, and their models. The aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself. In particular, model theorists also investigate the sets that can be defined in a model of a theory, and the relationship of such definable sets to each other. As a separate discipline, model theory goes back to Alfred Tarski, who first used the term "Theory of Models" in publication in 1954. Since the 1970s, the subject has been shaped decisively by Saharon Shelah's stability theory.

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete.

In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", or "for any". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other words, it is the predication of a property or relation to every member of the domain. It asserts that a predicate within the scope of a universal quantifier is true of every value of a predicate variable.

In mathematics, equality is a relationship between two quantities or, more generally, two mathematical expressions, asserting that the quantities have the same value, or that the expressions represent the same mathematical object. The equality between $A$ and $B$ is written $A = B$ , and pronounced " $A$ equals $B$ ". The symbol " $=$ " is called an "equals sign". Two objects that are not equal are said to be distinct.

In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell's paradox. Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics. Zermelo–Fraenkel set theory with the axiom of choice included is abbreviated ZFC, where C stands for "choice", and ZF refers to the axioms of Zermelo–Fraenkel set theory with the axiom of choice excluded.

In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.

In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.

In mathematical logic, positive set theory is the name for a class of alternative set theories in which the axiom of comprehension holds for at least the positive formulas $.$

In set theory, $-induction$ , also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property. Considered as an axiomatic principle, it is called the axiom schema of set induction.

In mathematical logic, Heyting arithmetic $is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.$

In the foundations of mathematics, Morse–Kelley set theory (MK), Kelley–Morse set theory (KM), Morse–Tarski set theory (MT), Quine–Morse set theory (QM) or the system of Quine and Morse is a first-order axiomatic set theory that is closely related to von Neumann–Bernays–Gödel set theory (NBG). While von Neumann–Bernays–Gödel set theory restricts the bound variables in the schematic formula appearing in the axiom schema of Class Comprehension to range over sets alone, Morse–Kelley set theory allows these bound variables to range over proper classes as well as sets, as first suggested by Quine in 1940 for his system ML.

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with " $" and " " of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.$

In logic, the monadic predicate calculus is the fragment of first-order logic in which all relation symbols in the signature are monadic, and there are no function symbols. All atomic formulas are thus of the form $, where is a relation symbol and is a variable.$

In mathematics and logic, Ackermann set theory (AST) is an axiomatic set theory proposed by Wilhelm Ackermann in 1956.

General set theory (GST) is George Boolos's (1998) name for a fragment of the axiomatic set theory Z. GST is sufficient for all mathematics not requiring infinite sets, and is the weakest known set theory whose theorems include the Peano axioms.

In set theory and mathematical logic, the Lévy hierarchy, introduced by Azriel Lévy in 1965, is a hierarchy of formulas in the formal language of the Zermelo–Fraenkel set theory, which is typically called just the language of set theory. This is analogous to the arithmetical hierarchy, which provides a similar classification for sentences of the language of arithmetic.

In mathematical set theory, the axiom of adjunction states that for any two sets x, y there is a set w = x ∪ {y} given by "adjoining" the set y to the set x. It is stated as

References

↑ Monk, J. Donald (1976). "Chapter 13: Some Decidable Theories". Mathematical Logic . Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. p. 240. ISBN 978-0-387-90170-1.
↑ Bachmair, L.; Ganzinger, H.; Waldmann, U. (1993). "Set constraints are the monadic class". [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science. pp. 75–83. doi:10.1109/LICS.1993.287598. hdl:11858/00-001M-0000-0014-B322-4. ISBN 0-8186-3140-6. S2CID 2351050.
↑ Rabin, Michael O. (July 1969). "Decidability of Second-Order Theories and Automata on Infinite Trees". Transactions of the American Mathematical Society. 141: 1–35. doi:10.2307/1995086. JSTOR 1995086.
↑ Monk, J. Donald (1976). "Chapter 13: Some Decidable Theories, Lemma 13.11". Mathematical Logic . Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. p. 241. ISBN 978-0-387-90170-1.

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[1] Monk, J. Donald (1976). "Chapter 13: Some Decidable Theories". Mathematical Logic . Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. p. 240. ISBN 978-0-387-90170-1.

[2] Bachmair, L.; Ganzinger, H.; Waldmann, U. (1993). "Set constraints are the monadic class". [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science. pp. 75–83. doi:10.1109/LICS.1993.287598. hdl:11858/00-001M-0000-0014-B322-4. ISBN 0-8186-3140-6. S2CID 2351050.

[3] Rabin, Michael O. (July 1969). "Decidability of Second-Order Theories and Automata on Infinite Trees". Transactions of the American Mathematical Society. 141: 1–35. doi:10.2307/1995086. JSTOR 1995086.

[4] Monk, J. Donald (1976). "Chapter 13: Some Decidable Theories, Lemma 13.11". Mathematical Logic . Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. p. 241. ISBN 978-0-387-90170-1.

[1]

[2]

[3]

[4]