Fix invalid references

Author: v--

text/first_order_natural_deduction.tex

@@ -586,7 +586,7 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 
   \item The term \enquote{eigenvariable} comes from \tcite{#2, where #1}{Gentzen1935LogischeSchließen} introduces natural deduction. In the corresponding English translation, \cite[293]{Gentzen1964LogicalDeduction}, eigenvariables are instead called \enquote{proper variables}. Both terms are currently used in English (e.g. \incite[\S 5.1.10]{Mimram2020ProgramEqualsProof} uses \enquote{eigenvariable}, while \incite[38]{TroelstraSchwichtenberg2000BasicProofTheory} uses \enquote{proper variable}).
 
-  Gentzen presents only two rules featuring eigenvariables, in which the variables must satisfy slightly differing constraints. We restate Gentzen's rules in \cref{def:fol_natural_deduction} and adapt them for \hyperref[def:higher_order_logic]{higher-order logic} in \cref{def:hol_quantifier_rules/eigenvariables}.
+  Gentzen presents only two rules featuring eigenvariables, in which the variables must satisfy slightly differing constraints. We formalize Gentzen's rules in \cref{def:fol_natural_deduction} and adapt them for \hyperref[def:higher_order_logic]{higher-order logic} in \cref{def:hol_natural_deduction}.
 
   \item Natural deduction proof trees are implemented in the module \identifier{math.logic.deduction.proof_tree} in \cite{notebook:code}.
 \end{comments}
@@ -697,7 +697,7 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
           \begin{prooftree}
             \hypo{ \syn\varphi[\synx \synsubst \syn\tau] }
             \hypo{ \syn\tau \syneq \syn\sigma }
-            \infer2[\ref{inf:def:hol_equality_rules/elim}]{ \syn\varphi[\synx \synsubst \syn\sigma] }
+            \infer2[\ref{inf:def:fol_natural_deduction/equality/elim}]{ \syn\varphi[\synx \synsubst \syn\sigma] }
           \end{prooftree}
         \end{equation*}
       \end{rightcolumn}

text/higher_order_logic.tex

@@ -330,9 +330,9 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
 
     So, we must disregard implicit judgmental equality.
 
-    \thmitem{rem:mltt_hol/rules} Some \hyperref[con:typing_rule]{typing rules} like \ref{inf:def:dependent_product/intro} transfer directly to their counterpart \ref{inf:def:hol_quantifier_rules/eigenvariables/forall_intro}, while other like \ref{inf:def:dependent_sum/elim} differ from \ref{inf:def:hol_quantifier_rules/eigenvariables/exists_elim} in subtle ways --- see \cref{rem:dependent_products_and_forall_quantifier_rules}.
+    \thmitem{rem:mltt_hol/rules} Some \hyperref[con:typing_rule]{typing rules} like \ref{inf:def:identity_type/intro} and \ref{inf:def:dependent_product/intro} translate directly to their counterparts \ref{inf:def:hol_natural_deduction/equality/intro} and \ref{inf:def:hol_natural_deduction/forall/intro}, while other like \ref{inf:def:dependent_sum/elim} differ from \ref{inf:def:hol_natural_deduction/exists/elim} in subtle ways --- see \cref{rem:dependent_products_and_forall_quantifier_rules}.
 
-    Finally, some logical rules like those in \cref{def:hol_equality_rules} have no type-theoretic counterpart.
+    Finally, some logical rules like the equality rule \ref{inf:def:hol_natural_deduction/equality/iff} have no type-theoretic counterpart.
 
     This requires us to state new rules rather than reuse those from \fullref{sec:dependent_types}.
   \end{thmenum}
@@ -418,7 +418,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
 \begin{comments}
   \item In a standard frame, it is sufficient to specify only the universes of sorts.
 
-  \item We adapt Andrew's definition from \cite[238]{Andrews2002Logic} to many-sorted signatures. Unlike Andrews, we refer to the individual sets as \enquote{universes} rather than \enquote{domains}; see \cref{rem:model_theory_universe_terminology}.
+  \item We adapt Andrew's definition from \cite[238]{Andrews2002Logic} to many-sorted signatures. Unlike Andrews, we refer to the individual sets as \enquote{universes} rather than \enquote{domains}; see \cref{rem:model_theory_structure_terminology}.
 
   Additionally, we distinguish between general and standard frames, while Andrews (and Henkin) only distinguish between general and standard \hyperref[def:hol_structure]{structures}.
 \end{comments}
@@ -512,7 +512,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
 \end{comments}
 
 \begin{remark}\label{rem:hol_definite_description}
-  Compared to Andrews and Farmer, we not only prefer the explicit typing rules from \cref{inf:def:hol_typing_rules} to the abbreviations from \cref{tab:rem:hol_formula_abbreviations}, but we also avoid the definite description operator \( \syndesc \) discussed in \cref{con:description_operator/iota}.
+  Compared to Andrews and Farmer, we not only prefer the explicit typing rules from \cref{def:hol_typing_rules} to the abbreviations from \cref{tab:rem:hol_formula_abbreviations}, but we also avoid the definite description operator \( \syndesc \) discussed in \cref{con:description_operator/iota}.
 
   Introducing this operator has some nontrivial consequences:
   \begin{thmenum}
@@ -1076,7 +1076,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
 
   Note that Andrews uses the abbreviations that we discuss in \cref{tab:rem:hol_formula_abbreviations}. Andrews spends considerable effort demonstrating that part of the familiar natural deduction rules from \cref{def:propositional_natural_deduction} are \hyperref[con:inference_rule_admissibility]{admissible}.
 
-  The axioms of the system are constructed so that they allow deriving many useful proofs. For example, axiom \( 4 \) allow performing \( \beta \)-reduction similarly to \ref{inf:def:hol_equality_rules/intro}. This axiom, along with rule \logic{R'}, allows proving \cref{thm:hol_equality_is_equivalence_relation}.
+  The axioms of the system are constructed so that they allow deriving many useful proofs. For example, axiom \( 4 \) allow performing \( \beta \)-reduction similarly to \ref{inf:def:hol_natural_deduction/equality/intro}. This axiom, along with rule \logic{R'}, allows proving \cref{thm:hol_natural_deduction_admissible_rules/equality}.
 
   An immediate downside to his system is that hypothesis discharging in rules such as \ref{inf:def:propositional_natural_deduction/imp/intro} requires rewriting the entire proof, akin to \fullref{alg:derivation_conclusion_hypothesis_introduction}, but more complicated.
 
@@ -1274,7 +1274,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
   First and foremost, a (syntactic or semantic) \term{theory} is, as in \cref{def:general_logic_theory}, a set of sentences closed under logical consequence. For any set of sentences \( \Gamma \), we denote its consequence closure by \( \cat{Th}(\Gamma) \), and say that \( \Gamma \) \term{axiomatizes} \( \cat{Th}(\Gamma) \).
 
   \begin{thmenum}
-    \thmitem{def:hol_theory/morphism} As in \cref{def:entailment_system_theory/morphism}, we call the \hyperref[def:hol_signature_category/morphisms]{first-order signature morphism} \( t: \Sigma \to \Sigma' \) a \term{theory morphisms} from \( (\Sigma, T) \) to \( (\Sigma', T') \) if the translation of the formulas in \( T \) belong to \( T' \).
+    \thmitem{def:hol_theory/morphism} As in \cref{def:entailment_system_theory/morphism}, we call the \hyperref[def:hol_signature_category]{signature morphism} \( t: \Sigma \to \Sigma' \) a \term{theory morphisms} from \( (\Sigma, T) \) to \( (\Sigma', T') \) if the translation of the formulas in \( T \) belong to \( T' \).
 
     \thmitem{def:hol_theory/extension} As for first-order theories, we call \( T^+ \) an \term{extension} of \( T \) if \( t \) is an inclusion map that only adds new signature symbols.
 
@@ -1454,7 +1454,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
 \end{proof}
 
 \begin{theorem}[Weak higher-order completeness]\label{thm:hol_weak_completeness}
-  The \hyperref[def:fol_natural_deduction]{classical higher-order natural deduction system} is \hyperref[def:general_logic/completeness]{complete} with respect to \hyperref[def:fol_semantics/standard]{general higher-order semantics}.
+  The \hyperref[def:fol_natural_deduction]{classical higher-order natural deduction system} is \hyperref[def:general_logic/completeness]{complete} with respect to \hyperref[def:hol_semantics/standard]{general higher-order semantics}.
 \end{theorem}
 \begin{comments}
   \item As discussed by \incite{Henkin1950CompletenessInTheoryOfTypes}, this does not hold for standard semantics.
@@ -1489,7 +1489,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
   \item This is one of several compactness theorems presented here --- see \cref{rem:logical_compactness_theorems}.
 \end{comments}
 \begin{proof}
-  \Cref{thm:hol_weak_semantic_compactness/relation} Follows from \fullref{thm:hol_compactness} via \cref{thm:completeness_implies_compactness}.
+  \Cref{thm:hol_weak_semantic_compactness/relation} Follows from \fullref{thm:hol_weak_compactness} via \cref{thm:completeness_implies_compactness}.
 
   The equivalence between the different conditions can be shown as in \fullref{thm:classical_propositional_semantic_compactness}.
 \end{proof}