Talk:Equational logic

Equational logic vs. equational propositional logic

This article seems not to separate two distinct concepts: equational logic (as described in the introduction, in the history and the first three rules, see [1]) and another concept, called equational propositional logic as described by [2] and used in the proof-section (which is very bad, because it refers to the numbering in the source). The == in equational propositional logic is neither the = from equational logic nor a function symbol, it is the ↔ from propositional logic. Regards --Chricho ∀ (talk) 18:54, 25 August 2012 (UTC)

I agree, except that all but the introduction has been copied (almost literally) from Gries' "equational (also called calculational) propositional logic" pages, including history and rules. The two concepts should be kept apart.

Under the title "equational logic", the material from the introduction (based on a source which is hardly reliable) and from Sakharov's MathWorld article could be used, and fleshed out; it could be linked as "main article" from the section First-order_logic#Equality_and_its_axioms, which contains some more useful material.

On the other hand, "equational propositional logic" appears to be a calculus of D.Gries intended to make propositional-logic inferences easier to understand and handle for computer scientists. Nevertheless, I consider it notable for Wikipedia, since it is far more elegant than many of its competitors. But maybe a section in Propositional logic would be sufficient, linking to Gries' pages rather than copying them (besides, in a poor way, as you noted above).

By the way, the section Propositional logic#Equivalence to equational logics, too, uses the notion "equational logic", in a sense that is close to Gries' (i.e. for an equational calculus of propositional logic, rather than a calculus of predicate logic with equality). We should devise appropriate disambiguation notes. - Jochen Burghardt (talk) 12:24, 12 February 2016 (UTC)

FYI, mergeto Theory of pure equality

Please see discussion at Talk:Theory of pure equality. 67.198.37.16 (talk) 21:21, 20 November 2021 (UTC)