View source for Equational logic

<!--This article has been texified automatically. Since there was no Nroff source code for this article, 
the semi-automatic procedure described at https://encyclopediaofmath.org/wiki/User:Maximilian_Janisch/latexlist
was used.
If the TeX and formula formatting is correct, please remove this message and the {{TEX|semi-auto}} category.

Out of 114 formulas, 114 were replaced by TEX code.-->

{{TEX|semi-auto}}{{TEX|done}}
Formal languages are mathematical models of the natural (informal) languages of mathematics (cf. also [[Formal languages and automata|Formal languages and automata]]). In [[Mathematical logic|mathematical logic]] (i.e., meta-mathematics) one builds several classes of formal languages, of which first-order logic and equational logic are especially important. Languages of the first class are most often used to give complete mathematical definitions of mathematical theories, their axioms and their rules of proof. Languages of the second class are used most often in [[Universal algebra|universal algebra]], and in automatic theorem proving procedures.

An equational language $L$ is a formal language whose alphabet consists of a countable set $V$ of variables, a set $\Phi$ of function symbols and an equality symbol $=$. Moreover, a function $\rho : \Phi \rightarrow \{ 0,1 , \ldots \}$ is given and for each $f \in \Phi$, $\rho ( f )$ denotes the number of argument places of $f$. If $\rho ( f ) = 0$, then $f$ is called a constant.

One associates with $L$ a class of algebras of type $L$, i.e. structures $\mathcal{A}$ of the form

\begin{equation*} \langle A , \tilde { f } \rangle _ { f \in \Phi }, \end{equation*}

where $A$ is a non-empty set; if $\rho ( f ) &gt; 0$, then $\widetilde { f }$ is a function with $\rho ( f )$ arguments running over $A$ and with values in $A$; if $\rho ( f ) = 0$, then $\tilde { f } \in A$.

One defines the set $T$ of terms of $L$ to be the least set of finite sequences of letters of $L$ such that $T$ contains the one-term sequence consisting of a variable or a constant, and such that if $t_{1} , \dots , t _ { \rho  (\, f ) } \in T$, then $f _{ t _ { 1 } \ldots t _ { \rho } ( f )} \in T$. If $\mathcal{A}$ is an algebra of type $L$ and $t \in T$, then $\widetilde { t }$ denotes a composition of some of the functions and constants $\widetilde { f }$, which is coded by $t$. A term of the form $f v _ { 1 } , \dots , v _ { \rho  ( f )}$, where $f \in \Phi$ and $v _ { i } \in V$, is called atomic.

The only truth-valued expressions of $L$ are equations, i.e., sequences of letters of the form

\begin{equation} \tag{a1} s = t, \end{equation}

where $s , t \in T$. One says that (a1) is true in $\mathcal{A}$ if and only if the objects $\tilde{s}$ and $\widetilde { t }$ are equal.

If $E$ is a set of equations, then $\mathcal{A}$ is called a model of $E$ if and only if all the equations of $E$ are true in $\mathcal{A}$. The class of all models of some set $E$ is called a variety.

For any $s , t \in T$ and $v \in V$, one denotes by

\begin{equation*} s \left( \begin{array} { l } { v } \\ { t } \end{array} \right) \end{equation*}

the term obtained from $s$ by substituting all occurrences of $v$ by $t$.

The rules of proof of $L$ are the following:

i) $t = t$ is accepted for all $t \in T$;

ii) $s = t$ yields $t = s$;

iii) $r = s$ and $s = t$ yield $r = t$;

iv) $q = r$ and $s = t$ yield

\begin{equation*} q \left( \begin{array} { l } { v } \\ { s } \end{array} \right) = r \left( \begin{array} { l } { v } \\ { t } \end{array} \right). \end{equation*}

A set $S$ of equations is called an equational theory if and only if $S$ is closed under the rules i)–iv). Thus, if $\mathcal{A}$ is a model of $E$, then $\mathcal{A}$ is also a model of the least equational theory including $E$.

The above concepts and rules were introduced in 1935 by G. Birkhoff, and he proved the following fundamental theorems.

Birkhoff's completeness theorem: If $S$ is an equational theory and $s = t$ is true in all the models of $S$, then $s = t$ belongs to $S$.

Birkhoff's characterization of varieties: A class $C$ of algebras of type $L$ is a variety if and only if it satisfies the following three conditions:

a) all subalgebras of the algebras of $C$ are in $C$;

b) all homomorphic images of the algebras of $C$ are in $C$;

c) for any subset $K$ of $C$, the direct product of the algebras in $K$ belongs to $C$.

These theorems are the roots of a very large literature, see [[#References|[a2]]], [[#References|[a4]]] and references therein.

In mathematical practice, as a rule one uses informal multi-sorted languages (cf. also [[Logical calculus|Logical calculus]]). Equational logic generalizes in a similar way. For example, a [[Module|module]] over a ring is a two-sorted algebra with two universes, an Abelian group and a ring, and its language has two separate sorts of variables for the elements of those universes. Every model $M$ of a first-order theory can be regarded as a two-sorted algebra whose universes are the universe of $M$ and a two-element Boolean algebra, while treating the relations of $M$ as Boolean-valued functions. Corresponding to that view (following [[#References|[a3]]]) there is a natural translation of any first-order language $L ^ { * }$ into a two-sorted equational language $L$. Namely, the formulas of $L ^ { * }$ are treated as Boolean-valued terms of $L$ and the terms of $L ^ { * }$ are treated as object-valued terms of $L$. The axioms and rules of first-order logic turn into the rules i)–iv) (adapted to the two-sorted language $L$) plus five axiom schemata:

1) $[ ( \varphi \rightarrow \psi ) \rightarrow ( ( \psi \rightarrow \chi ) \rightarrow ( \varphi \rightarrow \chi ) ) ] = 1$;

2) $( \varphi \rightarrow ( \neg \varphi \rightarrow \psi ) ) = 1$;

3) $( ( \neg \varphi \rightarrow \varphi ) \rightarrow \varphi ) = 1$;

4) $( 1 \rightarrow \varphi ) = \varphi$;

5) $\left( \varphi \rightarrow \varphi \left( \begin{array} { c } { x } \\ { \varepsilon x \varphi } \end{array} \right) \right) = 1$. Here $\varphi , \psi , \ldots$ run over formulas of $L ^ { * }$, the quantifiers of $L ^ { * }$ are understood as abbreviations, viz.

\begin{equation*} ( \exists x \varphi ( x ) ) = \varphi \left( \begin{array} { c } { x } \\ { \varepsilon x \varphi } \end{array} \right) \text { and } ( \forall x \varphi ( x ) ) = \varphi \left( \begin{array} { c } { x } \\ { \varepsilon x ( \neg \varphi ) } \end{array} \right), \end{equation*}

where $x$ is an object-valued variable, $\varepsilon x \varphi$ is an object-valued atomic term, called an $\varepsilon$-term, whose variables are the free variables of $\varphi$ other than $x$, 1)–3) are equational versions of the Łukasiewicz axioms for propositional calculus, 4) yields the proper version of [[Modus ponens|modus ponens]], and 5) is the equational version of Hilbert's axiom about the $\varepsilon$-symbol (which he formulated in 1925).

In this way, the [[Gödel completeness theorem|Gödel completeness theorem]] for first-order logic can be seen as a consequence of Birkhoff's completeness theorem stated above (see [[#References|[a3]]]). Moreover, equational logic corroborates a philosophical idea of H. Poincaré about the constructive and finitistic nature of mathematics. The same idea (in the context of set theory) was also expressed by D. Hilbert in 1904. Poincaré died in 1912, before the relevant mathematical concepts described above were developed by T. Skolem in 1920, Hilbert in 1925, and Birkhoff in 1935; see [[#References|[a2]]], [[#References|[a1]]]. Those concepts allow one to express this idea as follows. Quantifiers may suggest the actual existence of all objects of some infinite universes (a Platonic reality). But the above formalism shows that, at least in pure mathematics, they can be understood in a more concrete way, namely as abbreviations or blueprints for expressions involving certain $\varepsilon$-terms. And those $\varepsilon$-terms denote actually imagined objects or operations, thus they do not refer to nor imply the existence of any actually infinite universes. Hence the rules i)–iv) and the axiom schemata 1)–5) are constructive and finitistic in the sense of Poincaré and Hilbert.

Presently (1998), many researchers are trying to apply equational logic to obtain efficient automatic theorem proving procedures (see [[#References|[a5]]]).

====References====
<table><tr><td valign="top">[a1]</td> <td valign="top">  J. van Heijenoort,   "From Frege to Gödel: A source book in mathematical logic 1878-1931" , Harvard Univ. Press  (1977)  (Edition: Third, corrected)</td></tr><tr><td valign="top">[a2]</td> <td valign="top">  R.N. McKenzie,   G.F. McNulty,   W.F. Taylor,   "Algebras, lattices, varieties" , '''I''' , Wadsworth&amp;Brooks/Cole  (1987)</td></tr><tr><td valign="top">[a3]</td> <td valign="top">  J. Mycielski,   "Equational treatment of first-order logic"  ''Algebra Univ.'' , '''33'''  (1995)  pp. 26–39</td></tr><tr><td valign="top">[a4]</td> <td valign="top">  W.F. Taylor,   "Equational logic"  ''Houston J. Math.''  (1979)  (Survey issue)</td></tr><tr><td valign="top">[a5]</td> <td valign="top">  S.N. Burris,   "Logic for mathematics and computer science" , Prentice-Hall  (1998)</td></tr></table>