Talk:Theory of pure equality

mergefrom Equational logic - its the same thing.

I just added a merge-from tag to equational logic, as I beleive it is effectively talking about the same topic. I made the direction from there to here, since I believe that it is more commonly called "the theory of equality" in textbooks, rather than "equational logic". As the texts proceed, it is noted that the "theory of equality" or "equational theory" has some inference rules that take it beyond the free theory, those inference rules are the ones described in the equational logic article. All this is particularly notable, since the equational theory is kind of the very first theory that is more complicated than the free theory. It's the first (simplest, smallest) theory that adds ..., well, adds inference rules! (or constraints, presentations, propositional schemas, whatever you want to call them, something that removes some of the freedom.) Notable also that in model checking, pretty much all satisfiability modulo theories solvers throw in the equational theory as kind of the first non-trivial theory that they support. I'm going to let this merge proposal cool it's heels, here, to see how it is received. I'm busy doing other things, anyways. 67.198.37.16 (talk) 21:19, 20 November 2021 (UTC)[reply]

It appears to me that Equational logic is more general than Theory of pure equality, since the former allows for equational axioms (like ∀x.Pred(Succ(x))=x) while the latter does not. Therefore, if the articles are merged, the special article Theory of pure equality should become a part of the general Equational logic, not vice versa. - Jochen Burghardt (talk) 18:19, 21 November 2021 (UTC)[reply]

Actually, equational logic states that it does not allow quantifiers and theory of pure equality is a first-order theory so quantifiers are allowed. I agree that ideally we should have an article for the most general logic and discuss special cases as subsections. Another point of reference is Uninterpreted function which discusses the theory of uninterpreted functions like in the equational axiom example you wrote. Caleb Stanford (talk) 23:34, 21 November 2021 (UTC)[reply]

As far as I know, equational logic allows (for a formula in prenex normal form) universal, but not existential, quantification. The universal quantifiers are usually omitted; this may be meant in the article. On the other hand, I guess (but admittely are not sure) that there is just a single theory of pure equality and that this one doesn't use existential quantifiers. An expert in equational reasoning, like Pierre Lescanne [fr] (User:Pierre de Lyon) may help to clarify this issue. - Jochen Burghardt (talk) 09:36, 22 November 2021 (UTC)[reply]

I am not sure to be an expert and you are kind to say so. I looked at my American Heritage Dictionary and I am not fully satisfied with its definitions, but at least I see that equality is not the same as equation. Equality is somewhat static and equation is somewhat dynamic, implying a process to make sides equal. Moreover the Wikipedia articles assume that the underlying logic is classical. Therefore, for me, all this discussion raises more questions that it can really address them. Therefore, for now, I am not sure that a merge is needed. --PIerre.Lescanne (talk) 13:45, 22 November 2021 (UTC)[reply]

Hmm. OK. Well, I guess this breaks down into 4-5 sections: a description of what Löwenheim did in 1915, how/why one wishes to have an equational logic, what prenex has to do with it, its role in SMT, and finally (for me at least) its utility in modern programming to perform "static analysis" of expressions to simplify them, prior to any run-time dynamic evaluation. 67.198.37.16 (talk) 17:39, 1 December 2021 (UTC)[reply]

I just read this article. There may well be other related topics that are of interest, but the way this is stated, this article is clear: it's FOL logic with equality but no function or predicate symbols in the signature. It's decidable (with finite model property) and, since then extended in many different directions (WSkS, congruence closure for quantifier-free fragment, FOL theory of boolean algebras, other fragments of the classical decision problem as presented by Borger and Gurevich, etc.). So these generalizations are something to be discussed and possibly serve as an interesting basis of an educational article that explores connections between various concepts. But saying that this is FOL with equality seems like it's going against the title and the original intention of this article? — Preceding unsigned comment added by Vkuncak (talk • contribs) 10:50, 4 February 2022 (UTC)[reply]

If it's decidable, does that mean any extension to 2nd-order logic that is sound with respect to Leibniz's principle is a conservative extension of it? — Charles Stewart (talk) 07:24, 5 February 2022 (UTC)[reply]
Not sure if it follows from that, but I made the connections to some 2nd order theories.

The topic of this article is discussed in similar length in List_of_first-order_theories#Pure_identity_theories. That article is somewhat long, so maybe some of that material can be moved here, as it is more specific than what we've added with a few (historically very spread out) edits so far. Vkuncak (talk) 10:12, 5 February 2022 (UTC)[reply]

Oppose merge Unlike in the theory of pure equality, equational logic permits function symbols, and function symbols are indeed their main point of interest. Since the motivation for their study and the tasks they are trying to achieve are also very different, a merger would merely confuse readers rather than provide context. Felix QW (talk) 18:34, 7 April 2022 (UTC)[reply]