Namespaces
Variants
Actions

Difference between revisions of "Equational logic"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (AUTOMATIC EDIT (latexlist): Replaced 114 formulas out of 114 by TEX code with an average confidence of 2.0 and a minimal confidence of 2.0.)
 
Line 1: Line 1:
 +
<!--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.
 
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e1201401.png" /> is a formal language whose alphabet consists of a countable set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e1201402.png" /> of variables, a set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e1201403.png" /> of function symbols and an equality symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e1201404.png" />. Moreover, a function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e1201405.png" /> is given and for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e1201406.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e1201407.png" /> denotes the number of argument places of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e1201408.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e1201409.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014010.png" /> is called a constant.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014011.png" /> a class of algebras of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014013.png" />, i.e. structures <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014014.png" /> of the form
+
One associates with $L$ a class of algebras of type $L$, i.e. structures $\mathcal{A}$ of the form
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014015.png" /></td> </tr></table>
+
\begin{equation*} \langle A , \tilde { f } \rangle _ { f \in \Phi }, \end{equation*}
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014016.png" /> is a non-empty set; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014017.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014018.png" /> is a function with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014019.png" /> arguments running over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014020.png" /> and with values in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014021.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014022.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014023.png" />.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014024.png" /> of terms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014025.png" /> to be the least set of finite sequences of letters of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014026.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014027.png" /> contains the one-term sequence consisting of a variable or a constant, and such that if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014028.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014029.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014030.png" /> is an algebra of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014031.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014032.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014033.png" /> denotes a composition of some of the functions and constants <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014034.png" />, which is coded by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014035.png" />. A term of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014036.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014037.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014038.png" />, is called atomic.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014039.png" /> are equations, i.e., sequences of letters of the form
+
The only truth-valued expressions of $L$ are equations, i.e., sequences of letters of the form
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014040.png" /></td> <td valign="top" style="width:5%;text-align:right;">(a1)</td></tr></table>
+
\begin{equation} \tag{a1} s = t, \end{equation}
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014041.png" />. One says that (a1) is true in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014042.png" /> if and only if the objects <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014043.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014044.png" /> are equal.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014045.png" /> is a set of equations, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014046.png" /> is called a model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014047.png" /> if and only if all the equations of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014048.png" /> are true in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014049.png" />. The class of all models of some set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014050.png" /> is called a variety.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014051.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014052.png" />, one denotes by
+
For any $s , t \in T$ and $v \in V$, one denotes by
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014053.png" /></td> </tr></table>
+
\begin{equation*} s \left( \begin{array} { l } { v } \\ { t } \end{array} \right) \end{equation*}
  
the term obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014054.png" /> by substituting all occurrences of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014055.png" /> by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014056.png" />.
+
the term obtained from $s$ by substituting all occurrences of $v$ by $t$.
  
The rules of proof of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014057.png" /> are the following:
+
The rules of proof of $L$ are the following:
  
i) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014058.png" /> is accepted for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014059.png" />;
+
i) $t = t$ is accepted for all $t \in T$;
  
ii) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014060.png" /> yields <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014061.png" />;
+
ii) $s = t$ yields $t = s$;
  
iii) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014062.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014063.png" /> yield <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014064.png" />;
+
iii) $r = s$ and $s = t$ yield $r = t$;
  
iv) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014065.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014066.png" /> yield
+
iv) $q = r$ and $s = t$ yield
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014067.png" /></td> </tr></table>
+
\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014068.png" /> of equations is called an equational theory if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014069.png" /> is closed under the rules i)–iv). Thus, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014070.png" /> is a model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014071.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014072.png" /> is also a model of the least equational theory including <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014073.png" />.
+
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.
 
The above concepts and rules were introduced in 1935 by G. Birkhoff, and he proved the following fundamental theorems.
  
Birkhoff's completeness theorem: If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014074.png" /> is an equational theory and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014075.png" /> is true in all the models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014076.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014077.png" /> belongs to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014078.png" />.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014079.png" /> of algebras of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014080.png" /> is a variety if and only if it satisfies the following three conditions:
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014081.png" /> are in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014082.png" />;
+
a) all subalgebras of the algebras of $C$ are in $C$;
  
b) all homomorphic images of the algebras of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014083.png" /> are in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014084.png" />;
+
b) all homomorphic images of the algebras of $C$ are in $C$;
  
c) for any subset <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014085.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014086.png" />, the direct product of the algebras in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014087.png" /> belongs to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014088.png" />.
+
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.
 
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014089.png" /> of a first-order theory can be regarded as a two-sorted algebra whose universes are the universe of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014090.png" /> and a two-element Boolean algebra, while treating the relations of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014091.png" /> as Boolean-valued functions. Corresponding to that view (following [[#References|[a3]]]) there is a natural translation of any first-order language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014092.png" /> into a two-sorted equational language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014093.png" />. Namely, the formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014094.png" /> are treated as Boolean-valued terms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014095.png" /> and the terms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014096.png" /> are treated as object-valued terms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014097.png" />. The axioms and rules of first-order logic turn into the rules i)–iv) (adapted to the two-sorted language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014098.png" />) plus five axiom schemata:
+
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) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e12014099.png" />;
+
1) $[ ( \varphi \rightarrow \psi ) \rightarrow ( ( \psi \rightarrow \chi ) \rightarrow ( \varphi \rightarrow \chi ) ) ] = 1$;
  
2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140100.png" />;
+
2) $( \varphi \rightarrow ( \neg \varphi \rightarrow \psi ) ) = 1$;
  
3) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140101.png" />;
+
3) $( ( \neg \varphi \rightarrow \varphi ) \rightarrow \varphi ) = 1$;
  
4) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140102.png" />;
+
4) $( 1 \rightarrow \varphi ) = \varphi$;
  
5) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140103.png" />. Here <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140104.png" /> run over formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140105.png" />, the quantifiers of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140106.png" /> are understood as abbreviations, viz.
+
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.
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140107.png" /></td> </tr></table>
+
\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140108.png" /> is an object-valued variable, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140109.png" /> is an object-valued atomic term, called an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140111.png" />-term, whose variables are the free variables of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140112.png" /> other than <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140113.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140116.png" />-symbol (which he formulated in 1925).
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140117.png" />-terms. And those <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e120/e120140/e120140118.png" />-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.
+
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]]]).
 
Presently (1998), many researchers are trying to apply equational logic to obtain efficient automatic theorem proving procedures (see [[#References|[a5]]]).
  
 
====References====
 
====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>
+
<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>

Latest revision as of 17:00, 1 July 2020

Formal languages are mathematical models of the natural (informal) languages of mathematics (cf. also Formal languages and automata). In 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, 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 ) > 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 [a2], [a4] and references therein.

In mathematical practice, as a rule one uses informal multi-sorted languages (cf. also Logical calculus). Equational logic generalizes in a similar way. For example, a 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 [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, 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 for first-order logic can be seen as a consequence of Birkhoff's completeness theorem stated above (see [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 [a2], [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 [a5]).

References

[a1] J. van Heijenoort, "From Frege to Gödel: A source book in mathematical logic 1878-1931" , Harvard Univ. Press (1977) (Edition: Third, corrected)
[a2] R.N. McKenzie, G.F. McNulty, W.F. Taylor, "Algebras, lattices, varieties" , I , Wadsworth&Brooks/Cole (1987)
[a3] J. Mycielski, "Equational treatment of first-order logic" Algebra Univ. , 33 (1995) pp. 26–39
[a4] W.F. Taylor, "Equational logic" Houston J. Math. (1979) (Survey issue)
[a5] S.N. Burris, "Logic for mathematics and computer science" , Prentice-Hall (1998)
How to Cite This Entry:
Equational logic. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Equational_logic&oldid=50386
This article was adapted from an original article by Jan Mycielski (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article