Valuations of logical terms in higher-order logic

Author: v--

text/first_order_logic.tex

@@ -329,7 +329,7 @@ \section{First-order logic}\label{sec:first_order_logic}
 \end{definition}
 \begin{comments}
   \item Some authors like Peter Hinman in \incite[def. 2.1.15(iii)]{Hinman2005Logic} define \( I(p) \) to be a \hyperref[def:relation]{relation} \( I(p) \subseteq X^n \), however it is more convenient for us to work with Boolean-valued functions. The two approaches are equivalent as explained in \cref{rem:boolean_valued_functions_and_relations}.
-  \item Unlike in the rest of this monograph, when dealing with first-order structures directly, it is important to distinguish between the structure \( \mscrX \) as a pair and its domain \( X \) as a set. See \cref{rem:first_order_model_notation}.
+  \item Unlike in the rest of this monograph, when dealing with first-order structures directly, it is important to distinguish between the structure \( \mscrX \) as a pair and its domain \( X \) as a set. See \cref{rem:hol_structure_notation}.
 \end{comments}
 
 \begin{remark}\label{rem:empty_first_order_structures}

text/first_order_models.tex

@@ -6,12 +6,6 @@ \section{First-order models}\label{sec:first_order_models}
   \todo{Algebraic theories}
 \end{concept}
 
-\begin{definition}\label{def:propositional_model}\mcite[def. 1.4.1(i)]{Hinman2005Logic}
-  We say that the \hyperref[def:propositional_valuation/interpretation]{propositional interpretation} \( I \) is a \term{propositional model} of the set of \hyperref[def:propositional_syntax/formula]{propositional formulas} \( \Gamma \) if \( \Bracks{\varphi}_I = T \) for every formula \( \varphi \in \Gamma \).
-
-  We also say that \( I \) \term{satisfies} \( \Gamma \) and that \( \Gamma \) is \term{satisfiable} if there exists at least one model for it.
-\end{definition}
-
 \begin{remark}\label{rem:first_order_satisfiability_bivalence}
   We will now show why \cref{def:propositional_model} requires some adjustments for first-order formulas.
 
@@ -89,16 +83,6 @@ \section{First-order models}\label{sec:first_order_models}
   \item Since the formulas are closed, the result does not depend on the assignment. We only assignments as a technical tool because we avoid defining entailment within a structure. The problems of doing the latter are discussed in \cref{rem:first_order_satisfiability_bivalence}.
 \end{comments}
 
-\begin{remark}\label{rem:first_order_model_notation}
-  In first-order logic, \hyperref[def:first_order_structure]{structures} are defined as pairs \( \mscrX = (X, I) \). Each area of mathematics has its own conventions and structures are usually specified as simply as possible without being unambiguous (and sometimes even beyond non-ambiguity).
-
-  A popular convention is to use compatible letters like we did with \( X \) and \( \mscrX \) or \( G \) and \( \mscrG \), where the structure itself is named using calligraphic letters while the domain is named using the corresponding capital letter in normal font. This only works very simple cases where we can say \enquote{Let \( \mscrP = (P, \leq) \) be a \hyperref[def:partially_ordered_set]{partially ordered set}}.
-
-  The language of the \hyperref[def:group/theory]{theory of groups} has a signature consisting of three functional symbols and no predicate symbols. Specifying a structure for this language is thus the same as specifying a quadruple \( \mscrG = (G, e, (\anon)^{-1}, \cdot) \). We usually specify only the domain \( G \) and the basic structure needed to avoid ambiguity, for example \enquote{Let \( (G, \cdot) \) be a group}. This is technically wrong, but it is both convenient and conventional. The rest of the definition of the group can easily be inferred. In case of ambiguity, the simplest disambiguation is to use lower indices with the name of the structure, e.g. \( +_G \) and \( +_H \) may be the addition operation in different abelian groups.
-
-  Furthermore, stating that \( (G, \cdot, \leq, \mscrT) \) is a totally ordered topological group is cumbersome and can even raise questions; for example, is \( \mscrT \) the \hyperref[def:order_topology]{order topology} or just an arbitrary \hyperref[rem:topological_first_order_structures]{group topology}?
-\end{remark}
-
 \begin{remark}\label{rem:questions_regarding_structures}
   Within this section, we are interested in the following questions regarding \hyperref[def:first_order_structure]{first-order structure} and \hyperref[def:first_order_model]{models}:
 

text/henkin_semantics.tex

@@ -379,20 +379,20 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
 
     We describe in \cref{rem:hol_formula_abbreviations} how different authors offer different abbreviations leading to the same logical layer. These abbreviations depend on classical propositional equivalences like those in \cref{thm:classical_equivalences}.
 
-    We prefer a more straightforward approach, where each connective and quantifier has its own dedicated constant --- see \cref{def:hol_typing_rules}.
+    We prefer a more straightforward approach, where each connective and quantifier has its own dedicated constant --- see \cref{def:hol_formula_rules}.
   \end{thmenum}
 \end{remark}
 
 \begin{remark}\label{rem:hol_rule_formalization}
   The multi-layer approach to syntax, which we discuss in \cref{rem:hol_notational_shorthands/abbreviations}, makes it difficult to introduce a formalized language for expressing the \hyperref[def:inference_rule]{inference rules} of higher-order logic.
 
-  Since we will not focus on higher-order logic, we resort to stating all rules here only in the metalanguage (even the simple typing rules like those of \cref{def:hol_typing_rules}). Later, in \fullref{sec:first_order_logic}, we will extend the propositional schemas to encompass the new constructs required to state special cases of the rules presented here.
+  Since we will not focus on higher-order logic, we resort to stating all rules here only in the metalanguage (even the simple typing rules like those of \cref{def:hol_formula_rules}). Later, in \fullref{sec:first_order_logic}, we will extend the propositional schemas to encompass the new constructs required to state special cases of the rules presented here.
 
   Furthermore, rules like \cref{inf:def:hol_equality_rules/intro} are difficult to formalize.
 \end{remark}
 
 \begin{definition}\label{def:hol_term}\mimprovised
-  Over a fixed \hyperref[def:hol_signature]{signature} \( \Sigma \) of higher-order logic, suppose that the \( \muplambda \)-term \( M \) is \hyperref[def:typability]{typable} in the \hyperref[def:type_context]{type context} \( \Gamma \) with respect to the arrow typing rules \ref{inf:def:arrow_type/elim} and \ref{inf:def:arrow_type/intro/explicit}, the constant typing rule \ref{inf:def:hol_signature/nl_type} and the formula formation rules from \cref{def:hol_typing_rules}.
+  Over a fixed \hyperref[def:hol_signature]{signature} \( \Sigma \) of higher-order logic, suppose that the \( \muplambda \)-term \( M \) is \hyperref[def:typability]{typable} in the \hyperref[def:type_context]{type context} \( \Gamma \) with respect to the arrow typing rules \ref{inf:def:arrow_type/elim} and \ref{inf:def:arrow_type/intro/explicit}, the constant typing rule \ref{inf:def:hol_signature/nl_type} and the formula formation rules from \cref{def:hol_formula_rules}.
 
   Based on our discussion in \cref{rem:hol_notational_shorthands/variable_annotations}, call the pair \( (\Gamma, M) \) a \term{logical term} if all variables in \( \Gamma \) are free in \( M \). \Cref{thm:logical_term_type_uniqueness} shows that each logical term has a unique type \( \tau \).
 
@@ -403,7 +403,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
   \begin{thmenum}[resume=def:hol_term]
     \thmitem{def:hol_term/formula} If \( \tau \) is the type of propositions, we also call the logical term a \term{formula}.
 
-    As per \cref{rem:hol_notational_shorthands/placeholder_annotations}, we use the familiar symbols like \( \varphi \), \( \psi \) and \( \theta \) (without superscripts) for denoting formulas. \Cref{def:hol_typing_rules} lists some formation rules for formulas.
+    As per \cref{rem:hol_notational_shorthands/placeholder_annotations}, we use the familiar symbols like \( \varphi \), \( \psi \) and \( \theta \) (without superscripts) for denoting formulas. \Cref{def:hol_formula_rules} lists some formation rules for formulas.
 
     We denote the set of all formulas over \( \Sigma \) by \( \op*{Form}_\Sigma \).
 
@@ -435,36 +435,36 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
   Of course, most constants we will encounter will be non-letter symbols denoting binary operations, and for them we will prefer infix notation.
 \end{remark}
 
-\begin{definition}\label{def:hol_typing_rules}
+\begin{definition}\label{def:hol_formula_rules}
   In higher-order logic, we presuppose several \hyperref[def:lambda_term]{constant \( \muplambda \)-terms}, which we call \term{logical constants}. These are \( \synH_{\syntop}, \synH_{\synbot}, \synH_{\syneq}, \synH_{\synneg} \), as well as \( \synH_{\syncirc} \) for every \hyperref[def:propositional_alphabet/connectives]{propositional connective} and \( \synH_Q \) for every \hyperref[def:predicate_logic_alphabet/quantifiers]{quantifier}.
 
   We associate with them the following \hyperref[def:simple_typing_rule]{simple typing rules} (the braces indicate \hyperref[con:syntactic_abbreviation]{metalingual abbreviations} that more closely resemble the familiar syntax of predicate logic):
   \begin{paracol}{3}
     \begin{nthcolumn}{0}
       \ParacolAlignmentHack
-      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{\top} }]{inf:def:hol_typing_rules/top}
+      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{\top} }]{inf:def:hol_formula_rules/top}
         \begin{prooftree}
-          \infer0[\ref{inf:def:hol_typing_rules/top}]{ \underbrace{\synH_{\syntop}}_{\syntop}: \syn\omicron }
+          \infer0[\ref{inf:def:hol_formula_rules/top}]{ \underbrace{\synH_{\syntop}}_{\syntop}: \syn\omicron }
         \end{prooftree}
       \end{equation*}
     \end{nthcolumn}
 
     \begin{nthcolumn}{1}
       \ParacolAlignmentHack
-      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{\bot} }]{inf:def:hol_typing_rules/bot}
+      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{\bot} }]{inf:def:hol_formula_rules/bot}
         \begin{prooftree}
-          \infer0[\ref{inf:def:hol_typing_rules/bot}]{ \underbrace{\synH_{\syntop}}_{\synbot}: \syn\omicron }
+          \infer0[\ref{inf:def:hol_formula_rules/bot}]{ \underbrace{\synH_{\syntop}}_{\synbot}: \syn\omicron }
         \end{prooftree}
       \end{equation*}
     \end{nthcolumn}
 
     \begin{nthcolumn}{2}
       \ParacolAlignmentHack
-      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{=} }]{inf:def:hol_typing_rules/eq}
+      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{=} }]{inf:def:hol_formula_rules/eq}
         \begin{prooftree}
           \hypo{ M: \tau }
           \hypo{ N: \tau }
-          \infer2[\ref{inf:def:hol_typing_rules/eq}]{ \underbrace{\synH_{\syneq} M N}_{M^\tau \syneq N^\tau}: \syn\omicron }
+          \infer2[\ref{inf:def:hol_formula_rules/eq}]{ \underbrace{\synH_{\syneq} M N}_{M^\tau \syneq N^\tau}: \syn\omicron }
         \end{prooftree}
       \end{equation*}
     \end{nthcolumn}
@@ -473,38 +473,38 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
   \begin{paracol}{3}
     \begin{nthcolumn}{0}
       \ParacolAlignmentHack
-      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{\neg} }]{inf:def:hol_typing_rules/neg}
+      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{\neg} }]{inf:def:hol_formula_rules/neg}
         \begin{prooftree}
           \hypo{ \varphi: \syn\omicron }
-          \infer1[\ref{inf:def:hol_typing_rules/neg}]{ \underbrace{\synH_{\synneg} \varphi}_{\synneg \varphi}: \syn\omicron }
+          \infer1[\ref{inf:def:hol_formula_rules/neg}]{ \underbrace{\synH_{\synneg} \varphi}_{\synneg \varphi}: \syn\omicron }
         \end{prooftree}
       \end{equation*}
     \end{nthcolumn}
 
     \begin{nthcolumn}{1}
       \ParacolAlignmentHack
-      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{\syncirc} }]{inf:def:hol_typing_rules/conn}
+      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_{\syncirc} }]{inf:def:hol_formula_rules/conn}
         \begin{prooftree}
           \hypo{ \varphi: \syn\omicron }
           \hypo{ \psi: \syn\omicron }
-          \infer2[\ref{inf:def:hol_typing_rules/conn}]{ \underbrace{\synH_{\syncirc} \varphi \psi}_{\varphi \syncirc \psi}: \syn\omicron }
+          \infer2[\ref{inf:def:hol_formula_rules/conn}]{ \underbrace{\synH_{\syncirc} \varphi \psi}_{\varphi \syncirc \psi}: \syn\omicron }
         \end{prooftree}
       \end{equation*}
     \end{nthcolumn}
 
     \begin{nthcolumn}{2}
       \ParacolAlignmentHack
-      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_Q }]{inf:def:hol_typing_rules/quant}
+      \begin{equation*}\taglabel[\ensuremath{ \logic{H}_Q }]{inf:def:hol_formula_rules/quant}
         \begin{prooftree}
           \hypo{ x: \tau }
           \hypo{ \varphi: \syn\omicron }
-          \infer2[\ref{inf:def:hol_typing_rules/quant}]{ \underbrace{\synH_Q (\qabs {x^\tau} \varphi)}_{\quantifier Q {x^\tau} \varphi}: \syn\omicron }
+          \infer2[\ref{inf:def:hol_formula_rules/quant}]{ \underbrace{\synH_Q (\qabs {x^\tau} \varphi)}_{\quantifier Q {x^\tau} \varphi}: \syn\omicron }
         \end{prooftree}
       \end{equation*}
     \end{nthcolumn}
   \end{paracol}
 
-  The rules \ref{inf:def:hol_typing_rules/conn} and \ref{inf:def:hol_typing_rules/quant} are schemas --- we have a distinct rule for each propositional connective \( \syncirc \) and a distinct rule for every quantifier \( Q \).
+  The rules \ref{inf:def:hol_formula_rules/conn} and \ref{inf:def:hol_formula_rules/quant} are schemas --- we have a distinct rule for each propositional connective \( \syncirc \) and a distinct rule for every quantifier \( Q \).
 \end{definition}
 \begin{comments}
   \item We use \( \varphi \) and \( \psi \) as \( \muplambda \)-term placeholders and \( \tau \) as a (quantifiable) type placeholder.
@@ -518,7 +518,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
   The type of a \hyperref[def:hol_term]{higher-order logical term} is unique: for every logical term \( (\Gamma, M) \), if \( \Gamma \vdash M: \tau \) and \( \Gamma \vdash M: \tau' \), then \( \tau = \tau' \).
 \end{proposition}
 \begin{proof}
-  We must extend the recursion in the proof of \cref{thm:typed_term_habitation_uniqueness} to handle the new typing rules from \cref{def:hol_typing_rules}, as well as \ref{inf:def:hol_signature/nl_type}. The actual recursive cases are straightforward.
+  We must extend the recursion in the proof of \cref{thm:typed_term_habitation_uniqueness} to handle the new typing rules from \cref{def:hol_formula_rules}, as well as \ref{inf:def:hol_signature/nl_type}. The actual recursive cases are straightforward.
 \end{proof}
 
 \begin{remark}\label{rem:hol_formula_abbreviations}
@@ -528,7 +528,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
 
   \incite*{Henkin1963TheoryOfPropositionalTypes} presented a formulation that used only \( Q_{o \alpha \alpha } \) for \hyperref[def:predicate_logic_alphabet/equality]{equality}, acknowledging that one such constant is needed for each type \( \alpha \). His formulation is restricted to propositional formulas, but later in \cite{Henkin1975Identity} he extended it to all types supported by Church's original system.
 
-  We show concrete abbreviations in \cref{tab:rem:hol_formula_abbreviations}, based on the constant \( \synH_{\syneq} \), typable via the rule \ref{inf:def:hol_typing_rules/eq}. These abbreviations depend on classical propositional equivalences like those in \cref{thm:classical_equivalences}.
+  We show concrete abbreviations in \cref{tab:rem:hol_formula_abbreviations}, based on the constant \( \synH_{\syneq} \), typable via the rule \ref{inf:def:hol_formula_rules/eq}. These abbreviations depend on classical propositional equivalences like those in \cref{thm:classical_equivalences}.
 
   Most of these abbreviations are based on \bycite[212]{Andrews2002Logic}, with the exception of \( \syntop \), which is instead taken from \bycite[273]{Farmer2008STTVirtues}. In the abbreviation of \( \varphi \synwedge \psi \), as in \cref{def:lambda_term_substitution/sharp}, the function \( \sharp(V) \) gives the smallest identifier not in \( V \).
 
@@ -562,7 +562,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
 \end{remark}
 
 \begin{definition}\label{def:higher_order_logic_syntax}
-  We define \enquote{the \hyperref[con:syntax_semantics_duality]{syntax} of higher-order logic} over an \hyperref[def:hol_signature]{eponymous signature} as the corresponding \hyperref[def:simple_type_system]{simple type theory} restricted \hyperref[def:quantifiable_type]{quantifiable types}, with the usual arrow typing rules \ref{inf:def:arrow_type/elim} and \ref{inf:def:arrow_type/intro/explicit}, the constant typing rule \ref{inf:def:hol_signature/nl_type} and the formula formation rules from \cref{def:hol_typing_rules}.
+  We define \enquote{the \hyperref[con:syntax_semantics_duality]{syntax} of higher-order logic} over an \hyperref[def:hol_signature]{eponymous signature} as the corresponding \hyperref[def:simple_type_system]{simple type theory} restricted \hyperref[def:quantifiable_type]{quantifiable types}, with the usual arrow typing rules \ref{inf:def:arrow_type/elim} and \ref{inf:def:arrow_type/intro/explicit}, the constant typing rule \ref{inf:def:hol_signature/nl_type} and the formula formation rules from \cref{def:hol_formula_rules}.
 \end{definition}
 
 \begin{remark}\label{rem:mltt_hol}
@@ -841,7 +841,7 @@ \section{Higher-order logic}\label{sec:higher_order_logic}
   \end{paracol}
 \end{definition}
 \begin{comments}
-  \item The three rules are needed for \cref{thm:hol_equality_is_equivalence_relation} and \cref{thm:hol_equality_entails_equivalence}. The elimination rule generalizes rule \logic{R'} from Andrews' system \( \logic{Q}_0 \) --- see \cref{ex:hol_equality_rules_and_rule_r}
+  \item The three rules ensure that \cref{thm:hol_equality_is_equivalence_relation} and \cref{thm:hol_equality_entails_equivalence} hold, and their full power is demonstrated in \cref{ex:simplified_hol_predicate_definition}. The elimination rule generalizes rule \logic{R'} from Andrews' system \( \logic{Q}_0 \) --- see \cref{ex:hol_equality_rules_and_rule_r}
 
   An alternative to \ref{inf:def:hol_equality_rules/intro} could be, as in \cref{rem:hol_axiomatic_derivations}, a rule equating \hyperref[def:beta_eta_reduction]{\( \beta \)-equivalent} \( \muplambda \)-terms. Although the latter has its appeal, we avoid it due to its complexity.
 \end{comments}

text/higher_order_logic.tex

@@ -159,7 +159,7 @@ \chapter{Mathematical logic}\label{ch:mathematical_logic}
 
     \thmitem{rem:mathematical_logic_conventions/propositional_constants} We define the propositional constants for truth and falsity via \( \syntop \) and \( \synbot \) in the object language and by \( T \) and \( F \) in the metalanguage. We use \( \top \) and \( \bot \) in general \hyperref[def:lattice]{lattices}.
 
-    \thmitem{rem:mathematical_logic_conventions/structure_pairs} We often conflate structures in the metalogic (i.e. sets with functions and/or relations defined on them) with their domain --- see \cref{rem:first_order_model_notation} for a further discussion.
+    \thmitem{rem:mathematical_logic_conventions/structure_pairs} We often conflate structures in the metatheory (i.e. sets with functions and/or relations defined on them) with their domain --- see \cref{rem:hol_structure_notation} for a further discussion.
 
     \thmitem{rem:mathematical_logic_conventions/shorthands} We additionally use syntactic shorthands like \cref{rem:propositional_formula_notation_conventions} and \cref{rem:first_order_formula_conventions} when writing formulas. We will also find handy various \hyperref[con:syntactic_abbreviation]{abbreviations} like the \hyperref[con:description_operator/unique_existence]{unique existence quantifier} or the various ad-hoc predicates from \fullref{sec:naive_set_theory}.