\contentsline {section}{\numberline {1}Motivation}{3}
\contentsline {section}{\numberline {2}Introduction}{4}
\contentsline {section}{\numberline {3}{\sc Herbrand}'s {\it Modus Ponens}\/\hskip .07em-Free Calculus \\in the Eyes of \citet {heijenoort-herbrand}}{6}
\contentsline {subsection}{\numberline {3.1}\relax $\gamma $-Quantification}{7}
\contentsline {subsection}{\numberline {3.2}\relax $\delta $-Quantification}{9}
\contentsline {subsection}{\numberline {3.3}Simplification}{10}
\contentsline {section}{\numberline {4}\PropertyC }{11}
\contentsline {subsection}{\numberline {4.1}Prerequisites for \PropertyC }{11}
\contentsline {subsection}{\numberline {4.2}\PropertyC \ and \PropertyCstar }{13}
\contentsline {section}{\numberline {5}From \propertyC \ to a Linear Derivation}{15}
\contentsline {subsection}{\numberline {5.1}Informal Proof}{15}
\contentsline {subsection}{\numberline {5.2}Human-Oriented Formal Proof Construction in {\sc Heijen\discretionary {-}{}{}oort}'s Version of {\sc Herbrand}'s {\it Modus Ponens}\/\hskip .07em-Free Calculus}{16}
\contentsline {subsubsection}{\numberline {5.2.1}Phase\,1 of the Reduction: Rename Bound \relax $\delta $-Variables}{16}
\contentsline {subsubsection}{\numberline {5.2.2}Phase\,2 of the Reduction: Generalized Rule of \relax $\gamma $-Simplification}{17}
\contentsline {subsubsection}{\numberline {5.2.3}Phase\,3 of the Reduction: Generalized Rules of Quantification}{17}
\contentsline {subsubsection}{\numberline {5.2.4}Interlude: Why Side-Conditions are Always Satisfied}{19}
\contentsline {paragraph}{\Ruleofuniversaloidquantification }{19}
\contentsline {paragraph}{Generalized rule of \relax $\gamma $-quantification}{20}
\contentsline {subsubsection}{\numberline {5.2.5}Continuation of Phase\,3}{21}
\contentsline {subsubsection}{\numberline {5.2.6}Stepwise {\em Deductive}\/ Construction of the Same Proof?}{21}
\contentsline {subsection}{\numberline {5.3}Mechanical Proof Construction in {\sc Heijen\discretionary {-}{}{}oort}'s Version of\\{\sc Herbrand}'s {\it Modus Ponens}\/\hskip .07em-Free Calculus}{22}
\contentsline {subsection}{\numberline {5.4}Formal Proof in Our Free-Variable Calculus}{23}
\contentsline {section}{\numberline {6}{\sc Herbrand}'\unprotectedes \ Fundamental Theorem}{25}
\contentsline {section}{\numberline {7}Generalized Rules of Quantification in the Literature}{27}
\contentsline {section}{\numberline {8}{\sc Herbrand}'s Original Rules}{28}
\contentsline {section}{\numberline {9}{\sc Herbrand}'s ``False Lemma''\ and its Corrections}{29}
\contentsline {subsection}{\numberline {9.1}\unhbox \voidb@x \hbox {\sc Ber\discretionary {-}{}{}nay\unprotectedes }' Correction}{30}
\contentsline {subsection}{\numberline {9.2}{\sc G\unprotectedoe del}'s and {\sc Dreben}'s Correction}{30}
\contentsline {subsection}{\numberline {9.3}{\sc Heijen\discretionary {-}{}{}oort}'s Correction}{31}
\contentsline {section}{\numberline {10}Why {\sc Herbrand}'\unprotectedes \ Fundamental Theorem\ is Central, \\Though Not Deep}{33}
\contentsline {section}{\numberline {11}Conclusion and Future Work}{39}
\contentsline {section}{References}{41}
\contentsline {section}{Index}{49}