PAGE logic

BIBLIOGRAPHY

base: 		"http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/latest/vector/page.lgw",
peano:		"http:peano/latest/vector/page.lgw"

PREASSOCIATIVE  base:  bracket * end bracket,
		peano: peano zero,

		; - Proofs:
		; Section 4
		double rule prime mp,
		inference axiom prime a one,
		rule hypothesize,
		inference axiom prime a two,
		inference inference axiom prime a two,
		hypothetical rule prime mp,
		double inference inference axiom prime a two,
		double hypothetical rule prime mp,
		mendelson lemma one eight,
                inference mendelson lemma one eight,
                rule repetition,
		mendelson exercise one fourtyseven b,
		mendelson exercise one fourtyseven c,
		mendelson exercise one fourtyseven e,

		; Section 5
		mendelson lemma one eleven d, 			; Deduction example
		hypothetical inference axiom prime a one,
		hypothetical inference axiom prime a two,
		hypothetical inference inference axiom prime a two,
		hypothetical mendelson exercise one fourtyseven b,
		hypothetical mendelson exercise one fourtyseven c,
		mendelson lemma one eleven c,			; Double deduction example
		mendelson exercise one fourtyeight d,
		mendelson exercise one fourtyeight e,
		mendelson exercise one fourtyeight h,
                mendelson corollary one ten a,
                mendelson corollary one ten b,

		; Section 6
		inference axiom prime s one,
		inference inference axiom prime s one,
		inference axiom prime s two,
		hypothetical inference axiom prime s two,
		inference inference axiom prime s nine,
		rule induction,
							mendelson proposition three two a,
							mendelson proposition three two b,
		inference 				mendelson proposition three two b,
							mendelson proposition three two c,
		inference inference 			mendelson proposition three two c,
		hypothetical inference inference 	mendelson proposition three two c,
							mendelson proposition three two d,
		inference inference 			mendelson proposition three two d,
		hypothetical inference inference 	mendelson proposition three two d,
							mendelson proposition three two f,
							mendelson proposition three two f i,
							mendelson proposition three two f ii,
							mendelson proposition three two g,
							mendelson proposition three two g i,
							mendelson proposition three two g ii,
							mendelson proposition three two h,
							mendelson proposition three two h i,
							mendelson proposition three two h ii,

		; - Other:
		hypothesis,
		instance,
		conclusion
PREASSOCIATIVE  base:  * sub * end sub,
		peano: * peano var
PREASSOCIATIVE  base:  unicode start of text * end unicode text
PREASSOCIATIVE  base:  * bit nil
PREASSOCIATIVE  base:  * apply *
PREASSOCIATIVE  base:  * raw head,
		peano: * peano succ
PREASSOCIATIVE  base:  * times *,
		peano: * peano times *
PREASSOCIATIVE  base:  * plus *,
		peano: * peano plus *
PREASSOCIATIVE  base:  * term plus * end plus
POSTASSOCIATIVE base:  * raw pair *
POSTASSOCIATIVE base:  * comma *
PREASSOCIATIVE  base:  * boolean equal *,
		peano: * peano is *
PREASSOCIATIVE  base:  not *,
		peano: peano not *
PREASSOCIATIVE  base:  * and *,
		peano: * peano and *
PREASSOCIATIVE  base:  * or *,
		peano: * peano or *
PREASSOCIATIVE  peano: peano all * indeed *
POSTASSOCIATIVE base:  * macro imply *,
		peano: * peano imply *
POSTASSOCIATIVE base:  * guard *
PREASSOCIATIVE  base:  * select * else * end select
PREASSOCIATIVE  base:  lambda * dot *
PREASSOCIATIVE  base:  * init
PREASSOCIATIVE  base:  * at *,
		       * macro modus ponens *,
                       * macro first modus ponens * macro second modus ponens *,
		       * hypothetical macro modus ponens *,
		       * hypothetical macro first modus ponens * hypothetical macro second modus ponens *
POSTASSOCIATIVE base:  * infer *
PREASSOCIATIVE  base:  all * indeed *
POSTASSOCIATIVE base:  * rule plus *
POSTASSOCIATIVE base:  * cut *
PREASSOCIATIVE  base:  * proves *
PREASSOCIATIVE  base:  locally define * as * end line *,
		       line * hypothesis        modus ponens * modus ponens *                indeed * end line *,
		       line * hypothesis first  modus ponens * modus ponens *                indeed * end line *,
		       line * hypothesis second modus ponens * modus ponens *                indeed * end line *,
		       line * hypothesis double modus ponens * modus ponens * modus ponens * indeed * end line *,
		       line * hypothesis               indeed * end line *,
                       line * hypothesis because     * indeed * end line *,
		       line * hypothesis raw because * indeed * end line * 
POSTASSOCIATIVE base:  * then *
PREASSOCIATIVE  base:  * tab *
PREASSOCIATIVE  base:  * row *

BODY
"File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed
\renewenvironment{thebibliography}[1]
     {\list{\@biblabel{\@arabic\c@enumiv}}%
           {\settowidth\labelwidth{\@biblabel{#1}}%
            \leftmargin\labelwidth
            \advance\leftmargin\labelsep
            \@openbib@code
            \usecounter{enumiv}%
            \let\p@enumiv\@empty
            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
      \sloppy
      \clubpenalty4000
      \@clubpenalty \clubpenalty
      \widowpenalty4000%
      \sfcode`\.\@m}
     {\def\@noitemerr
       {\@latex@warning{Empty `thebibliography' environment}}%
      \endlist}
End of file
File page.tex
\documentclass [fleqn]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}

\usepackage{latexsym}
\usepackage[danish]{babel} % Danske betegnelser
\usepackage{lstdoc} % Kode listings
\usepackage{amssymb} % Ekstra matematik symboler, bl.a. \mathbb til maengder

% Lstlisting-settings                                                                                          
\definecolor{fillcolor}{rgb}{0.92,0.92,0.92}
\lstset{language=Caml,
  basicstyle=\ttfamily\tiny,
  stringstyle=\ttfamily\tiny,
  commentstyle=\ttfamily\tiny,
  identifierstyle=\ttfamily\tiny,
  keywordstyle=\ttfamily\tiny,
  stringstyle=\ttfamily\tiny,
  escapeinside={(*@}{@*)},
  numbers=left,
  numberstyle=\tiny,
  numbersep=5pt,
  showspaces=false,
  backgroundcolor=\color{fillcolor},
  classoffset=0,
  breaklines,
  extendedchars=true
}
\renewcommand{\lstlistingname}{pyk-eksempel}

\newcommand{\includecode}[1]{
  \lstinputlisting[frame=single,caption={#1},label=code:#1]{#1}
}

\setlength{\parindent}{0em}
%\setlength{\parskip}{1ex}

% The font of each Logiweb construct is under tight control except that
% strings are typeset in whatever font is in effect at the time of
% typesetting. This is done to enhance the readability of strings in the
% TeX source generated by Logiweb. The default font for typesetting
% strings is \rm:
\everymath{\rm}

\usepackage{makeidx}
\usepackage{page}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
\newlength{\bracketwidth}
\settowidth{\bracketwidth}{$[{}$}
\newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}}

\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=Logic}
\hypersetup{colorlinks=true}
\bibliographystyle{plain}

% \tex{something} writes something to page.otx for later inclusion
\newwrite\outex
\newtoks\toktex
\immediate\openout\outex=page.otx
\newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}}

% \test{something} writes something to page.tst for later inclusion
\newwrite\outest
\immediate\openout\outest=page.tst
\newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}}

% Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344).
% \afterheading suppresses indentation once, c.f. latex.ltx.
% \display{something} displays something as a displayed equation except
% that linebreaking is possible and displaymath is not turned on by default.
% The first paragraph after \display{something} is unindented.
% Glue below formulas may be wrong. The definition of \display misses
% something like \addvspace{\belowdisplayskip}.
\catcode`\@=11
\def\afterheading{\@afterheading}
\catcode`\@=12
\newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}}
\item #1\end{list}

\afterheading}
\newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}}
\item #1\end{list}

\afterheading}

\begin{document}
\title{Logik}
\author {Allan Hvam Petersen (220282-2137)}
\maketitle
\tableofcontents
"[ ragged right expansion ]"

\section{Forord}

Denne rapport er resultatet af et projektarbejde i kurset Logik p\aa{} K\o{}benhavns Universitet, udarbejdet i perioden 2. juni til 4. juli af Allan Hvam Petersen. Form\aa{}let med opgaven er at skrive et maskinchecket bevis i systemet Logiweb, som dermed danner grundlag for den resulterende karakter i kurset. L\ae{}seren af denne rapport b\o{}r v\ae{}re bekendt med dele af Logiweb-systemet samt, \LaTeX{} og have en matematisk grundforst\aa{}else. Hvis man fra andre Logiweb-sider \o{}nsker at referer til denne, kan f\o{}lgende kana-reference eller URL benyttes:

\display{\lgwLogicKana{}}

\display{\scriptsize{http://www.diku.dk/~grue/logiweb/20050502/home/ahvam/logic/latest/vector/page.lgw}}

Rapporten er inddelt i f\o{}lgende afsnit:

\begin{description}
  \item[Sammenfatning] Beskrivelse af projektforl\o{}bet, samt vurdering af l\o{}sningen.
  \item[Introduktion] Introduktion af opgaven og teknologi.
  \item[Propositions teorien] Opbygning af simple beviser.
  \item[Deduktion] Beskriver overs\ae{}ttelse af beviser p\aa{} Mendelson-form med hypoteser til beviser p\aa{} Logiweb-form, desuden definere afsnittet egne konstruktioner til beviser med hypoteser.
  \item[Peano Aritmetik] Beviser indenfor peano aritmetik.
\end{description}

Bilag er inddelt som f\o{}lger:

\begin{description}
  \item[Diverse] Samling af diverse definitioner.
  \item[\TeX\ Definitioner] \TeX\ definitioner for alle konstruktioner i dokumentet.
  \item[Prioritets Tabel] Prioritets tabel med nye konstruktioner.
  \item[Litteratur] Litteratur liste.
\end{description}

\section{Sammenfatning}

Opgaven er l\o{}st, og bevist af s\ae{}tning "[ math mendelson proposition three two h end math ]" fra \cite{mendelson} er udf\o{}rt indenfor Logi\-web-systemet. Endvidere er beviset korrekt, forudsat bevis-checkeren p\aa{} basis-siden er korrekt. Det endelige bevis kan ses i afsnit \ref{ssec:peano_three_two_h}. Beviset af "[ math mendelson proposition three two h end math ]" har ikke koncentreret sig s\aa{} meget om kreativitet og finde p\aa{} selve beviset, snarer at f\aa{} kendskab til detaljerne i Logiweb. Logiweb og de referede Logiweb-sider har til tider b\aa{}ret lidt pr\ae{}g af at systemet/siderne ikke har v\ae{}ret helt gennemtestet, men det har dog ogs\aa{} haft sin charme og givet en ekstra uventede udfordringer.

Denne logiweb-side referer til den seneste version af Klaus Grues basis-side, samt en modificeret version af hans seneste peano-side. Den modificerede version kan findes under mine logiweb publikationer p\aa{} adressen \url{http://www.diku.dk/~grue/logiweb/20050502/home/ahvam/}. Fra den originale peano-side, er alle beviserne samt nogle konstruktioner blevet fjernet og et par \TeX{} fejl er blevet udbedret. \AE{}ndringerne er foretaget for at undg\aa{} tvetydigheder p\aa{} denne side.

Enkelte af beviserne i denne rapport er ikke bevist i \cite{mendelson}, udarbejdelsen af disse beviser har til tider v\ae{}ret s\ae{}rdeles tidskr\ae{}vende. Endvidere er beviserne holdt s\aa{} enkelte og korte som muligt, men der er sikkert nogle f\aa{} der kan udformes endnu mere enkelt.

I afsnit \ref{ssec:deduktion_new} bliver der introduceret en r\ae{}kke makrodefinitioner, man med fordel kan udnytte til hypotetiske beviser. Konstruktionerne har n\ae{}ppe sparet mig for tid, da opbygningen af disse har v\ae{}ret en tidskr\ae{}vende opgave. Dog har konstruktionerne vist sig yderst anvendelige, da beviserne er blevet nemmere at skrive efter indf\o{}relsen af de nye konstruktioner.

Mange af beviserne i rapporten er skrevet om adskillige gange, i f\o{}rste omgang blev beviserne frem til "[ math mendelson proposition three two g end math ]" skrevet. Men da dette bevis fyldte over en hel side, var det p\aa{} tide at indf\o{}re de navngivnings-standarder og abstraktioner beskrevet i afsnit \ref{ssec:standarder} (Eksempelvis opdeling af induktionsbeviser). Beviserne var herefter stadig l\ae{}ngere og mere komplekse end de tilsvarende i \cite{mendelson}, derfor besluttede jeg mig for at lave de f\o{}r beskrevne makrodefinitioner. L\o{}bende var der blevet udformet s\aa{}kaldte omd\o{}bnings-beviser, der tog h\o{}jde for variabelfangst (sammenfald af metavariabler) som bevis-checkeren ikke tog h\o{}jde for p\aa{} det tidspunkt. Efter en del forvirring p\aa{} logiweb-maillinglisten omkring variabelfangst, besluttede Klaus sig for at implementere en l\o{}sning p\aa{} basis-siden. Herefter skulle mange af beviserne endnu engang omskrives/omd\o{}bes. Tilsammen har disse \ae{}ndringer v\ae{}ret med til at h\o{}jne kvaliteten af beviserne.

\section{Introduktion}

\subsection{Opgaveformulering}

M\aa{}let med denne rapport, er i sin enkelthed at bevise formelt at naturlige tal ($\mathbb{N}$) under kompositionen addition er kommutativ:

\[ x+y=y+x \]

Beviset for dette findes allerede i Mendelson \cite{mendelson}, men skal derp\aa{} bevises i Logi\-web-\linebreak[0]systemet. Beviset skal udtrykkes i sproget \texttt{pyk}, hvortil der findes en \texttt{pyk}-\linebreak[0]overs\ae{}tter som kan overs\ae{}tte \texttt{pyk}-kildetekst til Logiweb-sider. \texttt{pyk}-over\-s\ae{}t\-teren og Logiweb vil v\ae{}re til r\aa{}dighed p\aa{} DIKU's f\o{}rstedel-system p\aa{} hosten \texttt{bach-0}.

For ikke at starte p\aa{} hel bar bund i Logiweb, er det tilladt at referer til Klaus Grues basis- samt peano-side. Disse sider kan findes p\aa{} DIKU's Logiweb installation p\aa{} adressen \url{http://www.diku.dk/~grue/logiweb/20050502/home/grue/}.

\subsection{Logiweb og Pyk}

Logiweb er et system til distribution af formel matematik, en side i Logiweb har flere forskellige synsvinkler/ansigter:

\begin{description}
  \item[vector] Et bin\ae{}rt format af siden.
  \item[biblopgraphy] En liste af referencer en side referer til.
  \item[body] Selve teksten p\aa{} siden.
  \item[expansion] Siden efter makroekspansion.
  \item[diagnose] Eventuelle fejlbeskeder fra siden.
  \item[] osv.
\end{description}

En Logiweb-side uden reference til andre kaldes en basis-side. P\aa{} basis-sider er der p\aa{} forh\aa{}nd kun pr\ae{}defineret et minimal antal af konstruktioner. Det er herefter op til sidens skribent, at definere og indf\o{}re betydninger og udseende af nye konstruktioner. En basis-side har desuden enkelte privilegier som andre sider ikke har, med hensyn til erkl\ae{}ring af nye symboler og bootstrapping. Opbygningen af en basis-side kan v\ae{}re et st\o{}rre arbejde, som Klaus Grue heldigvis har gjort for os. Hans basis-side definerer bl.a. tal, lister, makroekspansion, bevis-checker og et utal af andre konstruktioner samt operationer. Hvis man refererer til andre sider kan man 'arve' de konstruktioner, der er beskrevet p\aa{} den refererede side. 

Genereringen af en Logiweb-side sker via overs\ae{}ttelse af en \texttt{pyk}-kildetekst. Et eksempel p\aa{} skelettet for en s\aa{}dan tekst kan ses i pyk-eksempel \ref{code:body.pyk}. I eksemplet er n\o{}gleord skrevet med stort, og navne med lille.

\includecode{body.pyk}

Eksemplet viser at man f\o{}rst skal give sin side et navn, derefter erkl\ae{}re man referencer til andre sider. Efter referencerne kommer konstruktionerne, som henholdsvis defineres post- (venstre) eller pr\ae{}-associative (h\o{}jre). R\ae{}kkef\o{}lgen af konstruktionerne angiver prioritet, og stjerner angiver pladser til operanter. En prioritets tabel for alle konstruktioner i dette dokument kan ses i bilag \ref{sec:prioritets_tabel}. \texttt{BODY}-ordet angiver at selve sidens start, siden kan inddeles i flere filer som man tekstuelt p\aa{}begynder og afslutter med andre bestemte n\o{}gleord. Indholdet af en side skrives i \TeX{}, iblandt selve teksten kan der laves en bestemt \texttt{pyk} 'omgivelse', der giver instruktioner til \texttt{pyk}-overs\ae{}tteren om at den skal overs\ae{}tte indholdet af omgivelsen. Til sidst i \texttt{pyk}-filen angiver man kommandoer til overs\ae{}ttelse af \texttt{.tex}-filerne.

For at give et eksempel p\aa{} hvad der kan st\aa{} i en \texttt{pyk} 'omgivelse', er \texttt{pyk}-eksempel \ref{code:fac.pyk} der har tre definitioner, inkluderet:

\includecode{fac.pyk}

Eksempel \ref{code:fac.pyk} koncentrerer sig omkring definition af en fakultetsfunktion ($n!$). Desuden belyser eksemplet ogs\aa{}, at konstruktioner kan have flere forskellige aspekter. Alle konstruktioner b\o{}r have defineret hvorledes de udtrykkes i sproget \texttt{pyk} selv (Definition 1). \texttt{tex}-aspektet beskriver hvordan en konstruktion skal vises i \TeX{} (Definition 2), og \texttt{value}-aspektet definere hvordan 'v\ae{}rdien' af et udtryk skal udregnes (Definition 3). Alle \TeX{} definitioner introduceret i dette dokument kan ses i bilag \ref{sec:tex}. Konstruktioner kan have adskillige aspekter, men de tre fra eksemplet er de mest centrale. 

For en komplet gennemgang af Logiweb, \texttt{pyk}, basis-siden og bevissystemet, kan \cite{grue:base} ses. 

\section{Propositions teorien}
\label{sec:prop}

\subsection{Definition}
\label{ssec:prop_definition}

Propositions teorien som introduceret i \cite{mendelson}, har en r\ae{}kke grundelementer der skal v\ae{}re p\aa{} plads f\o{}r peano aritmetik kan p\aa{}begyndes. Det anvendte sprog i teorien er yderst simpelt: \\

$\cal{T}$ $\rightarrow{}$ $\cal{V}$ ; $"[ not meta t ]"$ ; $\cal{T} \Rightarrow{} \cal{T}$ \\
$\cal{V}$ $\rightarrow{}$ $x_1$ ; $x_2$ ; $...$ \\

Hvor $\cal{T}$ angiver termer og $\cal{V}$ angiver en m\ae{}ngde variabler. Teorien har f\o{}lgende aksiomer, hvor prikkerne over operatorerne b\o{}r ignoreres af l\ae{}seren idet det bliver forklaret i afsnit \ref{sec:peano}:

\display{$A1':$ "[ math all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end math ]"}

\display{$A2':$ "[ math all meta a indeed all meta b indeed all meta c indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end math ]"}

\display{$A3':$ "[ math all meta a indeed all meta b indeed parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end math ]"}

Samt en enkelt inferens regel:

\display{$MP':$ "[ math all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b end math ]"}

\subsection{Standarder}
\label{ssec:standarder}

Da der igennem rapporten vil blive introduceret et forholdsvis stort antal s\ae{}tninger, er der indf\o{}rt  f\o{}lgende standarder til navngivning:

\begin{description}
  \item[$\textit{navn}_{d}$] S\ae{}tningen har f\aa{}et tilf\o{}jet et ekstra 'argument', men har stadig den samme 'virkning'. Effekten heraf er ofte at s\ae{}tning virker som 'dobbelt' \textit{navn} (heraf \textit{d} for dobbelt).
  \item[$\textit{navn}_{i}$] En af de \o{}verste implikations-operatorer i \textit{navn}'s parse-tr\ae{} er erstattet af en inferens-operator (heraf \textit{i} for inferens). Anvendes n\aa{}r \textit{navn} \o{}nskes anvendt p\aa{} tv\ae{}rs af linjer, eller til at spare et antal bevislinjer med modus ponens.
  \item[$\textit{navn}_{h}$] Hypotetisk version af \textit{navn} (heraf \textit{h} for hypotetisk). Alle undertr\ae{}er til en inferens-operator (p\aa{} n\ae{}r de undertr\ae{}er hvor den principale operator selv er en inferens-operator) i \textit{navn}'s parse-tr\ae{} har f\aa{}et tilf\o{}jet $\cal{H} \Rightarrow{}$ \o{}verst.
\end{description}

\textit{navn} er her s\ae{}tningens oprindelige navn, endvidere kan disse endelser kombineres for dermed at danne mere komplekse s\ae{}tninger. Hvis der eksempelvis tages udgangspunkt i "[ math axiom prime a one end math ]", kan aksiomets parse-tr\ae{} ses p\aa{} figur \ref{fig:prime_a_one_parsetree}.

\begin{figure}[htbp]
\begin{center}
\begin{picture}(60, 60)
\put(12, 48){\framebox(12, 12){$\ \Rightarrow{}$}}
\put(0,  24){\framebox(12, 12){$\cal{A}$}}
\put(36, 24){\framebox(12, 12){$\ \Rightarrow{}$}}
\put(24,  0){\framebox(12, 12){$\cal{B}$}}
\put(48,  0){\framebox(12, 12){$\cal{A}$}}

\put(6,  36){\line(1,1){12}}
\put(42, 36){\line(-2,1){24}}
\put(30, 12){\line(1,1){12}}
\put(54, 12){\line(-1,1){12}}
\end{picture}
\end{center}
\caption{$A1'$}
\label{fig:prime_a_one_parsetree}
\end{figure}

"[ math inference axiom prime a one end math ]" kan ses p\aa{} figur \ref{fig:prime_a_one_i_parsetree}, det bem\ae{}rkes at en implikations-operator er blevet udskiftet. Desuden kan $A1'_{ih}$ ses p\aa{} figur \ref{fig:prime_a_one_ih_parsetree}, hvor $\cal{H} \Rightarrow{}$ er tilf\o{}jet de enkelte undertr\ae{}er til $\vdash{}$.

\begin{figure}[htbp]
\begin{center}
\begin{picture}(60, 60)
\put(12, 48){\framebox(12, 12){$\ \vdash{}$}}
\put(0,  24){\framebox(12, 12){$\cal{A}$}}
\put(36, 24){\framebox(12, 12){$\ \Rightarrow{}$}}
\put(24,  0){\framebox(12, 12){$\cal{B}$}}
\put(48,  0){\framebox(12, 12){$\cal{A}$}}

\put(6,  36){\line(1,1){12}}
\put(42, 36){\line(-2,1){24}}
\put(30, 12){\line(1,1){12}}
\put(54, 12){\line(-1,1){12}}
\end{picture}
\end{center}
\caption{$A1'_{i}$}
\label{fig:prime_a_one_i_parsetree}
\end{figure}

\begin{figure}[htbp]
\begin{center}
\begin{picture}(108, 84)
\put(36, 72){\framebox(12, 12){$\ \vdash{}$}}
\put(12, 48){\framebox(12, 12){$\ \Rightarrow{}$}}
\put(60, 48){\framebox(12, 12){$\ \Rightarrow{}$}}
\put(0,  24){\framebox(12, 12){$\cal{H}$}}
\put(24, 24){\framebox(12, 12){$\cal{A}$}}
\put(48, 24){\framebox(12, 12){$\cal{H}$}}
\put(84, 24){\framebox(12, 12){$\ \Rightarrow{}$}}
\put(72,  0){\framebox(12, 12){$\cal{B}$}}
\put(96,  0){\framebox(12, 12){$\cal{A}$}}

\put(6,   36){\line(1,1){12}}
\put(54,  36){\line(1,1){12}}
\put(78,  12){\line(1,1){12}}
\put(102, 12){\line(-1,1){12}}
\put(30,  36){\line(-1,1){12}}
\put(90,  36){\line(-2,1){24}}
\put(66,  60){\line(-2,1){24}}
\put(18,  60){\line(2,1){24}}
\end{picture}
\end{center}
\caption{$A1'_{ih}$}
\label{fig:prime_a_one_ih_parsetree}
\end{figure}

Af specielle metavariabler kan $\cal{H}$ n\ae{}vnes, som bruges til hypotetiske s\ae{}tninger. $\cal{Y}$ bruges i induktionsbeviser, hvor der laves induktion over $\cal{Y}$. Induktionsbeviser bevises i tre skridt, '$\textit{navn}\ i$' beviser basis, '$\textit{navn}\ ii$' beviser induktionsskridtet og endelig '$\textit{navn}$' beviser selve s\ae{}tningen.

\subsection{Simple beviser}

I dette afsnit vil der v\ae{}re beviser for et antal lemmaer i propositions teorien, som danner grundlag for efterf\o{}lgende afsnit. Alle beviserne bliver bevist indenfor teorien "[ math system prime s end math ]", der er defineret p\aa{} \cite{grue:peano} som indeholder alle aksiomerne fra afsnit \ref{ssec:prop_definition}.

For at \o{}ge l\ae{}sbarheden introduceres  
"[ intro 
     var x macro modus ponens var y 
   pyk 
     "* macro modus ponens *" 
   tex "#1.
\unrhd #2." 
   end intro ]"
, som bliver makrodefinert til
"[ math 
     macro define 
       var x macro modus ponens var y 
     as 
       rule prime mp modus ponens var x modus ponens var y 
     end define 
   end math ]".

\subsubsection{Bevis $MP'_{d}$}

Det f\o{}rste bevis er 
"[ intro
      double rule prime mp
   pyk
     "double rule prime mp"
   tex
     "MP'_{d}"
   end intro ]"
som blot er en dobbelt anvendelse af "[ math rule prime mp end math ]". Denne s\ae{}tning reducerer typisk andre beviser med en linje. S\ae{}tningen er:

\display{
"[ math
   in theory
     system prime s
   lemma
     double rule prime mp
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta a infer meta b infer meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     double rule prime mp
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano imply meta b peano imply meta c end line

     line ell b premise meta a end line

     line ell c premise meta b end line

     line ell d because ell a macro modus ponens ell b indeed meta b peano imply meta c end line

                because ell d macro modus ponens ell c indeed meta c qed
   end math ]" \\

Idet "[ math double rule prime mp end math ]" er bevist, f\o{}lges eksemplet fra f\o{}r og 
"[ intro
     var x macro first modus ponens var y macro second modus ponens var z
   pyk
     "* macro first modus ponens * macro second modus ponens *"
   tex "#1.
\unrhd #2.
\unrhd #3."
   end intro ]"
introduceres, der p\aa{} samme m\aa{}de er makrodefineret til den dobbelte anvendelse  
"[ math
     macro define
       var x macro first modus ponens var y macro second modus ponens var z
     as
       double rule prime mp modus ponens var x modus ponens var y modus ponens var z
     end define
   end math ]"
.

\subsubsection{Bevis $A1'_{i}$}

Lemmaet 
"[ intro
      inference axiom prime a one
   pyk
     "inference axiom prime a one"
   tex
     "A1'_{i}"
   end intro ]"
er en inferens version af "[ math axiom prime a one end math ]", som det ses i s\ae{}tningen er en implikations-operator blevet udskiftet med en inferens-operator:

\display{
"[ math
   in theory
     system prime s
   lemma
     inference axiom prime a one
   says
     all meta a indeed all meta b indeed meta a infer meta b peano imply meta a
   end lemma
   end math ]"}

Beviset f\o{}leger: \\

"[ math
     system prime s
   proof of
     inference axiom prime a one
   reads
     arbitrary meta a end line
     arbitrary meta b end line

     line ell a premise meta a end line

     line ell b because axiom prime a one indeed meta a peano imply meta b peano imply meta a end line

                because ell b macro modus ponens ell a indeed meta b peano imply meta a qed

   end math ]" \\

Da denne s\ae{}tning er essentiel i nogle af de f\o{}lgende afsnit, gives den navnet 
"[ intro
      rule hypothesize
   pyk
     "rule hypothesize"
   tex
     "Hypothesize"
   end intro ]"
, der er makrodefineret til s\ae{}tningen selv  
"[ math
     macro define
       rule hypothesize
     as
       inference axiom prime a one
     end define
   end math ]"

\subsubsection{Bevis $A2'_{i}$}

"[ intro
      inference axiom prime a two
   pyk
     "inference axiom prime a two"
   tex
     "A2'_{i}"
   end intro ]" 
er endnu en inferens version af et aksiom. Lemmaet og beviset er som nedenst\aa{}ende:

\display{
"[ math
   in theory
     system prime s
   lemma
     inference axiom prime a two
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     inference axiom prime a two
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano imply meta b peano imply meta c end line

     line ell b because axiom prime a two indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line

                because ell b macro modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c qed

   end math ]"

\subsubsection{Bevis $A2'_{ii}$}

"[ intro
      inference inference axiom prime a two
   pyk
     "inference inference axiom prime a two"
   tex
     "A2'_{ii}"
   end intro ]"
er den f\o{}rste dobbelte inferens version af et lemma, som det ses i 
\display{
"[ math
   in theory
     system prime s
   lemma
     inference inference axiom prime a two
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta a peano imply meta b infer meta a peano imply meta c
   end lemma
   end math ]"}
udskiftes to implikations-operatorer - heraf de to \textit{i}er. I beviset kan den foreg\aa{}ende s\ae{}tning udnyttes: \\

"[ math
     system prime s
   proof of
     inference inference axiom prime a two
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano imply meta b peano imply meta c end line

     line ell b premise meta a peano imply meta b end line

     line ell c because inference axiom prime a two modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line

                because ell c macro modus ponens ell b indeed meta a peano imply meta c qed

   end math ]" \\

Anskues "[ math inference inference axiom prime a two end math ]", ses det at lighederne med "[ math rule prime mp end math ]" er mange. Reelt er det en hypotetisk version af "[ math rule prime mp end math ]", derfor bliver
"[ intro
      hypothetical rule prime mp
   pyk
     "hypothetical rule prime mp"
   tex
     "MP'_{h}"
   end intro ]"
defineret til
"[ math
     macro define
       hypothetical rule prime mp
     as
       inference inference axiom prime a two
     end define
   end math ]"
. Modus ponens blev f\o{}r defineret med $\unrhd{}$, herefter vil den hypotetiske version af denne ( 
"[ intro
     var x hypothetical macro modus ponens var y
   pyk
     "* hypothetical macro modus ponens *"
   tex "#1.
\unrhd_h #2."
   end intro ]"
) blive defineret til 
"[ math
     macro define
       var x hypothetical macro modus ponens var y
     as
       hypothetical rule prime mp modus ponens var x modus ponens var y
     end define
   end math ]"
.

\subsubsection{Bevis $A2'_{iid}$}

Den f\o{}rste brug af dobbelt-navnet ses af
"[ intro
      double inference inference axiom prime a two
   pyk
     "double inference inference axiom prime a two"
   tex
     "A2'_{iid}"
   end intro ]"
. S\ae{}tningen 
\display{
"[ math
   in theory
     system prime s
   lemma
     double inference inference axiom prime a two
   says
     all meta a indeed all meta b indeed all meta c indeed all meta d indeed meta a peano imply meta b peano imply meta c peano imply meta d infer meta a peano imply meta b infer meta a peano imply meta c infer meta a peano imply meta d 
   end lemma
   end math ]"}
giver perfekt mening i forhold til det s\ae{}nkede \textit{iid}. I beviset ses desuden ogs\aa{} at det centrale er den dobbelte brug af "[ math inference inference axiom prime a two end math ]": \\

"[ math
     system prime s
   proof of
     double inference inference axiom prime a two
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line
     arbitrary meta d end line

     line ell a premise meta a peano imply meta b peano imply meta c peano imply meta d end line

     line ell b premise meta a peano imply meta b end line

     line ell c premise meta a peano imply meta c end line

     line ell d because inference inference axiom prime a two modus ponens ell a modus ponens ell b indeed meta a peano imply meta c peano imply meta d end line

                because inference inference axiom prime a two modus ponens ell d modus ponens ell c indeed meta a peano imply meta d qed

   end math ]" \\

Forholdes lemmaet til "[ math double hypothetical rule prime mp end math ]", ses det at dette er en dobbelt hypotetisk modus ponens.
"[ intro
      double hypothetical rule prime mp
   pyk
     "double hypothetical rule prime mp"
   tex
     "MP'_{hd}"
   end intro ]"
bliver derfor makrodefineret til 
"[ math
     macro define
       double hypothetical rule prime mp
     as
       double inference inference axiom prime a two
     end define
   end math ]"
. P\aa{} samme m\aa{}de som f\o{}r bliver 
"[ intro
     var x hypothetical macro first modus ponens var y hypothetical macro second modus ponens var z
   pyk
     "* hypothetical macro first modus ponens * hypothetical macro second modus ponens var *"
   tex "#1.
\unrhd_h #2.
\unrhd_h #3."
   end intro ]"
defineret
"[ math
     macro define
       var x hypothetical macro first modus ponens var y hypothetical macro second modus ponens var z
     as
       double hypothetical rule prime mp modus ponens var x modus ponens var y modus ponens var z
     end define
   end math ]"
.

\subsubsection{Bevis $1.8$}

"[ intro
      mendelson lemma one eight
   pyk
     "mendelson lemma one eight"
   tex
     "Mendelson\ \textbf{1.8}"
   end intro ]"
er et grundl\ae{}ggende bevis i \cite{mendelson}. S\ae{}tningen -

\display{
"[ math
   in theory
     system prime s
   lemma
       mendelson lemma one eight
   says
       all meta a indeed meta a peano imply meta a
   end lemma
   end math ]"}

- siger at noget medf\o{}rer sig selv. \\

"[ math
     system prime s
   proof of
     mendelson lemma one eight
   reads
     arbitrary meta a end line

     line ell a because axiom prime a one indeed meta a peano imply parenthesis meta a peano imply meta a end parenthesis peano imply meta a end line

     line ell b because axiom prime a one indeed meta a peano imply meta a peano imply meta a end line

                because inference inference axiom prime a two modus ponens ell a modus ponens ell b indeed meta a peano imply meta a qed

   end math ]" \\

Ovenst\aa{}ende bevis af "[ math mendelson lemma one eight end math ]" bevises i \cite{mendelson} p\aa{} 5 linjer, hvor denne kun 3. Optimeringen er en konsekvens af de foreg\aa{}ende inferens-beviser.

\subsubsection{Bevis $1.8_{i}$}

At bevise
"[ intro
      inference mendelson lemma one eight
   pyk
     "inference mendelson lemma one eight"
   tex
     "Mendelson\ \textbf{1.8}_{i}"
   end intro ]"
som siger
"[ math
   in theory
     system prime s
   lemma
     inference mendelson lemma one eight
   says
     all meta a indeed meta a infer meta a
   end lemma
   end math ]"
, kan virke besynderligt, men efterf\o{}lgende vil dette vise sig nyttigt: \\

"[ math
     system prime s
   proof of
     inference mendelson lemma one eight
   reads
     arbitrary meta a end line

     line ell a premise meta a end line

     line ell b because mendelson lemma one eight indeed meta a peano imply meta a end line

                because ell b macro modus ponens ell a indeed meta a qed

   end math ]" \\

Beviet navngives 
"[ intro
      rule repetition
   pyk
     "rule repetition"
   tex
     "Repetition"
   end intro ]"
via makrodefinitionen \linebreak[4]
"[ math
     macro define
       rule repetition
     as
       inference mendelson lemma one eight
     end define
   end math ]"
.

\subsubsection{Bevis $1.47\ b$}

"[ intro
     mendelson exercise one fourtyseven b
   pyk
     "mendelson exercise one fourtyseven b"
   tex
     "Mendelson\ \textbf{1.47}\ b"
   end intro ]"
er en form for transitivets lemma p\aa{} implikation:

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson exercise one fourtyseven b
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b infer meta b peano imply meta c infer meta a peano imply meta c
   end lemma
   end math ]"}

Beviset udnytter flere af de foreg\aa{}ende lemmaer: \\

"[ math
     system prime s
   proof of
     mendelson exercise one fourtyseven b
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano imply meta b end line

     line ell b premise meta b peano imply meta c end line

     line ell c because inference axiom prime a one modus ponens ell b indeed meta a peano imply meta b peano imply meta c end line

                because inference inference axiom prime a two modus ponens ell c modus ponens ell a indeed meta a peano imply meta c qed

   end math ]"

\subsubsection{Bevis $1.47\ c$}

"[ intro
     mendelson exercise one fourtyseven c
   pyk
     "mendelson exercise one fourtyseven c"
   tex
     "Mendelson\ \textbf{1.47}\ c"
   end intro ]"
permutere r\ae{}kkef\o{}lgen af bestemte termer:

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson exercise one fourtyseven c
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b peano imply meta a peano imply meta c
   end lemma
   end math ]"}

For f\o{}rste gang benyttes den hypotetiske version af modus ponens: \\

"[ math
     system prime s
   proof of
     mendelson exercise one fourtyseven c
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano imply meta b peano imply meta c end line

     line ell b because inference axiom prime a two modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line

     line ell c because inference axiom prime a one modus ponens ell b indeed meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line

     line ell d because axiom prime a one indeed meta b peano imply meta a peano imply meta b end line

                because ell c hypothetical macro modus ponens ell d indeed meta b peano imply meta a peano imply meta c qed

   end math ]"

\subsubsection{Bevis $1.47\ e$}

Dette bevis er ikke en oprindelig opgave fra \cite{mendelson}, men grundt lighederne med de \o{}vrige beviser fra $1.47$-samlingen, placeret her. Selve lemmaet \linebreak[4]
"[ intro
     mendelson exercise one fourtyseven e
   pyk
     "mendelson exercise one fourtyseven e"
   tex
     "Mendelson\ \textbf{1.47}\ e"
   end intro ]"
siger f\o{}lgende:

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson exercise one fourtyseven e
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b infer meta a peano imply meta c
   end lemma
   end math ]"}

Nedenst\aa{}ende beviser "[ math mendelson exercise one fourtyseven e end math ]": \\

"[ math
     system prime s
   proof of
     mendelson exercise one fourtyseven e
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano imply meta b peano imply meta c end line

     line ell b premise meta b end line

     line ell c because mendelson exercise one fourtyseven c modus ponens ell a indeed meta b peano imply meta a peano imply meta c end line

                because ell c macro modus ponens ell b indeed meta a peano imply meta c qed

  end math ]"

\section{Deduktion}

\subsection{Definitioner}

Proposition 1.9 i \cite{mendelson} beviser, at man fra "[ math meta a infer meta b end math ]" kan bevise $\cal{A} \Rightarrow{} \cal{B}$. Bevis-konstruktionerne p\aa{} basis-siden giver ikke mulighed for at flytte p\aa{} $\vdash{}$-tegnet, n\aa{}r det f\o{}rst er sat med en pr\ae{}misse (\textit{Premise}). Beviset skal derfor udf\o{}res s\aa{}ledes at det korrekte resultat fremkommer direkte. Mendelson \cite{mendelson} bruger i fl\ae{}ng ordet \textit{hyp} eller \textit{hypothesis} om hypoteser, men for n\ae{}rv\ae{}rende sk\ae{}lnes mellem dem som pr\ae{}misser og hypoteser p\aa{} f\o{}lgende m\aa{}de:

\display{pr\ae{}misse $\vdash{}$ hypotese $\Rightarrow{}$ konklusion}

Ovenst\aa{}ende $\vdash{}$ st\aa{}r l\ae{}ngst til h\o{}jre i en s\ae{}tning - og da $\vdash{}$ er h\o{}jre associativ kan der v\ae{}re flere pr\ae{}misser i en s\ae{}tning. Desuden kaldes en 'hypotese' kun for en endelig hypotese, hvis det er noget der bliver hypotetisk antaget. Eksempelvis bliver Corollary 1.10 a fra \cite{mendelson}:

\[ \cal{B} \Rightarrow{} \cal{C},\ \cal{C} \Rightarrow{} \cal{D} \vdash{} \cal{B} \Rightarrow{} \cal{D} \]

skrevet p\aa{} f\o{}lgende m\aa{}de i Logiweb:

\display{"[ math meta b peano imply meta c infer meta c peano imply meta d infer meta b peano imply meta d end math ]"}

Hvor "[ math meta b peano imply meta c end math ]" er den f\o{}rste pr\ae{}misse, "[ math meta c peano imply meta d end math ]" den anden, "[ math meta b end math ]" er hypotesen og "[ math meta d end math ]" er konklusionen.

Nedenst\aa{}ende bevis p\aa{} mendelson-form af Lemma \textbf{1.11} d vil v\ae{}re gennem\-g\aa{}ende for dette afsnit (i mods\ae{}tning til \cite{mendelson} er implikation her h\o{}je-associativ): \\

\makebox [0.05\textwidth ][l]{$1$.}
\makebox [0.45\textwidth ][l]{$\neg{} \cal{A} \Rightarrow{} \neg{} \cal{B}$}\quad
\makebox [0.3\textwidth ][l]{Hyp}

\makebox [0.05\textwidth ][l]{$2$.}
\makebox [0.45\textwidth ][l]{$(\neg{} \cal{A} \Rightarrow{} \neg{} \cal{B}) \Rightarrow{} (\neg{} \cal{A} \Rightarrow{} \cal{B}) \Rightarrow{} \cal{A}$}\quad
\makebox [0.3\textwidth ][l]{Axiom (A3)}

\makebox [0.05\textwidth ][l]{$3$.}
\makebox [0.45\textwidth ][l]{$\cal{B} \Rightarrow{} \neg{} \cal{A} \Rightarrow{} \cal{B}$}\quad
\makebox [0.3\textwidth ][l]{Axiom (A1)}

\makebox [0.05\textwidth ][l]{$4$.}
\makebox [0.45\textwidth ][l]{$(\neg{} \cal{A} \Rightarrow{} \cal{B}) \Rightarrow{} \cal{A}$}\quad
\makebox [0.3\textwidth ][l]{1, 2, MP}

\makebox [0.05\textwidth ][l]{$5$.}
\makebox [0.45\textwidth ][l]{$\cal{B} \Rightarrow{} \cal{A}$}\quad
\makebox [0.3\textwidth ][l]{3, 4, Exercise 1.47 b}

\makebox [0.05\textwidth ][l]{$6$.}
\makebox [0.45\textwidth ][l]{$(\neg{} \cal{A} \Rightarrow{} \neg{} \cal{B}) \Rightarrow{} \cal{B} \Rightarrow{} \cal{A}$}\quad
\makebox [0.3\textwidth ][l]{1-5, deduction theorem} \\

I linje 5 bruger \cite{mendelson} dog Corollary \textbf{1.10} a, men da dette bevis ikke er lavet endnu, bliver Exercise \textbf{1.47} b udnyttet hvor effekten er den samme.

\subsection{Overs\ae{}ttelse}
\label{ssec:deduktion_oversaettelse}

Dette afsnit fremf\o{}rer en algoritme, der tager et bevis p\aa{} mendelson-form der benytter proposition 1.9 som input. Som output gives et bevis der kan bevises med beviskonstruktionerne fra basis-siden.

I det f\o{}lgende vil 
"[ intro
      hypothesis
   pyk
     "hypothesis"
   tex
     "\mathsf{hyp}"
   end intro ]" 
v\ae{}re en pladsholder for en given hypotese, 
"[ intro
      instance
   pyk
     "instance"
   tex
     "\mathsf{instance}"
   end intro ]"
for en instanciering af et aksiom eller lemma og
"[ intro
      conclusion
   pyk
     "conclusion"
   tex
     "\mathsf{conclusion}"
   end intro ]" for en konklusion.

Algoritmen tager en linje ad gangen, fortl\o{}bende fra linje 1. Linjen klassificeres herefter til en af f\o{}lgende typer og foretager overs\ae{}ttelsen:

\begin{itemize}
  \item Brug af hypotese
  \item Instanciering af aksiom/lemma
  \item Brug af lemma med modus ponens
  \item Brug af modus ponens
\end{itemize}

Overs\ae{}ttelsen af de enkelte typer ses i de f\o{}lgende afsnit. Selve overs\ae{}ttelsen s\o{}rger for, at der altid kommer til at s\aa{} det \o{}nskede "[ math hypothesis peano imply instance end math ]" - alts\aa{} en form for automatisk brug af Proposition 1.9.

\subsubsection{Brug af hypotese}
\label{ssec:deduktion_hypotese}

Mendelson-form:

\makebox [0.05\textwidth ][l]{$X$.}
\makebox [0.45\textwidth ][l]{$"[ hypothesis ]"$}\quad
\makebox [0.3\textwidth ][l]{Hyp} \\

Logiweb-form:

\makebox [0.1\textwidth ][l]{$LX.1$:}
\makebox [0.4\textwidth ][l]{$"[ mendelson lemma one eight ]" \gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"[ hypothesis peano imply hypothesis ]"$\hfill \makebox [0mm][l]{\quad ;}}

\subsubsection{Instanciering af aksiom/lemma}

Mendelson-form:

\makebox [0.05\textwidth ][l]{$X$.}
\makebox [0.45\textwidth ][l]{$"[ instance ]"$}\quad
\makebox [0.3\textwidth ][l]{Axiom/Lemma} \\

Logiweb-form:

\makebox [0.1\textwidth ][l]{$LX.1$:}
\makebox [0.4\textwidth ][l]{Axiom/Lemma $\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"[ instance ]"$\hfill \makebox [0mm][l]{\quad ;}}

\makebox [0.1\textwidth ][l]{$LX.2$:}
\makebox [0.4\textwidth ][l]{$"[ axiom prime a one ]"\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"[ instance peano imply hypothesis peano imply instance ]"$\hfill \makebox [0mm][l]{\quad ;}}

\makebox [0.1\textwidth ][l]{$LX$:}
\makebox [0.4\textwidth ][l]{LX.2 $\unrhd{}$ LX.1 $\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"[ hypothesis peano imply instance ]"$ \hfill \makebox [0mm][l]{\quad ;}}

\subsubsection{Brug af lemma med modus ponens}

Mendelson-form:

\makebox [0.05\textwidth ][l]{$X$.}
\makebox [0.45\textwidth ][l]{$"[ conclusion ]"$}\quad
\makebox [0.3\textwidth ][l]{Y, ..., Lemma} \\

Logiweb-form:

\makebox [0.1\textwidth ][l]{$LX$:}
\makebox [0.4\textwidth ][l]{$Lemma_{h}$ $\rhd{}$ Y $\rhd{}$ ... $\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"[ hypothesis peano imply conclusion ]"$ \hfill \makebox [0mm][l]{\quad ;}}

\subsubsection{Brug af modus ponens}

Bem\ae{}rk at \cite{mendelson} for det meste skriver argumenterne omvendt til MP end i "[ math system prime s end math ]". \\

Mendelson-form:

\makebox [0.05\textwidth ][l]{$X$.}
\makebox [0.45\textwidth ][l]{$"[ conclusion ]"$}\quad
\makebox [0.3\textwidth ][l]{Y, Z, MP} \\

Logiweb-form:

\makebox [0.1\textwidth ][l]{$LX.1$:}
\makebox [0.4\textwidth ][l]{$"[ axiom prime a two ]"\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"[ unicode capital z unicode end of text peano imply unicode capital y unicode end of text peano imply hypothesis peano imply conclusion ]"$\hfill \makebox [0mm][l]{\quad ;}}

\makebox [0.1\textwidth ][l]{$LX.2$:}
\makebox [0.4\textwidth ][l]{LX.1 $ \unrhd{} $ Z $\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"[ unicode capital y unicode end of text peano imply hypothesis peano imply conclusion ]"$\hfill \makebox [0mm][l]{\quad ;}}

\makebox [0.1\textwidth ][l]{$LX$:}
\makebox [0.4\textwidth ][l]{LX.2 $ \unrhd{} $ Y $\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"[ hypothesis peano imply conclusion ]"$\hfill \makebox [0mm][l]{\quad ;}}

\subsection{Eksempel}
\label{ssec:deduktion_eksempel}

Med udgangspunkt i eksemplet fra tidligere, anvendes overs\ae{}ttelses-algoritmen. Algoritmen kr\ae{}ver dog at "[ math hypothetical mendelson exercise one fourtyseven b end math ]" er bevist f\o{}rst - hvilket er foretaget i afsnit \ref{sssec:hyp_one_ fourtyseven_b}. 
"[ intro
      mendelson lemma one eleven d
   pyk
     "mendelson lemma one eleven d"
   tex
     "Mendelson\ \textbf{1.11}\ d"
   end intro ]"
vil herefter v\ae{}re navnet p\aa{} eksemplet, hvor s\ae{}tningen siger: 

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson lemma one eleven d
   says
     all meta a indeed all meta b indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply meta a
   end lemma
   end math ]"}

Idet udf\o{}relsen af beviset gennemg\aa{}s linje for linje, opn\aa{}s en enkelt anskuelse: \\

"[ math
     system prime s
   proof of
     mendelson lemma one eleven d
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     ; Line 1
     line ell a because mendelson lemma one eight indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply peano not meta a peano imply peano not meta b end line
     ; Line 2
     line ell b because axiom prime a three indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line 

     line ell c because axiom prime a one indeed parenthesis parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line

     line ell d because ell c macro modus ponens ell b indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line
     ; Line 3
     line ell e because axiom prime a one indeed meta b peano imply peano not meta a peano imply meta b end line

     line ell f because axiom prime a one indeed parenthesis meta b peano imply peano not meta a peano imply meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply peano not meta a peano imply meta b end line

     line ell g because ell f macro modus ponens ell e indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply peano not meta a peano imply meta b end line
     ; Line 4
     line ell h because axiom prime a two indeed parenthesis parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end parenthesis peano imply parenthesis parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line

     line ell i because ell h macro modus ponens ell d indeed parenthesis parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line
 
     line ell j because ell i macro modus ponens ell a indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line
     ; Line 5
                because hypothetical mendelson exercise one fourtyseven b modus ponens ell g modus ponens ell j indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply meta a qed

   end math ]"

\subsection{Optimering af eksempel}
\label{ssec:deduktion_optimering_eksempel}

Da kun aksiomer blev anvendt til definition af basisovers\ae{}ttelsen af beviser p\aa{} mendel\-son-form til logiweb-form, blev eksemplet i afsnit \ref{ssec:deduktion_eksempel} langt. Beviset reduceres betydeligt s\aa{}fremt der drages nytte af tidligere beviste s\ae{}tninger: \\

"[ math
     system prime s
   proof of
     mendelson lemma one eleven d
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     ; Line 1
     line ell a because mendelson lemma one eight indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply peano not meta a peano imply peano not meta b end line
     ; Line 2
     line ell b because axiom prime a three indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line

     line ell c because rule hypothesize modus ponens ell b indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line
     ; Line 3
     line ell d because axiom prime a one indeed meta b peano imply peano not meta a peano imply meta b end line

     line ell e because rule hypothesize modus ponens ell d indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply peano not meta a peano imply meta b end line
     ; Line 4
     line ell f because ell c hypothetical macro modus ponens ell a indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line

                because hypothetical mendelson exercise one fourtyseven b modus ponens ell e modus ponens ell f indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply meta a qed
   end math ]" \\

P\aa{} samme m\aa{}de som overs\ae{}ttelse fra bevis p\aa{} mendelson-form til bevis p\aa{} logiweb-form, kan man ogs\aa{} lave en overs\ae{}ttelse til optimeret logiweb-form. Denne overs\ae{}ttelse er dog ikke beskrevet i detaljer her, da den er forholdsvis enkel og fremg\aa{}r af eksemplet.

\subsection{Nye beviskonstruktioner}
\label{ssec:deduktion_new}

Selvom beviser kan laves p\aa{} optimeret logiweb-form, bliver beviserne stadig l\ae{}ngere og mere komplekse end de tilsvarende i \cite{mendelson}. En svaghed ved logiweb-formen er den eksplicitte angivelse af hypotesen hver gang, hvilket tager meget 'plads' i beviserne. Endvidere skal der anvendes en "[ math rule hypothesize end math ]" hver gang man instancierer et aksiom eller lemma. Form\aa{}let med dette afsnit er at afhj\ae{}lpe disse problemer, for dermed at lave beviser p\aa{} samme st\o{}rrelse som i \cite{mendelson}.

En m\aa{}de dette kunne implementeres, er ved at skrive deduktionsalgoritmen ind i selv bevischeckeren p\aa{} basis-siden. Dette vil dog v\ae{}re at skyde over m\aa{}let med denne opgave. Istedet bygges l\o{}sningsmodellen p\aa{} makrodefinitioner, der ekspandere ud til konstruktioner som bevischeckeren allerede kender.

Den f\o{}rste nye konstruktion til hypotetiske beviser er
"[ intro
     line var l hypothesis indeed var i end line var p
   pyk
     "line * hypothesis indeed * end line *"
   tex
     "
\newline \makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}\makebox [0.4\textwidth ][l]{$Hypothesis{}
\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$#2.
$\hfill \makebox [0mm][l]{\quad ;}}#3."
   end intro ]"
, som g\o{}r det ud for introduktion af en hypotese - svarende til afsnit \ref{ssec:deduktion_hypotese}. Selve konstruktionen er makrodefineret:

\display{ 
"[ math 
     macro define 
       line var l hypothesis indeed var i end line var p 
     as 
       parenthesis 
         mendelson lemma one eight 
       conclude 
         var i peano imply var i cut let hypothesis abbreviate var i in let var l abbreviate var i peano imply var i in var p 
       end parenthesis
     end define 
   end math ]"}

Konstruktionen har linjenummeret \textit{l}, konkludere \textit{i} og har en 'pointer' \textit{p} til den n\ae{}ste bevislinje. Ideen er at konstruktionen skal virke p\aa{} samme m\aa{}de som en $Hyp$ i \cite{mendelson}. F\o{}rst konkluderer makroen ud fra "[ math mendelson lemma one eight end math ]" at \textit{i} $\Rightarrow{}$ \textit{i}, herefter gemmer den hypotesen \textit{i} i den lokale makrodefinition "[ math hypothesis end math ]". Til sidst gemmer den konklusionen fra "[ math mendelson lemma one eight end math ]" i \textit{l}, s\aa{} andre linjer kan referer til denne. Det vigtigste ved linjen er at den 'husker' hypotesen, s\aa{} man dermed kan undg\aa{} at skrive den eksplicit p\aa{} efterf\o{}lgende linjer - den sorte prik efter linjenummeret angiver at linjen l\ae{}ses med hypotesen st\aa{}ende foran.

En lille teknisk detalje ved den nye konstruktion, er at den har pointeren til den n\ae{}ste bevislinje. Dermed kan konstruktionen ikke st\aa{} sidst i beviset. En mulig m\aa{}de at l\o{}se dette problem p\aa{}, kunne v\ae{}re at have to versioner af den nye konstruktion - en almindelig og en til den sidste linje. Denne l\o{}sning vil dog ikke v\ae{}re at foretr\ae{}kke, da den fordobler antallet af nye beviskonstruktioner. En nem l\o{}sning, og den valgte, p\aa{} problemet er at bruge lemmaet "[ math rule repetition end math ]" til at 'udfylde' den sidste linje.

\tex{
"[ math
     tex name define
       line var l hypothesis indeed var i end line var p
     as "
Line \, #1.
:\bullet{}\ Hypothesis
\gg #2.
; #3."
     end define
   end math ]"}

\subsubsection{Brug af regler}

Brug af aksiomer og lemmaer bliver igen delt op i kategorier - den ene hvor reglen instancieres direkte og den anden hvor reglen instancieres med brug af en eller flere modus ponens.

Som vist i afsnit \ref{ssec:deduktion_optimering_eksempel}, anvendes altid en "[ math rule hypothesize end math ]" n\aa{}r man instancere en regel som ikke brugere modus ponens. Alternativt skal der v\ae{}re hypotetiske versioner af alle regler - eksempelvis $A1'_{h}, A2'_{h}$ osv. Konstruktionen 
"[ intro
     line var l hypothesis because var a indeed var i end line var p
   pyk
     "line * hypothesis because * indeed * end line *"
   tex
     "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$#2.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#3.
$\hfill \makebox [0mm][l]{\quad ;}}#4."
   end intro ]"
laver automatisk en "[ math rule hypothesize end math ]" p\aa{} en instancering af en regel.

\display{
"[ math
     macro define
       line var l hypothesis because var a indeed var i end line var p
     as
       parenthesis
         var a
       conclude
         var i cut rule hypothesize modus ponens var i conclude hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p
       end parenthesis
     end define
   end math ]"}

Ovenst\aa{}ende makrodefinition har igen \textit{l}, \textit{i} og \textit{p} i lighed med tidligere. Endvidere har den \textit{a} som angiver argumentationen linjen er skrevet med. Makroen konkluderer f\o{}rst \textit{i} ud fra \textit{a}, hvorefter den laver den hypotetiske version af \textit{i} med en "[ math rule hypothesize end math ]" - bem\ae{}rk brugen af "[ math hypothesis end math ]", der opretholder proposition 1.9.

\tex{
"[ math
     tex name define
       line var l hypothesis because var a indeed var i end line var p
     as
       "
Line \, #1.
:\bullet{}\ #2.
\gg #3.
; #4."
     end define
   end math ]"}

Til instanciering af en regel med brug af modus ponens, kan konstruktionen 
"[ intro
     line var l hypothesis raw because var a indeed var i end line var p
   pyk
     "line * hypothesis raw because * indeed * end line *"
   tex
     "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$#2.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#3.
$\hfill \makebox [0mm][l]{\quad ;}}#4."
   end intro ]"
bruges. Selve makrodefinitionen:

\display{
"[ math
     macro define
       line var l hypothesis raw because var a indeed var i end line var p
     as
       parenthesis
         var a
       conclude
         hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p
       end parenthesis
     end define
   end math ]"}

er n\ae{}sten identisk med en af linje konstruktionerne p\aa{} basis-siden, p\aa{} n\ae{}r at hypotesen er skrevet foran hver konklusion. N\aa{}r denne konstruktion bruges skal man derfor huske kun at bruge hypotetiske versioner af regler, ellers gives en fejlmeddelelse.

\tex{
"[ math
     tex name define
       line var l hypothesis raw because var a indeed var i end line var p
     as
       "
Line \, #1.
:\bullet{}\ #2.
\gg #3.
; #4."
     end define
   end math ]"}

\subsubsection{Brug af MP lokalt}

Endelig kunne man godt n\o{}jes med de tre foreg\aa{}ende definitioner, men for at g\o{}re l\o{}sningen mere komplet vil der ogs\aa{} blive indf\o{}rt nye konstruktioner til brug af modus ponens i hypotetiske beviser.
"[ intro
     line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p
   pyk
     "line * hypothesis modus ponens * modus ponens * indeed * end line *"
   tex
     "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$#2.
\unrhd{} #3.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#4.
$\hfill \makebox [0mm][l]{\quad ;}}#5."
   end intro ]"
er blot en hypotetisk brug af modus ponens:

\display{
"[ math
     macro define
       line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p
     as
       parenthesis
         var u hypothetical macro modus ponens var v 
       conclude
         hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p
       end parenthesis
     end define
   end math ]"}

\tex{
"[ math
     tex name define
       line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p
     as
       "
Line \, #1.
:\bullet{}\ #2.
\unrhd{} #3.
\gg #4.
; #5."
     end define
   end math ]"}

"[ intro
     line var l hypothesis double modus ponens var u modus ponens var v modus ponens var z indeed var i end line var p
   pyk
     "line * hypothesis double modus ponens * modus ponens * modus ponens * indeed * end line *"
   tex
     "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$ #2.
\unrhd{} #3.
\unrhd{} #4.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#5.
$\hfill \makebox [0mm][l]{\quad ;}}#6."
   end intro ]"
definere den dobbelte brug af modus ponens: 

\display{
"[ math
     macro define
       line var l hypothesis double modus ponens var u modus ponens var v modus ponens var z indeed var i end line var p
     as
       parenthesis
         var u hypothetical macro first modus ponens var v hypothetical macro second modus ponens var z
       conclude
         hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p
       end parenthesis
     end define
   end math ]"}

\tex{
"[ math
     tex name define
       line var l hypothesis double modus ponens var u modus ponens var v modus ponens var z indeed var i end line var p
     as
       "
Line \, #1.
:\bullet{}\ #2.
\unrhd{} #3.
\unrhd{} #4.
\gg #5.
; #6."
     end define
   end math ]"}

\subsubsection{Brug af MP eksternt}

N\aa{}r modus ponens anvendes med et argument der referer ud af en hypotetisk 'blok', vil man f\aa{} problemer med at benytte de nye modus ponens konstruktioner fra det foreg\aa{}ende afsnit. Der er derfor igen lavet specielle konstruktioner til dette.

Referere en modus ponens ekstern i 1. argument, kan 
"[ intro
     line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p
   pyk
     "line * hypothesis first modus ponens * modus ponens * indeed * end line *"
   tex
     "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$ #2.
\circ{} \unrhd{} #3.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#4.
$\hfill \makebox [0mm][l]{\quad ;}}#5."
   end intro ]"
benyttes - cirklen angiver hvilket argument der er eksternt.

\display{
"[ math
     macro define
       line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p
     as
       parenthesis
         mendelson exercise one fourtyseven b modus ponens var v modus ponens var u
       conclude
         hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p
       end parenthesis
     end define
   end math ]"}

Makrodefinitionen er meget lig de foreg\aa{}ende, men tager blot h\o{}jde for at det ene argument st\aa{}r uden for blokken.

\tex{
"[ math
     tex name define
       line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p
     as
       "
Line \, #1.
:\bullet{}\ #2.
\circ{} \unrhd{} #3.
\gg #4.
; #5."
     end define
   end math ]"}

Ved modus ponens med reference eksternt i 2. argument, kan 
"[ intro
     line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p
   pyk
     "line * hypothesis second modus ponens * modus ponens * indeed * end line *"
   tex
     "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$ #2.
\unrhd{} #3.
\circ{} {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#4.
$\hfill \makebox [0mm][l]{\quad ;}}#5."
   end intro ]"
udnyttes. Makrodefinitionen er igen simpel:

\display{
"[ math
     macro define
       line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p
     as
       parenthesis
         mendelson exercise one fourtyseven e modus ponens var u modus ponens var v
       conclude
         hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p
       end parenthesis
     end define
   end math ]"}

\tex{
"[ math
     tex name define
       line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p
     as
       "
Line \, #1.
:\bullet{}\ #2.
\unrhd{} #3.
\circ{} \gg #4.
; #5."
     end define
   end math ]"}

\subsection{Eksempel med nye konstruktioner}

Da der er blevet lavet en m\ae{}ngede nye konstruktioner, er det oplagt at lave et eksempel med disse: \\

"[ math
     system prime s
   proof of
     mendelson lemma one eleven d
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     ; Line 1
     line ell a hypothesis indeed peano not meta a peano imply peano not meta b end line
     ; Line 2
     line ell b hypothesis because axiom prime a three indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line
     ; Line 3
     line ell c hypothesis because axiom prime a one indeed meta b peano imply peano not meta a peano imply meta b end line
     ; Line 4
     line ell d hypothesis modus ponens ell b modus ponens ell a indeed parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line
     ; Line 5
     line ell e hypothesis raw because hypothetical mendelson exercise one fourtyseven b modus ponens ell c modus ponens ell d indeed meta b peano imply meta a end line

                because rule repetition modus ponens ell e indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply meta a qed

   end math ]" \\

Som det ses antager beviset samme st\o{}rrelse som i \cite{mendelson}. Dog kan beviset reduceres lidt ved at indf\o{}re brug af $A3_{ih}$ - men beviset holdes p\aa{} samme m\aa{}de som i \cite{mendelson} for dermed at have et bedre sammenligningsgrundlag.

\subsection{Hypotetiske beviser}

Dette afsnit indeholder beviser for et antal hypotetiske s\ae{}tninger som anvendes senere. Beviserne udnytter de nye konstruktioner.

\subsubsection{Bevis $A1'_{ih}$}

"[ intro
      hypothetical inference axiom prime a one
   pyk
     "hypothetical inference axiom prime a one"
   tex
     "A1'_{ih}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     hypothetical inference axiom prime a one
   says
     all meta h indeed all meta a indeed all meta b indeed meta h peano imply meta a infer meta h peano imply meta b peano imply meta a
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     hypothetical inference axiom prime a one
   reads
     arbitrary meta h end line
     arbitrary meta a end line
     arbitrary meta b end line

     line ell a premise meta h peano imply meta a end line

     line ell b hypothesis indeed meta h end line

     line ell c hypothesis because axiom prime a one indeed meta a peano imply meta b peano imply meta a end line

     line ell e hypothesis modus ponens ell c modus ponens ell a indeed meta b peano imply meta a end line

                because rule repetition modus ponens ell e indeed meta h peano imply meta b peano imply meta a qed

   end math ]"

\subsubsection{Bevis $A2'_{ih}$}

"[ intro
      hypothetical inference axiom prime a two
   pyk
     "hypothetical inference axiom prime a two"
   tex
     "A2'_{ih}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     hypothetical inference axiom prime a two
   says
     all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano imply meta b peano imply meta c infer meta h peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     hypothetical inference axiom prime a two
   reads
     arbitrary meta h end line
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta h peano imply meta a peano imply meta b peano imply meta c end line

     line ell c hypothesis indeed meta h end line

     line ell d hypothesis because axiom prime a two indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line

     line ell e hypothesis modus ponens ell d modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line

                because rule repetition modus ponens ell e indeed meta h peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c qed

   end math ]"

\subsubsection{Bevis $A2'_{iih}$}

"[ intro
      hypothetical inference inference axiom prime a two
   pyk
     "hypothetical inference inference axiom prime a two"
   tex
     "A2'_{iih}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     hypothetical inference inference axiom prime a two
   says
     all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano imply meta b peano imply meta c infer meta h peano imply meta a peano imply meta b infer meta h peano imply meta a peano imply meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     hypothetical inference inference axiom prime a two
   reads
     arbitrary meta h end line
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta h peano imply meta a peano imply meta b peano imply meta c end line

     line ell b premise meta h peano imply meta a peano imply meta b end line

     line ell c hypothesis indeed meta h end line

     line ell d hypothesis because axiom prime a two indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line

     line ell e hypothesis double modus ponens ell d modus ponens ell a modus ponens ell b indeed meta a peano imply meta c end line

                because rule repetition modus ponens ell e indeed meta h peano imply meta a peano imply meta c qed

   end math ]"

\subsubsection{Bevis $1.47\ b_{h}$}
\label{sssec:hyp_one_ fourtyseven_b}

"[ intro
     hypothetical mendelson exercise one fourtyseven b
   pyk
     "hypothetical mendelson exercise one fourtyseven b"
   tex
     "Mendelson\ \textbf{1.47}\ b_{h}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     hypothetical mendelson exercise one fourtyseven b
   says
     all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano imply meta b infer meta h peano imply meta b peano imply meta c infer meta h peano imply meta a peano imply meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     hypothetical mendelson exercise one fourtyseven b
   reads
     arbitrary meta h end line
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta h peano imply meta a peano imply meta b end line

     line ell b premise meta h peano imply meta b peano imply meta c end line

     line ell c hypothesis indeed meta h end line

     line ell d hypothesis raw because hypothetical inference axiom prime a one modus ponens ell b indeed meta a peano imply meta b peano imply meta c end line

     line ell e hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell d modus ponens ell a indeed meta a peano imply meta c end line

                because rule repetition modus ponens ell e indeed meta h peano imply meta a peano imply meta c qed

   end math ]"

\subsubsection{Bevis $1.47\ c_{h}$}

"[ intro
     hypothetical mendelson exercise one fourtyseven c
   pyk
     "hypothetical mendelson exercise one fourtyseven c"
   tex
     "Mendelson\ \textbf{1.47}\ c_{h}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     hypothetical mendelson exercise one fourtyseven c
   says
     all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano imply meta b peano imply meta c infer meta h peano imply meta b peano imply meta a peano imply meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     hypothetical mendelson exercise one fourtyseven c
   reads
     arbitrary meta h end line
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta h peano imply meta a peano imply meta b peano imply meta c end line

     line ell b hypothesis indeed meta h end line

     line ell c hypothesis raw because hypothetical inference axiom prime a two modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line

     line ell e hypothesis raw because hypothetical inference axiom prime a one modus ponens ell c indeed meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line

     line ell f hypothesis because axiom prime a one indeed meta b peano imply meta a peano imply meta b end line

     line ell g hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell e modus ponens ell f indeed meta b peano imply meta a peano imply meta c end line

                because rule repetition modus ponens ell g indeed meta h peano imply meta b peano imply meta a peano imply meta c qed

   end math ]"

\subsection{Flere niveauer af deduktion}

I de foreg\aa{}ende afsnit blev deduktion i et niveau beskrevet, men der kan selv\-f\o{}lge\-lig ogs\aa{} laves deduktion i flere niveauer. Selve overs\ae{}ttelsesalgoritmen fra afsnit \ref{ssec:deduktion_oversaettelse}, kan igen bruges ved blot at starte fra den inderste hypotese og arbejde sig ud. Men igen vil beviserne blive betydelig st\o{}rre og mere komplekse end i \cite{mendelson}. En anden m\aa{}de beviserne kunne udformes, er at bruge de nye beviskonstruktioner til det yderste niveau, og s\aa{} lave det manuelt for de inderste. 
"[ intro
      mendelson lemma one eleven c
   pyk
     "mendelson lemma one eleven c"
   tex
     "Mendelson\ \textbf{1.11}\ c"
   end intro ]"
er et eksempel p\aa{} en s\ae{}tning der bruger 2 niveauer af deduktion. S\ae{}tningen er som f\o{}lger:

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson lemma one eleven c
   says
     all meta a indeed all meta b indeed peano not meta a peano imply meta a peano imply meta b
   end lemma
   end math ]"}

Nedenst\aa{}ende viser beviset af eksemplet: \\

"[ math
     system prime s
   proof of
     mendelson lemma one eleven c
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     ; Line 1
     line ell a hypothesis indeed peano not meta a end line
     ; Line 2
     line ell b hypothesis because mendelson lemma one eight indeed meta a peano imply meta a end line
     ; Line 3
     line ell c hypothesis because axiom prime a one indeed meta a peano imply peano not meta b peano imply meta a end line

     line ell d hypothesis raw because hypothetical inference axiom prime a one modus ponens ell c indeed meta a peano imply meta a peano imply peano not meta b peano imply meta a end line 
     ; Line 4
     line ell e hypothesis because axiom prime a one indeed peano not meta a peano imply peano not meta b peano imply peano not meta a end line

     line ell f hypothesis raw because hypothetical inference axiom prime a one modus ponens ell e indeed meta a peano imply peano not meta a peano imply peano not meta b peano imply peano not meta a end line
     ; Line 5
     line ell g hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell d modus ponens ell b indeed meta a peano imply peano not meta b peano imply meta a end line
     ; Line 6
     line ell h hypothesis modus ponens ell e modus ponens ell a indeed peano not meta b peano imply peano not meta a end line

     line ell i hypothesis raw because hypothetical inference axiom prime a one modus ponens ell h indeed meta a peano imply peano not meta b peano imply peano not meta a end line
     ; Line 7
     line ell j hypothesis because axiom prime a three indeed parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end line

     line ell k hypothesis raw because hypothetical inference axiom prime a one modus ponens ell j indeed meta a peano imply parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end line
     ; Line 8
     line ell l hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell k modus ponens ell i indeed meta a peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end line 
     ; Line 9
     line ell m hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell l modus ponens ell g indeed meta a peano imply meta b end line

                because rule repetition modus ponens ell m indeed peano not meta a peano imply meta a peano imply meta b qed
   end math ]" \\

P\aa{} samme m\aa{}de som der blev lavet nye makrodefinitioner for det f\o{}rste niveau af deduktion, kan der ogs\aa{} laves definitioner for det andet niveau. Disse definitioner er dog ikke defineret i denne rapport, da det vil g\o{}re rapporten un\o{}dvendig l\ae{}ngere fordi der kun vil v\ae{}re minimal brug for det i forhold til beviset af "[ math mendelson proposition three two h end math ]" (kommutativitet for addition).

\subsubsection{Konjunktion af hypoteser}

N\aa{}r man arbejder med deduktion i flere niveauer, kan man ogs\aa{} samle alle hypoteserne til en:

\display{"[ math hypothesis peano and hypothesis peano imply conclusion end math ]"}

Da $\dot{\wedge}$ binder st\ae{}rkere end $\dot{\Rightarrow}$, vil det overfor systemet blive opfattet som en enkelt hypotese. For at fuldf\o{}re disse beviser vil man ogs\aa{} f\aa{} brug for f\o{}lgende s\ae{}tninger: \\

"[ intro
      mendelson exercise one fourtyeight d
   pyk
     "mendelson exercise one fourtyeight d"
   tex
     "Mendelson\ \textbf{1.48}\ d"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson exercise one fourtyeight d
   says
     all meta a indeed all meta b indeed meta a peano and meta b peano imply meta a
   end lemma
   end math ]"}

"[ intro
      mendelson exercise one fourtyeight e
   pyk
     "mendelson exercise one fourtyeight e"
   tex
     "Mendelson\ \textbf{1.48}\ e"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson exercise one fourtyeight e
   says
     all meta a indeed all meta b indeed meta a peano and meta b peano imply meta b
   end lemma
   end math ]"}

"[ intro
      mendelson exercise one fourtyeight h
   pyk
     "mendelson exercise one fourtyeight h"
   tex
     "Mendelson\ \textbf{1.48}\ h"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson exercise one fourtyeight h
   says
     all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a peano and meta b
   end lemma
   end math ]"}


Bem\ae{}rk at disse s\ae{}tninger ikke er bevist, igen fordi der er minimal brug for deduktion i flere niveauer.

\subsection{Beviser med brug af deduktion}

Corollary 1.10 i \cite{mendelson} ligger op til anvendelse af Proposition 1.9, til nogle af de samme beviser som fra Exercise 1.47. Dette eksempel f\o{}lges, og begge s\ae{}tninger fra 1.10 vil blive bevist med de nye konstruktioner. Fremover vil Corollary 1.10 blive brugt i stedet for Exercise 1.47.

\subsubsection{Bevis $1.10\ a$}

"[ intro
      mendelson corollary one ten a
   pyk
     "mendelson corollary one ten a"
   tex
     "Mendelson\ \textbf{1.10}\ a"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson corollary one ten a
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b infer meta b peano imply meta c infer meta a peano imply meta c 
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson corollary one ten a
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano imply meta b end line

     line ell b premise meta b peano imply meta c end line

     line ell c hypothesis indeed meta a end line

     line ell d hypothesis first modus ponens ell a modus ponens ell c indeed meta b end line

     line ell e hypothesis first modus ponens ell b modus ponens ell d indeed meta c end line

                because rule repetition modus ponens ell e indeed meta a peano imply meta c qed
   end math ]"

\subsubsection{Bevis $1.10\ b$}

"[ intro
      mendelson corollary one ten b
   pyk
     "mendelson corollary one ten b"
   tex
     "Mendelson\ \textbf{1.10}\ b"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson corollary one ten b
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b infer meta a peano imply meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson corollary one ten b
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line
  
     line ell a premise meta a peano imply meta b peano imply meta c end line
  
     line ell b premise meta b end line

     line ell c hypothesis indeed meta a end line

     line ell d hypothesis first modus ponens ell a modus ponens ell c indeed meta b peano imply meta c end line

     line ell e hypothesis second modus ponens ell d modus ponens ell b indeed meta c end line

                because rule repetition modus ponens ell e indeed meta a peano imply meta c qed
  end math ]"

\section{Peano Aritmetik}
\label{sec:peano}

\subsection{Introduktion}

Peano aritmetik er en 1. ordens teori, det er derfor naturlig at introducere 1. ordens pr\ae{}dikat teorien f\o{}rst. 1. ordens pr\ae{}dikat teorien bygger videre p\aa{} propositions teorien, beskrevet i afsnit \ref{sec:prop}. Sproget fra propositions teorien er derfor en delm\ae{}ngde af 1. ordens pr\ae{}dikat teoriens sprog: \\

$\cal{F} \rightarrow{} \cal{R}\ ;\ "[ not meta f ]"\ ;\ "[ meta f ]" \Rightarrow{} "[ meta f]"\ ;\ "[ all meta v indeed meta f ]" $ \\
$\cal{R}$ $\rightarrow{}$ $A_{1}(\cal{P})$ ; $A_{2}(\cal{P})$ ; $...$ \\
$\cal{P} \rightarrow{} \cal{T}\ ;\ \cal{T}, \cal{P}$ \\
$\cal{T} \rightarrow{} \cal{V}\ ;\ \cal{C}\ ;\ \cal{T'}$ \\
$\cal{T'}$ $\rightarrow{}$ $f_{1}(\cal{P})$ ; $f_{2}(\cal{P})$ ; $...$ \\
$\cal{C}$ $\rightarrow{}$ $a_{1}$ ; $a_{2}$ ; $...$ \\
$\cal{V}$ $\rightarrow{}$ $x_{1}$ ; $x_{2}$ ; $...$ \\

Hvor $\cal{F}$ angiver formler, $\cal{R}$ relationssymboler, $\cal{P}$ parameterliste, $\cal{T}$ termer, $\cal{T'}$ funktioner, $\cal{C}$ konstanter og $\cal{V}$ variabler. 1. ordens teorien udbygger propositions teorien med yderlige 3 aksiomer:

\display{$A4':$ "[ math all meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub endorse peano all meta x indeed meta b peano imply meta a end math ]"}

\display{$A5':$ "[ math all meta x indeed all meta a indeed all meta b indeed peano nonfree quote meta x end quote in quote meta a end quote end nonfree endorse peano all meta x indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply peano all meta x indeed meta b end math ]"}

\display{$Gen':$ "[ math all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end math ]"}

Tegnet $\makebox [0mm][l]{$\vdash $}\,{\vdash }$ angiver sidebetingelser - alts\aa{} ting der skal v\ae{}re opfyldt f\o{}r aksiomet m\aa{} benyttes. Sidebetingelserne i $A4'$ og $A5'$ behandler ting som validering af substitution og betingelsen 'ikke fri for'. En ny ting i aksiomerne er $\dot{\forall}$, som er en objektkvantor der variere over variabler - i mods\ae{}tning til $\forall$ der variere over termer/formler.

Peano aritmetik har et enkelt relationssymbol, $=$ som herefter vil blive kalde lighed. Desuden har teorien en enkelt konstant 0 (nul) og tre funktioner $x'$, $x + y$ og $x \cdot{} y$. $x'$ er en efterf\o{}lger-funktion der giver det n\ae{}ste tal efter x, $x + y$ er addition og $x \cdot{} y$ er multiplikation.

Peano's teori har desuden f\o{}lgende aksiomer:

\display{$S1':$ "[ math all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end math ]"}

\display{$S2':$ "[ math all meta a indeed all meta b indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end math ]"}

\display{$S3':$ "[ math all meta a indeed not peano zero peano is meta a peano succ end math ]"}

\display{$S4':$ "[ math all meta a indeed all meta b indeed meta a peano succ peano is meta b peano succ peano imply meta a peano is meta b end math ]"}

\display{$S5':$ "[ math all meta a indeed meta a peano plus peano zero peano is meta a end math ]"}

\display{$S6':$ "[ math all meta a indeed all meta b indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end math ]"}

\display{$S7':$ "[ math all meta a indeed meta a peano times peano zero peano is peano zero end math ]"}

\display{$S8':$ "[ math all meta a indeed all meta b indeed meta a peano times parenthesis meta b peano succ end parenthesis peano is parenthesis meta a peano times meta b end parenthesis peano plus meta a end math ]"}

\display{$S9':$ "[ math all meta a indeed all meta b indeed all meta c indeed all meta x indeed macro newline peano sub meta b is meta a where meta x is peano zero end sub endorse peano sub meta c is meta a where meta x is meta x peano succ end sub endorse macro newline meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end math ]"}

Det f\o{}rste der springer en i \o{}jne n\aa{}r man ser aksiomerne er nok de prikker der er sat over alle operatorerne, samt p'et over lighedsoperatoren. Disse tegn har til form\aa{}l at skelne peano relaterede ting fra lignende ting defineret p\aa{} basis-side. Eksempelvis at skelne peano addition fra almindelig addition.

Ud fra $S1'$ (og lidt ekstra) kan det bevises at lighed er en \ae{}kvivalensrelation. $S5'$ til $S8'$ behandler rekursion af addition samt multiplikation og $S9'$ siger at princippet om matematisk induktion g\ae{}lder i peano aritmetik.

\subsection{Simple beviser i peano aritmetik}

Dette afsnit indeholder mest inferens- og hypotetiske-beviser af aksiomerne, men ogs\aa{} et par interessante beviser omkring induktion. Beviserne er lavet s\aa{} der kan spares et par linjer i senere beviser.

\subsubsection{Bevis $S1'_{i}$}

"[ intro
      inference axiom prime s one
   pyk
     "inference axiom prime s one"
   tex
     "S1'_{i}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     inference axiom prime s one
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b infer meta a peano is meta c peano imply meta b peano is meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     inference axiom prime s one
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano is meta b end line

     line ell b because axiom prime s one indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end line

                because ell b macro modus ponens ell a indeed meta a peano is meta c peano imply meta b peano is meta c qed

   end math ]"

\subsubsection{Bevis $S1'_{ii}$}

"[ intro
      inference inference axiom prime s one
   pyk
     "inference inference axiom prime s one"
   tex
     "S1'_{ii}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     inference inference axiom prime s one
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b infer meta a peano is meta c infer meta b peano is meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     inference inference axiom prime s one
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano is meta b end line

     line ell b premise meta a peano is meta c end line

     line ell c because inference axiom prime s one modus ponens ell a indeed meta a peano is meta c peano imply meta b peano is meta c end line

                because ell c macro modus ponens ell b indeed meta b peano is meta c qed

   end math ]"

\subsubsection{Bevis $S2'_{i}$}

"[ intro
      inference axiom prime s two
   pyk
     "inference axiom prime s two"
   tex
     "S2'_{i}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     inference axiom prime s two
   says
     all meta a indeed all meta b indeed meta a peano is meta b infer meta a peano succ peano is meta b peano succ 
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     inference axiom prime s two
   reads
     arbitrary meta a end line
     arbitrary meta b end line

     line ell a premise meta a peano is meta b end line

     line ell b because axiom prime s two indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end line

                because ell b macro modus ponens ell a indeed meta a peano succ peano is meta b peano succ qed

   end math ]"

\subsubsection{Bevis $S2'_{ih}$}

"[ intro
      hypothetical inference axiom prime s two
   pyk
     "hypothetical inference axiom prime s two"
   tex
     "S2'_{ih}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     hypothetical inference axiom prime s two
   says
     all meta h indeed all meta a indeed all meta b indeed meta h peano imply meta a peano is meta b infer meta h peano imply meta a peano succ peano is meta b peano succ
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     hypothetical inference axiom prime s two
   reads
     arbitrary meta h end line
     arbitrary meta a end line
     arbitrary meta b end line

     line ell a premise meta h peano imply meta a peano is meta b end line

     line ell b hypothesis indeed meta h end line

     line ell c hypothesis because axiom prime s two indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end line

     line ell d hypothesis modus ponens ell c modus ponens ell a indeed meta a peano succ peano is meta b peano succ end line

                because rule repetition modus ponens ell d indeed meta h peano imply meta a peano succ peano is meta b peano succ qed

   end math ]"

\subsubsection{Bevis $S9'_{ii}$}

"[ intro
      inference inference axiom prime s nine
   pyk
     "inference inference axiom prime s nine"
   tex
     "S9'_{ii}"
   end intro ]"
er en inferens-version af induktions-aksiomet. I selve s\ae{}tningen, er to implikationsoperatoere blevet udskiftet:

\display{
"[ math 
   in theory 
     system prime s 
   lemma 
     inference inference axiom prime s nine
   says
     all meta a indeed all meta b indeed all meta c indeed all meta y indeed peano sub meta b is meta a where meta y is peano zero end sub endorse peano sub meta c is meta a where meta y is meta y peano succ end sub endorse macro newline meta b infer peano all meta y indeed parenthesis meta a peano imply meta c end parenthesis infer peano all meta y indeed meta a 
   end lemma 
   end math ]"}

Selve beviset er ligefrem, det skal dog bem\ae{}rkes hvordan sidebetingelser kan elimineres: \\

"[ math
     system prime s
   proof of
     inference inference axiom prime s nine
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line
     arbitrary meta y end line

     line ell a side condition peano sub meta b is meta a where meta y is peano zero end sub end line

     line ell b side condition peano sub meta c is meta a where meta y is meta y peano succ end sub end line

     line ell c premise meta b end line

     line ell d premise peano all meta y indeed parenthesis meta a peano imply meta c end parenthesis end line

     line ell e because axiom prime s nine modus probans ell a modus probans ell b indeed meta b peano imply peano all meta y indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta y indeed meta a end line

                because ell e macro first modus ponens ell c macro second modus ponens ell d indeed peano all meta y indeed meta a qed

   end math ]"

\subsubsection{Bevis $Induction$}

For at lette anvendelsen af induktion er s\ae{}tningen
"[ intro
      rule induction
   pyk
     "rule induction"
   tex
     "Induction"
   end intro ]"
blevet lavet, s\ae{}tningen siger f\o{}lgende:

\display{
"[ math
   in theory
     system prime s
   lemma
     rule induction
   says
     all meta a indeed all meta b indeed all meta c indeed all meta y indeed peano sub meta b is meta a where meta y is peano zero end sub endorse peano sub meta c is meta a where meta y is meta y peano succ end sub endorse macro newline peano sub quote meta a end quote is quote meta a end quote where quote meta y end quote is quote meta y end quote end sub endorse meta b infer meta a peano imply meta c infer meta a
   end lemma
   end math ]"}

Grundtanken med s\ae{}tningen er at anvende den direkte p\aa{} ens basis og induktionsskridt, for direkte at f\aa{} det \o{}nskede resultat. I s\ae{}tningen er der tilf\o{}jet en ekstra sidebetingelse, s\aa{} $A4'$ kan instancieres: \\

"[ math
     system prime s
   proof of
     rule induction
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line
     arbitrary meta y end line

     line ell a side condition peano sub meta b is meta a where meta y is peano zero end sub end line

     line ell b side condition peano sub meta c is meta a where meta y is meta y peano succ end sub end line

     line ell w side condition peano sub quote meta a end quote is quote meta a end quote where quote meta y end quote is quote meta y end quote end sub end line

     line ell c premise meta b end line

     line ell d premise meta a peano imply meta c end line

     line ell e because rule prime gen modus ponens ell d indeed peano all meta y indeed parenthesis meta a peano imply meta c end parenthesis end line

     line ell f because inference inference axiom prime s nine modus probans ell a modus probans ell b modus ponens ell c modus ponens ell e indeed peano all meta y indeed meta a end line

     line ell g because axiom prime a four modus probans ell w indeed peano all meta y indeed meta a peano imply meta a end line
 
                because ell g macro modus ponens ell f indeed meta a qed  

   end math ]"

\subsection{Beviser i proposition 3.2}

Dette afsnit fremf\o{}re det endelige bevis, beviserne f\o{}lger \cite{mendelson} meget t\ae{}t. Der bevises desuden en r\ae{}kke inferensversioner af s\ae{}tningerne.

\subsubsection{Bevis $3.2\ a$}

"[ intro 
      mendelson proposition three two a
   pyk 
     "mendelson proposition three two a"
   tex 
     "Mendelson\ \textbf{3.2}\ a" 
   end intro ]"

\display{
"[ math 
   in theory 
     system prime s 
   lemma 
     mendelson proposition three two a
   says 
     all meta a indeed meta a peano is meta a
   end lemma 
   end math ]"}

"[ math
     system prime s
   proof of 
     mendelson proposition three two a
   reads
     arbitrary meta a end line

     line ell a because axiom prime s five indeed meta a peano plus peano zero peano is meta a end line
     
                because inference inference axiom prime s one modus ponens ell a modus ponens ell a indeed meta a peano is meta a qed
     
   end math ]"

\subsubsection{Bevis $3.2\ b$}

"[ intro
      mendelson proposition three two b
   pyk
     "mendelson proposition three two b"
   tex
     "Mendelson\ \textbf{3.2}\ b"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two b
   says
     all meta a indeed all meta b indeed meta a peano is meta b peano imply meta b peano is meta a
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two b
   reads
     arbitrary meta a end line
     arbitrary meta b end line

     line ell a because axiom prime s one indeed meta a peano is meta b peano imply meta a peano is meta a peano imply meta b peano is meta a end line

     line ell b because mendelson proposition three two a indeed meta a peano is meta a end line

                because mendelson corollary one ten b modus ponens ell a modus ponens ell b indeed meta a peano is meta b peano imply meta b peano is meta a qed

   end math ]"

\subsubsection{Bevis $3.2\ b_{i}$}

"[ intro
      inference mendelson proposition three two b
   pyk
     "inference mendelson proposition three two b"
   tex
     "Mendelson\ \textbf{3.2}\ b_{i}"
   end intro ]"

"[ math
   in theory
     system prime s
   lemma
     inference mendelson proposition three two b
   says
     all meta a indeed all meta b indeed meta a peano is meta b infer meta b peano is meta a
   end lemma
   end math ]"

"[ math
     system prime s
   proof of
     inference mendelson proposition three two b
   reads
     arbitrary meta a end line
     arbitrary meta b end line

     line ell a premise meta a peano is meta b end line

     line ell b because mendelson proposition three two b indeed meta a peano is meta b peano imply meta b peano is meta a end line

                because ell b macro modus ponens ell a indeed meta b peano is meta a qed

   end math ]"

\subsubsection{Bevis $3.2\ c$}

"[ intro
      mendelson proposition three two c
   pyk
     "mendelson proposition three two c"
   tex
     "Mendelson\ \textbf{3.2}\ c"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two c
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c 
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two c
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a because axiom prime s one indeed meta b peano is meta a peano imply meta b peano is meta c peano imply meta a peano is meta c end line

     line ell b because mendelson proposition three two b indeed meta a peano is meta b peano imply meta b peano is meta a end line

                because mendelson corollary one ten a modus ponens ell b modus ponens ell a indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c qed

   end math ]" \\

"[ math mendelson proposition three two a end math ]" (refleksivititet), "[ math mendelson proposition three two b end math ]" (symmetri) og\linebreak[4] "[ math mendelson proposition three two c end math ]" (transitivitet) udg\o{}r tilsammen beviset for at lighed i peano aritmetik er en \ae{}kvivalensrelation. 

\subsubsection{Bevis $3.2\ c_{ii}$}

"[ intro
      inference inference mendelson proposition three two c
   pyk
     "inference inference mendelson proposition three two c"
   tex
     "Mendelson\ \textbf{3.2}\ c_{ii}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     inference inference mendelson proposition three two c
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b infer meta b peano is meta c infer meta a peano is meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     inference inference mendelson proposition three two c
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano is meta b end line

     line ell b premise meta b peano is meta c end line

     line ell c because mendelson proposition three two c indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c end line

                because ell c macro first modus ponens ell a macro second modus ponens ell b indeed meta a peano is meta c qed

   end math ]"

\subsubsection{Bevis $3.2\ c_{iih}$}

"[ intro
      hypothetical inference inference mendelson proposition three two c
   pyk
     "hypothetical inference inference mendelson proposition three two c"
   tex
     "Mendelson\ \textbf{3.2}\ c_{iih}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     hypothetical inference inference mendelson proposition three two c
   says
     all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano is meta b infer meta h peano imply meta b peano is meta c infer meta h peano imply meta a peano is meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     hypothetical inference inference mendelson proposition three two c
   reads
     arbitrary meta h end line
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta h peano imply meta a peano is meta b end line

     line ell b premise meta h peano imply meta b peano is meta c end line

     line ell c hypothesis indeed meta h end line

     line ell d hypothesis because mendelson proposition three two c indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c end line

     line ell e hypothesis double modus ponens ell d modus ponens ell a modus ponens ell b indeed meta a peano is meta c end line

                because rule repetition modus ponens ell e indeed meta h peano imply meta a peano is meta c qed

   end math ]"

\subsubsection{Bevis $3.2\ d$}

"[ intro
      mendelson proposition three two d
   pyk
     "mendelson proposition three two d"
   tex
     "Mendelson\ \textbf{3.2}\ d"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two d
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta c peano is meta b peano imply meta a peano is meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two d
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a because mendelson proposition three two c indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c end line

     line ell b because mendelson exercise one fourtyseven c modus ponens ell a indeed meta b peano is meta c peano imply meta a peano is meta b peano imply meta a peano is meta c end line

     line ell c because mendelson proposition three two b indeed meta c peano is meta b peano imply meta b peano is meta c end line

     line ell d because mendelson corollary one ten a modus ponens ell c modus ponens ell b indeed meta c peano is meta b peano imply meta a peano is meta b peano imply meta a peano is meta c end line

                because mendelson exercise one fourtyseven c modus ponens ell d indeed meta a peano is meta b peano imply meta c peano is meta b peano imply meta a peano is meta c qed

   end math ]"

\subsubsection{Bevis $3.2\ d_{ii}$}

"[ intro
      inference inference mendelson proposition three two d
   pyk
     "inference inference mendelson proposition three two d"
   tex
     "Mendelson\ \textbf{3.2}\ d_{ii}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     inference inference mendelson proposition three two d
   says
     all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b infer meta c peano is meta b infer meta a peano is meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     inference inference mendelson proposition three two d
   reads
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta a peano is meta b end line

     line ell b premise meta c peano is meta b end line

     line ell c because mendelson proposition three two d indeed meta a peano is meta b peano imply meta c peano is meta b peano imply meta a peano is meta c end line

                because ell c macro first modus ponens ell a macro second modus ponens ell b indeed meta a peano is meta c qed

   end math ]"

\subsubsection{Bevis $3.2\ d_{iih}$}

"[ intro
      hypothetical inference inference mendelson proposition three two d
   pyk
     "hypothetical inference inference mendelson proposition three two d"
   tex
     "Mendelson\ \textbf{3.2}\ d_{iih}"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     hypothetical inference inference mendelson proposition three two d
   says
     all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano is meta b infer meta h peano imply meta c peano is meta b infer meta h peano imply meta a peano is meta c
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     hypothetical inference inference mendelson proposition three two d
   reads
     arbitrary meta h end line
     arbitrary meta a end line
     arbitrary meta b end line
     arbitrary meta c end line

     line ell a premise meta h peano imply meta a peano is meta b end line

     line ell b premise meta h peano imply meta c peano is meta b end line

     line ell c hypothesis indeed meta h end line

     line ell d hypothesis because mendelson proposition three two d indeed meta a peano is meta b peano imply meta c peano is meta b peano imply meta a peano is meta c end line

     line ell e hypothesis double modus ponens ell d modus ponens ell a modus ponens ell b indeed meta a peano is meta c end line

                because rule repetition modus ponens ell e indeed meta h peano imply meta a peano is meta c qed

   end math ]"

\subsubsection{Bevis $3.2\ f$}

"[ intro
      mendelson proposition three two f i
   pyk
     "mendelson proposition three two f i"
   tex
     "Mendelson\ \textbf{3.2}\ f\ i"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two f i
   says
     peano zero peano is peano zero peano plus peano zero
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two f i
   reads
     line ell a because axiom prime s five indeed peano zero peano plus peano zero peano is peano zero end line

                because inference mendelson proposition three two b modus ponens ell a indeed peano zero peano is peano zero peano plus peano zero qed

   end math ]" \\

"[ intro
      mendelson proposition three two f ii
   pyk
     "mendelson proposition three two f ii"
   tex
     "Mendelson\ \textbf{3.2}\ f\ ii"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two f ii
   says
     peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ  
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two f ii
   reads
     ; Line 1
     line ell a hypothesis indeed peano x peano is peano zero peano plus peano x end line
     ; Line 2
     line ell b hypothesis because axiom prime s six indeed peano zero peano plus peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ end line

     ; Line 3
     line ell c hypothesis raw because hypothetical inference axiom prime s two modus ponens ell a indeed peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ end line

     ; Line 4
     line ell d hypothesis raw because hypothetical inference inference mendelson proposition three two d modus ponens ell c modus ponens ell b indeed peano x peano succ peano is peano zero peano plus peano x peano succ end line

                because rule repetition modus ponens ell d indeed peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ qed

   end math ]" \\

"[ intro
      mendelson proposition three two f 
   pyk
     "mendelson proposition three two f"
   tex
     "Mendelson\ \textbf{3.2}\ f"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two f
   says
     peano x peano is peano zero peano plus peano x
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two f
   reads
     line ell a because mendelson proposition three two f i indeed peano zero peano is peano zero peano plus peano zero end line

     line ell b because mendelson proposition three two f ii indeed peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end line

                because rule induction modus ponens ell a modus ponens ell b indeed peano x peano is peano zero peano plus peano x qed

   end math ]"

\subsubsection{Bevis $3.2\ g$}

I denne s\ae{}tning er $x$ og $y$ blevet byttet om, ombytningen er gjort s\aa{} den kommer til at passe i beviset til "[ math mendelson proposition three two h end math ]". \\

"[ intro
      mendelson proposition three two g i
   pyk
     "mendelson proposition three two g i"
   tex
     "Mendelson\ \textbf{3.2}\ g\ i"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two g i
   says
     peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two g i
   reads
     ; Line 1
     line ell a because axiom prime s five indeed peano y peano succ peano plus peano zero peano is peano y peano succ end line
     ; Line 2
     line ell b because axiom prime s five indeed peano y peano plus peano zero peano is peano y end line
     ; Line 3
     line ell c because inference axiom prime s two modus ponens ell b indeed parenthesis peano y peano plus peano zero end parenthesis peano succ peano is peano y peano succ end line
     ; Line 4
                because inference inference mendelson proposition three two d modus ponens ell a modus ponens ell c indeed peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ qed

   end math ]"

"[ intro
      mendelson proposition three two g ii
   pyk
     "mendelson proposition three two g ii"
   tex
     "Mendelson\ \textbf{3.2}\ g\ ii"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two g ii
   says
     peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two g ii
   reads
     ; Line 1
     line ell a hypothesis indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line
     ; Line 2
     line ell b hypothesis because axiom prime s six indeed peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano succ peano plus peano x end parenthesis peano succ end line
     ; Line 3
     line ell c hypothesis raw because hypothetical inference axiom prime s two modus ponens ell a indeed parenthesis peano y peano succ peano plus peano x end parenthesis peano succ peano is parenthesis parenthesis peano y peano plus peano x end parenthesis peano succ end parenthesis peano succ end line
     ; Line 4
     line ell e hypothesis raw because hypothetical inference inference mendelson proposition three two c modus ponens ell b modus ponens ell c indeed peano y peano succ peano plus peano x peano succ peano is parenthesis parenthesis peano y peano plus peano x end parenthesis peano succ end parenthesis peano succ end line
     ; Line 5
     line ell g hypothesis because axiom prime s six indeed peano y peano plus peano x peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line
     ; Line 6
     line ell h hypothesis raw because hypothetical inference axiom prime s two modus ponens ell g indeed parenthesis peano y peano plus peano x peano succ end parenthesis peano succ peano is parenthesis parenthesis peano y peano plus peano x end parenthesis peano succ end parenthesis peano succ end line
     ; Line 7
     line ell j hypothesis raw because hypothetical inference inference mendelson proposition three two d modus ponens ell e modus ponens ell h indeed peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ end line

                because rule repetition modus ponens ell j indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ qed 
   end math ]"


"[ intro
      mendelson proposition three two g
   pyk
     "mendelson proposition three two g"
   tex
     "Mendelson\ \textbf{3.2}\ g"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two g
   says
     peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ 
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two g
   reads
     line ell a because mendelson proposition three two g i indeed peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ end line
     
     line ell b because mendelson proposition three two g ii indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ end line

                because rule induction modus ponens ell a modus ponens ell b indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ qed

   end math ]"

\subsubsection{Bevis $3.2\ h$}
\label{ssec:peano_three_two_h}

"[ intro
      mendelson proposition three two h i
   pyk
     "mendelson proposition three two h i"
   tex
     "Mendelson\ \textbf{3.2}\ h\ i"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two h i
   says
     peano x peano plus peano zero peano is peano zero peano plus peano x
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two h i
   reads
     ; Line 1
     line ell a because axiom prime s five indeed peano x peano plus peano zero peano is peano x end line
     ; Line 2
     line ell b because mendelson proposition three two f indeed peano x peano is peano zero peano plus peano x end line
     ; Line 3
                because inference inference mendelson proposition three two c modus ponens ell a modus ponens ell b indeed peano x peano plus peano zero peano is peano zero peano plus peano x qed 

   end math ]"

"[ intro
      mendelson proposition three two h ii
   pyk
     "mendelson proposition three two h ii"
   tex
     "Mendelson\ \textbf{3.2}\ h\ ii"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two h ii
   says
     peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two h ii
   reads
     ; Line 1
     line ell a hypothesis indeed peano x peano plus peano y peano is peano y peano plus peano x end line 
     ; Line 2 
     line ell b hypothesis because axiom prime s six indeed peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ end line
     ; Line 3
     line ell c hypothesis because mendelson proposition three two g indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line
     ; Line 4
     line ell d hypothesis raw because hypothetical inference axiom prime s two modus ponens ell a indeed parenthesis peano x peano plus peano y end parenthesis peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line
     ; Line 5
     line ell f hypothesis raw because hypothetical inference inference mendelson proposition three two c modus ponens ell b modus ponens ell d indeed peano x peano plus peano y peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line
     ; Line 6
     line ell h hypothesis raw because hypothetical inference inference mendelson proposition three two d modus ponens ell f modus ponens ell c indeed peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end line

                because rule repetition modus ponens ell h indeed peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x qed

   end math ]"

"[ intro
      mendelson proposition three two h
   pyk
     "mendelson proposition three two h"
   tex
     "Mendelson\ \textbf{3.2}\ h"
   end intro ]"

\display{
"[ math
   in theory
     system prime s
   lemma
     mendelson proposition three two h
   says
     peano x peano plus peano y peano is peano y peano plus peano x
   end lemma
   end math ]"}

"[ math
     system prime s
   proof of
     mendelson proposition three two h
   reads
     line ell a because mendelson proposition three two h i indeed peano x peano plus peano zero peano is peano zero peano plus peano x end line

     line ell b because mendelson proposition three two h ii indeed peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end line

                because rule induction modus ponens ell a modus ponens ell b indeed peano x peano plus peano y peano is peano y peano plus peano x qed

   end math ]"

\appendix

\section{Diverse}

"[ math pyk define logic as "logic" end define end math ]"


\section{\TeX\ Definitioner}
\label{sec:tex}

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\immediate\closeout\outex
\input{./page.otx}
\item \mbox{}
\end{list}

%\section{Test}

%\begin{list}{}{
%\setlength{\leftmargin}{5em}
%\setlength{\itemindent}{-5em}}
%\immediate\closeout\outest
%\input{./page.tst}
%\end{list}

\section{Prioritets Tabel}
\label{sec:prioritets_tabel}
"[ flush left math priority table Priority end table end math end left ]"

\section{Litteratur}

\bibliography{./page}

\end{document}

End of file
File page.bib
@book         {mendelson,
  author =    {Elliott Mendelson},
  title =     {Introduction to Mathematical Logic},
  publisher = {Chapman and Hall/CRC},
  year =      {1997},
  edition =   {4.}}

@book         {grue:base,
  author =    {Klaus Grue},
  title =     {A Logiweb base page},
  publisher = {http://www.diku.dk/~grue/logiweb/ 20050502/home/grue/base/latest/},
  year =      {2005}}

@book         {grue:peano,
  author =    {Klaus Grue},
  title =     {Peano arithmetic},
  publisher = {http://www.diku.dk/~grue/logiweb/ 20050502/home/grue/peano-axioms/latest/},
  year =      {2005}}

End of file
File body.pyk
PAGE name

BIBLIOGRAPHY
base: refference

PREASSOCIATIVE  * fac
POSTASSOCIATIVE * apply *

BODY
''files and content

commands''
End of file
File fac.pyk
math pyk define var x fac as ''* fac'' end define end math  ; Definition 1

math tex define var x fac as ''#1.!'' end define end math  ; Definition 2

math
  value define
    var x fac
  as
    tagged if var x tagged equal zero then
      one
    else
      var x times parenthesis var x minus one end parenthesis fac end if
  end define
end math  ; Definition 3
End of file
latex page
makeindex page
bibtex page
latex page
makeindex page
latex page"