\contentsline {section}{\numberline {1}Overview}{5}
\contentsline {subsection}{\numberline {1.1}Localizing Our Work in the Field of Artificial Intelligence (AI)}{5}
\contentsline {subsection}{\numberline {1.2}New in the First Edition of 2011 compared to \cite {wirth-hilbert-seki}}{5}
\contentsline {subsection}{\numberline {1.3}New in This Edition of 2024 compared to the First Edition}{6}
\contentsline {subsection}{\numberline {1.4}Organization}{6}
\contentsline {section}{\numberline {2}Introduction to Free Atoms and Variables}{7}
\contentsline {subsection}{\numberline {2.1}Essential Notions and Notation}{7}
\contentsline {subsection}{\numberline {2.2}Bound and Free Atoms}{8}
\contentsline {subsection}{\numberline {2.3}Variables}{8}
\contentsline {subsection}{\numberline {2.4}Instantiation of Variables and Free Atoms}{9}
\contentsline {section}{\numberline {3}Introduction to Reductive Inference Rules}{11}
\contentsline {subsection}{\numberline {3.1}Tautologies}{11}
\contentsline {subsection}{\numberline {3.2}\relax $\alpha $-Rules}{11}
\contentsline {subsection}{\numberline {3.3}\relax $\beta $-Rules}{12}
\contentsline {subsection}{\numberline {3.4}\relax $\gamma $-Rules}{12}
\contentsline {subsection}{\numberline {3.5}\relax $\delta ^- $-Rules}{13}
\contentsline {subsection}{\numberline {3.6}\relax $\delta ^+ $-Rules}{14}
\contentsline {subsection}{\numberline {3.7}Global and Practical Aspects of Inference Systems}{15}
\contentsline {subsection}{\numberline {3.8}\math \gamma -Multiplicity}{16}
\contentsline {subsection}{\numberline {3.9}Skolem\discretionary {-}{}{}ization}{16}
\contentsline {section}{\numberline {4}Introduction to \hilbertsepsilon }{17}
\contentsline {subsection}{\numberline {4.1}Motivation}{17}
\contentsline {subsection}{\numberline {4.2}Requirements Specification}{17}
\contentsline {subsection}{\numberline {4.3}Overview}{17}
\contentsline {subsection}{\numberline {4.4}From the \relax $\iota $\ to the \relax $\varepsilon $}{18}
\contentsline {subsubsection}{\numberline {4.4.1}The Symbols for the \relax $\iota $-Operator}{18}
\contentsline {subsubsection}{\numberline {4.4.2}The Essential Idea of the \relax $\iota $-Operator}{18}
\contentsline {subsubsection}{\numberline {4.4.3}Elementary Semantics Without Straightforward Overspecification}{19}
\contentsline {subsubsection}{\numberline {4.4.4}Overspecified \relax $\iota $-Operators}{20}
\contentsline {subsubsection}{\numberline {4.4.5}A Completely Defined, but Not Overspecified \relax $\iota $-Operator}{21}
\contentsline {subsection}{\numberline {4.5}The \relax $\varepsilon $\ as an Improvement over the \relax $\iota $}{22}
\contentsline {subsection}{\numberline {4.6}On the \relax $\varepsilon $'s Proof-Theoretic Origin}{22}
\contentsline {subsubsection}{\numberline {4.6.1}The \relax $\varepsilon $-Formula and the Historical Sources of the \relax $\varepsilon $}{22}
\contentsline {subsubsection}{\numberline {4.6.2}The Original Explanation of the \relax $\varepsilon $}{23}
\contentsline {subsubsection}{\numberline {4.6.3}Defining the Quantifiers via the \relax $\varepsilon $}{23}
\contentsline {subsubsection}{\numberline {4.6.4}The \relax $\varepsilon $-Theorems}{24}
\contentsline {subsection}{\numberline {4.7}Quantifier Elimination and Subordinate \relax $\varepsilon $-terms}{26}
\contentsline {subsection}{\numberline {4.8}Our Objective}{29}
\contentsline {subsection}{\numberline {4.9}Indefinite and Committed Choice}{29}
\contentsline {subsection}{\numberline {4.10}Do not be afraid of Indefiniteness!}{30}
\contentsline {subsection}{\numberline {4.11}Replacing \relax $\varepsilon $-Terms with Variables}{32}
\contentsline {subsection}{\numberline {4.12}Why We Do Not Abandon the \math \varepsilon -Symbol}{34}
\contentsline {subsection}{\numberline {4.13}Crucial Representational Change, but nothing more yet?}{34}
\contentsline {subsection}{\numberline {4.14}Instantiating Choice-Conditioned Variables (``\relax $\varepsilon $-Substitution'')}{35}
\contentsline {section}{\numberline {5}Formal Presentation of Our Syntax}{39}
\contentsline {subsection}{\numberline {5.1}Basic Notions and Notation}{39}
\contentsline {subsection}{\numberline {5.2}Choice Functions}{40}
\contentsline {subsection}{\numberline {5.3}Variables, Atoms, Constants, and Substitutions}{40}
\contentsline {subsection}{\numberline {5.4}Consistent Posi\discretionary {-}{}{}\discretionary {tive/}{Ne}{tive/Ne}\discretionary {-}{}{}ga\discretionary {-}{}{}tive\ Vari\discretionary {-}{}{}able-Con\discretionary {-}{}{}di\discretionary {-}{}{}tions}{41}
\contentsline {subsection}{\numberline {5.5}Extensions, \math \sigma -Updates, and \pair P N-Sub\discretionary {-}{}{}sti\discretionary {-}{}{}tu\discretionary {-}{}{}tions}{43}
\contentsline {subsection}{\numberline {5.6}Choice-Conditions}{44}
\contentsline {subsection}{\numberline {5.7}Extending Extensions and \relax $\sigma $-Updates to Choice-Conditions}{45}
\contentsline {section}{\numberline {6}Example: Henkin\ Quantification}{47}
\contentsline {section}{\numberline {7}Formal Presentation of our Semantics}{51}
\contentsline {subsection}{\numberline {7.1}Semantic Presuppositions}{51}
\contentsline {subsection}{\numberline {7.2}Semantic Relations and \relax $\@mathcal {S} $-Raising-Valu\discretionary {-}{}{}ations}{53}
\contentsline {subsection}{\numberline {7.3}Compatibility of Choice-Conditions}{54}
\contentsline {subsection}{\numberline {7.4}Existence of Compatible Raising-Valuations}{54}
\contentsline {subsection}{\numberline {7.5}\Validity C{\pair P N}}{55}
\contentsline {subsection}{\numberline {7.6}Validity of Our Version \relax $Q_C $ of Hilbert--\unhbox \voidb@x \hbox {Ber\discretionary {-}{}{}nay\unprotectedes }' Axiom \relax $(\varepsilon _0) $}{57}
\contentsline {subsection}{\numberline {7.7}The Main Lemma on Substitution of Variables}{57}
\contentsline {section}{\numberline {8}Reduction}{59}
\contentsline {subsection}{\numberline {8.1}Mutual Reduction of \relax $\alpha $-, \relax $\beta $-, \relax $\gamma $-, \relax $\delta $-Rules}{60}
\contentsline {subsection}{\numberline {8.2}From Safe Proof Steps to Lemma Application and Instantiation of Variables}{60}
\contentsline {subsubsection}{\numberline {8.2.1}Application of Induction Hypotheses and Lemmas}{61}
\contentsline {subsubsection}{\numberline {8.2.2}Instantiation of Variables}{62}
\contentsline {subsection}{\numberline {8.3}Monotonicity, Instantiation of Variables and Free Atoms}{63}
\contentsline {subsection}{\numberline {8.4}Leisen\discretionary {-}{}{}ring's Axiom (E2) becomes Valid}{64}
\contentsline {section}{\numberline {9}Summary and Discussion}{67}
\contentsline {subsection}{\numberline {9.1}Posi\discretionary {-}{}{}\discretionary {tive/}{Ne}{tive/Ne}\discretionary {-}{}{}ga\discretionary {-}{}{}tive\ Vari\discretionary {-}{}{}able-Con\discretionary {-}{}{}di\discretionary {-}{}{}tions}{67}
\contentsline {subsection}{\numberline {9.2}Semantics of Posi\discretionary {-}{}{}\discretionary {tive/}{Ne}{tive/Ne}\discretionary {-}{}{}ga\discretionary {-}{}{}tive\ Vari\discretionary {-}{}{}able-Con\discretionary {-}{}{}di\discretionary {-}{}{}tions}{67}
\contentsline {subsection}{\numberline {9.3}Replacing \relax $\varepsilon $-Terms with Variables}{68}
\contentsline {subsection}{\numberline {9.4}Semantics of Choice-Conditions}{68}
\contentsline {subsection}{\numberline {9.5}Substitution of Variables (``\math \varepsilon -Substitution'') }{68}
\contentsline {subsection}{\numberline {9.6}Where Have All the \relax $\varepsilon $-Terms Gone?}{69}
\contentsline {subsection}{\numberline {9.7}Are We Breaking with Traditional Treatment of Hilbert's \nlbmath \varepsilon ?}{70}
\contentsline {section}{\numberline {10}Conclusion}{71}
\contentsline {section}{\numberline {A}Are Liberalized \relax $\delta $-Rules Always More Liberal?}{73}
\contentsline {section}{\numberline {B}Semantics for \hilbertsepsilon \ in the Literature}{75}
\contentsline {subsection}{\numberline {B.1}Right-Unique Semantics}{75}
\contentsline {subsubsection}{\numberline {B.1.1}Extensionality:\\ \ackermannplain 's (II,4) \ = \ \bourbakiplain 's (S7) \ = \ \leisenringplain 's (E2)}{75}
\contentsline {subsubsection}{\numberline {B.1.2}Weaker than (E2), but still Right-Unique}{76}
\contentsline {subsubsection}{\numberline {B.1.3}Overspecification even beyond (E2)}{76}
\contentsline {subsubsection}{\numberline {B.1.4}Strengthening Semantics to Turn Axiomatizations Complete}{77}
\contentsline {subsubsection}{\numberline {B.1.5}Roots of the Misunderstanding of a Right-Uniqueness Requirement}{78}
\contentsline {subsection}{\numberline {B.2}Indefinite Semantics in the Literature}{80}
\contentsline {section}{\numberline {C}On Formalizing Vari\discretionary {-}{}{}able-Con\discretionary {-}{}{}di\discretionary {-}{}{}tions}{81}
\contentsline {section}{Proofs}{83}
\contentsline {section}{References}{97}
\contentsline {section}{Index}{113}