Add some notes on ambiguity during Skolemization

Author: v--

text/first_order_theories.tex

@@ -1012,6 +1012,8 @@ \section{First-order theories}\label{sec:first_order_theories}
 
   Optionally, fix also a \hyperref[def:fol_semantics/model]{model} \( \mscrX = (X, I) \) of \( \varphi \) and a \hyperref[def:choice_function]{choice function} \( c \) for the subsets of \( X \).
 
+  We will also need an operation \( \sharp_m \), similar to the one for substitution discussed in \cref{def:atomic_lambda_term_substitution/sharp}, that provides us with a fresh function symbol of arity \( m \). For definiteness, suppose that \( \sharp_m(F) \) is \( a^m \), where \( a \) is the smallest \hyperref[def:variable_identifier]{small Latin identifiers} such that \( a^m \) is not in \( F \).
+
   We will use recursion on \( k \leq n \) to build a quadruple \( (\Sigma_k, \phi_k, U_k, \mscrX_k) \) consisting of the following:
   \begin{itemize}
     \item \( \Sigma_k \) is an extension of \( \Sigma \).
@@ -1061,7 +1063,9 @@ \section{First-order theories}\label{sec:first_order_theories}
 
     \thmitem{alg:fol_skolemization/existential} At step \( k > 0 \), suppose that \( Q_k = \synexists \). Let \( U_k \coloneqq U_{k-1} \) and suppose that \( x_{i_1}, \ldots, x_{i_m} \) are the variables in \( U_k = U_{k-1} \).
 
-    Fix a new function symbol \( f_k \) of arity \( m \). Define \( \Sigma_k \) to be the extension of \( \Sigma_{k-1} \) with \( f_k \) and let
+    The function \( \sharp_m \) discussed above gives us a new function symbol \( f_k \) of arity \( m \).
+
+    Define \( \Sigma_k \) to be the extension of \( \Sigma_{k-1} \) with \( f_k \) and let
     \begin{equation*}
       \psi_k \coloneqq \psi_{k-1}[x_k \mapsto f_k(x_{i_1}, \ldots, x_{i_m})].
     \end{equation*}
@@ -1076,14 +1080,16 @@ \section{First-order theories}\label{sec:first_order_theories}
 
     Let \( I_k \) be the extension of the interpretation \( I_{k-1} \) to \( f \) such that
     \begin{equation*}
-      I_k(f)\parens[\big]{ v(x_{i_1}), \ldots, v(x_{i_m}) } \coloneqq c(A_v).
+      I_k(f)\parens[\big]{ v(x_{i_1}), \ldots, v(x_{i_m}) } \coloneqq c(A_v),
     \end{equation*}
+    where \( c \) is the choice function we have fixed in the beginning.
 
     We call \( I_k(f) \) a \term[en=Skolem function (\cite[thm. 2.3.34]{Hinman2005Logic})]{Skolem function}. Naturally, we let \( \mscrX_k \coloneqq (X, I_k) \).
   \end{thmenum}
 \end{algorithm}
 \begin{comments}
   \item The overall premise of Skolemization is described in \cref{rem:definitional_extensions_and_skolemization}.
+  \item There are two sources of ambiguity in the algorithm --- the choice of Skolem function symbols and the choice of the functions themselves. The disambiguation that we may find useful depends on the situation.
   \item This algorithm can be found as \identifier{math.logic.skolemization.skolemize} in \cite{notebook:code}.
 \end{comments}