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[x := E]$ 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.

class="wikitable"
scope="row" style="text-align: left" \| Substitution \| If $P$ is a theorem, then so is $P[x := E]$ . \| $\vdash P \qquad \rightarrow \qquad \vdash P[x := E]$
scope="row" style="text-align: left" \| Leibniz \| If $P = Q$ is a theorem, then so is $E[x:= P] = E[x:= Q]$ . \| $\vdash P = Q \qquad \rightarrow \qquad \vdash E[x := P] = E[x := Q]$
scope="row" style="text-align: left" style="text-align: left" \| Transitivity \| If $P = Q$ and $Q = R$ are theorems, then so is $P = R$ . \| $\vdash P = Q, \; \vdash Q = R \qquad \rightarrow \qquad \vdash P = R$
scope="row" style="text-align: left" \| Equanimity \| If $P$ and $P \equiv Q$ are theorems, then so is $Q$ . \| $\vdash P, \; \vdash P \equiv Q \qquad \rightarrow \qquad \vdash Q$

class="wikitable"

scope="row" style="text-align: left" | Substitution

| If $P$ is a theorem, then so is $P[x := E]$ .

| $\vdash P \qquad \rightarrow \qquad \vdash P[x := E]$

scope="row" style="text-align: left" | Leibniz

| If $P = Q$ is a theorem, then so is $E[x:= P] = E[x:= Q]$ .

| $\vdash P = Q \qquad \rightarrow \qquad \vdash E[x := P] = E[x := Q]$

scope="row" style="text-align: left" style="text-align: left" | Transitivity

| If $P = Q$ and $Q = R$ are theorems, then so is $P = R$ .

| $\vdash P = Q, \; \vdash Q = R \qquad \rightarrow \qquad \vdash P = R$

scope="row" style="text-align: left" | Equanimity

| If $P$ and $P \equiv Q$ are theorems, then so is $Q$ .

| $\vdash P, \; \vdash P \equiv Q \qquad \rightarrow \qquad \vdash Q$

Gries, D. (2010). Introduction to equational logic . Retrieved from http://www.cs.cornell.edu/home/gries/Logic/Equational.html {{Webarchive|url=https://web.archive.org/web/20190923093229/http://www.cs.cornell.edu/home/gries/Logic/Equational.html |date=2019-09-23 }}

Proof

We explain how the four inference rules are used in proofs, using the proof of {{clarify span| $\lnot p \equiv p \equiv \bot$ |reason=Insert parantheses to disambiguate the formula.|date=November 2021}}. 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{array}{lcl}
(0) & & \lnot p \equiv p \equiv \bot \\
(1) & = & \quad \left\langle\; (3.9),\; \lnot(p \equiv q) \equiv \lnot p \equiv q,\; \text{with}\ q := p \;\right\rangle \\
(2) & & \lnot (p \equiv p) \equiv \bot \\
(3) & = & \quad \left\langle\; \text{Identity of}\ \equiv (3.9),\; \text{with}\ q := p \;\right\rangle \\
(4) & & \lnot \top \equiv \bot & (3.8)
\end{array}$

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)[p := 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.

References

External links

[http://mathworld.wolfram.com/EquationalLogic.html Sakharov, Alex. "Equational Logic." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein.]

Category:Mathematical logic

equational logic

Syllogism

Proof

See also

References

External links