Talk:Equational 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 [http://mathworld.wolfram.com/EquationalLogic.html]) and another concept, called equational propositional logic as described by [http://www.cs.cornell.edu/gries/logic/Equational.html] 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 [http://www.cs.cornell.edu/gries/Logic/Calculationalhistory.html history] and [http://www.cs.cornell.edu/gries/Logic/Calculational.html#Inference 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)

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