% $Id: intro.tex,v 1.2 2008-11-13 23:05:14 logik Exp $

\documentclass[11pt,draft,a4paper]{amsart}
\RequirePackage[latin1]{inputenc}
\RequirePackage{bussproofs}
\RequirePackage{amssymb}
\RequirePackage{verbatim}
\RequirePackage{alltt}
\RequirePackage{enumerate} %allows \begin{comment} text \end{comment}
\RequirePackage{url}
% \RequirePackage{infrule}  %infrule.sty von Benjamin Pierce

% see http://www.ctan.org/tex-archive/help/Catalogue/entries/natbib.html
\RequirePackage[round]{natbib}

% Font commands
\newcommand{\B}{\boldsymbol}
   % Bold math symbol, use as \B{a}
\newcommand{\C}[1]{\mathcal{#1}}
   % Euler Script - only caps, use as \C{A}
\newcommand{\D}[1]{\mathbb{#1}}
   % Doubles - only caps, use as \D{A}
\newcommand{\F}[1]{\mathfrak{#1}}
   % Fraktur, use as \F{a}

% Logic: formulas
\newcommand{\allnc}{\forall^{\mathsf{U}}} %constructive, no comp. content
% \newcommand{\allnc}{\forall^{\mathrm{nc}}} %constructive, no comp. content
\newcommand{\bigland}{\mathop{\hbox{$\bigwedge$\kern-.6em$\bigwedge$}}}
\newcommand{\biglor}{\mathop{\hbox{$\bigvee$\kern-.6em$\bigvee$}}}
\newcommand{\exL}{\exists^{\mathsf{L}}}
\newcommand{\exR}{\exists^{\mathsf{R}}}
\newcommand{\exU}{\exists^{\mathsf{U}}}
\newcommand{\exnc}{\exists^{\mathrm{nc}}} %constructive, with no comp. content
\newcommand{\ex}{\exists} %constructive version, written without *
\newcommand{\excl}{\tilde{\exists}} %classical, with logical falsum
\newcommand{\exca}{\tilde{\exists}} %classical, arithmetical falsum
\newcommand{\falsum}{\bot}
\newcommand{\inTo}{\hookrightarrow}
% \newcommand{\inTo}{\twoheadrightarrow}
\newcommand{\landL}{\land^{\mathsf{L}}}
\newcommand{\landR}{\land^{\mathsf{R}}}
\newcommand{\landU}{\land^{\mathsf{U}}}
% \newcommand{\linto}{\multimap} %replaced by \outTo
\newcommand{\lorL}{\lor^{\mathsf{L}}}
\newcommand{\lorR}{\lor^{\mathsf{R}}}
\newcommand{\lorU}{\lor^{\mathsf{U}}}
\newcommand{\lorbreve}{\mathrel{\breve{\lor}}}
\newcommand{\ltensor}{\otimes}
\newcommand{\lorcl}{\mathrel{\tilde{\lor}}}
\newcommand{\outTo}{\to}
\newcommand{\tonc}{\to^{\mathsf{U}}}
\newcommand{\tobreve}{\mathrel{\breve{\to}}}
\newcommand{\truth}{\top}

% Logic: rules
\newcommand{\allI}{{\forall}^{+}}
\newcommand{\allE}{{\forall}^{-}}
\newcommand{\allncI}{({\allnc})^{+}}
\newcommand{\allncE}{({\allnc})^{-}}
% \newcommand{\allncI}{{\allnc}^{+}}
% \newcommand{\allncE}{{\allnc}^{-}}
\newcommand{\exI}{{\ex}^{+}}
\newcommand{\exE}{{\ex}^{-}}
\newcommand{\exLI}{{(\exL)}^{+}}
\newcommand{\exRI}{{(\exR)}^{+}}
\newcommand{\exUI}{{(\exU)}^{+}}
\newcommand{\exLE}{{(\exL)}^{-}}
\newcommand{\exRE}{{(\exR)}^{-}}
\newcommand{\exUE}{{(\exU)}^{-}}
\newcommand{\falsumE}{\falsum^{-}}
\newcommand{\impI}{{\to}^{+}}
\newcommand{\impE}{{\to}^{-}}
\newcommand{\landI}{{\land}^{+}}
\newcommand{\landLI}{{(\landL)}^{+}}
\newcommand{\landRI}{{(\landR)}^{+}}
\newcommand{\landUI}{{(\landU)}^{+}}
\newcommand{\landE}{\land^{-}}
\newcommand{\landEzero}{{\land}^{-}_0}
\newcommand{\landEone}{{\land}^{-}_1}
\newcommand{\landLE}{{(\landL)}^{-}}
\newcommand{\landRE}{{(\landR)}^{-}}
\newcommand{\landUE}{{(\landU)}^{-}}
\newcommand{\lorI}{\lor^{+}}
\newcommand{\lorIzero}{\lor^{+}_0}
\newcommand{\lorIone}{\lor^{+}_1}
\newcommand{\lorLIzero}{(\lorL)^{+}_0}
\newcommand{\lorLIone}{(\lorL)^{+}_1}
\newcommand{\lorRIzero}{(\lorR)^{+}_0}
\newcommand{\lorRIone}{(\lorR)^{+}_1}
\newcommand{\lorUIzero}{(\lorU)^{+}_0}
\newcommand{\lorUIone}{(\lorU)^{+}_1}
\newcommand{\lorE}{\lor^{-}}
\newcommand{\lorLE}{(\lorL)^{-}}
\newcommand{\lorRE}{(\lorR)^{-}}
\newcommand{\lorUE}{(\lorU)^{-}}
\newcommand{\lorIi}{\lor^{+}_i}
% \newcommand{\orcE}{\lor^{-}}
% \newcommand{\orcIzero}{\lor^{+}_0}
% \newcommand{\orcIone}{\lor^{+}_1}
\newcommand{\tobreveI}{({\tobreve})^{+}}
\newcommand{\tobreveE}{({\tobreve})^{-}}
\newcommand{\toncI}{({\tonc})^{+}}
\newcommand{\toncE}{({\tonc})^{-}}

% Languages
\newcommand{\Fun}{\mathrm{Fun}}
\newcommand{\Rel}{\mathrm{Rel}}
\newcommand{\Ter}{\mathrm{Ter}}

% Lambda calculus
\newcommand{\cnv}{\mapsto}
\newcommand{\red}{\rightarrow}
\newcommand{\redl}{\leftarrow}
\newcommand{\redlstar}{\leftarrow^*}
\newcommand{\redlplus}{\leftarrow^+}
\newcommand{\redstar}{\rightarrow^*}
\newcommand{\redplus}{\rightarrow^+}

% Logic: proof terms
\newcommand{\exelim}[2]{(#1.#2)}
\newcommand{\lorelim}[4]{(#1.#2,#3.#4)}

% Algebras
\newcommand{\branch}{\mathrm{Branch}}
\newcommand{\bs}{\mathit{b}\!\mathit{s}}
\newcommand{\CasesAxiom}{\mathrm{Cases}}
\newcommand{\cons}{\mathrm{cons}}
\newcommand{\constr}{\mathrm{C}}
% \newcommand{\constr}{\mathrm{constr}}
\newcommand{\emp}{\mathrm{Empty}}
\newcommand{\even}{\mathrm{even}}
\newcommand{\evenodd}{\mathrm{evenodd}}
\newcommand{\false}{\mathsf{f\kern-0.14em f}}
% \newcommand{\frec}{\C{F}}
\newcommand{\grec}{\C{F}}
% \newcommand{\find}{\mathrm{FInd}}
\newcommand{\ind}{\mathrm{Ind}}
\newcommand{\leaf}{\mathrm{Leaf}}
\newcommand{\nil}{\mathrm{nil}}
\newcommand{\odd}{\mathrm{odd}}
\newcommand{\rec}{\C{R}}
\newcommand{\suc}{\mathrm{S}}
\newcommand{\Sup}{\mathrm{Sup}}
\newcommand{\ST}{\delta}
\newcommand{\tcons}{\mathrm{Tcons}}
% \newcommand{\termUnit}{\varepsilon}
\newcommand{\termUnit}{\mathbf{u}}
\newcommand{\termTensorIntro}{\typeTensor^+}
\newcommand{\termTensorElim}{\typeTensor^-}
\newcommand{\termProdIntro}{\typeProd^+}
\newcommand{\termProdElimLeft}{\mathrm{fst}}
\newcommand{\termProdElimRight}{\mathrm{snd}}
\newcommand{\tlist}{\mathrm{tlist}}
\newcommand{\tree}{\mathrm{tree}}
\newcommand{\true}{\mathsf{t\kern-0.14em t}}

% Types
\newcommand{\Ty}{\mathrm{Ty}}
\newcommand{\constrtypes}[1]{\mathrm{KT}_{#1}}
\newcommand{\typeBin}{\mathrm{bin}}
% \newcommand{\typeBin}{\mathbf{Bin}}
\newcommand{\typeB}{\mathbf{B}}
\newcommand{\typeInTo}{\hookrightarrow}
% \newcommand{\typeInTo}{\twoheadrightarrow}
% \newcommand{\typeLinTo}{\multimap} ;replaced by \typeOutTo
% \newcommand{\typeL}[1]{\mathrm{list}(#1)}
\newcommand{\typeL}[1]{\mathbf{L}(#1)}
% \newcommand{\typeN}{\mathrm{nat}}
\newcommand{\typeN}{\mathbf{N}}
\newcommand{\typeOutTo}{\to}
\newcommand{\typeP}{\mathbf{P}}
\newcommand{\typeProd}{\times}
% \newcommand{\typeProd}{\land} %Stans proposal
\newcommand{\typeSum}{+}
\newcommand{\typeTensor}{\times}
% \newcommand{\typeTensor}{\land}
% \newcommand{\typeTensor}{\otimes}
\newcommand{\typeTerm}{\mathrm{term}}
\newcommand{\typeTo}{\to} %Stans proposal
% \newcommand{\typeTo}{\Rightarrow}
\newcommand{\typeTree}{\mathbf{T}}
\newcommand{\typeType}{\mathrm{type}}
% \newcommand{\typeUnit}{\mathrm{unit}}
\newcommand{\typeUnit}{\mathbf{U}}
% \newcommand{\typeW}{\mathrm{word}}
\newcommand{\typeW}{\mathbf{W}}

% Arithmetic
% \newcommand{\caseBooleConst}{\mathrm{if}^{\typeB}}
\newcommand{\caseNatConst}{\C{C}}
% \newcommand{\caseNatConst}{\mathrm{if}^{\typeN}}
\newcommand{\caseBooleConst}{\mathrm{if}}
\newcommand{\caseListConst}{\C{C}}
% \newcommand{\caseListConst}{\B{c}}
\newcommand{\one}{\mathrm{1}}
\newcommand{\p}{P}
\newcommand{\s}{S}
% \newcommand{\p}{\mathrm{P}}
% \newcommand{\s}{\mathrm{S}}
\newcommand{\termSumIntroLeft}{\mathrm{inl}}
\newcommand{\termSumIntroRight}{\mathrm{inr}}
\newcommand{\termSumElim}{\typeSum^-}

% Systems
\newcommand{\A}{\mathrm{A}} %Arithmetic
\newcommand{\ACF}{\mathrm{ACF}} %Arithmetic for computable functionals
\newcommand{\EA}{\mathrm{EA}} %Elementary arithmetic
\newcommand{\EACF}{\mathrm{E}\textrm{-}\mathrm{ACF}} %E ACF
\newcommand{\EAIO}{\mathrm{EA({;})}} %Elementary arithmetic
\newcommand{\EHA}{\mathrm{E}\textrm{-}\mathrm{HA}} %E Heyting arithmetic
\newcommand{\EID}{\mathrm{E}\textrm{-}\mathrm{ID}}
\newcommand{\ELID}{\mathrm{E}\textrm{-}\mathrm{LID}} %E LID
\newcommand{\EPA}{\mathrm{E}\textrm{-}\mathrm{PA}} %E Peano Arithmetic
\newcommand{\HA}{\mathrm{HA}} %Heyting Arithmetic
\newcommand{\ID}{\mathrm{ID}} %Arithmetic with inductively defined predicates
\newcommand{\IDelta}{\mathrm{I}\Delta}
\newcommand{\Ilev}{\mathbf{Z}} 
\newcommand{\ISigma}{\mathrm{I}\Sigma}
\newcommand{\IPi}{\mathrm{I}\Pi}
\newcommand{\ISigmaCl}{\mathrm{I}\tilde{\Sigma}}
\newcommand{\IPiCl}{\mathrm{I}\tilde{\Pi}}
\newcommand{\LID}{\mathrm{LID}} %Logic of Inductive Definitions
\newcommand{\LRA}{\mathrm{LA({;})}} %Linear two-sorted arithmetic
\newcommand{\LRT}{\mathrm{LT({;})}} %Linear two-sorted Goedel T
\newcommand{\ML}{\mathrm{ML}} %Minimal logic
\newcommand{\PA}{\mathrm{PA}} %Peano Arithmetic
\newcommand{\PV}{\mathrm{PV}}
\newcommand{\RA}{\mathrm{A({;})}} %Two-sorted Arithmetic
\newcommand{\RAOne}{\Sigma_1\textrm{-}\mathrm{A({;})}}
% \newcommand{\RAOne}{\mathrm{A({;})}^{1}}
\newcommand{\RT}{\mathrm{T({;})}} %Two-sorted Goedel T
\newcommand{\RTOne}{\mathrm{T}_{1}\mathrm{({;})}}
% \newcommand{\RTOne}{\mathrm{T({;})}^{1}}
\newcommand{\T}{\mathrm{T}} %Goedels T
\newcommand{\WEHA}{\mathrm{WE}\textrm{-}\mathrm{HA}} %WE Heyting Arithmetic
\newcommand{\WEPA}{\mathrm{WE}\textrm{-}\mathrm{PA}} %WE Peano Arithmetic
\newcommand{\id}{\mathrm{id}}
\newcommand{\Zth}{\mathrm{Z}}
\newcommand{\LCF}{\mathrm{LCF}}

% Axioms
\newcommand{\AC}{\mathrm{AC}} %axiom of choice
\newcommand{\Deltaca}{\tilde{\Delta}}
\newcommand{\IP}{\mathrm{IP}} %independence of premise
\newcommand{\IPca}{\tilde{\mathrm{IP}}} %indep. of premise, class arith version
\newcommand{\IQ}{\mathrm{IQ}} %independence of quantifier
\newcommand{\MP}{\mathrm{MP}} %Markov's principle
\newcommand{\MPca}{\tilde{\mathrm{MP}}}%Markov's principle, class arith version
\newcommand{\QFAC}{\mathrm{QF}\textrm{-}\mathrm{AC}} %quantifier-free AC
\newcommand{\QFACca}{\mathrm{QF}\textrm{-}\tilde{\mathrm{AC}}}
\newcommand{\UNC}{\mathrm{UNC}} %Uniformity principle for nc universal quant
\newcommand{\WKL}{\mathrm{WKL}} %weak Koenig's Lemma
\newcommand{\WKLca}{\tilde{\mathrm{WKL}}}

% Extraction
\newcommand{\extrCon}[1]{\extrTer{#1}}          %extracted context
\newcommand{\extrTy}[1]{\tau(#1)}
\newcommand{\extrTyP}[1]{\tau^{+}(#1)}
\newcommand{\extrTyN}[1]{\tau^{-}(#1)}
\newcommand{\extrTer}[1]{\lbrack\!\lbrack#1\rbrack\!\rbrack}
\newcommand{\extrTerP}[1]{\lbrack\!\lbrack#1\rbrack\!\rbrack^{+}}
\newcommand{\extrTerN}[1]{\lbrack\!\lbrack#1\rbrack\!\rbrack^{-}}
\newcommand{\extrTerMajP}[1]{\lbrack\!\lbrack#1\rbrack\!\rbrack^{\ast +}}
\newcommand{\extrTerMajN}[1]{\lbrack\!\lbrack#1\rbrack\!\rbrack^{\ast -}}
\newcommand{\nulltype}{\varepsilon}
\newcommand{\nullterm}{\varepsilon}

% Inductively generated predicates
\newcommand{\Acc}{\mathrm{Acc}}
\newcommand{\algAcc}{\mathrm{algAcc}}
\newcommand{\LAnd}{\mathrm{And}}
\newcommand{\LAndL}{\mathrm{AndL}}
\newcommand{\LAndR}{\mathrm{AndR}}
\newcommand{\LAndU}{\mathrm{AndU}}
\newcommand{\LOr}{\mathrm{Or}}
\newcommand{\LOrL}{\mathrm{OrL}}
\newcommand{\LOrR}{\mathrm{OrR}}
\newcommand{\LOrU}{\mathrm{OrU}}
\newcommand{\Barid}{\mathrm{Bar}}
\newcommand{\clauses}[1]{\mathrm{KF}_{#1}}
% \newcommand{\clauses}{\mathrm{KF}}
\newcommand{\Ex}{\mathrm{Ex}}
\newcommand{\ExL}{\mathrm{ExL}}
\newcommand{\ExR}{\mathrm{ExR}}
\newcommand{\ExU}{\mathrm{ExU}}
\newcommand{\Even}{\mathrm{Even}}
\newcommand{\Ev}{\mathrm{Ev}}
\newcommand{\formulas}{\mathrm{F}}
\newcommand{\Od}{\mathrm{Od}}
% \newcommand{\Or}{\mathrm{Or}}
\newcommand{\preds}{\mathrm{Preds}}
\newcommand{\Good}{\mathrm{Good}}
\newcommand{\Tree}{\mathrm{Tree}}
\newcommand{\Tlist}{\mathrm{Tlist}}
\newcommand{\TrCl}{\mathrm{TrCl}}

% Computability
\newcommand{\Con}{\mathrm{Con}}
\newcommand{\entails}{\vdash}
\newcommand{\InCon}{\mathrm{InCon}}

% abhs01
\newcommand{\activation}{\mathrm{Activation}}
\newcommand{\Add}{\mathrm{Add}}
\newcommand{\assumption}{\mathrm{Assumption}}
\newcommand{\axiom}{\mathrm{Axiom}}
\newcommand{\cextrTy}[1]{\tau^{\mathrm{c}}({#1})}   %cleaned extracted type
\newcommand{\cextrTer}[1]{\extrTer{#1}^{\mathrm{c}}}%cleaned extracted term
\newcommand{\cextrCon}[1]{\cextrTer{#1}}            %cleaned extracted context
\newcommand{\clean}[1]{\mathop{\mathrm{c}}(#1)}
\newcommand{\conItA}[1]{\{ {#1} \}}
\newcommand{\contraction}{\mathrm{Contraction}}
\newcommand{\dbound}[2]{\vartheta_{#1}(#2)}
\newcommand{\dlength}[2]{\#_{#1}(#2)}
\newcommand{\emptycontext}{\cdot}
\newcommand{\HAder}[3]{{#1}\mid{#2} \vdash {#3}}
\newcommand{\HAeq}{=^{e}}
\newcommand{\HAitA}[1]{\{ {#1} \}}
\newcommand{\HAtyped}[4]{{#1}\mid{#2} \vdash {#3}\colon {#4}}
\newcommand{\Ins}{\mathrm{Ins}}
\newcommand{\NSIT}{\mathrm{NSIT}}
\newcommand{\NSIHA}{\mathrm{NSIHA}}
\newcommand{\numfv}[1]{|\FV(#1)|}
\newcommand{\pair}[2]{\langle #1 , #2 \rangle}
\newcommand{\passification}{\mathrm{Passification}}
\newcommand{\pred}{\mathrm{P}}
\newcommand{\projleft}[1]{\pi_0(#1)}
\newcommand{\projright}[1]{\pi_1(#1)}
\newcommand{\rednumfv}[1]{\to_{#1}}
\newcommand{\Set}{\D{S}}
\newcommand{\Sort}{\mathrm{Sort}}
\newcommand{\typeD}{\diamond}
\newcommand{\typeLrhoInd}{\typeL{\rho}\textrm{-}\mathrm{Ind}}
\newcommand{\typeLrhoStrongInd}{\typeL{\rho}\textrm{-}\mathrm{Ind}^+}
\newcommand{\typeNStrongInd}{\typeN\textrm{-}\mathrm{Ind}^+}
\newcommand{\VarBed}{\hbox{\texttt{VarCond}}}
\newcommand{\weakening}{\mathrm{Weakening}}

% BBLS06
\newcommand{\boole}{\mathrm{boole}}
\newcommand{\Cor}{\mathrm{Cor}}
\newcommand{\Free}{F}
\newcommand{\lnf}[1]{\mathrm{nf}(#1)} 
\newcommand{\HatF}{\mathrm{Hat}}
\newcommand{\HatIota}{\mathrm{HatL}}
\newcommand{\inn}{\mathrm{in}}
\newcommand{\nat}{\mathrm{nat}}
\newcommand{\Lh}{\mathrm{Lh}}
\newcommand{\listconstr}{\mathrm{list}}
\newcommand{\nbe}{nor\-ma\-li\-zation-by-evalu\-ation}
\newcommand{\Mod}{\mathrm{Mod}}
\newcommand{\ModIota}{\mathrm{ModL}}
\newcommand{\OmegaPart}{P}
\newcommand{\overwrite}[3]{#1[#2\mapsto #3]}
\newcommand{\reflect}{{\uparrow}}
\newcommand{\reify}{{\downarrow}} 
\newcommand{\SA}{\mathrm{SA}}
\newcommand{\SCr}{\mathrm{SCr}}
\newcommand{\term}{\mathrm{term}}
\newcommand{\Typ}{\mathrm{Typ}}
\newcommand{\type}{\mathrm{type}}
\newcommand{\types}{\mathrm{types}}
\newcommand{\Valtyp}{\mathrm{Valtyp}}

% Additions for the recursion theory course, WS 2006
% Computability
\newcommand{\dotminus}{\mathbin{{{-\mkern -9.5mu%
\mathchoice{\raise 2pt\hbox{$\cdot$}\mkern6mu}%
{\raise 2pt\hbox{$\cdot$}\mkern6mu}%
{\raise 1.5pt\hbox{$\scriptstyle\cdot$}\mkern4mu}%
{\raise 1pt\hbox{$\scriptscriptstyle\cdot$}\mkern4mu}}}}}
\newcommand{\Elementary}{\mathrm{Elem}}
\newcommand{\Prim}{\mathrm{Prim}}
\newcommand{\Prime}{\mathrm{Prime}}
\newcommand{\comp}{\mathrm{comp}}
\newcommand{\state}{\mathrm{state}}
\newcommand{\tr}{\mathrm{tr}}
\newcommand{\dc}{\mathrm{dc}}
\newcommand{\Comp}{\mathrm{Comp}}
% \newcommand{\ifthenelse}[3]
% {\textbf{if\ } #1 \textbf{\ then\ } #2 \textbf{\ else\ } #3}
\newcommand{\compose}[2]{#1 \textbf{\ ;\ } #2}
\newcommand{\composethree}[3]{#1 \textbf{\ ;\ } #2 \textbf{\ ;\ } #3}
\newcommand{\composefour}[4]
{#1 \textbf{\ ;\ } #2 \textbf{\ ;\ } #3 \textbf{\ ;\ } #4}
\newcommand{\ifthenelsefi}[3]
{\textbf{if\ } #1 \textbf{\ then\ } #2 \textbf{\ else\ } #3 \textbf{\ fi}}
\newcommand{\forloop}[2]
{\textbf{for\ } #1 \textbf{\ do\ } #2 \textbf{\ od}}
\newcommand{\whileloop}[2]
{\textbf{while\ } #1 \textbf{\ do\ } #2 \textbf{\ od}}
% \newcommand{\Add}{\mathrm{Add}}
\newcommand{\Subt}{\mathrm{Subt}}
\newcommand{\Mult}{\mathrm{Mult}}
\newcommand{\hd}{\mathrm{hd}}
\newcommand{\tl}{\mathrm{tl}}

% \renewcommand{\equiv}{\leftrightarrow}

% Goedel theorems
\newcommand{\Sub}{\mathrm{Sub}}
\newcommand{\Prf}{\mathrm{Prf}}
\newcommand{\PR}{\mathrm{PR}}
\newcommand{\Th}{\mathrm{Th}}
\newcommand{\sub}{\mathrm{sub}}
\newcommand{\Symb}{\mathrm{Symb}}
\newcommand{\For}{\mathrm{For}}
\newcommand{\substval}{\mathrm{substval}}

\newcommand{\restrict}{\mathrm{restrict}}
\newcommand{\Ranv}{\mathrm{Ranv}}
\newcommand{\ranv}{\mathrm{ranv}}
\newcommand{\newvar}{\mathrm{newvar}}
\newcommand{\BV}{\mathrm{BV}}
\newcommand{\newranv}{\mathrm{newranv}}
\newcommand{\msetleft}{\{\!\{}
\newcommand{\msetright}{\}\!\}}
\newcommand{\msm}{\mathrm{msm}}
\newcommand{\msrm}{\mathrm{msrm}}
\newcommand{\mseq}{\mathrm{mseq}}
\newcommand{\Herl}{\mathrm{Herl}}
\newcommand{\Deriv}{\mathrm{Deriv}}
% \newcommand{\Abl}{\mathrm{Abl}}
\newcommand{\Stabax}{\mathrm{Stabax}}
\newcommand{\app}{\mathrm{app}}
\newcommand{\gen}{\mathrm{gen}}
\newcommand{\dotand}{\mathbin{\dot\land}}
% \newcommand{\doteq}{\mathbin{\dot=}}
\newcommand{\dotneg}{\mathord{\dot\neg}}
\newcommand{\dotto}{\mathbin{\dot\to}}
\newcommand{\ran}{\mathrm{ran}}
\newcommand{\Ax}{\mathrm{Ax}}
\newcommand{\Refut}{\mathrm{Refut}}
% \newcommand{\Cons}{\mathrm{Cons}}
\newcommand{\Thm}{\mathrm{Thm}}
\newcommand{\falsity}{\bot}
\newcommand{\falsityF}{\mathbf{F}}
% \newcommand{\falsityF}{\D{F}}
% \newcommand{\falsityF}{\mathsf{F\kern-0.14em F}}
\newcommand{\falsityid}{\bot_{\mathrm{id}}}

% rt
\newcommand{\acc}{\mathrm{acc}}
\newcommand{\Card}{\mathrm{Card}}
\newcommand{\CK}{\mathrm{CK}}
\newcommand{\concat}[2]{\hbox{$#1$ {\bf ;} $#2$}}
\newcommand{\Field}{\mathrm{Field}}
\newcommand{\fordo}[2]{\hbox{{\bf for} $#1$ {\bf do} $#2$ {\bf od}}}
\newcommand{\gfp}[1]{\C{C}_{#1}}
\newcommand{\Init}{\mathrm{Init}}
\newcommand{\lfp}[1]{\C{I}_{#1}}
\newcommand{\LinOrd}{\mathrm{LinOrd}}
\newcommand{\KB}{\mathrm{KB}}
\newcommand{\On}{\mathrm{On}}
\newcommand{\Seq}{\mathrm{Seq}}
\newcommand{\Tot}{\mathrm{Tot}}
\newcommand{\WOrd}{\mathrm{WOrd}}

% Miscellaneous
\newcommand{\AllFor}{\mathrm{AllFor}}
\newcommand{\andb}{\mathrel{\mathrm{andb}}}
\newcommand{\atom}{\mathrm{atom}}
\newcommand{\AtomFor}{\mathrm{AtomFor}}
\newcommand{\ar}{\mathrm{ar}}
\newcommand{\BNFdef}{\mathtt{\; ::= \;}}
\newcommand{\BNFor}{\mid}
\newcommand{\bottom}{\bot}
\newcommand{\card}[1]{\#(#1)}
\newcommand{\caseof}[2]{[\textbf{case}\; #1\; \textbf{of}\; #2]}
\newcommand{\Cases}{\C{C}}
% \newcommand{\Cases}{\mathrm{Cases}}
\newcommand{\con}[3]{#2 ::_{#1} #3}
% \newcommand{\con}[3]{\cons_{#1}{#2}{#3}}
\newcommand{\cond}{\mathrm{cond}}
\newcommand{\CV}{\mathrm{CV}}
\newcommand{\cvind}{\mathrm{cvind}}
\newcommand{\dotcup}{\mathrel{\dot\cup}}
\newcommand{\defeq}{:=}
% \newcommand{\defeq}{=_{\mathrm{def}}}
% \newcommand{\defeq}{\equiv}
\newcommand{\defequiv}{:=}
% \newcommand{\defequiv}{\equiv_{\mathrm{def}}}
% \newcommand{\defequiv}{:\equiv}
% \newcommand{\defequiv}{:\Longleftrightarrow}
% \newcommand{\defequiv}{\;\;:\Longleftrightarrow\;\;}
\newcommand{\dep}[1]{\mathrm{dp}(#1)} %depth of a formula or proof tree
% \newcommand{\dist}{\mathrm{dist}}
\newcommand{\dom}{\mathrm{dom}}
\newcommand{\eexp}{{\eta{\uparrow}}}
\newcommand{\Efq}{\mathrm{Efq}}
\newcommand{\EfqLog}{\mathrm{Efq}\textrm{-}\mathrm{Log}}
\newcommand{\Efqdummy}{a_0}
\newcommand{\Eq}{\mathrm{Eq}}
\newcommand{\eqdef}{=:}
\newcommand{\EqI}{\mathrm{Eq}^{+}}
\newcommand{\EqE}{\mathrm{Eq}^{-}}
\newcommand{\Elim}{\mathrm{Elim}}
\newcommand{\emptyseq}{\langle\rangle}
\newcommand{\en}{\mathrm{en}}
\newcommand{\eps}{\varepsilon}
\newcommand{\exf}{\mathrm{neg}}
% \newcommand{\exf}{\ex\textrm{-}\mathrm{free}}
\newcommand{\ext}{\mathrm{ext}}
\newcommand{\FA}{\mathrm{FA}}
\newcommand{\Fib}{G}
\newcommand{\fini}{{\vbox{\hrule\hbox{%  
\vrule height1.3ex\hskip0.8ex\vrule}\hrule}}}
\newcommand{\fin}{\mathrm{fin}}
% \newcommand{\FInd}{\mathrm{FInd}}
\newcommand{\fix}{\C{Y}}
\newcommand{\forces}{\Vdash}
\newcommand{\fvt}{\mathrm{fvt}}
\newcommand{\fwert}{{0}}
\newcommand{\FV}{\mathrm{FV}}
\newcommand{\GInd}{\mathrm{GInd}}
\newcommand{\goe}[3]{|#1|^{#2}_{#3}}
\newcommand{\goemr}[3]{\norm{#1}^{#2}_{#3}}
\newcommand{\head}{\mathrm{hd}}
% \newcommand{\head}{\mathrm{head}}
\newcommand{\height}[1]{|#1|} %height of a formula or proof tree
% \newcommand{\height}[1]{|#1|} %height of a formula or proof tree
\newcommand{\ic}{\mathrm{[}\mathrm{ic}\mathrm{]}}
% \newcommand{\ID}{\mathrm{ID}}
\newcommand{\If}{\mathrm{If}}
\newcommand{
  \ifthenelse}[3]{[\textbf{if}\; #1\; \textbf{then}\; #2\; \textbf{else}\; #3]}
\newcommand{\imp}{\Rightarrow}
\newcommand{\impb}{\mathrel{\mathrm{impb}}}
\newcommand{\ImpFor}{\mathrm{ImpFor}}
\newcommand{\incons}{\mathrm{incons}}
\newcommand{\Ind}{\mathrm{Ind}}
\newcommand{\infseq}[3]{#1 \colon N \, \vdash^{#2} \, #3} %agreed on 03-01-15
\newcommand{\infseqr}[4]{#1 \colon N \, \vdash^{#2}_{\Sigma_{#3}}\, #4}
\newcommand{\inquotes}[1]{``#1''}
\newcommand{\Intro}{\mathrm{Intro}}
\newcommand{\lambdanc}{\lambda^{\mathsf{U}}}
\newcommand{\lev}[1]{\mathrm{lev}(#1)}
% \newcommand{\lh}{\mathrm{lh}}
\newcommand{\lh}[1]{\mathrm{lh}(#1)}
\newcommand{\Lim}{\mathrm{Lim}}
\newcommand{\listappend}{\mathbin{{:}{+}{:}}}
\newcommand{\listrev}{\mathrm{Rev}}
\newcommand{\maj}{\mathrel{\mathrm{maj}}}
\newcommand{\mon}{\mathrm{mon}}
\newcommand{\mr}{\mathrel{\mathbf{r}}}
% \newcommand{\mr}{\,\mathbf{r}\,}
% \newcommand{\mr}{\mathrel{\mathrm{mr}}}
% \newcommand{\mr}{\,\mathrm{mr}\,}
% \newcommand{\mr}{\,\underline{\mathbf{mr}}\,}
\newcommand{\mrAAA}{\mathrel{\mathrm{mr}_{\C{A}}}}
\newcommand{\mref}{\mathbf{ef}}
\newcommand{\mrind}{\textbf{r}}
\newcommand{\new}{\mathrm{new}}
\newcommand{\nf}[1]{\mathrm{nf}(#1)}
\newcommand{\Nf}{\mathrm{Nf}}
\newcommand{\nhd}{\mathrm{nhd}}
\newcommand{\norm}[1]{| \! |#1| \! |}
\newcommand{\orb}{\mathrel{\mathrm{orb}}}
\newcommand{\pcond}{\mathrm{pcond}}
\newcommand{\Prog}{\mathrm{Prog}}
\newcommand{\Proper}{\mathrm{Proper}}
\newcommand{\Rev}{\mathrm{Rev}}
\newcommand{\rf}[3]{\mathrm{rf}(#1;#2;#3)}
\newcommand{\SC}{\mathrm{SC}}
\newcommand{\set}[2]{\{\,#1\mid#2\,\}}
\newcommand{\size}[1]{\norm{#1}} %size of a proof tree or formula
% \newcommand{\size}[1]{|#1|} %size of a proof tree or formula
\newcommand{\sg}{\mathrm{sg}}
\newcommand{\smaj}{\mathrel{\mathrm{s}\textrm{-}\mathrm{maj}}}
\newcommand{\sn}{\mathrm{sn}}
\newcommand{\SE}{\mathrm{SE}} %structural existence
\newcommand{\SN}{\mathrm{SN}}
\newcommand{\Spec}{\mathrm{Spec}}
\newcommand{\SProg}{\mathrm{SProg}}
\newcommand{\Stab}{\mathrm{Stab}}
\newcommand{\STotal}{\mathrm{ST}}
% \newcommand{\STotal}{\mathrm{STotal}}
\newcommand{\subst}[3]{#1[#2:= #3]}
\newcommand{\substnarrow}[3]{#1[#2{:=}#3]}
\newcommand{\Succ}{\mathrm{Succ}}
\newcommand{\tail}{\mathrm{tl}}
% \newcommand{\tail}{\mathrm{tail}}
\newcommand{\termfam}[1]{#1^{\infty}}
\newcommand{\tok}{\mathrm{tok}}
\newcommand{\Total}{T}
% \newcommand{\Total}{\mathrm{Total}}
\newcommand{\Truthax}{\mathrm{Ax}_{\true}}
\newcommand{\UP}{\mathrm{UP}}
\newcommand{\val}[1]{\lbrack\!\lbrack#1\rbrack\!\rbrack}
\newcommand{\valop}[1]{\lbrack#1\rbrack}
\newcommand{\valstrict}[1]{\lbrace\!\!\lbrace#1\rbrace\!\!\rbrace}
\newcommand{\Var}{\mathrm{Var}}
\newcommand{\vars}{\mathrm{vars}}
\newcommand{\Wf}{\mathrm{Wf}}
\newcommand{\ws}{\mathit{w}\!\mathit{s}}
\newcommand{\wwert}{{1}}
\newcommand{\Zero}{\mathrm{Zero}}

% comment out the following lines if you would 
%  like to revert to the old notation.
% \renewcommand{\termUnit}{\mathsf{x\kern-0.14em x}}
% \renewcommand{\nil}{\varepsilon}
% \renewcommand{\con}[3]{#3 *_{#1} #2}

\makeindex

\newenvironment{enumeratei}{\begin{enumerate}[\upshape (i)]}
                           {\end{enumerate}}
   % produces (i), (ii), etc,  Cross-reference with \eqref
\newenvironment{enumeratea}{\begin{enumerate}[\upshape (a)]}
                           {\end{enumerate}}
   % produces (a), (b), etc,  Cross-reference with \eqref

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem*{theorem*}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem*{lemma*}{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem*{corollary*}{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem*{proposition*}{Proposition}
\newtheorem{claim}[theorem]{Claim}
\newtheorem*{claim*}{Claim}
\newtheorem*{axiom*}{Axiom}
\newtheorem*{namedtheorem}{\theoremname}
\newcommand{\theoremname}{testing}
\newenvironment{named}[1]{\renewcommand{\theoremname}{#1}
  \begin{namedtheorem}}
  {\end{namedtheorem}}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem*{definition*}{Definition}
\newtheorem{notation}[theorem]{Notation}
\newtheorem*{notation*}{Notation}
\newtheorem{convention}[theorem]{Convention}
\newtheorem*{convention*}{Convention}
\newtheorem{example}[theorem]{Example}
\newtheorem*{example*}{Example}
\newtheorem{examples}[theorem]{Examples}
\newtheorem*{examples*}{Examples}
\newtheorem{exercise}[theorem]{Exercise}
\newtheorem*{exercise*}{Exercise}
\newtheorem{exercises}[theorem]{Exercises}
\newtheorem*{exercises*}{Exercises}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem*{remark*}{Remark}
\newtheorem{remarks}[theorem]{Remarks}
\newtheorem*{remarks*}{Remarks}
\newtheorem{note}[theorem]{Note}
\newtheorem*{note*}{Note}
\newtheorem*{acknowledgement*}{Acknowledgement}
\newtheorem{problem}{Problem}
\newtheorem*{problem*}{Problem}
\newtheorem{solution}{Solution}
\newtheorem*{solution*}{Solution}

% \renewcommand\thesection{\thechapter.\arabic{section}} %Urban
% \renewcommand\thesubsection{\thesection.\arabic{subsection}} %Urban
% \renewcommand\thetheorem{\thesection.\arabic{theorem}} %Urban
% \renewcommand\thetable{\thesection.\arabic{table}} %Urban

% \numberwithin{section}{chapter}
% \numberwithin{equation}{chapter}
% \numberwithin{equation}{section}
% \numberwithin{equation}{theorem}

\allowdisplaybreaks[4]
\setlength{\textheight}{19 true cm}

\begin{document}

\title{Introduction to the Minlog proof assistant} 
\author {}
\maketitle


% \tableofcontents


\section{Introduction}

This is a tutorial\footnote{The present text is an updated and
  extended version of an earlier one written by Laura Crosilla, which
  again took inspiration from Martin Ruckert's tutorial for an older
  version of \textsc{Minlog}.  Monika Seisenberger provided comments
  and examples.} to the proof assistant \textsc{Minlog}, version 4.0,
developed by Helmut Schwichtenberg and members of the logic group at
the University of Munich
\url{www.mathematik.uni-muenchen.de/logik/welcome.html}.  It is
implemented in \textsc{Scheme} and runs under every \textsc{Scheme}
version supporting the Revised$^5$ Report on the Algorithmic Language
\textsc{Scheme}.  \textsc{Minlog}'s favorite dialect is Petite Chez
\textsc{Scheme} from Cadence Research Systems, which is freely
distributed at the Internet address \url{www.scheme.com}.  The
\textsc{Minlog} system can be downloaded from
\url{www.minlog-system.de}.

\begin{comment}
  Goals: (1) Experiment with extraction of computational content
  from proofs.  (2) Keep the underlying logic simple: minimal logic with
  introduction and elimination rules for $\to, \forall$, plus
  inductively defined predicates.

  The \textsc{Minlog} system has been under development since around 1990.
  Its first appearence is in \citet{Schwichtenberg93a}.
  My sincere thanks go to the many contributors:  
  % Klaus Aehlig (many contributions, in particular efficiency related issues),
  Freiric Barral (reflection),
  Holger Benl (Dijkstra algorithm, inductive data types),
  Ulrich Berger (very many contributions),
  Michael Bopp (program development by proof transformation),
  Wilfried Buchholz (translation of classical proof into intuitionistic ones),
  Luca Chiarabini (program development by proof transformation),
  Laura Crosilla (tutorial),
  Matthias Eberl (normalization by evaluation),
  Dan Hernest (Dialectica interpretation),
  Simon Huber (many contributions, including guarded recursion and general
  induction),
  Felix Joachimski (many contributions, in particular translation of classical
  proofs into intuitionistic ones, producing Tex output, documentation),
  Ralph Matthes (documentation),
  Karl-Heinz Niggl (program development by proof transformation),
  Jaco van de Pol (experiments concerning monotone functionals),
  Florian Ranzi (higher order matching),
  Diana Ratiu ($A$-translation, decoration),
  Martin Ruckert (many contributions, in particular parsing and the MPC tool),
  Stefan Schimanski (pretty printing, system related questions),
  Robert Stärk (alpha equivalence),
  Monika Seisenberger (many contributions, including inductive definitions and
  translation of classical proofs into intuitionistic ones),
  Klaus Thiel (constructive ordinals),
  Trifon Trifonov (many contributions, including Dialectica interpretation),
  Klaus Weich (proof search, the Fibonacci numbers example),
  Wolfgang Zuber (documentation).
\end{comment}

\section{Getting started}
The purpose of this text is to give a very basic introduction to the
\textsc{Minlog} system by means of some simple examples.  For a
thorough presentation of \textsc{Minlog} and the motivation behind it
the reader should consult the reference manual.  %\cite{minlogman}.
The papers listed in the \textsc{Minlog} web page also provide a more
detailed and advanced description of the system.  In addition, the
\textsc{Minlog} distribution comes equipped with a directory of
examples, to which the user is referred.  The source code finally
provides the ultimate reference.

In order install \textsc{Minlog}, follow the instructions on the web
site.  An easy way to use it is the \inquotes{Proof General} framework
provided there.  An alternative is the following.  One essentially
needs a shell in which to run \textsc{Minlog} and also an editor in
which to edit and keep a record of the commands for later sessions.
In this text we shall refer to \textsc{Gnu Emacs}.  While working with
\textsc{Emacs}, the ideal would be to split the window in two parts,
one with the file in which to store the commands, and the other with
the \textsc{Minlog} interactive section taking place.  It is assumed
tacitly that you are using an \textsc{Unix}-like operating system and
that \textsc{Minlog} is installed in \texttt{\~{}/minlog}, where \~{}
denotes as usual your home directory.  To prepare for running Petite
Scheme, after installing Petite Chez \textsc{Scheme} the file
\texttt{.emacs} should contain the lines
\begin{verbatim}
  (setq scheme-program-name "petite")
  (autoload 'run-petite "petite" "Run an inferior Scheme" t)
\end{verbatim}
Then after starting \textsc{Emacs} use the commands
\begin{alignat*}{2}
  &\texttt{M-x run-petite <enter>}
  \\
  &\texttt{Ctrl-x 2}
  &\quad& \hbox{(splits the window into two)}
  \\
  &\texttt{Ctrl-x Ctrl-f file.scm}
  && \hbox{(creates \texttt{file.scm} for storing commands)}
\end{alignat*}
Then type into \texttt{file.scm} the command
\begin{alignat*}{2}
  &\texttt{(load "\~{}/minlog/init.scm")}
\end{alignat*}
and execute it.
\begin{comment}
  For this it is recommended to use
  the startup script \texttt{\~{}/minlog/minlog} which takes files as
  (optional) arguments. For example
  \begin{quote}
    \texttt{\~{}/minlog/minlog file.scm}
  \end{quote}
  opens a new Emacs-Window which is split into two parts. The upper part
  containes the file \texttt{(Buffer file.scm)} whereas the lower part
  shows the \textsc{Minlog} response \texttt{(Buffer *minlog*)}.

  If you have already an open emacs window and do not want to open
  a new one then you can invoke minlog by loading the file
  \texttt{minlog.el}:
  \begin{quote}
    \texttt{M-x load-file <enter>}\\
    \texttt{\~{}/minlog/minlog.el}
  \end{quote}
  [* Needs to be updated *]
\end{comment}
To execute a command of your file, one simply places the cursor at the
end of it (after the closing parenthesis), and types \texttt{Ctrl-x
  Ctrl-e}.  In general, \texttt{Ctrl-x Ctrl-e} will enable us to
process any command we type in \texttt{file.scm}, but one at the
time.  To process a whole series of commands, one can highlight the
region of interest and type \texttt{Ctrl-c Ctrl-r}.  We should also
mention at this point that to undo one step, it is enough to give the
command \texttt{(undo)}, while \texttt{(undo n)} will undo the last
$n$ steps.  Finally, type \texttt{(exit)} to end a \textsc{Scheme}
session and \texttt{Ctrl-x Ctrl-c} to exit \textsc{Emacs}.


\begin{comment}
  \section{Algebras and terms}

  \paragraph{To do}
  Define the booleans.  How to declare typed variables.  Gives
  two constants.  Then zero, successor.  Say which constructors have
  been defined.  Exercise (with solutions in an appendix): binary trees.
  Build terms from variables and constants.  Example of input of terms
  using \texttt{pt}.  Explain \texttt{term-to-type}; give examples.  For
  instance, \texttt{Factorial} or also (simultaneously) \texttt{Even}
  and \texttt{Odd} with computation rules.  Explain normalization and
  give examples.  Exercises (with solutions).

  \subsection{Booleans, natural numbers, lists}
  Canonical inhabitants.


  \subsection{Recursion}
  Guarded recursion.


  \subsection{Defined functions}
  Computation and rewrite rules.

  \subsection{Normalization}


  \section{Formulas} 

  \subsection{Prime formulas, implication and the universal quantifier}
  Formulas are built from prime formulas by $\to$ and $\forall$.  Prime
  formulas are of the form $R(t_{1}, \dots, t_{n})$ where $R$ is a
  predicate symbol of some arity $(\rho_{1}, \dots, \rho_{n})$, with
  $t_{i}$ a term of type $\rho_{i}$.  An important example of a
  predicate is Leibniz equality $\Eq$ of arity $(\rho, \rho)$.  Then
  $\Eq(r,s)$, where $r,s$ are terms of the same type $\rho$, is a prime
  formula.

  For example, $\Eq(n,m)$ is a formula, which can be defined in
  \textsc{Minlog} by typing \texttt{(pf "Eq n m")}, where \texttt{n}, \texttt{m} are declared variables of type
  \texttt{nat}.  Similarly one can input $\Eq(0,1)$, written as
  \texttt{(pf "Eq 0
    1")}.
  An implication is written as \texttt{(pf "A -> B")},
  and universal quantification as \texttt{(pf "all x Q x")}.  For
  examples, the formulas
  \begin{align*}
    &\forall_y \Eq(x+y,y) \to \Eq(x,0),
    \\
    &\forall_{x,y}(\Eq(x,y) \to \Eq(y,x))
  \end{align*}
  are entered in \textsc{Minlog} as follows:
  \begin{align*}
    &\hbox{\texttt{(pf "all y Eq(x+y)y -> Eq x 0")}}
    \\
    &\hbox{\texttt{(pf "all x,y(Eq x y -> Eq y x))}}.
  \end{align*}
  We can lift a boolean term $r$ to a (decidable) prime formula by
  forming $\Eq(r, \true)$; in \textsc{Minlog} we write \texttt{(pf "Eq r
    true")} or shorter as \texttt{(pf "r")}.  This must not be confused
  with the boolean \emph{term} \texttt{r}, which should be entered as
  \texttt{(pt "r")}.  We define falsity by $\falsityF \defeq \Eq(\false,
  \true)$; in \textsc{Minlog} this is written \texttt{(pf "F")}.
  Similarly the formula $\Eq(\true, \true)$ is written \texttt{(pf
    "T")}.


  \subsection{Weak existential}
  Folding and unfolding.

  \begin{remark*}[Dot notation]
    We may use \inquotes{.} to indicate the scope of a quantifier, with
    the convention that it binds as far as possible.  To switch this
    feature off (which we do in this text) execute
    \texttt{(set!\ DOT-NOTATION \#f)}.
  \end{remark*}

  \section{Proofs}

  \subsubsection*{To do}  
  Leibniz equality defined by the clause $\allnc_x \Eq(x,x)$.  Use the
  following as axioms, and say that all these could be derived from
  \begin{equation*} \Eq^{-} \colon \forall_{x,y} \bigl( \Eq(x,y) \to
    \forall_x C(x,x) \to C(x,y) \bigr).  \end{equation*} Compatibility
  of $\Eq$: $\forall_{x, y} \bigl(\Eq(x, y) \to A(x) \to A(y) \bigr)$.
  Take Ex Falso Quodlibet: $\falsityF \to A$ as axiom.  Exercise: Using
  compatibility of $\Eq$ prove symmetry and transitivity.


  \subsection{Introduction and elimination rules for $\to, \forall$}
\end{comment}

\section{Propositional proofs}


\subsection{A first example}
We shall start from a simple example in propositional logic.  Suppose
we want to prove the tautology
\begin{equation*}
  (A \to (B \to C)) \to ((A \to B) \to (A \to C)).
\end{equation*}
In the following we shall make use of the convention of association to
the right of the parentheses, which is assumed by \textsc{Minlog}.
Therefore the formula above becomes: $(A \to B \to C) \to (A \to B)
\to A \to C$.  It is very important, especially in the beginning, to
pay the maximum attention to this and similar conventions to prevent
mistakes.  It is probably a good idea to rather exceed in parentheses
in the first examples.  \textsc{Minlog} will automatically delete the
parenthesis which are not needed, therefore facilitating the reading.

\subsubsection*{Making a sketch of the proof}
We need in the first place to make an informal plan on how to prove
this tautology.  While making this plan we should consider the
following fact.  \textsc{Minlog} (mainly) implements \inquotes{goal
  driven reasoning}, also called \inquotes{backward chaining}.  That
means that we start by writing the conclusion we aim at as our goal
and then, step by step, refine this goal by applying to it appropriate
logical rules, until we reach the point of having no more goals to
solve.  In other words, \textsc{Minlog} keeps a list of goals and
updates it each time a logical rule is applied.  A logical rule will
have the effect of reducing the proof of a formula, the goal, to the
proof of one or more other formulas, which will become the new goals.
The proof is completed when the list of goals is empty.

In this case the tautology we want to prove is a series of
implications, hence we will have to make use of basic rules for
\inquotes{deconstructing} implications.  The first move will then be
to assume that the antecedent of the outmost implication is true and
try to derive the consequent from it.  That is, we assume $A \to B \to
C$ and want to derive $(A \to B) \to A \to C$; hence we set the latter
as our new goal.  Then we observe that $(A \to B) \to A \to C$ is an
implication and can be treated in the same way; so we now assume $A
\to B \to C$ and $A \to B$ and want to derive $A \to C$.  Clearly, we
can make the same step once more and obtain $A \to B \to C$, $A \to B$
and $A$ as our premises and try to derive $C$ from them.  Now we
observe that in order to prove $C$ under the assumption $A \to B \to
C$, we simply need to prove both $A$ and $B$ under the same
assumption.  Obviously $A$ is proved, as it is one of our assumptions,
and $B$ immediately follows from $A \to B$ and $A$.


\subsubsection*{Writing the formula}
Once we have an idea on how to prove the formula, we can start
implementing the proof in \textsc{Minlog}.  The initial step would then
be to write the formula in \textsc{Minlog}.  For this purpose, we
declare three predicate constants $A$, $B$ and $C$ by writing:
\begin{verbatim}
(add-predconst-name "A" "B" "C" (make-arity))
\end{verbatim}
The expression \texttt{(make-arity)} produces the empty arity for $A$,
$B$ and $C$ (see the reference manual for a
description of \texttt{(make-arity)}).  \textsc{Minlog} will then
write:
\begin{verbatim}
; ok, predicate constant A: (arity) added
; ok, predicate constant B: (arity) added
; ok, predicate constant C: (arity) added 
> 
\end{verbatim}
Subsequently, we write the formula and give it a name, say
\texttt{distr} (for distributivity of implication):
\begin{verbatim}
(define distr (pf "(A -> B -> C) -> (A -> B) -> A -> C"))
\end{verbatim}
This command has the effect of defining a new variable \texttt{distr}
and attaching to it the \textsc{Scheme} object which is produced by the
function \texttt{pf} applied to the formula we entered.  In fact, the
function \texttt{pf}, short for \inquotes{parse formula}%
\index{parse formula}, takes a string as argument and returns a
\textsc{Scheme} object.  This \textsc{Scheme} object is the way
\textsc{Minlog} stores the string, or, equivalently, it is the
\emph{internal form} in \textsc{Minlog} of our formula, and
\texttt{distr} is a name referring to it.  By typing \texttt{(pp
  distr)}, one can see the value of this variable.


\subsubsection*{Implementing the proof}
We now want to prove this formula with \textsc{Minlog}.  In order to
do this we clearly need to set the formula as our goal.

\subsubsection*{Setting the goal}
Typically, the goals in a proof will be numbered and the top goal will
be denoted by the number 1, preceded by a question mark.  To set
\texttt{distr} as our goal, we type:
\begin{verbatim}
(set-goal distr)
\end{verbatim}
\textsc{Minlog} will print:
\begin{verbatim}
; ?_1: (A -> B -> C) -> (A -> B) -> A -> C
>
\end{verbatim}


\subsubsection*{The proof}
We have seen in the sketch of the proof that the first step for
proving the tautology is to assume the antecedent of the implication
and turn the consequent into our new goal.  This is simply done by
writing:
\begin{verbatim}
(assume 1)
\end{verbatim}
Here the number \texttt{1} is needed in order to identify and name the 
hypothesis. \textsc{Minlog} will denote this hypothesis by \texttt{1}:
\begin{verbatim} 
; ok, we now have the new goal 
; ?_2: (A -> B) -> A -> C from
;   1:A -> B -> C
> 
\end{verbatim}
We repeat the assume command to decompose the implication in the 
new goal:
\begin{verbatim} 
(assume 2)
\end{verbatim}

\begin{verbatim} 
; ok, we now have the new goal 
; ?_3: A -> C from
;   1:A -> B -> C
;   2:A -> B
> 
\end{verbatim}
And we decompose the goal once more:
\begin{verbatim}
(assume 3)
\end{verbatim}

\begin{verbatim} 
; ok, we now have the new goal 
; ?_4: C from
;   1:A -> B -> C
;   2:A -> B
;   3:A
> 
\end{verbatim}
We now need to start using our assumptions.  As already mentioned, in
order to prove \texttt{C} it is enough to prove both \texttt{A} and
\texttt{B}, by assumption \texttt{1}.  Therefore we write: \sloppy
\texttt{(use 1)}.  This has the effect of splitting the goal in two
distinct subgoals (note how the subgoals are numbered):
\begin{verbatim}
(use 1)

; ok, ?_4 can be obtained from
; ?_6: B from
;   1:A -> B -> C
;   2:A -> B
;   3:A

; ?_5: A from
;   1:A -> B -> C
;   2:A -> B
;   3:A
> 
\end{verbatim}
Then we write:
\begin{verbatim}
(use 3)
 
; ok, ?_5 is proved.  The active goal now is
; ?_6: B from
;   1:A -> B -> C
;   2:A -> B
;   3:A
> 
\end{verbatim}
And conclude the proof by: 
\begin{verbatim} 
(use 2)

; ok, ?_6 can be obtained from
; ?_7: A from
;   1:A -> B -> C
;   2:A -> B
;   3:A
> 

(use 3)

; ok, ?_7 is proved.  Proof finished.
>
\end{verbatim}
To see a record of the complete proof, simply type
\texttt{(display-proof)}.  Another useful command is
\texttt{(display-proof-expr)}.  See the manual for a description of
the various \texttt{display} commands available in \textsc{Minlog}.

We observe that an alternative to using the \texttt{define} command at
the beginning of the proof and then separately setting the goal, would
be to directly set the formula one wants to prove as a goal, that is
writing \texttt{(set-goal (pf "(A -> B -> C) -> (A -> B) -> A ->
  C"))}.  Note also that the first three \texttt{assume} commands
could be replaced by only one, i.e., \texttt{(assume 1 2 3)}.  In
alternative to the last two \texttt{use} commands, we could have given
only one command: \texttt{(use-with 2 3)}, which amounts to applying a
cut to the premises 2 and 3.  A final remark is that in case of rather
complex proofs, it is convenient to name specific hypothesis, in place
of making use of bare numbers. One than can simply use the
\texttt{assume} commands, followed by the name of the assumption in
double quotes.

\begin{exercise}
  \label{Ex:3ab}
  Prove
  \begin{enumeratea}
  \item $A \to B \to A$,
  \item $(A \to B \to C) \to B \to A \to C$.
  \end{enumeratea}
\end{exercise}

\begin{exercise}
  \label{Ex:8abc}
  Prove (with $\lnot A$ defined to be $A \to \falsum$)
  \begin{enumeratea}
  \item $(A \to B) \to \neg B \to \neg A$,
  \item $\neg (A \to B) \to \neg B$,
  \item $\neg \neg (A \to B) \to \neg \neg A \to \neg \neg B$.
  \end{enumeratea}
\end{exercise}

Before starting to read the next section, it is advisable to consult
the reference manual for a compendium of the commands utilized in this
example.  It is worth noticing that in general these commands have a
wider applicability than their usage as now presented.


\subsection{A second example: classical logic}
\textsc{Minlog} implements minimal logic.  If we want to prove a
proposition which is true in classical logic but not in minimal logic,
we explicitly need to state and use principles which are classical in
nature.  In the following example we shall use Stability, which is
added to \textsc{Minlog} as a global assumption.  Roughly speaking, a
global assumption is a proposition which can be recalled at any time,
if needed, and whose proof does not concern us at the moment (hence it
can also be an assumption with no proof).  In order to check which
global assumptions we have at our disposal we type:
\texttt{(display-global-assumptions)}.  To check a particular global
assumption whose name we already know, we write \texttt{pp} (which is
short for \texttt{pretty-print}) followed by the name of the
assumption we want to check, e.g., \texttt{(pp "Stab-Log")}.  Of
course we can also introduce our own global assumptions and remove
them at any time (see the reference manual for the specific commands).

Stability is the logical law for which, for any proposition $A$,
$\lnot \lnot A \to A$ holds.  In \textsc{Minlog}, $\lnot A$ is defined
to be $A \to \falsum$, i.e., $A$ implies falsum.  Stability is
therefore the following proposition: $((A \to \falsum) \to
\falsum) \to A$.

Suppose we want to prove the tautology:
\begin{equation*}
  ((A \to B) \to A) \to A, 
\end{equation*}
which is known as \emph{Peirce formula}\index{Peirce formula}.  For
this second example, we will assume that the reader has prepared a
sketch of the proof, and we will only give an intuitive idea of the
proof, preferring to rather concentrate on the \textsc{Minlog}
interaction, which will be given in its complete form.
 
As in the previous example, we observe first of all that the goal is
an implication, hence we will assume its antecedent, $(A \to B) \to
A$, and try to prove its consequent, $A$.  Now classical logic comes
into play, because in order to prove $A$, we will assume that its
negation holds and try to get a contradiction from it.  This will be
achieved by use of Stability.  We further note that in order to make
the argument work, we will need at some stage to resort to another
global assumption, the principle of \inquotes{ex falso quodlibet}.
This principle allows one to conclude any formula from a proof of
falsum, i.e., it is the principle: $\falsum \to A$, for arbitrary
$A$.

We start by setting the goal and assuming the antecedent of the 
implication:
\begin{verbatim}
(add-predconst-name "A" "B" (make-arity))
(define peirce-formula  (pf "((A -> B) -> A) -> A"))
(set-goal peirce-formula)
(assume 1)
\end{verbatim}
We obtain:
\begin{verbatim}
; ok, we now have the new goal 
; ?_2: A from
;   1:(A -> B) -> A
> 
\end{verbatim}

We now apply Stability, which is stored in \textsc{Minlog} with the
name \texttt{Stab-Log}, so that the goal $A$ will be replaced by its
double negation: $(A \to \falsum) \to \falsum$.  Note that
$\falsum$ is called \texttt{bot} in \textsc{Minlog}.
\begin{verbatim}
(use "Stab-Log")

; ok, ?_2 can be obtained from
; ?_3: (A -> bot) -> bot from
;   1:(A -> B) -> A
> 
\end{verbatim}
Since this is an implication, we let:
\begin{verbatim}
(assume 2)

; ok, we now have the new goal 
; ?_4: bot from
;   1:(A -> B) -> A
;   2:A -> bot
> 
\end{verbatim}
We then use hypothesis 2 to replace the goal $\falsum$ by $A$.
\begin{verbatim}
(use 2)

; ok, ?_4 can be obtained from
; ?_5: A from
;   1:(A -> B) -> A
;   2:A -> bot
> 
\end{verbatim}
Also $A$ can be replaced by $A \to B$ by use of hypothesis 1.
Subsequently, we can assume the antecedent of the new goal, $A$, and
call it \inquotes{hypothesis 3}:
\begin{verbatim}
(use 1)

; ok, ?_5 can be obtained from
; ?_6: A -> B from
;   1:(A -> B) -> A
;   2:A -> bot
> 

(assume 3)

; ok, we now have the new goal 
; ?_7: B from
;   1:(A -> B) -> A
;   2:A -> bot
;   3:A
>
\end{verbatim}
Now we can make use of the principle of ex falso quodlibet: if we
want to prove $B$, we can instead prove falsum, since from falsum
anything follows, and in particular $B$.  Therefore our goal can be
updated to $\falsum$ by the following instance of \texttt{use}:

\begin{verbatim}
(use "Efq-Log")

; ok, ?_7 can be obtained from:
; ?_8: bot from
;   1:(A -> B) -> A
;   2:A -> bot
;   3:A
> 
\end{verbatim}
The next two steps are obvious.
\begin{verbatim}
(use 2)

; ok, ?_8 can be obtained from
; ?_9: A from
;   1:(A -> B) -> A
;   2:A -> bot
;   3:A
> 

(use 3)

; ok, ?_9 is proved.  Proof finished.
>
\end{verbatim}


\subsection{Conjunction}
To conclude this section on propositional logic, we give a short
example of a tautology which uses conjunction.  We want to prove
\begin{equation*}
  A \land B \to B \land A
\end{equation*}
We shall simply record the code of our \textsc{Minlog} proof, asking
the reader to check \textsc{Minlog}'s reply at each step. A few
comments will be added at the end.
\begin{verbatim}
(add-predconst-name "A" "B" (make-arity))
(set-goal (pf "A & B -> B & A"))
(assume 1)
(split)
(use 1)
(use 1)
\end{verbatim}
The command \texttt{(split)} operates on the goal if it is a 
conjunction and it has the effect of splitting it into its two 
components. The command \texttt{use} is utilized to 
obtain the left (respectively the right) conjunct in the 
assumption and \inquotes{\texttt{use}} it to derive the goal.

The reader is encouraged to try and prove other examples of 
tautologies.


\subsection{Searching for proofs in propositional logic}
\textsc{Minlog} allows for automatic proof search.  There are two
distinct facilities for performing an automatic search in
\textsc{Minlog}.  The first is given by the command \texttt{(prop)}
and exemplifies Hudelmaier-Dyckhoff's search for the case of minimal
propositional logic (see e.g.\ \citet{Hudelmaier89},
\citet{Dyckhoff92}).  The second is given by the command
\texttt{(search)} and allows to automatically find proofs also for
some quantified formulas; it will be treated later.

\texttt{prop} will first look for a proof in propositional minimal
logic.  If it fails to find a proof for the given proposition, it will
try with intuitionistic logic, by adding appropriate instances of
\inquotes{ex falso quodlibet}.  If this search also gives no positive
answer, it will try to find a proof in classical logic, by adding
appropriate instances of Stability.

To apply this search algorithm, one simply needs to type
\texttt{(prop)} after stating the goal or at any point of a proof from
which one guesses that (minimal) propositional logic would suffice.
If \textsc{Minlog} finds a proof, one can then display it by means of
any of the display commands available for proofs; for example by
writing \texttt{dnp} (which is a shortcut for
\texttt{display-normalized-proof}).

The reader is encouraged to apply the command to the first examples of
propositional logic of this tutorial, including \inquotes{Peirce's
  law}.


\section{Predicate logic}
% Every total relation which is symmetric and transitive is reflexive.
% Drinker formula, using \texttt{(Inhab alpha)} instead of a free
% variable.

\subsection{A first example} 
We now exemplify how to prove a statement in predicate logic.

Suppose we want to prove that every total relation which is symmetric
and transitive is reflexive.  For simplicity we shall work with
natural numbers.  We hence want to prove the following statement:
\begin{align*} 
        &\forall_{n,m}(R n m \to R m n) \land
        \forall_{n,m,k} (R n m \land R m k \to R n k) \to{}
        \\
        &\forall_{n}(\ex_{m} R n m \to R n n),
\end{align*}
where $n$, $m$, $k$ vary on natural numbers, while $R$ is a binary
predicate on natural numbers.

Before starting to prove the claim, we observe that we can
equivalently express it by another formula which is simpler to prove
in \textsc{Minlog}, e.g., by one in which the conjunctions have been
replaced by appropriate implications.  That is, we can instead prove
the following formula:
\begin{align*} 
        &\forall_{n,m}(R n m \to R m n) \to
        \forall_{n,m,k} (R n m \to R m k \to R n k) \to{}
        \\
        &\forall_{n,m}(R n m \to R n n).
\end{align*}
The strategy of first simplifying the goal may in some cases
considerably reduces the amount of time needed to prove a statement.
However, there might be cases in which one prefers to prove a more
complex formula, for example when proving a lemma which is then used
in the proof of a more intricate theorem.  For completeness and for a
comparison, we shall also record a proof of the original goal, at the
end of this section.

Since the predicate $R$ is required to vary on natural numbers, we
first of all load a file, already available with the distribution,
which introduces the algebra of natural numbers and some operations on
them, like for example addition.  This is obtained by typing:
\begin{verbatim}
(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)
\end{verbatim}
Here the \texttt{COMMENT-FLAG} is temporarily set to \texttt{\#f}
to suppress unwanted comments while loading the file.

We can now introduce the constant $R$. We also want to facilitate our
work a bit further and separately introduce the two assumptions
$\forall_{n,m}(R n m \to R m n)$ and $\forall_{n,m,k}(R n m \to R m k
\to R n k)$.  We do this by means of a \texttt{define} command, which
enables us to give a name to each assumption. We then use these name
to make a formula in implication form.

In the following \texttt{py} is the analogous for types of the
function parse formula.  Note also that the file \texttt{nat.scm}
already introduces $m$, $n$ and $k$ as \inquotes{default} variables on
the natural numbers, hence we do not need to explicitly declare them
here, too.
\begin{verbatim}
(add-predconst-name "R" (make-arity (py "nat") (py "nat")))
(define Symm (pf "all n,m(R n m  -> R m n)"))
(define Tran (pf "all n,m,k(R n m -> R m k -> R n k)"))
\end{verbatim}

We now state the goal:
\begin{verbatim}
(set-goal (mk-imp Symm Tran (pf "all n,m(R n m -> R n n)")))

; ?_1: all n,m(R n m -> R m n) 
       -> all n,m,k(R n m -> R m k -> R n k) 
       -> all n,m(R n m -> R n n)
> 
\end{verbatim}
Note that in this specific case, we could have directly written the
two formulas as antecedents of the implication, avoiding the detour
through a \texttt{define} command.  In case of more complex formulas,
however, or when we need to use the same formulas for various proofs
through one session, this strategy can be quite useful.

We now observe that the goal is an implication, so that the first step
would be to write \texttt{(assume "Symm" "Tran")}.  By this command we
would obtain a universally quantified formula and we would then need
to proceed to eliminate the quantifiers.  This can be accomplished by
another \texttt{assume} command in which we specify two natural
numbers.  For simplicity we here fix the natural numbers $n$ and $m$.
So we would write \texttt{(assume "n" "m")}.  This would produce an
implication which would also need to be eliminate by another
\texttt{assume} command, say \texttt{(assume 1)}.  We can put all
these commands together by writing:
\begin{verbatim} 
(assume "Symm" "Tran" "n" "m" 1)

; ok, we now have the new goal 
; ?_2: R n n from
;   Symm:all n,m(R n m -> R m n)
;   Tran:all n,m,k(R n m -> R m k -> R n k)
;   n  m  3:R n m
> 
\end{verbatim}
The next move is to make use of our assumptions.  It is clear that if
we take $k$ to be $n$ in \texttt{Tran}, then the goal can be obtained
by an instance of \texttt{Symm}, and the proof is easily completed.
We here utilize \texttt{use} by additionally providing a term,
\texttt{"m"}, which will instantiate the only variable which can not
be automatically inferred by unification.  In the following
\texttt{pt} stands for parse term.
\begin{verbatim} 
(use "Tran" (pt "m"))

; ?_4: R m n from
;   Symm:all n,m(R n m -> R m n)
;   Tran:all n,m,k(R n m -> R m k -> R n k)
;   n  m  3:R n m

; ?_3: R n m from
;   Symm:all n,m(R n m -> R m n)
;   Tran:all n,m,k(R n m -> R m k -> R n k)
;   n  m  3:R n m
>
\end{verbatim}
The \texttt{use} command has the effect of replacing the current goal
with two new goals.  These are obtained from \texttt{Tran} by
instantiating the quantifiers with \texttt{n}, \texttt{m} and
\texttt{n} (the two \texttt{n} being inferred by unification) and then
by replacing the goal with the antecedents of the resulting instance
of \texttt{Tran}.

We can now write:
\begin{verbatim}
(use 3)

> ; ok, ?_3 is proved.  The active goal now is
; ?_4: R m n from
;   Symm:all n,m(R n m -> R m n)
;   Tran:all n,m,k(R n m -> R m k -> R n k)
;   n  m  3:R n m
>
\end{verbatim}
We finally employ \texttt{Symm} and another \texttt{use}:
\begin{verbatim} 
(use "Symm")

; ok, ?_4 can be obtained from
; ?_5: R n m from
;   Symm:all n,m(R n m -> R m n)
;   Tran:all n,m,k(R n m -> R m k -> R n k)
;   n  m  3:R n m
> 

(use 3)

; ok, ?_5 is proved.  Proof finished.
> 
\end{verbatim}


\begin{exercise}
  \label{Ex:3cd}
  Prove
  \begin{enumeratea}
  \item $\forall_{x} \forall_{y} A \to \forall_{y} \forall_{x} A$,
  \item $\forall_{x} \forall_{y} A(x,y) \to \forall_{x} A(x,x)$.
  \end{enumeratea}
\end{exercise}


\subsection{The same example}
We here present a \textsc{Minlog} proof of the original goal of the
previous example, as it allows us to exemplify the use of some new
commands.  We shall leave the proof uncommented and make a few remarks
at the end.  The reader will have to examine the proof and check
\textsc{Minlog}'s interaction.
\begin{verbatim}
(add-predconst-name "R" (make-arity (py "nat") (py "nat")))
(set-goal (pf "all n,m(R n m  -> R m n) &
               all n,m,k(R n m & R m k -> R n k) ->
               all n(ex m R n m -> R n n)"))
(assume 1)
(inst-with 1 'left)
(inst-with 1 'right)
(drop 1)
(name-hyp 2 "Symm")
(name-hyp 3 "Tran")
(assume "n" 4)
(ex-elim 4)
(assume "m" 5)
(cut (pf "R m n"))
(assume 6)
(use-with 3 (pt "n") (pt "m") (pt "n") "?")
(drop "Symm" "Tran" 4)
(split)
(use 5)
(use 6)
(use-with "Symm" (pt "n") (pt "m") 5)
\end{verbatim}

The \texttt{use-with} command is similar to the \texttt{use} command,
but when applied to a universal quantifier it requires to explicitly
specify the terms one wants to instantiate.  In its first occurrence
in the proof above we write \texttt{"?"} to indicate that
\textsc{Minlog} will have to replace the current goal with a new goal.
In the second occurrence of \texttt{use-with}, \textsc{Minlog} will
instantiate as specified the universal quantifiers in premise 2 and
then use hypothesis 5 to prove the goal.

The command \texttt{inst-with} is analogous to \texttt{use-with}, but
operates for forward reasoning; hence it allows one to simplify the
hypothesis, instead of the conclusion.  In this case,
\texttt{(inst-with 1 'left)} has the effect of producing the left
component of the conjunction which constitutes the first hypothesis.
Similarly for the right component.

\texttt{ex-elim} eliminates an existential quantifier and produces a
new universally quantified goal.

As to \texttt{cut}, this command enables one to introduce new goals.
\texttt{(cut A)} has the effect of replacing goal $B$ by two new
goals, $A \to B$ and $A$.

In the proof above we have also made use of the commands \texttt{drop}
and \texttt{name-hyp}. The first allows one to remove one or more
hypothesis from the present context, to make the proof more readable.
In fact, it simply replaces the current goal with another goal in
which the hypothesis \inquotes{dropped} are not displayed anymore (but
they are not removed in general, as should be clear from the example
above).  The second command has similar \inquotes{cosmetic} purposes,
and allows one to rename a specific hypothesis and hence to work with
names given by the user instead of numbers produced by default.  Both
these commands result especially useful in the case of long and
intricate proofs.


\subsection{Another example with classical logic}
We conclude this section on predicate logic with a final example of a
formula which requires classical logic.  We want to prove the
following:
\begin{equation*}
  \excl_x(Q x \to \forall_y Q y),
\end{equation*}
where $Q$ is now a unary predicate, and we do not require $Q$ to range
on the natural numbers.  In addition, the existential quantifier,
$\excl$, is here a classical existential quantifier, to be
distinguished from the existential quantifier we encountered in the
previous example.  A classical quantifier $\excl_x$ is nothing more
than an abbreviation for $\lnot \forall_x \lnot$.

The formula we want to prove is known as the \inquotes{drinker}
formula, as it says something like: \inquotes{in a bar, there is a
  person such that if this person drinks then everybody drinks}.

One could state the goal either by direct use of the classical
existential quantifier (called \texttt{excl} in \textsc{Minlog}) or by
replacing it with its meaning by use of the universal quantifier.  In
the first case one would write:
\begin{verbatim}
(set-goal (pf "excl x(Q x -> all y Q y)"))
\end{verbatim}
\textsc{Minlog} would then automatically replace the \texttt{excl}
quantifier by its meaning when performing the first command.

Otherwise we can state the formula as follows:
\begin{verbatim}
(set-goal (pf "all x((Q x -> all y Q y) -> bot) -> bot"))
\end{verbatim}

In our implementation we shall introduce $Q$ as a predicate on an
arbitrary type, say $\alpha$.  \textsc{Minlog} already has a type
variable \texttt{alpha} as default, and we shall use it in the
following (hence no declaration of the type \texttt{alpha} is needed).

In the proof we need to provide a particular term of type
\texttt{alpha}, to instantiate the generalized variable \texttt{x} in
the premise.  However, since we do not know anything about the type
\texttt{alpha}, we provide such an instance as a \inquotes{canonical
  inhabitant}\index{inhabitant!canonical} of type \texttt{alpha},
written as \texttt{(Inhab alpha)}.  When we later instantiate the type
variable \texttt{alpha} by say \texttt{nat}, we can provide a canonical
inhabitant of type \texttt{nat} by a computation rule
\begin{equation*}
  \hbox{\texttt{(Inhab nat) $\mapsto$ $0$}}
\end{equation*}
As otherwise the proof is quite simple and does not introduce any
further new notion, we only write the code, letting the reader verify
it in \textsc{Minlog}.
\begin{verbatim}
(add-predconst-name "Q" (make-arity (py "alpha")))
(add-var-name "x" "y" (py "alpha"))

(set-goal (pf "all x((Q x -> all y Q y) -> bot) -> bot"))
(assume 1)
(use 1 (pt "(Inhab alpha)"))
(assume 2 "x")
(use "Stab-Log") 
(assume 3)
(use 1 (pt "x"))
(assume 4)
(use "Efq-Log")
(use-with 3 4)
\end{verbatim}
We can store the proof as a theorem to be used later on with the
command:
\begin{verbatim}
(save "Drinker")
\end{verbatim}


\section{Solutions to the exercises}
For exercise~\eqref{Ex:3ab} possible solutions are
\begin{verbatim}
(set-goal (pf "A -> B -> A"))
(assume "u" "v")
(use "u")
\end{verbatim}
  and
\begin{verbatim}
(set-goal (pf "(A -> B -> C) -> B -> A -> C"))
(assume "u" "v" "w")
(use "u")
(use "w")
(use "v")
\end{verbatim}

For exercise~\eqref{Ex:8abc} possible solutions are
\begin{verbatim}
(set-goal (pf "(A -> B) -> (B -> bot) -> A -> bot"))
(assume "u" "v" "w")
(use "v")
(use "u")
(use "w")
\end{verbatim}
and
\begin{verbatim}
(set-goal (pf "((A -> B) -> bot) -> B -> bot"))
(assume "u" "v")
(use "u")
(assume "w")
(use "v")
\end{verbatim}
and
\begin{verbatim}
(set-goal (pf "(((A -> B) -> bot) -> bot) ->
               ((A -> bot) -> bot) -> ((B -> bot) -> bot)"))
(assume "u" "v" "w")
(prop)
\end{verbatim}

For exercise~\eqref{Ex:3cd} possible solutions are
\begin{verbatim}
(add-pvar-name "R" (make-arity (py "alpha") (py "alpha")))
(add-var-name "x" "y" (py "alpha"))

(set-goal (pf "all x,y R x y -> all y,x R x y"))
(assume "u" "y" "x")
(use "u")
\end{verbatim}
and
\begin{verbatim}
(set-goal (pf "all x,y R x y -> all x R x x"))
(assume "u" "x")
(use "u")
\end{verbatim}

\section{Useful Commands for \textsc{Emacs} and Petite \textsc{Scheme}}

\subsection{Emacs}
\begin{itemize}
\item Start \textsc{Emacs}: \texttt{emacs \&}
\item Leave \textsc{Emacs}: \texttt{C-x C-c}   
\item Split a window in two: \texttt{C-x 2}
\item Move to another buffer: \texttt{C-x b} 
  (then specify the buffer's name)
\item Move to another window: \texttt{C-x o}
\item Load a file: \texttt{C-x C-f} 
  (then give a name of a file with extension \texttt{.scm})
\item Save a file: \texttt{C-x C-s}
\item Exit from the Minibuffer: \texttt{C-g}
\end{itemize}


\subsection{Scheme}
\begin{itemize}
\item Load  \textsc{(Petite) Scheme}:  \texttt{M-x run-petite}
\item Evaluate a \textsc{Scheme} expression: \texttt{C-x C-e}
\item Evaluate a region: mark the region and then \texttt{C-c C-r}
\item Kill a process: \texttt{C-c C-c} 
\item Leave the debug: \texttt{r}
\item End a \textsc{Scheme} session: \texttt{(exit)}
\item Comment: \texttt{;}
\end{itemize}

\begin{enumerate}[]
\item \texttt{C = Control} or \texttt{Strg}
\item \texttt{M = Meta} or \texttt{Esc} or \texttt{Alt}.  
\end{enumerate}


\bibliographystyle{abbrvnat}
\bibliography{a-z,temp}
\printindex
\end{document}


\subsection{Induction}
\subsubsection*{To do}
General induction.


\subsubsection*{Induction on the natural numbers.} We now present a
simple proof which exemplifies the use of induction on the natural
numbers.  The formula to prove is the following:
\begin{equation*}
  \forall_{n,m}(n + m = m + n).
\end{equation*}
This can be proved by induction on the natural numbers as follows: we
fix an $n$ and show that $n + 0 = 0 + n$ and also that if $n + m = m +
n$ then $n + \suc(m) = \suc(m) + n$.

As before we will make use of a file already available in the
distribution which contains the definitions of the algebra of the
natural numbers and also of the operations of addition and
multiplication on the natural numbers.  These are defined by means of
computation and rewrite rules.  If the file is not already
loaded\footnote{It is a good practice to run a new \textsc{Minlog}
  session when loading new files which could turn out to be
  incompatible with previously loaded files or previous definitions.},
we type:
\begin{verbatim}
(load "~/minlog/init.scm")
(set! DOT-NOTATION #f)

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)
\end{verbatim}

We set the goal by letting:
\begin{verbatim}
(set-goal (pf "all n,m n+m=m+n"))
\end{verbatim}

We now instantiate the first quantifier with \texttt{n}:
\begin{verbatim}
(assume "n")

; ok, we now have the new goal 
; ?_2: all m n+m=m+n from
;   n
> 
\end{verbatim}
We apply induction by simply typing:
\begin{verbatim}
(ind)
\end{verbatim}
The command \texttt{ind} requires a universally quantified goal and
applies induction to it in accord to the definition of the specific
algebra type (in this case $nat$).  \textsc{Minlog}'s reply will be
something like this:
\begin{verbatim} 
; ok, ?_2 can be obtained from
; ?_4: all n1280(n+n1280=n1280+n -> n+Succ n1280=Succ n1280+n) from
;   n  m1278

; ?_3: n+0=0+n from
;   n  m1278
> 
\end{verbatim}
We then replace the goal with its normal form by letting:
\begin{verbatim}
(normalize-goal) 

; ok, the normalized goal is
; ?_5: T from
;   n  m1278
>      
\end{verbatim}
The latter command can be abbreviated with \texttt{ng} and it will
normalize the goal by using the computation rules for \texttt{+}
introduced in the file \texttt{nat.scm}.

The goal is now proved by simply appealing to the axiom
\texttt{Truth-Axiom} (which can be used as an argument to the
\texttt{use} command).

\begin{verbatim}
(use "Truth-Axiom")

; ok, ?_5 is proved.  The active goal now is
; ?_4: all n1280(n+n1280=n1280+n -> n+Succ n1280=Succ n1280+n) from
;   n  m1278
> 
\end{verbatim}
We can now instantiate the quantified variable \texttt{n1280} by
\texttt{m}:
\begin{verbatim}
(assume "m" 1)

; ok, we now have the new goal 
; ?_6: n+Succ m=Succ m+n from
;   n  m1278  m  1:n+m=m+n
> 
\end{verbatim}
Finally we normalize the goal and use the assumption:
\begin{verbatim}
(ng) 

; ok, the normalized goal is
; ?_7: n+m=m+n from
;   n  m1278  m  1:n+m=m+n
> 
\end{verbatim}

\begin{verbatim}
(use 1)
; ok, ?_7 is proved.  Proof finished.
>
\end{verbatim}

To see the proof:
\begin{verbatim}
(display-proof)
\end{verbatim}


\subsubsection*{Another example} 
We now present another example of induction on the natural numbers,
which introduces some additional features of \textsc{Minlog}.

Suppose we want to prove that for all natural numbers $n$, $2 \cdot n$
is even.  We define two new \emph{program constants} \texttt{Odd} and
\texttt{Even} which take a natural number as argument and give a
boolean (true or false) as output.  The behaviour of these program
constants can be specified by means of \emph{computation rules}.  In
this case the computation rules will simultaneously characterize
\texttt{Odd} and \texttt{Even}.  The command used to introduce a new
program constant is \texttt{add-program-constant}.  It will require
the name of the constant and its type; further arguments may be the
degree of totality, the token type (e.g., \texttt{const}) and the
arity.  In the following, the type of the new constants \texttt{Odd}
and \texttt{Even} will be introduced by means of the command
\texttt{mk-arrow}, which produces an arrow type.

The behaviour of a new program constant can be specified by
introducing one or more computation rules for it.  This is
accomplished by use of the command \texttt{add-computation-rule},
having two arguments: a left hand side and a right hand side.  The
right hand side specifies the result of the computation rule for the
argument indicated in the left hand side.

The following implementation of the example should clarify how to use
these commands.
\begin{verbatim}
(add-program-constant
  "Odd" (mk-arrow (py "nat") (py "boole")) t-deg-one)
(add-program-constant
  "Even" (mk-arrow (py "nat") (py "boole")) t-deg-one)
(add-computation-rule (pt "Odd 0") (pt "False")) 
(add-computation-rule (pt "Even 0") (pt "True")) 
(add-computation-rule (pt "Odd(Succ n)") (pt "Even n"))
(add-computation-rule (pt "Even(Succ n)") (pt "Odd n"))

(set-goal (pf "all n Even(2*n)"))
(ind)
(ng)
(use "Truth-Axiom")
(ng)
(assume "n" 1)
(use 1)
\end{verbatim}


\subsubsection*{Induction on lists}
The following example is an exercise on lists over an arbitrary type
$\alpha$.  Also this example illustrates the use of induction, but
since we now deal with \emph{infinitary algebras} (see the reference
manual) the task will result a bit harder than when working with the
natural numbers.

Together with the file \texttt{nat.scm}, we now need to load also the
file \texttt{list.scm}, which contains basic definitions and
operations on lists over an arbitrary type $\alpha$.  We recommend to
go through the file before starting to work at this example.

We shall introduce a function, $\listrev$, on lists which has the
effect of reverting a list, and then prove the following:
\begin{equation*}
  \forall_{y,z}(\Eq(\listrev(y \listappend z)) 
  ((\listrev\, z) \listappend (\listrev\, y))),
\end{equation*}
where $y$ and $z$ are lists over an arbitrary type $\alpha$ and
$\listappend$ denotes the append function on lists as defined in
\texttt{list.scm}.  Note that we here need to use the predicate
$Equal$ instead of $=$ because the algebra of lists over $\alpha$ is
possibly an infinitary algebra and hence equality for it has to be
treated as a predicate constant with appropriate axioms (see the
reference manual).

Before stating the goal we need to define $\listrev$.  This has to be
defined by induction, by first giving its value for the empty list and
then saying how it applies to a non-empty list.  The two defining
conditions for $\listrev$ will be the following:
\begin{align*}
  &\listrev\,(\nil\, \alpha) = (\nil\, \alpha),
  \\
  &\listrev\,(a::y) = (\listrev\, y) \listappend (a{:})
\end{align*}
where, according to the notation in \texttt{list.scm}, $(\nil\,
\alpha)$ denotes the empty list over the type $\alpha$, $a::y$ denotes
the list obtained by adding the object $a$ of type $\alpha$ to the
list $y$ (over $\alpha$), while $a{:}$ is the one element list
obtained from $a$.

First of all we load the file \texttt{list.scm}.
\begin{verbatim}
(set! COMMENT-FLAG #f)
(libload "list.scm")
(set! COMMENT-FLAG #t)
\end{verbatim}

To simplify our work, we declare some variables of the appropriate
types:
\begin{verbatim}
(add-var-name "a" "b" (py "alpha"))
(add-var-name "u" "v" "w" "s" (py "list alpha"))
\end{verbatim}
We then declare a new program constant, \texttt{Rev}, which takes a
list over \texttt{alpha} as argument and gives another list over
\texttt{alpha} as output.
\begin{verbatim}
(add-program-constant 
  "Rev" (py "list alpha => list alpha") t-deg-one 'const 1)
\end{verbatim}

We can now introduce two computation rules which correspond to the two
conditions for $\listrev$ presented above.
\begin{verbatim}
(add-computation-rule (pt "(Rev alpha)(Nil alpha)") 
                      (pt "(Nil alpha)"))
(add-computation-rule (pt "(Rev alpha)(a::w)") 
                      (pt "((Rev alpha)w):+:(a:)"))
\end{verbatim}
Now we could start proving the goal:
\begin{verbatim}
all w,s Equal((Rev alpha)(w:+:s)) 
             (((Rev alpha)s):+:((Rev alpha) w)))
\end{verbatim}
With the purpose of simplifying our proof, we now deliberately
introduce three \inquotes{ad hoc} global assumptions which will be
used as lemmata in the proof of the main goal.  We prove one of these
global assumptions at the end of the main proof, and leave the others
as an exercise for the reader.

\begin{verbatim}
(add-global-assumption
 "Reff" (pf "all a,w,s(Equal w s -> Equal(a::w)(a::s))"))

(add-global-assumption
 "Eqrev" (pf "all w,s,u(Equal w s -> Equal(w:+:u)(s:+:u))"))

(add-global-assumption
 "Asrev" (pf "all v,s,w,u(Equal v((s:+:w):+:u) ->
                          Equal v(s:+:(w:+:u)))"))
\end{verbatim}
We now prove a short lemma which says that any list, $z$, is equal to
the list obtained by appending the empty list to $z$.
\begin{verbatim}
; Lemma
(set-goal (pf "all s Equal s(s:+:(Nil alpha))"))
(ind)
(ng)
(use "Eq-Refl")
(assume "a" "w" 1)
(use "Reff")
(use 1)
(save "AppendEmpty")
\end{verbatim}
We note that by writing \texttt{(use "Eq-Refl")}, we make use of the
axiom of reflexivity for \texttt{Equal}.  The lemma and the global
assumptions stated above can now be used to prove the goal.
\begin{verbatim}
(set-goal
 (pf "all w,s Equal((Rev alpha)(w:+:s))
                   ((Rev alpha)s:+:(Rev alpha)w)"))
(ind)
(ng)
(assume "s")
(use "AppendEmpty")
(assume "a" "w")
(ng)
(assume 1 "s")
(use "Asrev")
(use "Eqrev")
(use 1)
\end{verbatim}
Finally, we show how to prove the global assumption \texttt{Eqrev}, as
it is a typical application of equality reasoning.

\begin{verbatim} 
(set-goal (pf "all w,s,u(Equal w s ->
                         Equal(w:+:u)(s:+:u))"))
(strip)
(simp 1)
(use "Eq-Refl")
\end{verbatim}
Note the command \texttt{strip} which moves at one time all
universally quantified variables and hypotheses of the current goal
into the context.

\texttt{simp} simplifies a proof which involves the predicate
\texttt{Equal}, by substituting \inquotes{Equal} terms in the goal.


\section{Search}
The command \texttt{(search)} embodies a search algorithm based on
\citet{Miller91b} and ideas of Berger (see the \textsc{Minlog}
reference manual or \citet{Schwichtenberg04} for details on the
algorithm and for some differences with Miller's algorithm).  The
command \texttt{search} enables us to automatically find a proof for a
wider class of formulas compared with \texttt{prop}, since it also
works for formulae with quantifiers (see the reference manual for a
detailed description of the class of formulae dealt with by
\texttt{search}).

\subsubsection*{Search}
The \texttt{search} command is more powerful then \texttt{prop} since
it allows us to automatically find proofs also for some quantified
formulas, but it only operates a search in minimal logic. If one wants
to apply this command to a classical formula like \inquotes{Peirce's
  law}, one could for example add the appropriate instance of
\inquotes{ex falso quodlibet} and of Stability as antecedents of the
goal.  In case of more complex proofs, in which one can not easily
modify the actual goal, an alternative would be to avail oneself of a
more complete use of the \texttt{search} command which allows us to
specify some global assumptions or theorems or even hypothesis from
the given context which one would like to be used in the resulting
proof.\footnote{It is important to notice that in \textsc{Minlog} we
  do not quantify over propositions, hence one needs to exercise some
  care in choosing the global assumptions to be used in
  \texttt{search}.  In the case of \inquotes{Peirce's law}, one would
  need to pass e.g.\ from the global assumption \texttt{Efq-Log} to a
  theorem which is a specific instance of it, and make use of the
  latter in \texttt{search}.}  Since the search space in the case of
quantified formulas can become really vast, this possibility of
declaring specific assumptions to be used in the proof can be very
useful, especially if we also state the maximum number of
multiplicities we allow for each assumption (i.e., the maximum number
of times each assumption can be used in the proof).  One can also use
this same device to exclude the use of a specific assumption in the
proof, simply by letting its multiplicity to be $0$.

To use the plain version of \texttt{search}, one simply writes
\texttt{(search)}.  See the reference manual for the precise syntax of
the command \texttt{search} when other assumptions are invoked with
the respective multiplicities.

\subsubsection*{An example with \texttt{search}}
As an example for the use of \texttt{search}, we apply the algorithm
to the following problem: if $f$ is a continuous function then $f$
composed with itself is also a continuous function.  We suggest to
solve the problem as follows.
\begin{verbatim}
(add-var-name "x" "y" (py "alpha"))
(add-tvar-name "beta")
(add-var-name "U" "V" "W" (py "beta"))
(add-predconst-name
  "in" (make-arity (py "alpha") (py "beta")))
(add-var-name "f" (py "alpha=>alpha"))

(set-goal
 (pf "all f(
 all x,V(in(f x)V -> 
         excl U(in x U & all y(in y U -> in(f y)V))) -> 
 all x,W(in(f(f x))W -> 
         excl U(in x U & all y(in y U -> in(f(f y))W))))"))
(search)
(dnp)
\end{verbatim}
Note that one can switch on a verbose form of search by letting: 
\texttt{(set! VERBOSE-SEARCH \#t)}
before calling \texttt{search}. In this way one can see the single
steps performed by the search algorithm and detect possible
difficulties in finding a proof.


\section{Inductively defined predicates}
One of the main tools for developments in \textsc{Minlog}
is to use inductively defined sets.  For the theory and some
comments on the implementation see \citet{Seisenberger03}.

\subsection{Examples}
Transitive closure: Let $\prec$ be a binary relation.  The
\emph{transitive closure}%
\index{transitive closure} of $\prec$ is inductively defined as
follows.  The introduction axioms are
\begin{align*}
  &\forall_{x,y}(x \prec y \to \TrCl(x,y)),
  \\
  &\forall_{x,y,z}(x \prec y \to \TrCl(y,z) \to \TrCl(x,z))
\end{align*}
and the elimination axiom is
\begin{equation*}
  \begin{split}
    \forall_{x, y} \bigl( \TrCl(x, y) \to {}
    &\forall_{x,y}
    (x \prec y \to A(x,y)) \to
    \\
    &\forall_{x,y,z}(x \prec y \to
    \TrCl(y,z) \to A(y,z) \to A(x,z)) \to
    \\
    &A(x, y) \bigr).
  \end{split}
\end{equation*}
In \textsc{Minlog} this definition is written as follows.  We first
need to declare \texttt{x} and $\texttt{y}$ as variables of a type
\texttt{alpha} and \texttt{R} as a predicate variable of arity
\texttt{(alpha alpha)}.
\begin{verbatim}
(load "~/minlog/init.scm")
(set! DOT-NOTATION #f)

(add-var-name "x" "y" "z" (py "alpha"))
(add-pvar-name "R" (make-arity (py "alpha") (py "alpha")))

(add-ids (list (list "TrCl" 
               (make-arity (py "alpha") (py "alpha"))
               "algTrCl"))
         '("all x,y(R x y -> TrCl x y)"
           "InitTrCl")
         '("all x,y,z(R x y -> TrCl y z -> TrCl x z)"
           "GenTrCl"))
\end{verbatim}


\section{Proof interpretations}
\subsection{Refined $A$-translation}
Based on \citet{BergerBuchholzSchwichtenberg02}.


\subsection{Dialectica interpretation}


\section{Computational content}


\subsection{The type of a formula}


\subsection{Realizability}


\subsection{Extracted terms}
For constructive proofs, as well as for weak existential proofs, using
the refined $A$-translation or Gödel's Dialectica interpretation.


\subsection{Uniformity, decoration of proofs}
Based on \citet{Berger93a, Berger05}.


\appendix

\section{Solutions to the exercises}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
