Reduce intuitionistic first-order logic to a single remark

v-- · v-- · commit 54def5331626 · 2026-01-17T20:58:55.000+02:00
diff --git a/bibliography/books.bib b/bibliography/books.bib
@@ -2536,6 +2536,16 @@ @book{ДимитровЯнев2007ВероятностиИСтатистика
   title = {Вероятности и статистика}
 }
 
+@book{Драгалин1979Интуиционизм,
+  author = {Альберт Григорьевич Драгалин},
+  date = {1979},
+  language = {russian},
+  publisher = {Наука},
+  shortauthor = {Drаgаlin},
+  subtitle = {Введение в теорию доказательств},
+  title = {Математический интуиционизм}
+}
+
 @book{Драганов2022ТеорияНаМярката,
   author = {Борислав Драганов},
   date = {2022},
diff --git a/packages/math_macros.sty b/packages/math_macros.sty
@@ -41,7 +41,6 @@
 % Semantic logical symbols
 \NewDocumentCommand \semtop       {} {\mathbfsf{T}}
 \NewDocumentCommand \sembot       {} {\mathbfsf{F}}
-\NewDocumentCommand \semeq        {} {\mathrel{\approx}}
 
 % Syntactic symbols
 \NewDocumentCommand \syn         {m} {{\dot{#1}}}
diff --git a/src/notebook/math/logic/structure/formula_visitor.py b/src/notebook/math/logic/structure/formula_visitor.py
@@ -76,6 +76,6 @@ def visit_existential(self, formula: QuantifierFormula) -> bool:
         )
 
 
-# This is def:fol_denotation/formulas in the monograph
+# This is alg:fol_formula_denotation/formulas in the monograph
 def evaluate_formula[T](formula: Formula, structure: FormalLogicStructure[T], assignment: VariableAssignment[T] | None = None) -> bool:
     return FormulaEvaluationVisitor(structure, assignment or VariableAssignment()).visit(formula)
diff --git a/src/notebook/math/logic/structure/term_visitor.py b/src/notebook/math/logic/structure/term_visitor.py
@@ -20,6 +20,6 @@ def visit_function(self, term: FunctionApplication) -> T:
         return self.structure.apply(term.symbol, *(self.visit(arg) for arg in term.arguments))
 
 
-# This is def:fol_denotation/terms in the monograph
+# This is alg:fol_term_denotation in the monograph
 def evaluate_term[T](term: Term, structure: FormalLogicStructure[T], assignment: VariableAssignment[T] | None = None) -> T:
     return TermEvaluationVisitor(structure, assignment or VariableAssignment()).visit(term)
diff --git a/text/algebras_over_semirings.tex b/text/algebras_over_semirings.tex
@@ -483,7 +483,7 @@ \section{Algebras over semirings}\label{sec:algebras_over_semirings}
 
     A polynomial \( f(\mscrX) \) in \( R[\mscrX] \) has its coefficients in \( R \), but the indeterminates are placeholders whose variables need to be \hi{explicitly} assignment values in some algebra \( M \) over \( R \) (not necessarily \( R \) itself).
 
-    \thmitem{con:free_construction/assignment} In analogy with how we define denotations for first-order logical terms in \cref{def:fol_denotation/terms}, we rely on an \term{assignment} \( e: \mscrX \to M \) to supply a value for each indeterminate.
+    \thmitem{con:free_construction/assignment} In analogy with how we define denotations for first-order logical terms in \cref{alg:fol_term_denotation}, we rely on an \term{assignment} \( e: \mscrX \to M \) to supply a value for each indeterminate.
 
     This contrasts with a metalingual variable like \( x \) that can refer to some element of \( M \). The indeterminate \( X \) is a standalone entity that requires an explicit assignment \( e \).
 
diff --git a/text/boolean_functions.tex b/text/boolean_functions.tex
@@ -9,7 +9,7 @@ \section{Boolean functions}\label{sec:boolean_functions}
 
   The names of the operations in \( \BbbT \) are often adapted as to reflect their use in logic; see \cref{def:standard_boolean_functions}.
 
-  For \hyperref[con:predicate_logic]{predicate logic}, we must additionally require that \( \BbbT \) is \hyperref[def:heyting_algebra/complete]{complete}\fnote{It is possible to make this completeness requirement implicit by relying on \hyperref[def:dedekind_macnielle_completion]{Dedekind-MacNeille completion}.} in order to be able to define denotations for \hyperref[con:predicate_logic/quantifiers]{quantifiers} in \cref{def:fol_denotation}.
+  For \hyperref[con:predicate_logic]{predicate logic}, we must additionally require that \( \BbbT \) is \hyperref[def:heyting_algebra/complete]{complete}\fnote{It is possible to make this completeness requirement implicit by relying on \hyperref[def:dedekind_macnielle_completion]{Dedekind-MacNeille completion}.} in order to be able to define denotations for \hyperref[con:predicate_logic/quantifiers]{quantifiers} in \cref{alg:fol_formula_denotation}.
 
   We will consider different algebras depending on the situation:
   \begin{thmenum}
diff --git a/text/first_order_logic.tex b/text/first_order_logic.tex
diff --git a/text/henkin_semantics.tex b/text/henkin_semantics.tex
@@ -71,7 +71,7 @@ \section{Henkin semantics}\label{sec:henkin_semantics}
 \begin{comments}
   \item The assignment \( v \) is well-defined as a function since it is the set-theoretic \hyperref[def:disjoint_union]{disjoint union} of a family of functions \( \seq{ v_\tau }_{\tau \in \op*{\BbbQ_\Sigma}} \), where \( v_\tau: \op*{Var} \to X_\tau \).
 
-  \item Compared to Andrews, we elaborate on modified assignments so that they more closely resemble their counterparts in first-order logic defined in \cref{def:fol_denotation/modified_assignment}.
+  \item Compared to Andrews, we elaborate on modified assignments so that they more closely resemble their counterparts in first-order logic defined in \cref{alg:fol_formula_denotation/modified_assignment}.
 \end{comments}
 
 \begin{definition}\label{def:hol_term_denotation}\mimprovised
@@ -110,7 +110,7 @@ \section{Henkin semantics}\label{sec:henkin_semantics}
   If the denotation \( \Bracks{ M^\tau }_\mscrX^v \) coincides for any variable assignment \( v \), we use the simplified notation \( \Bracks{ \varphi }_\mscrX \). This is the case for \hyperref[def:hol_term/closed]{closed logical terms}, but it is also more general --- see \cref{rem:implicit_quantification_and_deduction}.
 \end{definition}
 \begin{comments}
-  \item We take the definition of denotation for arbitrary terms from \cite[238]{Andrews2002Logic}. For formulas, we generalize the denotations of first-order formulas defined in \cref{def:fol_denotation}.
+  \item We take the definition of denotation for arbitrary terms from \cite[238]{Andrews2002Logic}. For formulas, we generalize the denotations of first-order formulas defined in \cref{alg:fol_formula_denotation}.
 
   \item As per \cref{rem:hol_parametrized_denotation}, due to the availability of \( \muplambda \)-abstraction, we will not be interested in treating formulas with free variables as functions (unlike in propositional or first-order logic).
 \end{comments}
diff --git a/text/logical_consequence.tex b/text/logical_consequence.tex
@@ -607,7 +607,7 @@ \section{Logical consequence}\label{sec:logical_consequence}
 \begin{concept}\label{con:intuitionistic_logic}\mimprovised
   By \term[ru=интуиционисткая логика (\cite[58]{ШеньВерещагин2017ЯзыкиИИсчисления}), en=intuitionistic logic (\cite[8]{TroelstraSchwichtenberg2000BasicProofTheory})]{intuitionistic logic} we will mean the generalization of \hyperref[con:classical_logic]{classical logic} where instead of \fullref{thm:propositional_semantic_lem}, we have the strictly weaker \fullref{thm:propositional_semantic_efq} stating that everything can be proven from a contradiction.
 
-  We will also discuss two \hyperref[def:general_logic]{general logics} --- the one defined in \cref{def:propositional_logic} for \hyperref[def:propositional_formula]{propositional formulas}, with the \hyperref[def:truth_value_algebra/intuitionistic]{intuitionistic} \hyperref[def:propositional_institution]{propositional institution} and the corresponding \hyperref[def:propositional_natural_deduction]{natural deduction system}, and the one defined in \cref{def:first_order_logic} for \hyperref[def:fol_formula]{first-order formulas}, with the corresponding \hyperref[def:fol_natural_deduction]{natural deduction system}.
+  We will define a \hyperref[def:general_logic]{general logic} for \hyperref[def:propositional_formula]{propositional formulas} in \cref{def:propositional_logic}, with the \hyperref[def:truth_value_algebra/intuitionistic]{intuitionistic} \hyperref[def:propositional_institution]{propositional institution} and the corresponding \hyperref[def:propositional_natural_deduction]{natural deduction system}. In \cref{def:fol_natural_deduction}, we will extend intuitionistic natural deduction to \hyperref[def:fol_formula]{first-order formulas}.
 \end{concept}
 \begin{comments}
   \item Intuitionistic logic can also be called \enquote{constructive logic} due to the \hyperref[con:brouwer_heyting_kolmogorov_interpretation]{Brouwer-Heyting-Kolmogorov interpretation}.
diff --git a/text/logical_theories.tex b/text/logical_theories.tex
@@ -38,7 +38,7 @@ \section{Logical theories}\label{sec:logical_theories}
 
   \NecessitySubProof Let \( \Gamma \) be inconsistent and suppose that \( \mscrX = (X, I) \) is a model of \( \Gamma \). Fix any valuation \( v \) in \( \mscrX \). Since \( \Gamma \vdash \synbot \), \fullref{thm:classical_first_order_logic_soundness_and_complete} implies that \( \Bracks{\synbot}_v = T \).
 
-  By the \hyperref[def:fol_denotation/formula_denotation]{definition of formula valuation}, however, we have \( \Bracks{\synbot}_v = F \). The obtained contradiction shows that \( \mscrX \) cannot be a model of \( \Gamma \) and since this structure was chosen arbitrarily, we conclude that \( \Gamma \) is unsatisfiable.
+  By the \hyperref[alg:fol_formula_denotation/formula_denotation]{definition of formula valuation}, however, we have \( \Bracks{\synbot}_v = F \). The obtained contradiction shows that \( \mscrX \) cannot be a model of \( \Gamma \) and since this structure was chosen arbitrarily, we conclude that \( \Gamma \) is unsatisfiable.
 \end{proof}
 
 \paragraph{The L\"owenheim-Skolem theorems}
diff --git a/text/propositional_completeness.tex b/text/propositional_completeness.tex
@@ -643,7 +643,7 @@ \section{Propositional completeness}\label{sec:propositional_completeness}
 
   It remains for \( \Bracks{\psi \synvee \theta}_I \) to be \( \semtop \).
 
-  \NecessitySubProof* Suppose that \( \Bracks{\psi \synvee \theta}_I = \semtop \). \Cref{thm:propositional_denotation_characterization/disjunction} implies that \( \Bracks{\psi}_I = \semtop \) or \( \Bracks{\theta}_I = \semtop \).
+  \NecessitySubProof* Suppose that \( \Bracks{\psi \synvee \theta}_I = \semtop \). \Cref{thm:propositional_satisfaction_characterization/disjunction} implies that \( \Bracks{\psi}_I = \semtop \) or \( \Bracks{\theta}_I = \semtop \).
 
   If \( \Bracks{\psi}_I = \semtop \), the inductive hypothesis implies that \( \Gamma \vdash \psi \), and we can use \ref{inf:def:propositional_natural_deduction/or/intro_left} to conclude that \( \Gamma \vdash (\psi \synvee \theta) \).
 
@@ -653,21 +653,21 @@ \section{Propositional completeness}\label{sec:propositional_completeness}
 
   \SufficiencySubProof* Suppose that \( \Gamma \vdash (\psi \synimplies \theta) \).
 
-  We will utilize \cref{thm:propositional_denotation_characterization/conditional}, by which it is sufficient to show that \( \Bracks{\psi}_I = \semtop \) implies \( \Bracks{\theta}_I = \semtop \) in order to deduce \( \Bracks{\psi \synimplies \theta}_I = \semtop \).
+  We will utilize \cref{thm:propositional_satisfaction_characterization/conditional}, by which it is sufficient to show that \( \Bracks{\psi}_I = \semtop \) implies \( \Bracks{\theta}_I = \semtop \) in order to deduce \( \Bracks{\psi \synimplies \theta}_I = \semtop \).
 
   By the inductive hypothesis on \( \psi \), if \( \Bracks{\psi}_I = \semtop \), we have \( \Gamma \vdash \psi \). Since \( \Gamma \) is a theory, \( \psi \) belongs to \( \Gamma \).
 
   \Cref{thm:propositional_natural_deduction_deduction_theorem} implies that \( \Gamma, \psi \vdash \theta \), i.e. \( \Gamma \vdash \theta \). By the inductive hypothesis on \( \theta \), we have \( \Bracks{\theta}_I = \semtop \).
 
-  It follows from \cref{thm:propositional_denotation_characterization/conditional} that \( \Bracks{\psi \synimplies \theta}_I = \semtop \).
+  It follows from \cref{thm:propositional_satisfaction_characterization/conditional} that \( \Bracks{\psi \synimplies \theta}_I = \semtop \).
 
   \NecessitySubProof* Conversely, suppose that \( \Bracks{\psi \synimplies \theta}_I = \semtop \).
 
   We have two possibilities:
   \begin{itemize}
     \item If \( \Gamma \vdash \psi \), the inductive hypothesis on \( \psi \) implies that \( \Bracks{\psi}_I = \semtop \).
 
-    \Cref{thm:propositional_denotation_characterization/conditional} implies that \( \Bracks{\theta}_I = \semtop \), and the inductive hypothesis on \( \theta \) implies that \( \Gamma \vdash \theta \).
+    \Cref{thm:propositional_satisfaction_characterization/conditional} implies that \( \Bracks{\theta}_I = \semtop \), and the inductive hypothesis on \( \theta \) implies that \( \Gamma \vdash \theta \).
 
     The rule \ref{inf:def:propositional_natural_deduction/imp/intro} then allows us to construct a proof tree deriving \( \psi \synimplies \theta \) from \( \Gamma \).
 
@@ -688,13 +688,13 @@ \section{Propositional completeness}\label{sec:propositional_completeness}
 
   \SufficiencySubProof* Suppose that \( \Gamma \vdash (\psi \syniff \theta) \).
 
-  Due to \cref{thm:propositional_denotation_characterization/biconditional}, it is sufficient to show that \( \Bracks{\psi}_I = \semtop \) if and only if \( \Bracks{\theta}_I = \semtop \) in order to deduce \( \Bracks{\psi \syniff \theta}_I = \semtop \).
+  Due to \cref{thm:propositional_satisfaction_characterization/biconditional}, it is sufficient to show that \( \Bracks{\psi}_I = \semtop \) if and only if \( \Bracks{\theta}_I = \semtop \) in order to deduce \( \Bracks{\psi \syniff \theta}_I = \semtop \).
 
   If \( \Bracks{\psi} = \semtop \), the inductive hypothesis on \( \psi \) implies that \( \Gamma \vdash \psi \). Then \ref{inf:def:propositional_natural_deduction/iff/elim_right} allows deriving \( \theta \) from \( \Gamma \), which by the inductive hypothesis on \( \theta \) implies that \( \Bracks{\theta} = \semtop \).
 
   In the other direction, if \( \Bracks{\theta} = \semtop \), we simply use \ref{inf:def:propositional_natural_deduction/iff/elim_left} instead.
 
-  \NecessitySubProof* Suppose that \( \Bracks{\psi \syniff \theta}_I = \semtop \). \Cref{thm:propositional_denotation_characterization/biconditional} implies that \( \Bracks{\psi}_I = \semtop \) if and only if \( \Bracks{\theta}_I = \semtop \).
+  \NecessitySubProof* Suppose that \( \Bracks{\psi \syniff \theta}_I = \semtop \). \Cref{thm:propositional_satisfaction_characterization/biconditional} implies that \( \Bracks{\psi}_I = \semtop \) if and only if \( \Bracks{\theta}_I = \semtop \).
 
   \begin{itemize}
     \item If \( \Bracks{\psi}_I = \Bracks{\theta}_I = \semtop \), by the inductive hypothesis, we conclude that \( \Gamma \vdash \psi \) and \( \Gamma \vdash \theta \). The rule \ref{inf:def:propositional_natural_deduction/iff/intro} allows constructing a proof tree deriving \( \psi \syniff \theta \) from \( \Gamma \).
diff --git a/text/propositional_formula_transformation.tex b/text/propositional_formula_transformation.tex
@@ -144,9 +144,9 @@ \section{Propositional formula transformation}\label{sec:propositional_formula_t
 \begin{definition}\label{def:substitution_schema_alphabet}\mimprovised
   The \hyperref[def:formal_language/alphabet]{alphabet} of \hyperref[con:improper_symbol]{improper symbols} for substitution schemas consists of the following:
   \begin{thmenum}
-    \thmitem{def:substitution_schema_alphabet/brackets} The brackets \enquote{\( [ \)} and \enquote{\( ] \)}.
-
     \thmitem{def:substitution_schema_alphabet/connective} The connective \enquote{\( \synsubst \)}.
+
+    \thmitem{def:substitution_schema_alphabet/brackets} The brackets \enquote{\( [ \)} and \enquote{\( ] \)} as auxiliary symbols.
   \end{thmenum}
 \end{definition}
 
diff --git a/text/propositional_logic.tex b/text/propositional_logic.tex
diff --git a/text/ramified_types.tex b/text/ramified_types.tex
diff --git a/text/rings.tex b/text/rings.tex
diff --git a/text/unisorted_unification.tex b/text/unisorted_unification.tex

Original file line number	Diff line number	Diff line change
`@@ -76,6 +76,6 @@ def visit_existential(self, formula: QuantifierFormula) -> bool:`
`76`	`76`	`)`
`77`	`77`
`78`	`78`
`79`		`-# This is def:fol_denotation/formulas in the monograph`
	`79`	`+# This is alg:fol_formula_denotation/formulas in the monograph`
`80`	`80`	`def evaluate_formula[T](formula: Formula, structure: FormalLogicStructure[T], assignment: VariableAssignment[T] \| None = None) -> bool:`
`81`	`81`	`return FormulaEvaluationVisitor(structure, assignment or VariableAssignment()).visit(formula)`