\contentsline {section}{\numberline {1}Introduction}{1}{section.1}
\contentsline {section}{\numberline {2}Notation}{2}{section.2}
\contentsline {subsection}{\numberline {2.1}Hiding construct}{2}{subsection.2.1}
\contentsline {subsection}{\numberline {2.2}Metaquantification}{2}{subsection.2.2}
\contentsline {subsection}{\numberline {2.3}The `Arbitrary' proof constructor}{4}{subsection.2.3}
\contentsline {subsection}{\numberline {2.4}Macro indentation}{4}{subsection.2.4}
\contentsline {subsection}{\numberline {2.5}Protected macro expansion}{4}{subsection.2.5}
\contentsline {subsection}{\numberline {2.6}Object quantification}{4}{subsection.2.6}
\contentsline {subsection}{\numberline {2.7}Proof constructs}{4}{subsection.2.7}
\contentsline {subsection}{\numberline {2.8}Modus ponens at the object level}{5}{subsection.2.8}
\contentsline {section}{\numberline {3}Side conditions}{5}{section.3}
\contentsline {subsection}{\numberline {3.1}Logiweb terms}{5}{subsection.3.1}
\contentsline {subsection}{\numberline {3.2}Deduction}{6}{subsection.3.2}
\contentsline {subsection}{\numberline {3.3}Avoidance}{8}{subsection.3.3}
\contentsline {subsection}{\numberline {3.4}Substition}{8}{subsection.3.4}
\contentsline {section}{\numberline {4}Proofs}{9}{section.4}
\contentsline {subsection}{\numberline {4.1}Proofs of FOL axioms using the inference of deduction}{9}{subsection.4.1}
\contentsline {subsection}{\numberline {4.2}A proof of $ \@mathsf {x} + \@mathsf {y} = \@mathsf {y} + \@mathsf {x}$}{10}{subsection.4.2}