Update obsolete references

Author: v--

text/algebras_over_semirings.tex

@@ -96,7 +96,7 @@ \section{Algebras over semirings}\label{sec:algebras_over_semirings}
   \item If \( A \) is also an \( R \)-algebra, we denote the set of all \( R \)-\hyperref[def:algebra_over_semiring/homomorphism]{algebra homomorphisms} by \( \hom(A, N) \) in accordance with the general notation for \hyperref[def:category/morphisms]{categorical morphism sets}.
 \end{comments}
 \begin{proof}
-  By \cref{thm:functions_over_model_form_model}, \( N \) is both an \( R \)-semiring and an \( R \)-semimodule. Compatibility comes from left distributivity in \( N \).
+  By \cref{thm:fol_equational_theory_models/functions}, \( N \) is both an \( R \)-semiring and an \( R \)-semimodule. Compatibility comes from left distributivity in \( N \).
 \end{proof}
 
 \paragraph{Semigroup algebras}

text/first_order_structures.tex

@@ -25,6 +25,22 @@ \section{First-order structures}\label{sec:first_order_structures}
   \item Substructures correspond to \hyperref[def:categorical_subobject]{categorical subobjects}; see \cref{thm:fol_categorical_subobjects}.
 \end{comments}
 
+\begin{example}\label{ex:replacing_functional_symbols_via_relations}
+  Consider the \hyperref[def:semigroup/theory]{theory of semigroups}. We have a functional symbol \( \cdot \), which we can also represent via the ternary predicate \( p(x, y, z) \), which holds for \( (a, b, c) \) in some structure \( \mscrX = (X, I) \) if and only if \( a \cdot b = c \).
+
+  If we choose to work only with the relation, the signature would not have any function symbols, and every subset of \( X \) would induce a substructure.
+
+  This also introduces a complication, however. We must ensure that the relation represents a function, and this can be done via the axiom
+  \begin{equation*}
+    \qforall x \qforall y \qExists z p(x, y, z),
+  \end{equation*}
+  where we have used the unique existence shorthand from \cref{rem:fol_exists_unique_abbreviation}.
+
+  In this setting, a model of the theory of semigroups must satisfy this axiom, and thus it is possible for a substructure not to be a model.
+
+  For example, the negative real numbers are not a semigroup under multiplication because the product of two negative numbers is positive. A functional symbol encodes this requirement into the definition of a substructure. But otherwise we must encode this via formulas, which makes the definition of substructure trivial, but now it is possible for a substructure not to be a model.
+\end{example}
+
 \begin{proposition}\label{thm:fol_substructure_characterization}
   Given a structure \( \mscrX = (X, I) \), the subset \( A \subseteq X \) \hyperref[def:fol_substructure/induces]{induces} a substructure of \( \mscrX \) if and only if it is closed under \( I(f) \) for every function symbol \( f \).
 \end{proposition}

text/rings.tex

@@ -1141,7 +1141,7 @@ \section{Rings}\label{sec:rings}
       (\xi \syneq 0) \synvee \qexists \eta (\xi \cdot \eta \syneq 1).
     \end{equation}
 
-    These axioms are not \hyperref[def:positive_formula]{positive formulas}, hence many structural theorems from \fullref{sec:first_order_models} fail to hold for them.
+    The resulting theory is no longer an \hyperref[def:fol_equational_theory]{equational theory}, hence many theorems from \fullref{sec:equational_theories} to hold for them.
 
     \thmitem{def:field/homomorphism}\mcite[453]{Knapp2016BasicAlgebra} A \hyperref[def:fol_homomorphism]{first-order homomorphism} between fields is simply a \hyperref[def:ring/homomorphism]{unital ring homomorphism}.
 

text/semigroups.tex

@@ -263,7 +263,7 @@ \section{Semigroups}\label{sec:semigroups}
 
   \SubProofOf{thm:zero_morphisms_pointed/kernel}
 
-  \SubProof*{Proof that \( \ker f \) is a submodel of \( A \)} As the preimage of the submodel \( \set{ e_B } \) of \( B \), \( \ker f \) is a substructure of \( A \) as a consequence of \cref{thm:def:fol_homomorphism/preimage_is_substructure}. As a substructure, \( \ker f \) is a model of \( \Gamma \) as a consequence of \cref{thm:substructure_is_model}.
+  \SubProof*{Proof that \( \ker f \) is a submodel of \( A \)} As the preimage of the submodel \( \set{ e_B } \) of \( B \), \( \ker f \) is a substructure of \( A \) as a consequence of \cref{thm:def:fol_homomorphism/preimage_is_substructure}. As a substructure, \( \ker f \) is a model of \( \Gamma \) as a consequence of \cref{thm:fol_equational_theory_models/substructure}.
 
   \SubProof*{Proof that \( (\ker f, \iota) \) is an equalizer cone} The following diagram must commute:
   \begin{equation*}
@@ -287,7 +287,7 @@ \section{Semigroups}\label{sec:semigroups}
 
   \SubProofOf{thm:zero_morphisms_pointed/cokernel}
 
-  \SubProof*{Proof that \( \co\ker f \) is a model of \( \Gamma \)} Follows from \cref{thm:quotient_preserves_positive_formulas}.
+  \SubProof*{Proof that \( \co\ker f \) is a model of \( \Gamma \)} Follows from \cref{thm:fol_equational_theory_models/quotient}.
 
   \SubProof*{Proof that \( (\co\ker f, \pi) \) is a coequalizer cocone} The following diagram must commute:
   \begin{equation*}
@@ -326,7 +326,7 @@ \section{Semigroups}\label{sec:semigroups}
 
   Therefore, the set-theoretic image \( f[A] \) necessarily belongs to the category-theoretic image \( \img f \).
 
-  \Cref{thm:def:fol_substructure/homomorphism_image} implies that \( f[A] \) is a substructure of \( B \) and \cref{thm:substructure_is_model} implies that it is a model of \( \Gamma \). Hence, \( f[A] \) is an object in the category \( \cat{C} \).
+  \Cref{thm:def:fol_substructure/homomorphism_image} implies that \( f[A] \) is a substructure of \( B \) and \cref{thm:fol_equational_theory_models/substructure} implies that it is a model of \( \Gamma \). Hence, \( f[A] \) is an object in the category \( \cat{C} \).
 
   As a substructure of \( \mscrY \), it is closed under function applications in \( \mscrY \), hence it contains the equivalence class of \( e_B \) under \( {\cong} \).
 

text/semimodules.tex

@@ -353,7 +353,7 @@ \section{Semimodules}\label{sec:semimodules}
   \end{equation*}
 
   \begin{thmenum}
-    \thmitem{def:free_semimodule/operations} \Cref{thm:functions_over_model_form_model} implies that \( R^{\oplus A} \) is a semiring with the elementwise addition and multiplication inherited from \( R \). Scalar multiplication by \( r \in R \) can be defined as multiplication by the \hyperref[def:constant_function]{constant function} at \( r \).
+    \thmitem{def:free_semimodule/operations} \Cref{thm:fol_equational_theory_models/functions} implies that \( R^{\oplus A} \) is a semiring with the elementwise addition and multiplication inherited from \( R \). Scalar multiplication by \( r \in R \) can be defined as multiplication by the \hyperref[def:constant_function]{constant function} at \( r \).
 
     \thmitem{def:free_semimodule/inclusion} We start with the canonical inclusion
     \begin{equation*}

text/semirings.tex

@@ -408,20 +408,6 @@ \section{Semirings}\label{sec:semirings}
   We say that a \hyperref[def:semiring]{semiring} is \term[ru=целостное (\cite[def. 3.5.1]{Винберг2014КурсАлгебры})]{entire} if it has no \hyperref[def:divisibility]{nontrivial zero divisors}, neither left nor right.
 \end{definition}
 
-\begin{remark}\label{rem:entire_semiring_axiom}
-  The following first-order axiom, based on \cite[def. III.1.10]{Aluffi2009Algebra}, ensures that a semiring is \hyperref[def:entire_semiring]{entire}:
-  \begin{equation}\label{eq:rem:entire_semiring_axiom}
-    \synx \cdot \syny \syneq 0 \synimplies (\synx \syneq 0 \synvee \syny \syneq 0).
-  \end{equation}
-
-  It is technically not a \hyperref[def:positive_formula]{positive formula} because it contains an implication, but rewriting the conditional via \eqref{eq:thm:classical_equivalences/conditional_as_disjunction}, we obtain another formula that is more obviously not positive:
-  \begin{equation*}
-    \synneg (\synx \cdot \syny \syneq 0) \synvee \synx \syneq 0 \synvee \syny \syneq 0.
-  \end{equation*}
-
-  As a side effect, results from \fullref{sec:first_order_models} concerning positive formulas do not hold for \hyperref[def:integral_domain]{integral domains} and especially \hyperref[def:field]{fields}.
-\end{remark}
-
 \begin{example}\label{ex:def:entire_semiring}
   We list examples of (non-)\hyperref[def:entire_semiring]{entire} semirings:
   \begin{thmenum}