Add a section on equational theories

Author: v--

notebook.tex

@@ -213,6 +213,7 @@
   \include{text/first_order_models}
   \include{text/unisorted_unification}
   \include{text/first_order_natural_deduction}
+  \include{text/equational_theories}
   \include{text/higher_order_logic}
   \include{text/higher_order_natural_deduction}
   \include{text/henkin_semantics}

text/equational_theories.tex

@@ -0,0 +1,49 @@
+\section{Equational theories}\label{sec:equational_theories}
+
+\paragraph{Theory of pure equality}
+
+\begin{definition}\label{def:pure_equality}\mimprovised
+  Over the empty \hyperref[def:fol_signature]{first-order signature}, consider the \hyperref[def:fol_theory]{theory} axiomatized by an empty set of sentences. Its only terms are variables and its atomic formulas are either logical constants or equality formulas. For this reason, we call it the \term{theory of pure equality} and denote it by \( \op*{Th}_{\syneq} \). Similarly, we denote the signature by \( \op*{Sign}_{\syneq} \).
+\end{definition}
+
+\begin{proposition}\label{thm:pure_equality_isomorphism}
+  The \hyperref[def:pure_equality]{theory of pure equality} \( \op*{Th}_{\syneq} \) for \hyperref[def:fol_structure]{structures} has the following basic properties:
+  \begin{thmenum}
+    \thmitem{thm:pure_equality_isomorphism/function} Every function \( f: X \to Y \) between the structures \( \mscrX = (X, I) \) and \( \mscrY = (Y, J) \) over \( \op*{Sign}_{\syneq} \) is a \hyperref[def:fol_homomorphism]{homomorphism}.
+
+    \thmitem{thm:pure_equality_isomorphism/subset} Given two structures \( \mscrX = (X, I) \) and \( \mscrY = (Y, J) \) over \( \op*{Sign}_{\syneq} \), if \( X \) is a subset of \( Y \), \( \mscrX \) is a substructure of \( \mscrY \).
+
+    \thmitem{thm:pure_equality_isomorphism/model} Every structure over \( \op*{Sign}_{\syneq} \) is a model of \( \op*{Th}_{\syneq} \).
+
+    \thmitem{thm:pure_equality_isomorphism/extensions} Every theory over every signature is an \hyperref[def:fol_theory/extension]{extension} of \( \op*{Th}_{\syneq} \).
+
+    \thmitem{thm:pure_equality_isomorphism/isomorphism} Two structures over \( \op*{Sign}_{\syneq} \) are \hyperref[def:fol_isomorphism]{isomorphic} if and only if they have the same \hyperref[thm:cardinality_existence]{cardinality}.
+
+    \thmitem{thm:pure_equality_isomorphism/finite_elementary_equivalence} Two \hi{finite} structures over \( \op*{Sign}_{\syneq} \) are \hyperref[def:elementary_equivalence]{elementary equivalent} if and only if they have the same cardinality.
+  \end{thmenum}
+\end{proposition}
+\begin{proof}
+  \SubProofOf{thm:pure_equality_isomorphism/function} The function \( f: X \to Y \) is vacuously a homomorphism because there are no function or predicate symbols.
+
+  \SubProofOf{thm:pure_equality_isomorphism/subset} Also vacuous.
+
+  \SubProofOf{thm:pure_equality_isomorphism/model} Since \( \op*{Th}_{\syneq} \) is the consequence closure of the empty set, \cref{thm:institutional_satisfaction_closure} implies that every structure \( \mscrX \) over \( \op*{Sign}_{\syneq} \) satisfying \( \varnothing \) also satisfies \( \op*{Th}_{\syneq} \).
+
+  \SubProofOf{thm:pure_equality_isomorphism/extensions} The proof is trivial, but we will spell out the details.
+
+  Let \( \iota: \op*{Sign}_{\syneq} \to \Sigma \) be the signature inclusion morphism into some signature \( \Sigma \).
+
+  Consider some structure \( \mscrX \) over \( \Sigma \). Its \hyperref[def:fol_reduct_along_morphism]{reduct} \( \red_\iota(\mscrX) \) along \( \iota \) is a structure over \( \op*{Sign}_{\syneq} \). \Cref{thm:pure_equality_isomorphism/model} implies that \( \red_\iota(\mscrX) \) satisfies \( \op*{Th}_{\syneq} \), and \cref{def:institution/satisfaction} implies that \( \mscrX \) satisfies the translation \( \op*{Sen}(\iota)[\op*{Th}_{\syneq}] \).
+
+  \SubProofOf{thm:pure_equality_isomorphism/isomorphism} Let \( \mscrX = (X, I) \) and \( \mscrY = (Y, J) \) be two structures over \( \op*{Sign}_{\syneq} \).
+
+  \SufficiencySubProof* Let \( h: X \to Y \) be an isomorphism. Then it is bijective, hence \( X \) and \( Y \) have the same cardinality.
+
+  \NecessitySubProof* Suppose that \( X \) and \( Y \) have the same cardinality. Then there exists a bijective map \( h: X \to Y \), which is vacuously an isomorphism because there are no function or predicate symbols.
+
+  \SubProofOf{thm:pure_equality_isomorphism/finite_elementary_equivalence}
+
+  \SufficiencySubProof* \Cref{thm:def:elementary_equivalence/finite} implies that, if two structures are finite and elementarily equivalent, they are isomorphic.
+
+  \NecessitySubProof* \Cref{thm:pure_equality_isomorphism/isomorphism} implies that, if two structures have the same cardinality, they are isomorphic. Then \cref{thm:def:elementary_embedding/isomorphism} implies that they are elementarily equivalent.
+\end{proof}

text/first_order_logic.tex

@@ -1670,49 +1670,3 @@ \section{First-order logic}\label{sec:first_order_logic}
 
   Again, we can use the cardinality control formulas from \cref{thm:cardinality_control_formulas}. We have \( \mscrX \vDash \chi^{\geq n} \) for every \( n \geq 1 \). By elementary equivalence, \( \mscrY \vDash \chi^{\geq n} \) for every \( n \geq 1 \), which implies that \( Y \) is also infinite.
 \end{proof}
-
-\begin{definition}\label{def:pure_equality}\mimprovised
-  Over the empty \hyperref[def:fol_signature]{first-order signature}, consider the \hyperref[def:fol_theory]{theory} axiomatized by an empty set of sentences. Its only terms are variables and its atomic formulas are either logical constants or equality formulas. For this reason, we call it the \term{theory of pure equality} and denote it by \( \op*{Th}_{\syneq} \). Similarly, we denote the signature by \( \op*{Sign}_{\syneq} \).
-\end{definition}
-
-\begin{proposition}\label{thm:pure_equality_isomorphism}
-  The \hyperref[def:pure_equality]{theory of pure equality} \( \op*{Th}_{\syneq} \) for \hyperref[def:fol_structure]{structures} has the following basic properties:
-  \begin{thmenum}
-    \thmitem{thm:pure_equality_isomorphism/function} Every function \( f: X \to Y \) between the structures \( \mscrX = (X, I) \) and \( \mscrY = (Y, J) \) over \( \op*{Sign}_{\syneq} \) is a \hyperref[def:fol_homomorphism]{homomorphism}.
-
-    \thmitem{thm:pure_equality_isomorphism/subset} Given two structures \( \mscrX = (X, I) \) and \( \mscrY = (Y, J) \) over \( \op*{Sign}_{\syneq} \), if \( X \) is a subset of \( Y \), \( \mscrX \) is a substructure of \( \mscrY \).
-
-    \thmitem{thm:pure_equality_isomorphism/model} Every structure over \( \op*{Sign}_{\syneq} \) is a model of \( \op*{Th}_{\syneq} \).
-
-    \thmitem{thm:pure_equality_isomorphism/extensions} Every theory over every signature is an \hyperref[def:fol_theory/extension]{extension} of \( \op*{Th}_{\syneq} \).
-
-    \thmitem{thm:pure_equality_isomorphism/isomorphism} Two structures over \( \op*{Sign}_{\syneq} \) are \hyperref[def:fol_isomorphism]{isomorphic} if and only if they have the same \hyperref[thm:cardinality_existence]{cardinality}.
-
-    \thmitem{thm:pure_equality_isomorphism/finite_elementary_equivalence} Two \hi{finite} structures over \( \op*{Sign}_{\syneq} \) are \hyperref[def:elementary_equivalence]{elementary equivalent} if and only if they have the same cardinality.
-  \end{thmenum}
-\end{proposition}
-\begin{proof}
-  \SubProofOf{thm:pure_equality_isomorphism/function} The function \( f: X \to Y \) is vacuously a homomorphism because there are no function or predicate symbols.
-
-  \SubProofOf{thm:pure_equality_isomorphism/subset} Also vacuous.
-
-  \SubProofOf{thm:pure_equality_isomorphism/model} Since \( \op*{Th}_{\syneq} \) is the consequence closure of the empty set, \cref{thm:institutional_satisfaction_closure} implies that every structure \( \mscrX \) over \( \op*{Sign}_{\syneq} \) satisfying \( \varnothing \) also satisfies \( \op*{Th}_{\syneq} \).
-
-  \SubProofOf{thm:pure_equality_isomorphism/extensions} The proof is trivial, but we will spell out the details.
-
-  Let \( \iota: \op*{Sign}_{\syneq} \to \Sigma \) be the signature inclusion morphism into some signature \( \Sigma \).
-
-  Consider some structure \( \mscrX \) over \( \Sigma \). Its \hyperref[def:fol_reduct_along_morphism]{reduct} \( \red_\iota(\mscrX) \) along \( \iota \) is a structure over \( \op*{Sign}_{\syneq} \). \Cref{thm:pure_equality_isomorphism/model} implies that \( \red_\iota(\mscrX) \) satisfies \( \op*{Th}_{\syneq} \), and \cref{def:institution/satisfaction} implies that \( \mscrX \) satisfies the translation \( \op*{Sen}(\iota)[\op*{Th}_{\syneq}] \).
-
-  \SubProofOf{thm:pure_equality_isomorphism/isomorphism} Let \( \mscrX = (X, I) \) and \( \mscrY = (Y, J) \) be two structures over \( \op*{Sign}_{\syneq} \).
-
-  \SufficiencySubProof* Let \( h: X \to Y \) be an isomorphism. Then it is bijective, hence \( X \) and \( Y \) have the same cardinality.
-
-  \NecessitySubProof* Suppose that \( X \) and \( Y \) have the same cardinality. Then there exists a bijective map \( h: X \to Y \), which is vacuously an isomorphism because there are no function or predicate symbols.
-
-  \SubProofOf{thm:pure_equality_isomorphism/finite_elementary_equivalence}
-
-  \SufficiencySubProof* \Cref{thm:def:elementary_equivalence/finite} implies that, if two structures are finite and elementarily equivalent, they are isomorphic.
-
-  \NecessitySubProof* \Cref{thm:pure_equality_isomorphism/isomorphism} implies that, if two structures have the same cardinality, they are isomorphic. Then \cref{thm:def:elementary_embedding/isomorphism} implies that they are elementarily equivalent.
-\end{proof}