Equational logic

First-order equational logic consists of quantifier-free terms of ordinary first-order logic, with equality as the only predicate symbol. The model theory of this logic was developed into universal algebra by Birkhoff, Grätzer, and Cohn. It was later made into a branch of category theory by Lawvere ("algebraic theories").equational logic. (n.d.). The Free On-line Dictionary of Computing. Retrieved October 24, 2011, from Dictionary.com website: http://dictionary.reference.com/browse/equational+logic

The terms of equational logic are built up from variables and constants using function symbols (or operations).

Syllogism

Here are the four inference rules of logic. P := E/math> denotes textual substitution of expression $E$ for variable $x$ in expression $P$. Next, $b = c$ denotes equality, for $b$ and $c$ of the same type, while $b \equiv c$, or equivalence, is defined only for $b$ and $c$ of type boolean. For $b$ and $c$ of type boolean, $b = c$ and $b \equiv c$ have the same meaning.

Gries, D. (2010). Introduction to equational logic . Retrieved from http://www.cs.cornell.edu/home/gries/Logic/Equational.html

Proof

We explain how the four inference rules are used in proofs, using the proof of . The logic symbols $\top$ and $\bot$ indicate "true" and "false," respectively, and $\lnot$ indicates " not." The theorem numbers refer to theorems of ''A Logical Approach to Discrete Math''.

$\begin (0) & & \lnot p \equiv p \equiv \bot \\ (1) & = & \quad \left\langle\; (3.9),\; \lnot(p \equiv q) \equiv \lnot p \equiv q,\; \text\ q := p \;\right\rangle \\ (2) & & \lnot (p \equiv p) \equiv \bot \\ (3) & = & \quad \left\langle\; \text\ \equiv (3.9),\; \text\ q := p \;\right\rangle \\ (4) & & \lnot \top \equiv \bot & (3.8) \end$

First, lines $(0)$–$(2)$ show a use of inference rule Leibniz:

$(0) = (2)$

is the conclusion of Leibniz, and its premise $\lnot(p \equiv p) \equiv \lnot p \equiv p$ is given on line $(1)$. In the same way, the equality on lines $(2)$–$(4)$ are substantiated using Leibniz.

The "hint" on line $(1)$ is supposed to give a premise of Leibniz, showing what substitution of equals for equals is being used. This premise is theorem $(3.9)$ with the substitution $p := q$, i.e.

(\lnot(p \equiv q) \equiv \lnot p \equiv q) := q

This shows how inference rule Substitution is used within hints.

From $(0) = (2)$ and $(2) = (4)$, we conclude by inference rule Transitivity that $(0) = (4)$. This shows how Transitivity is used.

Finally, note that line $(4)$, $\lnot \top \equiv \bot$, is a theorem, as indicated by the hint to its right. Hence, by inference rule Equanimity, we conclude that line $(0)$ is also a theorem. And $(0)$ is what we wanted to prove.

See also

* Theory of pure equality

References

{{reflist

External links

Sakharov, Alex. "Equational Logic." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein.

Mathematical logic