"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
"
begin ragged right
end "
\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 "
begin math mendelson proposition three two h end math
end " 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 "
begin math mendelson proposition three two h end math
end " 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 "
begin math mendelson proposition three two g end math
end " 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}$ ; $"
begin not metavar var t end metavar
end "$ ; $\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':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end math
end "}
\display{$A2':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end math
end "}
\display{$A3':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end math
end "}
Samt en enkelt inferens regel:
\display{$MP':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar end math
end "}
\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 "
begin math axiom prime a one end math
end ", 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}
"
begin math inference axiom prime a one end math
end " 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 "
begin math system prime s end math
end ", 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
"
begin math define pyk of var x macro modus ponens var y as text "* macro modus ponens *" end text end define end math
then math define tex of var x macro modus ponens var y as text "#1.
\unrhd #2." end text end define end math
end "
, som bliver makrodefinert til
"
begin math define macro of var x macro modus ponens var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x macro modus ponens var y as rule prime mp modus ponens var x modus ponens var y end define end quote end define end define end math
end ".
\subsubsection{Bevis $MP'_{d}$}
Det f\o{}rste bevis er
"
begin math define pyk of double rule prime mp as text "double rule prime mp" end text end define end math
then math define tex of double rule prime mp as text "MP'_{d}" end text end define end math
end "
som blot er en dobbelt anvendelse af "
begin math rule prime mp end math
end ". Denne s\ae{}tning reducerer typisk andre beviser med en linje. S\ae{}tningen er:
\display{
"
begin math define statement of double rule prime mp as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar infer metavar var b end metavar infer metavar var c end metavar end define end math
end "}
"
begin math define proof of double rule prime mp as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar infer metavar var b end metavar infer rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar conclude metavar var c end metavar end quote state proof state cache var c end expand end define end math
end " \\
Idet "
begin math double rule prime mp end math
end " er bevist, f\o{}lges eksemplet fra f\o{}r og
"
begin math define pyk of var x macro first modus ponens var y macro second modus ponens var z as text "* macro first modus ponens * macro second modus ponens *" end text end define end math
then math define tex of var x macro first modus ponens var y macro second modus ponens var z as text "#1.
\unrhd #2.
\unrhd #3." end text end define end math
end "
introduceres, der p\aa{} samme m\aa{}de er makrodefineret til den dobbelte anvendelse
"
begin math define macro of var x macro first modus ponens var y macro second modus ponens var z as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "
.
\subsubsection{Bevis $A1'_{i}$}
Lemmaet
"
begin math define pyk of inference axiom prime a one as text "inference axiom prime a one" end text end define end math
then math define tex of inference axiom prime a one as text "A1'_{i}" end text end define end math
end "
er en inferens version af "
begin math axiom prime a one end math
end ", som det ses i s\ae{}tningen er en implikations-operator blevet udskiftet med en inferens-operator:
\display{
"
begin math define statement of inference axiom prime a one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer metavar var b end metavar peano imply metavar var a end metavar end define end math
end "}
Beviset f\o{}leger: \\
"
begin math define proof of inference axiom prime a one as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer axiom prime a one conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end " \\
Da denne s\ae{}tning er essentiel i nogle af de f\o{}lgende afsnit, gives den navnet
"
begin math define pyk of rule hypothesize as text "rule hypothesize" end text end define end math
then math define tex of rule hypothesize as text "Hypothesize" end text end define end math
end "
, der er makrodefineret til s\ae{}tningen selv
"
begin math define macro of rule hypothesize as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define rule hypothesize as inference axiom prime a one end define end quote end define end define end math
end "
\subsubsection{Bevis $A2'_{i}$}
"
begin math define pyk of inference axiom prime a two as text "inference axiom prime a two" end text end define end math
then math define tex of inference axiom prime a two as text "A2'_{i}" end text end define end math
end "
er endnu en inferens version af et aksiom. Lemmaet og beviset er som nedenst\aa{}ende:
\display{
"
begin math define statement of inference axiom prime a two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
"
begin math define proof of inference axiom prime a two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer axiom prime a two conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $A2'_{ii}$}
"
begin math define pyk of inference inference axiom prime a two as text "inference inference axiom prime a two" end text end define end math
then math define tex of inference inference axiom prime a two as text "A2'_{ii}" end text end define end math
end "
er den f\o{}rste dobbelte inferens version af et lemma, som det ses i
\display{
"
begin math define statement of inference inference axiom prime a two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
udskiftes to implikations-operatorer - heraf de to \textit{i}er. I beviset kan den foreg\aa{}ende s\ae{}tning udnyttes: \\
"
begin math define proof of inference inference axiom prime a two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var b end metavar infer inference axiom prime a two modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end " \\
Anskues "
begin math inference inference axiom prime a two end math
end ", ses det at lighederne med "
begin math rule prime mp end math
end " er mange. Reelt er det en hypotetisk version af "
begin math rule prime mp end math
end ", derfor bliver
"
begin math define pyk of hypothetical rule prime mp as text "hypothetical rule prime mp" end text end define end math
then math define tex of hypothetical rule prime mp as text "MP'_{h}" end text end define end math
end "
defineret til
"
begin math define macro of hypothetical rule prime mp as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define hypothetical rule prime mp as inference inference axiom prime a two end define end quote end define end define end math
end "
. Modus ponens blev f\o{}r defineret med $\unrhd{}$, herefter vil den hypotetiske version af denne (
"
begin math define pyk of var x hypothetical macro modus ponens var y as text "* hypothetical macro modus ponens *" end text end define end math
then math define tex of var x hypothetical macro modus ponens var y as text "#1.
\unrhd_h #2." end text end define end math
end "
) blive defineret til
"
begin math define macro of var x hypothetical macro modus ponens var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "
.
\subsubsection{Bevis $A2'_{iid}$}
Den f\o{}rste brug af dobbelt-navnet ses af
"
begin math define pyk of double inference inference axiom prime a two as text "double inference inference axiom prime a two" end text end define end math
then math define tex of double inference inference axiom prime a two as text "A2'_{iid}" end text end define end math
end "
. S\ae{}tningen
\display{
"
begin math define statement of double inference inference axiom prime a two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar infer metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var d end metavar end define end math
end "}
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 "
begin math inference inference axiom prime a two end math
end ": \\
"
begin math define proof of double inference inference axiom prime a two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar infer metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar peano imply metavar var c end metavar infer inference inference axiom prime a two modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar cut inference inference axiom prime a two modus ponens metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var d end metavar modus ponens metavar var a end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var d end metavar end quote state proof state cache var c end expand end define end math
end " \\
Forholdes lemmaet til "
begin math double inference inference axiom prime a two end math
end ", ses det at dette er en dobbelt hypotetisk modus ponens.
"
begin math define pyk of double hypothetical rule prime mp as text "double hypothetical rule prime mp" end text end define end math
then math define tex of double hypothetical rule prime mp as text "MP'_{hd}" end text end define end math
end "
bliver derfor makrodefineret til
"
begin math define macro of double hypothetical rule prime mp as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define double hypothetical rule prime mp as double inference inference axiom prime a two end define end quote end define end define end math
end "
. P\aa{} samme m\aa{}de som f\o{}r bliver
"
begin math define pyk of var x hypothetical macro first modus ponens var y hypothetical macro second modus ponens var var z as text "* hypothetical macro first modus ponens * hypothetical macro second modus ponens var *" end text end define end math
then math define tex of var x hypothetical macro first modus ponens var y hypothetical macro second modus ponens var var z as text "#1.
\unrhd_h #2.
\unrhd_h #3." end text end define end math
end "
defineret
"
begin math define macro of var x hypothetical macro first modus ponens var y hypothetical macro second modus ponens var var z as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x hypothetical macro first modus ponens var y hypothetical macro second modus ponens var var z as double hypothetical rule prime mp modus ponens var x modus ponens var y modus ponens var z end define end quote end define end define end math
end "
.
\subsubsection{Bevis $1.8$}
"
begin math define pyk of mendelson lemma one eight as text "mendelson lemma one eight" end text end define end math
then math define tex of mendelson lemma one eight as text "Mendelson\ \textbf{1.8}" end text end define end math
end "
er et grundl\ae{}ggende bevis i \cite{mendelson}. S\ae{}tningen -
\display{
"
begin math define statement of mendelson lemma one eight as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano imply metavar var a end metavar end define end math
end "}
- siger at noget medf\o{}rer sig selv. \\
"
begin math define proof of mendelson lemma one eight as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed axiom prime a one conclude metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar cut axiom prime a one conclude metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar cut inference inference axiom prime a two modus ponens metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar modus ponens metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar conclude metavar var a end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end " \\
Ovenst\aa{}ende bevis af "
begin math mendelson lemma one eight end math
end " 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
"
begin math define pyk of inference mendelson lemma one eight as text "inference mendelson lemma one eight" end text end define end math
then math define tex of inference mendelson lemma one eight as text "Mendelson\ \textbf{1.8}_{i}" end text end define end math
end "
som siger
"
begin math define statement of inference mendelson lemma one eight as system prime s infer all metavar var a end metavar indeed metavar var a end metavar infer metavar var a end metavar end define end math
end "
, kan virke besynderligt, men efterf\o{}lgende vil dette vise sig nyttigt: \\
"
begin math define proof of inference mendelson lemma one eight as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed metavar var a end metavar infer mendelson lemma one eight conclude metavar var a end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var a end metavar modus ponens metavar var a end metavar conclude metavar var a end metavar end quote state proof state cache var c end expand end define end math
end " \\
Beviet navngives
"
begin math define pyk of rule repetition as text "rule repetition" end text end define end math
then math define tex of rule repetition as text "Repetition" end text end define end math
end "
via makrodefinitionen \linebreak[4]
"
begin math define macro of rule repetition as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define rule repetition as inference mendelson lemma one eight end define end quote end define end define end math
end "
.
\subsubsection{Bevis $1.47\ b$}
"
begin math define pyk of mendelson exercise one fourtyseven b as text "mendelson exercise one fourtyseven b" end text end define end math
then math define tex of mendelson exercise one fourtyseven b as text "Mendelson\ \textbf{1.47}\ b" end text end define end math
end "
er en form for transitivets lemma p\aa{} implikation:
\display{
"
begin math define statement of mendelson exercise one fourtyseven b as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
Beviset udnytter flere af de foreg\aa{}ende lemmaer: \\
"
begin math define proof of mendelson exercise one fourtyseven b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer inference axiom prime a one modus ponens metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut inference inference axiom prime a two modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $1.47\ c$}
"
begin math define pyk of mendelson exercise one fourtyseven c as text "mendelson exercise one fourtyseven c" end text end define end math
then math define tex of mendelson exercise one fourtyseven c as text "Mendelson\ \textbf{1.47}\ c" end text end define end math
end "
permutere r\ae{}kkef\o{}lgen af bestemte termer:
\display{
"
begin math define statement of mendelson exercise one fourtyseven c as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
For f\o{}rste gang benyttes den hypotetiske version af modus ponens: \\
"
begin math define proof of mendelson exercise one fourtyseven c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer inference axiom prime a two modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut inference axiom prime a one modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut inference inference axiom prime a two modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\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]
"
begin math define pyk of mendelson exercise one fourtyseven e as text "mendelson exercise one fourtyseven e" end text end define end math
then math define tex of mendelson exercise one fourtyseven e as text "Mendelson\ \textbf{1.47}\ e" end text end define end math
end "
siger f\o{}lgende:
\display{
"
begin math define statement of mendelson exercise one fourtyseven e as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
Nedenst\aa{}ende beviser "
begin math mendelson exercise one fourtyseven e end math
end ": \\
"
begin math define proof of mendelson exercise one fourtyseven e as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar infer mendelson exercise one fourtyseven c modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\section{Deduktion}
\subsection{Definitioner}
Proposition 1.9 i \cite{mendelson} beviser, at man fra "
begin math metavar var a end metavar infer metavar var b end metavar end math
end " 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{"
begin math metavar var b end metavar peano imply metavar var c end metavar infer metavar var c end metavar peano imply metavar var d end metavar infer metavar var b end metavar peano imply metavar var d end metavar end math
end "}
Hvor "
begin math metavar var b end metavar peano imply metavar var c end metavar end math
end " er den f\o{}rste pr\ae{}misse, "
begin math metavar var c end metavar peano imply metavar var d end metavar end math
end " den anden, "
begin math metavar var b end metavar end math
end " er hypotesen og "
begin math metavar var d end metavar end math
end " 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
"
begin math define pyk of hypothesis as text "hypothesis" end text end define end math
then math define tex of hypothesis as text "\mathsf{hyp}" end text end define end math
end "
v\ae{}re en pladsholder for en given hypotese,
"
begin math define pyk of instance as text "instance" end text end define end math
then math define tex of instance as text "\mathsf{instance}" end text end define end math
end "
for en instanciering af et aksiom eller lemma og
"
begin math define pyk of conclusion as text "conclusion" end text end define end math
then math define tex of conclusion as text "\mathsf{conclusion}" end text end define end math
end " 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 "
begin math hypothesis peano imply instance end math
end " - 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]{$"
begin hypothesis
end "$}\quad
\makebox [0.3\textwidth ][l]{Hyp} \\
Logiweb-form:
\makebox [0.1\textwidth ][l]{$LX.1$:}
\makebox [0.4\textwidth ][l]{$"
begin mendelson lemma one eight
end " \gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"
begin hypothesis peano imply hypothesis
end "$\hfill \makebox [0mm][l]{\quad ;}}
\subsubsection{Instanciering af aksiom/lemma}
Mendelson-form:
\makebox [0.05\textwidth ][l]{$X$.}
\makebox [0.45\textwidth ][l]{$"
begin instance
end "$}\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 }{$"
begin instance
end "$\hfill \makebox [0mm][l]{\quad ;}}
\makebox [0.1\textwidth ][l]{$LX.2$:}
\makebox [0.4\textwidth ][l]{$"
begin axiom prime a one
end "\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"
begin instance peano imply hypothesis peano imply instance
end "$\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 }{$"
begin hypothesis peano imply instance
end "$ \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]{$"
begin conclusion
end "$}\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 }{$"
begin hypothesis peano imply conclusion
end "$ \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 "
begin math system prime s end math
end ". \\
Mendelson-form:
\makebox [0.05\textwidth ][l]{$X$.}
\makebox [0.45\textwidth ][l]{$"
begin conclusion
end "$}\quad
\makebox [0.3\textwidth ][l]{Y, Z, MP} \\
Logiweb-form:
\makebox [0.1\textwidth ][l]{$LX.1$:}
\makebox [0.4\textwidth ][l]{$"
begin axiom prime a two
end "\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$"
begin unicode capital z unicode end of text peano imply unicode capital y unicode end of text peano imply hypothesis peano imply conclusion
end "$\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 }{$"
begin unicode capital y unicode end of text peano imply hypothesis peano imply conclusion
end "$\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 }{$"
begin hypothesis peano imply conclusion
end "$\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 "
begin math hypothetical mendelson exercise one fourtyseven b end math
end " er bevist f\o{}rst - hvilket er foretaget i afsnit \ref{sssec:hyp_one_ fourtyseven_b}.
"
begin math define pyk of mendelson lemma one eleven d as text "mendelson lemma one eleven d" end text end define end math
then math define tex of mendelson lemma one eleven d as text "Mendelson\ \textbf{1.11}\ d" end text end define end math
end "
vil herefter v\ae{}re navnet p\aa{} eksemplet, hvor s\ae{}tningen siger:
\display{
"
begin math define statement of mendelson lemma one eleven d as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end define end math
end "}
Idet udf\o{}relsen af beviset gennemg\aa{}s linje for linje, opn\aa{}s en enkelt anskuelse: \\
"
begin math define proof of mendelson lemma one eleven d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed mendelson lemma one eight conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar cut axiom prime a three conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut axiom prime a one conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut axiom prime a one conclude metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar cut axiom prime a one conclude metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar modus ponens metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar cut axiom prime a two conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut hypothetical mendelson exercise one fourtyseven b modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "
\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: \\
"
begin math define proof of mendelson lemma one eleven d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed mendelson lemma one eight conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar cut axiom prime a three conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut inference axiom prime a one modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut axiom prime a one conclude metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar cut inference axiom prime a one modus ponens metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar cut inference inference axiom prime a two modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut hypothetical mendelson exercise one fourtyseven b modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end " \\
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 "
begin math inference axiom prime a one end math
end " 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
"
begin math define pyk of line var l hypothesis indeed var i end line var p as text "line * hypothesis indeed * end line *" end text end define end math
then math define tex of line var l hypothesis indeed var i end line var p as text "
\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 text end define end math
end "
, som g\o{}r det ud for introduktion af en hypotese - svarende til afsnit \ref{ssec:deduktion_hypotese}. Selve konstruktionen er makrodefineret:
\display{
"
begin math define macro of line var l hypothesis indeed var i end line var p as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "}
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 "
begin math mendelson lemma one eight end math
end " at \textit{i} $\Rightarrow{}$ \textit{i}, herefter gemmer den hypotesen \textit{i} i den lokale makrodefinition "
begin math hypothesis end math
end ". Til sidst gemmer den konklusionen fra "
begin math mendelson lemma one eight end math
end " 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 "
begin math inference mendelson lemma one eight end math
end " til at 'udfylde' den sidste linje.
\tex{
"
begin math define tex name of line var l hypothesis indeed var i end line var p as text "
Line \, #1.
:\bullet{}\ Hypothesis
\gg #2.
; #3." end text end define end math
end "}
\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 "
begin math inference axiom prime a one end math
end " 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
"
begin math define pyk of line var l hypothesis because var a indeed var i end line var p as text "line * hypothesis because * indeed * end line *" end text end define end math
then math define tex of line var l hypothesis because var a indeed var i end line var p as text "
\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 text end define end math
end "
laver automatisk en "
begin math inference axiom prime a one end math
end " p\aa{} en instancering af en regel.
\display{
"
begin math define macro of line var l hypothesis because var a indeed var i end line var p as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "}
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 "
begin math inference axiom prime a one end math
end " - bem\ae{}rk brugen af "
begin math hypothesis end math
end ", der opretholder proposition 1.9.
\tex{
"
begin math define tex name of line var l hypothesis because var a indeed var i end line var p as text "
Line \, #1.
:\bullet{}\ #2.
\gg #3.
; #4." end text end define end math
end "}
Til instanciering af en regel med brug af modus ponens, kan konstruktionen
"
begin math define pyk of line var l hypothesis raw because var a indeed var i end line var p as text "line * hypothesis raw because * indeed * end line *" end text end define end math
then math define tex of line var l hypothesis raw because var a indeed var i end line var p as text "
\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 text end define end math
end "
bruges. Selve makrodefinitionen:
\display{
"
begin math define macro of line var l hypothesis raw because var a indeed var i end line var p as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "}
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{
"
begin math define tex name of line var l hypothesis raw because var a indeed var i end line var p as text "
Line \, #1.
:\bullet{}\ #2.
\gg #3.
; #4." end text end define end math
end "}
\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.
"
begin math define pyk of line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p as text "line * hypothesis modus ponens * modus ponens * indeed * end line *" end text end define end math
then math define tex of line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p as text "
\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 text end define end math
end "
er blot en hypotetisk brug af modus ponens:
\display{
"
begin math define macro of line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "}
\tex{
"
begin math define tex name of line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p as text "
Line \, #1.
:\bullet{}\ #2.
\unrhd{} #3.
\gg #4.
; #5." end text end define end math
end "}
"
begin math define pyk of 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 text "line * hypothesis double modus ponens * modus ponens * modus ponens * indeed * end line *" end text end define end math
then math define tex of 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 text "
\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 text end define end math
end "
definere den dobbelte brug af modus ponens:
\display{
"
begin math define macro of 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 lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 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 quote end define end define end math
end "}
\tex{
"
begin math define tex name of 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 text "
Line \, #1.
:\bullet{}\ #2.
\unrhd{} #3.
\unrhd{} #4.
\gg #5.
; #6." end text end define end math
end "}
\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
"
begin math define pyk of line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p as text "line * hypothesis first modus ponens * modus ponens * indeed * end line *" end text end define end math
then math define tex of line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p as text "
\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 text end define end math
end "
benyttes - cirklen angiver hvilket argument der er eksternt.
\display{
"
begin math define macro of line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "}
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{
"
begin math define tex name of line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p as text "
Line \, #1.
:\bullet{}\ #2.
\circ{} \unrhd{} #3.
\gg #4.
; #5." end text end define end math
end "}
Ved modus ponens med reference eksternt i 2. argument, kan
"
begin math define pyk of line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p as text "line * hypothesis second modus ponens * modus ponens * indeed * end line *" end text end define end math
then math define tex of line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p as text "
\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 text end define end math
end "
udnyttes. Makrodefinitionen er igen simpel:
\display{
"
begin math define macro of line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote 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 quote end define end define end math
end "}
\tex{
"
begin math define tex name of line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p as text "
Line \, #1.
:\bullet{}\ #2.
\unrhd{} #3.
\circ{} \gg #4.
; #5." end text end define end math
end "}
\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: \\
"
begin math define proof of mendelson lemma one eleven d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed mendelson lemma one eight conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar cut axiom prime a three conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut inference axiom prime a one modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut axiom prime a one conclude metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar cut inference axiom prime a one modus ponens metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar cut inference inference axiom prime a two modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut hypothetical mendelson exercise one fourtyseven b modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut inference mendelson lemma one eight modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end " \\
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}$}
"
begin math define pyk of hypothetical inference axiom prime a one as text "hypothetical inference axiom prime a one" end text end define end math
then math define tex of hypothetical inference axiom prime a one as text "A1'_{ih}" end text end define end math
end "
\display{
"
begin math define statement of hypothetical inference axiom prime a one as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar infer metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end define end math
end "}
"
begin math define proof of hypothetical inference axiom prime a one as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar infer mendelson lemma one eight conclude metavar var h end metavar peano imply metavar var h end metavar cut axiom prime a one conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut inference axiom prime a one modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut inference inference axiom prime a two modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar conclude metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut inference mendelson lemma one eight modus ponens metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar conclude metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $A2'_{ih}$}
"
begin math define pyk of hypothetical inference axiom prime a two as text "hypothetical inference axiom prime a two" end text end define end math
then math define tex of hypothetical inference axiom prime a two as text "A2'_{ih}" end text end define end math
end "
\display{
"
begin math define statement of hypothetical inference axiom prime a two as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
"
begin math define proof of hypothetical inference axiom prime a two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer mendelson lemma one eight conclude metavar var h end metavar peano imply metavar var h end metavar cut axiom prime a two conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut inference axiom prime a one modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut inference inference axiom prime a two modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut inference mendelson lemma one eight modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $A2'_{iih}$}
"
begin math define pyk of hypothetical inference inference axiom prime a two as text "hypothetical inference inference axiom prime a two" end text end define end math
then math define tex of hypothetical inference inference axiom prime a two as text "A2'_{iih}" end text end define end math
end "
\display{
"
begin math define statement of hypothetical inference inference axiom prime a two as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
"
begin math define proof of hypothetical inference inference axiom prime a two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer mendelson lemma one eight conclude metavar var h end metavar peano imply metavar var h end metavar cut axiom prime a two conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut inference axiom prime a one modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut double inference inference axiom prime a two modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut inference mendelson lemma one eight modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $1.47\ b_{h}$}
\label{sssec:hyp_one_ fourtyseven_b}
"
begin math define pyk of hypothetical mendelson exercise one fourtyseven b as text "hypothetical mendelson exercise one fourtyseven b" end text end define end math
then math define tex of hypothetical mendelson exercise one fourtyseven b as text "Mendelson\ \textbf{1.47}\ b_{h}" end text end define end math
end "
\display{
"
begin math define statement of hypothetical mendelson exercise one fourtyseven b as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
"
begin math define proof of hypothetical mendelson exercise one fourtyseven b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer mendelson lemma one eight conclude metavar var h end metavar peano imply metavar var h end metavar cut hypothetical inference axiom prime a one modus ponens metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut hypothetical inference inference axiom prime a two modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut inference mendelson lemma one eight modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $1.47\ c_{h}$}
"
begin math define pyk of hypothetical mendelson exercise one fourtyseven c as text "hypothetical mendelson exercise one fourtyseven c" end text end define end math
then math define tex of hypothetical mendelson exercise one fourtyseven c as text "Mendelson\ \textbf{1.47}\ c_{h}" end text end define end math
end "
\display{
"
begin math define statement of hypothetical mendelson exercise one fourtyseven c as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
"
begin math define proof of hypothetical mendelson exercise one fourtyseven c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer mendelson lemma one eight conclude metavar var h end metavar peano imply metavar var h end metavar cut hypothetical inference axiom prime a two modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut hypothetical inference axiom prime a one modus ponens metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut inference axiom prime a one modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut hypothetical inference inference axiom prime a two modus ponens metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut inference mendelson lemma one eight modus ponens metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var h end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\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.
"
begin math define pyk of mendelson lemma one eleven c as text "mendelson lemma one eleven c" end text end define end math
then math define tex of mendelson lemma one eleven c as text "Mendelson\ \textbf{1.11}\ c" end text end define end math
end "
er et eksempel p\aa{} en s\ae{}tning der bruger 2 niveauer af deduktion. S\ae{}tningen er som f\o{}lger:
\display{
"
begin math define statement of mendelson lemma one eleven c as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end define end math
end "}
Nedenst\aa{}ende viser beviset af eksemplet: \\
"
begin math define proof of mendelson lemma one eleven c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed mendelson lemma one eight conclude peano not metavar var a end metavar peano imply peano not metavar var a end metavar cut mendelson lemma one eight conclude metavar var a end metavar peano imply metavar var a end metavar cut inference axiom prime a one modus ponens metavar var a end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar cut axiom prime a one conclude metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar cut inference axiom prime a one modus ponens metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar cut hypothetical inference axiom prime a one modus ponens peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar cut axiom prime a one conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar cut inference axiom prime a one modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar cut hypothetical inference axiom prime a one modus ponens peano not metavar var a end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar cut hypothetical inference inference axiom prime a two modus ponens peano not metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar modus ponens peano not metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar cut inference inference axiom prime a two modus ponens peano not metavar var a end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar modus ponens peano not metavar var a end metavar peano imply peano not metavar var a end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar cut hypothetical inference axiom prime a one modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar cut axiom prime a three conclude peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut inference axiom prime a one modus ponens peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut hypothetical inference axiom prime a one modus ponens peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut hypothetical inference inference axiom prime a two modus ponens peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar modus ponens peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply peano not metavar var a end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut hypothetical inference inference axiom prime a two modus ponens peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar modus ponens peano not metavar var a end metavar peano imply metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut inference mendelson lemma one eight modus ponens peano not metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude peano not metavar var a end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end quote state proof state cache var c end expand end define end math
end " \\
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 "
begin math mendelson proposition three two h end math
end " (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{"
begin math peano not hypothesis peano imply peano not hypothesis peano imply conclusion end math
end "}
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: \\
"
begin math define pyk of mendelson exercise one fourtyeight d as text "mendelson exercise one fourtyeight d" end text end define end math
then math define tex of mendelson exercise one fourtyeight d as text "Mendelson\ \textbf{1.48}\ d" end text end define end math
end "
\display{
"
begin math define statement of mendelson exercise one fourtyeight d as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar end define end math
end "}
"
begin math define pyk of mendelson exercise one fourtyeight e as text "mendelson exercise one fourtyeight e" end text end define end math
then math define tex of mendelson exercise one fourtyeight e as text "Mendelson\ \textbf{1.48}\ e" end text end define end math
end "
\display{
"
begin math define statement of mendelson exercise one fourtyeight e as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var b end metavar end define end math
end "}
"
begin math define pyk of mendelson exercise one fourtyeight h as text "mendelson exercise one fourtyeight h" end text end define end math
then math define tex of mendelson exercise one fourtyeight h as text "Mendelson\ \textbf{1.48}\ h" end text end define end math
end "
\display{
"
begin math define statement of mendelson exercise one fourtyeight h as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar end define end math
end "}
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$}
"
begin math define pyk of mendelson corollary one ten a as text "mendelson corollary one ten a" end text end define end math
then math define tex of mendelson corollary one ten a as text "Mendelson\ \textbf{1.10}\ a" end text end define end math
end "
\display{
"
begin math define statement of mendelson corollary one ten a as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
"
begin math define proof of mendelson corollary one ten a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer mendelson lemma one eight conclude metavar var a end metavar peano imply metavar var a end metavar cut mendelson exercise one fourtyseven b modus ponens metavar var a end metavar peano imply metavar var a end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var b end metavar cut mendelson exercise one fourtyseven b modus ponens metavar var a end metavar peano imply metavar var b end metavar modus ponens metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var c end metavar cut inference mendelson lemma one eight modus ponens metavar var a end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $1.10\ b$}
"
begin math define pyk of mendelson corollary one ten b as text "mendelson corollary one ten b" end text end define end math
then math define tex of mendelson corollary one ten b as text "Mendelson\ \textbf{1.10}\ b" end text end define end math
end "
\display{
"
begin math define statement of mendelson corollary one ten b as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
"
begin math define proof of mendelson corollary one ten b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar infer mendelson lemma one eight conclude metavar var a end metavar peano imply metavar var a end metavar cut mendelson exercise one fourtyseven b modus ponens metavar var a end metavar peano imply metavar var a end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut mendelson exercise one fourtyseven e modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar cut inference mendelson lemma one eight modus ponens metavar var a end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\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}\ ;\ "
begin not metavar var f end metavar
end "\ ;\ "
begin metavar var f end metavar
end " \Rightarrow{} "
begin metavar var f end metavar
end "\ ;\ "
begin all metavar var v end metavar indeed metavar var f end metavar
end " $ \\
$\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':$ "
begin math all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar end math
end "}
\display{$A5':$ "
begin math all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var a end metavar end quote end nonfree endorse peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar end math
end "}
\display{$Gen':$ "
begin math all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar end math
end "}
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':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar end math
end "}
\display{$S2':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ end math
end "}
\display{$S3':$ "
begin math all metavar var a end metavar indeed not peano zero peano is metavar var a end metavar peano succ end math
end "}
\display{$S4':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano succ peano is metavar var b end metavar peano succ peano imply metavar var a end metavar peano is metavar var b end metavar end math
end "}
\display{$S5':$ "
begin math all metavar var a end metavar indeed metavar var a end metavar peano plus peano zero peano is metavar var a end metavar end math
end "}
\display{$S6':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano plus metavar var b end metavar peano succ peano is metavar var a end metavar peano plus metavar var b end metavar peano succ end math
end "}
\display{$S7':$ "
begin math all metavar var a end metavar indeed metavar var a end metavar peano times peano zero peano is peano zero end math
end "}
\display{$S8':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano times metavar var b end metavar peano succ peano is metavar var a end metavar peano times metavar var b end metavar peano plus metavar var a end metavar end math
end "}
\display{$S9':$ "
begin math all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse metavar var b end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end math
end "}
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}$}
"
begin math define pyk of inference axiom prime s one as text "inference axiom prime s one" end text end define end math
then math define tex of inference axiom prime s one as text "S1'_{i}" end text end define end math
end "
\display{
"
begin math define statement of inference axiom prime s one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar end define end math
end "}
"
begin math define proof of inference axiom prime s one as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer axiom prime s one conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar cut rule prime mp modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar modus ponens metavar var a end metavar peano is metavar var b end metavar conclude metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $S1'_{ii}$}
"
begin math define pyk of inference inference axiom prime s one as text "inference inference axiom prime s one" end text end define end math
then math define tex of inference inference axiom prime s one as text "S1'_{ii}" end text end define end math
end "
\display{
"
begin math define statement of inference inference axiom prime s one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer metavar var a end metavar peano is metavar var c end metavar infer metavar var b end metavar peano is metavar var c end metavar end define end math
end "}
"
begin math define proof of inference inference axiom prime s one as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer metavar var a end metavar peano is metavar var c end metavar infer inference axiom prime s one modus ponens metavar var a end metavar peano is metavar var b end metavar conclude metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar cut rule prime mp modus ponens metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar modus ponens metavar var a end metavar peano is metavar var c end metavar conclude metavar var b end metavar peano is metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $S2'_{i}$}
"
begin math define pyk of inference axiom prime s two as text "inference axiom prime s two" end text end define end math
then math define tex of inference axiom prime s two as text "S2'_{i}" end text end define end math
end "
\display{
"
begin math define statement of inference axiom prime s two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer metavar var a end metavar peano succ peano is metavar var b end metavar peano succ end define end math
end "}
"
begin math define proof of inference axiom prime s two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer axiom prime s two conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ cut rule prime mp modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ modus ponens metavar var a end metavar peano is metavar var b end metavar conclude metavar var a end metavar peano succ peano is metavar var b end metavar peano succ end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $S2'_{ih}$}
"
begin math define pyk of hypothetical inference axiom prime s two as text "hypothetical inference axiom prime s two" end text end define end math
then math define tex of hypothetical inference axiom prime s two as text "S2'_{ih}" end text end define end math
end "
\display{
"
begin math define statement of hypothetical inference axiom prime s two as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar infer metavar var h end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ end define end math
end "}
"
begin math define proof of hypothetical inference axiom prime s two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar infer mendelson lemma one eight conclude metavar var h end metavar peano imply metavar var h end metavar cut axiom prime s two conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ cut inference axiom prime a one modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ conclude metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ cut inference inference axiom prime a two modus ponens metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ modus ponens metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ cut inference mendelson lemma one eight modus ponens metavar var h end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ conclude metavar var h end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $S9'_{ii}$}
"
begin math define pyk of inference inference axiom prime s nine as text "inference inference axiom prime s nine" end text end define end math
then math define tex of inference inference axiom prime s nine as text "S9'_{ii}" end text end define end math
end "
er en inferens-version af induktions-aksiomet. I selve s\ae{}tningen, er to implikationsoperatoere blevet udskiftet:
\display{
"
begin math define statement of inference inference axiom prime s nine as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var y end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var y end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var y end metavar is metavar var y end metavar peano succ end sub endorse metavar var b end metavar infer peano all metavar var y end metavar indeed metavar var a end metavar peano imply metavar var c end metavar infer peano all metavar var y end metavar indeed metavar var a end metavar end define end math
end "}
Selve beviset er ligefrem, det skal dog bem\ae{}rkes hvordan sidebetingelser kan elimineres: \\
"
begin math define proof of inference inference axiom prime s nine as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var y end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var y end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var y end metavar is metavar var y end metavar peano succ end sub endorse metavar var b end metavar infer peano all metavar var y end metavar indeed metavar var a end metavar peano imply metavar var c end metavar infer axiom prime s nine modus probans peano sub metavar var b end metavar is metavar var a end metavar where metavar var y end metavar is peano zero end sub modus probans peano sub metavar var c end metavar is metavar var a end metavar where metavar var y end metavar is metavar var y end metavar peano succ end sub conclude metavar var b end metavar peano imply peano all metavar var y end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var y end metavar indeed metavar var a end metavar cut double rule prime mp modus ponens metavar var b end metavar peano imply peano all metavar var y end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var y end metavar indeed metavar var a end metavar modus ponens metavar var b end metavar modus ponens peano all metavar var y end metavar indeed metavar var a end metavar peano imply metavar var c end metavar conclude peano all metavar var y end metavar indeed metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $Induction$}
For at lette anvendelsen af induktion er s\ae{}tningen
"
begin math define pyk of rule induction as text "rule induction" end text end define end math
then math define tex of rule induction as text "Induction" end text end define end math
end "
blevet lavet, s\ae{}tningen siger f\o{}lgende:
\display{
"
begin math define statement of rule induction as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var y end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var y end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var y end metavar is metavar var y end metavar peano succ end sub endorse peano sub quote metavar var a end metavar end quote is quote metavar var a end metavar end quote where quote metavar var y end metavar end quote is quote metavar var y end metavar end quote end sub endorse metavar var b end metavar infer metavar var a end metavar peano imply metavar var c end metavar infer metavar var a end metavar end define end math
end "}
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: \\
"
begin math define proof of rule induction as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var y end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var y end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var y end metavar is metavar var y end metavar peano succ end sub endorse peano sub quote metavar var a end metavar end quote is quote metavar var a end metavar end quote where quote metavar var y end metavar end quote is quote metavar var y end metavar end quote end sub endorse metavar var b end metavar infer metavar var a end metavar peano imply metavar var c end metavar infer rule prime gen modus ponens metavar var a end metavar peano imply metavar var c end metavar conclude peano all metavar var y end metavar indeed metavar var a end metavar peano imply metavar var c end metavar cut inference inference axiom prime s nine modus probans peano sub metavar var b end metavar is metavar var a end metavar where metavar var y end metavar is peano zero end sub modus probans peano sub metavar var c end metavar is metavar var a end metavar where metavar var y end metavar is metavar var y end metavar peano succ end sub modus ponens metavar var b end metavar modus ponens peano all metavar var y end metavar indeed metavar var a end metavar peano imply metavar var c end metavar conclude peano all metavar var y end metavar indeed metavar var a end metavar cut axiom prime a four modus probans peano sub quote metavar var a end metavar end quote is quote metavar var a end metavar end quote where quote metavar var y end metavar end quote is quote metavar var y end metavar end quote end sub conclude peano all metavar var y end metavar indeed metavar var a end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens peano all metavar var y end metavar indeed metavar var a end metavar peano imply metavar var a end metavar modus ponens peano all metavar var y end metavar indeed metavar var a end metavar conclude metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "
\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$}
"
begin math define pyk of mendelson proposition three two a as text "mendelson proposition three two a" end text end define end math
then math define tex of mendelson proposition three two a as text "Mendelson\ \textbf{3.2}\ a" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two a as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano is metavar var a end metavar end define end math
end "}
"
begin math define proof of mendelson proposition three two a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed axiom prime s five conclude metavar var a end metavar peano plus peano zero peano is metavar var a end metavar cut inference inference axiom prime s one modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar modus ponens metavar var a end metavar peano plus peano zero peano is metavar var a end metavar conclude metavar var a end metavar peano is metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $3.2\ b$}
"
begin math define pyk of mendelson proposition three two b as text "mendelson proposition three two b" end text end define end math
then math define tex of mendelson proposition three two b as text "Mendelson\ \textbf{3.2}\ b" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two b as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var a end metavar end define end math
end "}
"
begin math define proof of mendelson proposition three two b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed axiom prime s one conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var a end metavar peano imply metavar var b end metavar peano is metavar var a end metavar cut mendelson proposition three two a conclude metavar var a end metavar peano is metavar var a end metavar cut mendelson corollary one ten b modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var a end metavar peano imply metavar var b end metavar peano is metavar var a end metavar modus ponens metavar var a end metavar peano is metavar var a end metavar conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $3.2\ b_{i}$}
"
begin math define pyk of inference mendelson proposition three two b as text "inference mendelson proposition three two b" end text end define end math
then math define tex of inference mendelson proposition three two b as text "Mendelson\ \textbf{3.2}\ b_{i}" end text end define end math
end "
"
begin math define statement of inference mendelson proposition three two b as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer metavar var b end metavar peano is metavar var a end metavar end define end math
end "
"
begin math define proof of inference mendelson proposition three two b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer mendelson proposition three two b conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var a end metavar modus ponens metavar var a end metavar peano is metavar var b end metavar conclude metavar var b end metavar peano is metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $3.2\ c$}
"
begin math define pyk of mendelson proposition three two c as text "mendelson proposition three two c" end text end define end math
then math define tex of mendelson proposition three two c as text "Mendelson\ \textbf{3.2}\ c" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two c as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar end define end math
end "}
"
begin math define proof of mendelson proposition three two c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed axiom prime s one conclude metavar var b end metavar peano is metavar var a end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut mendelson proposition three two b conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var a end metavar cut mendelson corollary one ten a modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var a end metavar modus ponens metavar var b end metavar peano is metavar var a end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar end quote state proof state cache var c end expand end define end math
end " \\
"
begin math mendelson proposition three two a end math
end " (refleksivititet), "
begin math mendelson proposition three two b end math
end " (symmetri) og\linebreak[4] "
begin math mendelson proposition three two c end math
end " (transitivitet) udg\o{}r tilsammen beviset for at lighed i peano aritmetik er en \ae{}kvivalensrelation.
\subsubsection{Bevis $3.2\ c_{ii}$}
"
begin math define pyk of inference inference mendelson proposition three two c as text "inference inference mendelson proposition three two c" end text end define end math
then math define tex of inference inference mendelson proposition three two c as text "Mendelson\ \textbf{3.2}\ c_{ii}" end text end define end math
end "
\display{
"
begin math define statement of inference inference mendelson proposition three two c as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer metavar var b end metavar peano is metavar var c end metavar infer metavar var a end metavar peano is metavar var c end metavar end define end math
end "}
"
begin math define proof of inference inference mendelson proposition three two c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer metavar var b end metavar peano is metavar var c end metavar infer mendelson proposition three two c conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut double rule prime mp modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar modus ponens metavar var a end metavar peano is metavar var b end metavar modus ponens metavar var b end metavar peano is metavar var c end metavar conclude metavar var a end metavar peano is metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $3.2\ c_{iih}$}
"
begin math define pyk of hypothetical inference inference mendelson proposition three two c as text "hypothetical inference inference mendelson proposition three two c" end text end define end math
then math define tex of hypothetical inference inference mendelson proposition three two c as text "Mendelson\ \textbf{3.2}\ c_{iih}" end text end define end math
end "
\display{
"
begin math define statement of hypothetical inference inference mendelson proposition three two c as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar infer metavar var h end metavar peano imply metavar var b end metavar peano is metavar var c end metavar infer metavar var h end metavar peano imply metavar var a end metavar peano is metavar var c end metavar end define end math
end "}
"
begin math define proof of hypothetical inference inference mendelson proposition three two c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar infer metavar var h end metavar peano imply metavar var b end metavar peano is metavar var c end metavar infer mendelson lemma one eight conclude metavar var h end metavar peano imply metavar var h end metavar cut mendelson proposition three two c conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut inference axiom prime a one modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut double inference inference axiom prime a two modus ponens metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar modus ponens metavar var h end metavar peano imply metavar var b end metavar peano is metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut inference mendelson lemma one eight modus ponens metavar var h end metavar peano imply metavar var a end metavar peano is metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano is metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $3.2\ d$}
"
begin math define pyk of mendelson proposition three two d as text "mendelson proposition three two d" end text end define end math
then math define tex of mendelson proposition three two d as text "Mendelson\ \textbf{3.2}\ d" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two d as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar end define end math
end "}
"
begin math define proof of mendelson proposition three two d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed mendelson proposition three two c conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut mendelson exercise one fourtyseven c modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var c end metavar conclude metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut mendelson proposition three two b conclude metavar var c end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar cut mendelson corollary one ten a modus ponens metavar var c end metavar peano is metavar var b end metavar peano imply metavar var b end metavar peano is metavar var c end metavar modus ponens metavar var b end metavar peano is metavar var c end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar conclude metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut mendelson exercise one fourtyseven c modus ponens metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $3.2\ d_{ii}$}
"
begin math define pyk of inference inference mendelson proposition three two d as text "inference inference mendelson proposition three two d" end text end define end math
then math define tex of inference inference mendelson proposition three two d as text "Mendelson\ \textbf{3.2}\ d_{ii}" end text end define end math
end "
\display{
"
begin math define statement of inference inference mendelson proposition three two d as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer metavar var c end metavar peano is metavar var b end metavar infer metavar var a end metavar peano is metavar var c end metavar end define end math
end "}
"
begin math define proof of inference inference mendelson proposition three two d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar infer metavar var c end metavar peano is metavar var b end metavar infer mendelson proposition three two d conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut double rule prime mp modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar modus ponens metavar var a end metavar peano is metavar var b end metavar modus ponens metavar var c end metavar peano is metavar var b end metavar conclude metavar var a end metavar peano is metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $3.2\ d_{iih}$}
"
begin math define pyk of hypothetical inference inference mendelson proposition three two d as text "hypothetical inference inference mendelson proposition three two d" end text end define end math
then math define tex of hypothetical inference inference mendelson proposition three two d as text "Mendelson\ \textbf{3.2}\ d_{iih}" end text end define end math
end "
\display{
"
begin math define statement of hypothetical inference inference mendelson proposition three two d as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar infer metavar var h end metavar peano imply metavar var c end metavar peano is metavar var b end metavar infer metavar var h end metavar peano imply metavar var a end metavar peano is metavar var c end metavar end define end math
end "}
"
begin math define proof of hypothetical inference inference mendelson proposition three two d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar infer metavar var h end metavar peano imply metavar var c end metavar peano is metavar var b end metavar infer mendelson lemma one eight conclude metavar var h end metavar peano imply metavar var h end metavar cut mendelson proposition three two d conclude metavar var a end metavar peano is metavar var b end metavar peano imply metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut inference axiom prime a one modus ponens metavar var a end metavar peano is metavar var b end metavar peano imply metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut double inference inference axiom prime a two modus ponens metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar peano imply metavar var c end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar modus ponens metavar var h end metavar peano imply metavar var a end metavar peano is metavar var b end metavar modus ponens metavar var h end metavar peano imply metavar var c end metavar peano is metavar var b end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano is metavar var c end metavar cut inference mendelson lemma one eight modus ponens metavar var h end metavar peano imply metavar var a end metavar peano is metavar var c end metavar conclude metavar var h end metavar peano imply metavar var a end metavar peano is metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $3.2\ f$}
"
begin math define pyk of mendelson proposition three two f i as text "mendelson proposition three two f i" end text end define end math
then math define tex of mendelson proposition three two f i as text "Mendelson\ \textbf{3.2}\ f\ i" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two f i as system prime s infer peano zero peano is peano zero peano plus peano zero end define end math
end "}
"
begin math define proof of mendelson proposition three two f i as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude peano zero peano plus peano zero peano is peano zero cut inference mendelson proposition three two b modus ponens peano zero peano plus peano zero peano is peano zero conclude peano zero peano is peano zero peano plus peano zero end quote state proof state cache var c end expand end define end math
end " \\
"
begin math define pyk of mendelson proposition three two f ii as text "mendelson proposition three two f ii" end text end define end math
then math define tex of mendelson proposition three two f ii as text "Mendelson\ \textbf{3.2}\ f\ ii" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two f ii as system prime s infer var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ end define end math
end "}
"
begin math define proof of mendelson proposition three two f ii as lambda var c dot lambda var x dot proof expand quote system prime s infer mendelson lemma one eight conclude var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano is peano zero peano plus var x peano var cut axiom prime s six conclude peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut inference axiom prime a one modus ponens peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ conclude var x peano var peano is peano zero peano plus var x peano var peano imply peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut hypothetical inference axiom prime s two modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano is peano zero peano plus var x peano var conclude var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut hypothetical inference inference mendelson proposition three two d modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply peano zero peano plus var x peano var peano succ peano is peano zero peano plus var x peano var peano succ conclude var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut inference mendelson lemma one eight modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ conclude var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ end quote state proof state cache var c end expand end define end math
end " \\
"
begin math define pyk of mendelson proposition three two f as text "mendelson proposition three two f" end text end define end math
then math define tex of mendelson proposition three two f as text "Mendelson\ \textbf{3.2}\ f" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two f as system prime s infer var x peano var peano is peano zero peano plus var x peano var end define end math
end "}
"
begin math define proof of mendelson proposition three two f as lambda var c dot lambda var x dot proof expand quote system prime s infer mendelson proposition three two f i conclude peano zero peano is peano zero peano plus peano zero cut mendelson proposition three two f ii conclude var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ cut rule induction modus ponens peano zero peano is peano zero peano plus peano zero modus ponens var x peano var peano is peano zero peano plus var x peano var peano imply var x peano var peano succ peano is peano zero peano plus var x peano var peano succ conclude var x peano var peano is peano zero peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "
\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 "
begin math mendelson proposition three two h end math
end ". \\
"
begin math define pyk of mendelson proposition three two g i as text "mendelson proposition three two g i" end text end define end math
then math define tex of mendelson proposition three two g i as text "Mendelson\ \textbf{3.2}\ g\ i" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two g i as system prime s infer var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ end define end math
end "}
"
begin math define proof of mendelson proposition three two g i as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var y peano var peano succ peano plus peano zero peano is var y peano var peano succ cut axiom prime s five conclude var y peano var peano plus peano zero peano is var y peano var cut inference axiom prime s two modus ponens var y peano var peano plus peano zero peano is var y peano var conclude var y peano var peano plus peano zero peano succ peano is var y peano var peano succ cut inference inference mendelson proposition three two d modus ponens var y peano var peano succ peano plus peano zero peano is var y peano var peano succ modus ponens var y peano var peano plus peano zero peano succ peano is var y peano var peano succ conclude var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ end quote state proof state cache var c end expand end define end math
end "
"
begin math define pyk of mendelson proposition three two g ii as text "mendelson proposition three two g ii" end text end define end math
then math define tex of mendelson proposition three two g ii as text "Mendelson\ \textbf{3.2}\ g\ ii" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two g ii as system prime s infer var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ end define end math
end "}
"
begin math define proof of mendelson proposition three two g ii as lambda var c dot lambda var x dot proof expand quote system prime s infer mendelson lemma one eight conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut axiom prime s six conclude var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano succ cut inference axiom prime a one modus ponens var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano succ cut hypothetical inference axiom prime s two modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut hypothetical inference inference mendelson proposition three two c modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano succ peano plus var x peano var peano succ modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut axiom prime s six conclude var y peano var peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut inference axiom prime a one modus ponens var y peano var peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut hypothetical inference axiom prime s two modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano plus var x peano var peano succ peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut hypothetical inference inference mendelson proposition three two d modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano plus var x peano var peano succ peano succ peano is var y peano var peano plus var x peano var peano succ peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut inference mendelson lemma one eight modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ end quote state proof state cache var c end expand end define end math
end "
"
begin math define pyk of mendelson proposition three two g as text "mendelson proposition three two g" end text end define end math
then math define tex of mendelson proposition three two g as text "Mendelson\ \textbf{3.2}\ g" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two g as system prime s infer var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ end define end math
end "}
"
begin math define proof of mendelson proposition three two g as lambda var c dot lambda var x dot proof expand quote system prime s infer mendelson proposition three two g i conclude var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ cut mendelson proposition three two g ii conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ cut rule induction modus ponens var y peano var peano succ peano plus peano zero peano is var y peano var peano plus peano zero peano succ modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ peano imply var y peano var peano succ peano plus var x peano var peano succ peano is var y peano var peano plus var x peano var peano succ peano succ conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ end quote state proof state cache var c end expand end define end math
end "
\subsubsection{Bevis $3.2\ h$}
\label{ssec:peano_three_two_h}
"
begin math define pyk of mendelson proposition three two h i as text "mendelson proposition three two h i" end text end define end math
then math define tex of mendelson proposition three two h i as text "Mendelson\ \textbf{3.2}\ h\ i" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two h i as system prime s infer var x peano var peano plus peano zero peano is peano zero peano plus var x peano var end define end math
end "}
"
begin math define proof of mendelson proposition three two h i as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var x peano var peano plus peano zero peano is var x peano var cut mendelson proposition three two f conclude var x peano var peano is peano zero peano plus var x peano var cut inference inference mendelson proposition three two c modus ponens var x peano var peano plus peano zero peano is var x peano var modus ponens var x peano var peano is peano zero peano plus var x peano var conclude var x peano var peano plus peano zero peano is peano zero peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "
"
begin math define pyk of mendelson proposition three two h ii as text "mendelson proposition three two h ii" end text end define end math
then math define tex of mendelson proposition three two h ii as text "Mendelson\ \textbf{3.2}\ h\ ii" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two h ii as system prime s infer var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var end define end math
end "}
"
begin math define proof of mendelson proposition three two h ii as lambda var c dot lambda var x dot proof expand quote system prime s infer mendelson lemma one eight conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var cut axiom prime s six conclude var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ cut inference axiom prime a one modus ponens var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ cut mendelson proposition three two g conclude var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut inference axiom prime a one modus ponens var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ cut hypothetical inference axiom prime s two modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut hypothetical inference inference mendelson proposition three two c modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var x peano var peano plus var y peano var peano succ modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ cut hypothetical inference inference mendelson proposition three two d modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano plus var x peano var peano succ modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var y peano var peano succ peano plus var x peano var peano is var y peano var peano plus var x peano var peano succ conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var cut inference mendelson lemma one eight modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "
"
begin math define pyk of mendelson proposition three two h as text "mendelson proposition three two h" end text end define end math
then math define tex of mendelson proposition three two h as text "Mendelson\ \textbf{3.2}\ h" end text end define end math
end "
\display{
"
begin math define statement of mendelson proposition three two h as system prime s infer var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var end define end math
end "}
"
begin math define proof of mendelson proposition three two h as lambda var c dot lambda var x dot proof expand quote system prime s infer mendelson proposition three two h i conclude var x peano var peano plus peano zero peano is peano zero peano plus var x peano var cut mendelson proposition three two h ii conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var cut rule induction modus ponens var x peano var peano plus peano zero peano is peano zero peano plus var x peano var modus ponens var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var peano imply var x peano var peano plus var y peano var peano succ peano is var y peano var peano succ peano plus var x peano var conclude var x peano var peano plus var y peano var peano is var y peano var peano plus var x peano var end quote state proof state cache var c end expand end define end math
end "
\appendix
\section{Diverse}
"
begin math define pyk of logic as text "logic" end text end define end math
end "
\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}
"
begin flush left math define priority of logic as preassociative priority logic equal priority base equal priority bracket x end bracket equal priority big bracket x end bracket equal priority math x end math equal priority flush left x end left equal priority var x equal priority var y equal priority var z equal priority proclaim x as x end proclaim equal priority define x of x as x end define equal priority pyk equal priority tex equal priority tex name equal priority priority equal priority x equal priority true equal priority if x then x else x end if equal priority introduce x of x as x end introduce equal priority value equal priority claim equal priority bottom equal priority function f of x end function equal priority identity x end identity equal priority false equal priority untagged zero equal priority untagged one equal priority untagged two equal priority untagged three equal priority untagged four equal priority untagged five equal priority untagged six equal priority untagged seven equal priority untagged eight equal priority untagged nine equal priority zero equal priority one equal priority two equal priority three equal priority four equal priority five equal priority six equal priority seven equal priority eight equal priority nine equal priority var a equal priority var b equal priority var c equal priority var d equal priority var e equal priority var f equal priority var g equal priority var h equal priority var i equal priority var j equal priority var k equal priority var l equal priority var m equal priority var n equal priority var o equal priority var p equal priority var q equal priority var r equal priority var s equal priority var t equal priority var u equal priority var v equal priority var w equal priority tagged parenthesis x end tagged equal priority tagged if x then x else x end if equal priority array x is x end array equal priority left equal priority center equal priority right equal priority empty equal priority substitute x set x to x end substitute equal priority map tag x end tag equal priority raw map untag x end untag equal priority map untag x end untag equal priority normalizing untag x end untag equal priority apply x to x end apply equal priority apply one x to x end apply equal priority identifier x end identifier equal priority identifier one x plus id x end identifier equal priority array plus x and x end plus equal priority array remove x array x level x end remove equal priority array put x value x array x level x end put equal priority array add x value x index x value x level x end add equal priority bit x of x end bit equal priority bit one x of x end bit equal priority example rack equal priority vector hook equal priority bibliography hook equal priority dictionary hook equal priority body hook equal priority codex hook equal priority expansion hook equal priority code hook equal priority cache hook equal priority diagnose hook equal priority pyk aspect equal priority tex aspect equal priority texname aspect equal priority value aspect equal priority message aspect equal priority macro aspect equal priority definition aspect equal priority unpack aspect equal priority claim aspect equal priority priority aspect equal priority lambda identifier equal priority apply identifier equal priority true identifier equal priority if identifier equal priority quote identifier equal priority proclaim identifier equal priority define identifier equal priority introduce identifier equal priority hide identifier equal priority pre identifier equal priority post identifier equal priority eval x stack x cache x end eval equal priority eval two x ref x id x stack x cache x end eval equal priority eval three x function x stack x cache x end eval equal priority eval four x arguments x stack x cache x end eval equal priority lookup x stack x default x end lookup equal priority abstract x term x stack x cache x end abstract equal priority quote x end quote equal priority expand x state x cache x end expand equal priority expand two x definition x state x cache x end expand equal priority expand list x state x cache x end expand equal priority macro equal priority macro state equal priority zip x with x end zip equal priority assoc one x address x index x end assoc equal priority protect x end protect equal priority self equal priority macro define x as x end define equal priority value define x as x end define equal priority intro define x as x end define equal priority pyk define x as x end define equal priority tex define x as x end define equal priority tex name define x as x end define equal priority priority table x end table equal priority macro define one equal priority macro define two x end define equal priority macro define three x end define equal priority macro define four x state x cache x definition x end define equal priority state expand x state x cache x end expand equal priority quote expand x term x stack x end expand equal priority quote expand two x term x stack x end expand equal priority quote expand three x term x stack x value x end expand equal priority quote expand star x term x stack x end expand equal priority parenthesis x end parenthesis equal priority aspect x subcodex x end aspect equal priority aspect x term x cache x end aspect equal priority tuple x end tuple equal priority tuple one x end tuple equal priority tuple two x end tuple equal priority let two x apply x end let equal priority let one x apply x end let equal priority claim define x as x end define equal priority checker equal priority check x cache x end check equal priority check two x cache x def x end check equal priority check three x cache x def x end check equal priority check list x cache x end check equal priority check list two x cache x value x end check equal priority test x end test equal priority false test x end test equal priority raw test x end test equal priority message equal priority message define x as x end define equal priority the statement aspect equal priority statement equal priority statement define x as x end define equal priority example axiom equal priority example scheme equal priority example rule equal priority absurdity equal priority contraexample equal priority example theory primed equal priority example lemma equal priority metavar x end metavar equal priority meta a equal priority meta b equal priority meta c equal priority meta d equal priority meta e equal priority meta f equal priority meta g equal priority meta h equal priority meta i equal priority meta j equal priority meta k equal priority meta l equal priority meta m equal priority meta n equal priority meta o equal priority meta p equal priority meta q equal priority meta r equal priority meta s equal priority meta t equal priority meta u equal priority meta v equal priority meta w equal priority meta x equal priority meta y equal priority meta z equal priority sub x set x to x end sub equal priority sub star x set x to x end sub equal priority the empty set equal priority example remainder equal priority make visible x end visible equal priority intro x index x pyk x tex x end intro equal priority intro x pyk x tex x end intro equal priority error x term x end error equal priority error two x term x end error equal priority proof x term x cache x end proof equal priority proof two x term x end proof equal priority sequent eval x term x end eval equal priority seqeval init x term x end eval equal priority seqeval modus x term x end eval equal priority seqeval modus one x term x sequent x end eval equal priority seqeval verify x term x end eval equal priority seqeval verify one x term x sequent x end eval equal priority sequent eval plus x term x end eval equal priority seqeval plus one x term x sequent x end eval equal priority seqeval minus x term x end eval equal priority seqeval minus one x term x sequent x end eval equal priority seqeval deref x term x end eval equal priority seqeval deref one x term x sequent x end eval equal priority seqeval deref two x term x sequent x def x end eval equal priority seqeval at x term x end eval equal priority seqeval at one x term x sequent x end eval equal priority seqeval infer x term x end eval equal priority seqeval infer one x term x premise x sequent x end eval equal priority seqeval endorse x term x end eval equal priority seqeval endorse one x term x side x sequent x end eval equal priority seqeval est x term x end eval equal priority seqeval est one x term x name x sequent x end eval equal priority seqeval est two x term x name x sequent x def x end eval equal priority seqeval all x term x end eval equal priority seqeval all one x term x variable x sequent x end eval equal priority seqeval cut x term x end eval equal priority seqeval cut one x term x forerunner x end eval equal priority seqeval cut two x term x forerunner x sequent x end eval equal priority computably true x end true equal priority claims x cache x ref x end claims equal priority claims two x cache x ref x end claims equal priority the proof aspect equal priority proof equal priority lemma x says x end lemma equal priority proof of x reads x end proof equal priority in theory x lemma x says x end lemma equal priority in theory x antilemma x says x end antilemma equal priority in theory x rule x says x end rule equal priority in theory x antirule x says x end antirule equal priority verifier equal priority verify one x end verify equal priority verify two x proofs x end verify equal priority verify three x ref x sequents x diagnose x end verify equal priority verify four x premises x end verify equal priority verify five x ref x array x sequents x end verify equal priority verify six x ref x list x sequents x end verify equal priority verify seven x ref x id x sequents x end verify equal priority cut x and x end cut equal priority head x end head equal priority tail x end tail equal priority rule one x theory x end rule equal priority rule x subcodex x end rule equal priority rule tactic equal priority plus x and x end plus equal priority theory x end theory equal priority theory two x cache x end theory equal priority theory three x name x end theory equal priority theory four x name x sum x end theory equal priority example axiom lemma primed equal priority example scheme lemma primed equal priority example rule lemma primed equal priority contraexample lemma primed equal priority example axiom lemma equal priority example scheme lemma equal priority example rule lemma equal priority contraexample lemma equal priority example theory equal priority ragged right equal priority ragged right expansion equal priority parameter term x stack x seed x end parameter equal priority parameter term star x stack x seed x end parameter equal priority instantiate x with x end instantiate equal priority instantiate star x with x end instantiate equal priority occur x in x substitution x end occur equal priority occur star x in x substitution x end occur equal priority unify x with x substitution x end unify equal priority unify star x with x substitution x end unify equal priority unify two x with x substitution x end unify equal priority ell a equal priority ell b equal priority ell c equal priority ell d equal priority ell e equal priority ell f equal priority ell g equal priority ell h equal priority ell i equal priority ell j equal priority ell k equal priority ell l equal priority ell m equal priority ell n equal priority ell o equal priority ell p equal priority ell q equal priority ell r equal priority ell s equal priority ell t equal priority ell u equal priority ell v equal priority ell w equal priority ell x equal priority ell y equal priority ell z equal priority ell big a equal priority ell big b equal priority ell big c equal priority ell big d equal priority ell big e equal priority ell big f equal priority ell big g equal priority ell big h equal priority ell big i equal priority ell big j equal priority ell big k equal priority ell big l equal priority ell big m equal priority ell big n equal priority ell big o equal priority ell big p equal priority ell big q equal priority ell big r equal priority ell big s equal priority ell big t equal priority ell big u equal priority ell big v equal priority ell big w equal priority ell big x equal priority ell big y equal priority ell big z equal priority ell dummy equal priority sequent reflexivity equal priority tactic reflexivity equal priority sequent commutativity equal priority tactic commutativity equal priority the tactic aspect equal priority tactic equal priority tactic define x as x end define equal priority proof expand x state x cache x end expand equal priority proof expand list x state x cache x end expand equal priority proof state equal priority conclude one x cache x end conclude equal priority conclude two x proves x cache x end conclude equal priority conclude three x proves x lemma x substitution x end conclude equal priority conclude four x lemma x end conclude equal priority peano equal priority peano zero equal priority peano one equal priority peano two equal priority peano a equal priority peano b equal priority peano c equal priority peano d equal priority peano e equal priority peano f equal priority peano g equal priority peano h equal priority peano i equal priority peano j equal priority peano k equal priority peano l equal priority peano m equal priority peano n equal priority peano o equal priority peano p equal priority peano q equal priority peano r equal priority peano s equal priority peano t equal priority peano u equal priority peano v equal priority peano w equal priority peano x equal priority peano y equal priority peano z equal priority peano nonfree x in x end nonfree equal priority peano nonfree star x in x end nonfree equal priority peano free x set x to x end free equal priority peano free star x set x to x end free equal priority peano sub x is x where x is x end sub equal priority peano sub star x is x where x is x end sub equal priority system s equal priority axiom a one equal priority axiom a two equal priority axiom a three equal priority axiom a four equal priority axiom a five equal priority axiom s one equal priority axiom s two equal priority axiom s three equal priority axiom s four equal priority axiom s five equal priority axiom s six equal priority axiom s seven equal priority axiom s eight equal priority axiom s nine equal priority rule mp equal priority rule gen equal priority system prime s equal priority axiom prime a one equal priority axiom prime a two equal priority axiom prime a three equal priority axiom prime a four equal priority axiom prime a five equal priority axiom prime s one equal priority axiom prime s two equal priority axiom prime s three equal priority axiom prime s four equal priority axiom prime s five equal priority axiom prime s six equal priority axiom prime s seven equal priority axiom prime s eight equal priority axiom prime s nine equal priority rule prime mp equal priority rule prime gen equal priority double rule prime mp equal priority inference axiom prime a one equal priority rule hypothesize equal priority inference axiom prime a two equal priority inference inference axiom prime a two equal priority hypothetical rule prime mp equal priority double inference inference axiom prime a two equal priority double hypothetical rule prime mp equal priority mendelson lemma one eight equal priority inference mendelson lemma one eight equal priority rule repetition equal priority mendelson exercise one fourtyseven b equal priority mendelson exercise one fourtyseven c equal priority mendelson exercise one fourtyseven e equal priority mendelson lemma one eleven d equal priority hypothetical inference axiom prime a one equal priority hypothetical inference axiom prime a two equal priority hypothetical inference inference axiom prime a two equal priority hypothetical mendelson exercise one fourtyseven b equal priority hypothetical mendelson exercise one fourtyseven c equal priority mendelson lemma one eleven c equal priority mendelson exercise one fourtyeight d equal priority mendelson exercise one fourtyeight e equal priority mendelson exercise one fourtyeight h equal priority mendelson corollary one ten a equal priority mendelson corollary one ten b equal priority inference axiom prime s one equal priority inference inference axiom prime s one equal priority inference axiom prime s two equal priority hypothetical inference axiom prime s two equal priority inference inference axiom prime s nine equal priority rule induction equal priority mendelson proposition three two a equal priority mendelson proposition three two b equal priority inference mendelson proposition three two b equal priority mendelson proposition three two c equal priority inference inference mendelson proposition three two c equal priority hypothetical inference inference mendelson proposition three two c equal priority mendelson proposition three two d equal priority inference inference mendelson proposition three two d equal priority hypothetical inference inference mendelson proposition three two d equal priority mendelson proposition three two f equal priority mendelson proposition three two f i equal priority mendelson proposition three two f ii equal priority mendelson proposition three two g equal priority mendelson proposition three two g i equal priority mendelson proposition three two g ii equal priority mendelson proposition three two h equal priority mendelson proposition three two h i equal priority mendelson proposition three two h ii equal priority hypothesis equal priority instance equal priority conclusion end priority greater than preassociative priority x sub x end sub equal priority x prime equal priority x assoc x end assoc equal priority x set x to x end set equal priority x set multi x to x end set equal priority x peano var end priority greater than preassociative priority unicode start of text x end unicode text equal priority unicode end of text equal priority text x end text equal priority text x plus x equal priority text x plus indent x equal priority
unicode newline x equal priority unicode space x equal priority unicode exclamation mark x equal priority unicode quotation mark x equal priority unicode number sign x equal priority unicode dollar sign x equal priority unicode percent x equal priority unicode ampersand x equal priority unicode apostrophe x equal priority unicode left parenthesis x equal priority unicode right parenthesis x equal priority unicode asterisk x equal priority unicode plus sign x equal priority unicode comma x equal priority unicode hyphen x equal priority unicode period x equal priority unicode slash x equal priority unicode zero x equal priority unicode one x equal priority unicode two x equal priority unicode three x equal priority unicode four x equal priority unicode five x equal priority unicode six x equal priority unicode seven x equal priority unicode eight x equal priority unicode nine x equal priority unicode colon x equal priority unicode semicolon x equal priority unicode less than x equal priority unicode equal sign x equal priority unicode greater than x equal priority unicode question mark x equal priority unicode commercial at x equal priority unicode capital a x equal priority unicode capital b x equal priority unicode capital c x equal priority unicode capital d x equal priority unicode capital e x equal priority unicode capital f x equal priority unicode capital g x equal priority unicode capital h x equal priority unicode capital i x equal priority unicode capital j x equal priority unicode capital k x equal priority unicode capital l x equal priority unicode capital m x equal priority unicode capital n x equal priority unicode capital o x equal priority unicode capital p x equal priority unicode capital q x equal priority unicode capital r x equal priority unicode capital s x equal priority unicode capital t x equal priority unicode capital u x equal priority unicode capital v x equal priority unicode capital w x equal priority unicode capital x x equal priority unicode capital y x equal priority unicode capital z x equal priority unicode left bracket x equal priority unicode backslash x equal priority unicode right bracket x equal priority unicode circumflex x equal priority unicode underscore x equal priority unicode grave accent x equal priority unicode small a x equal priority unicode small b x equal priority unicode small c x equal priority unicode small d x equal priority unicode small e x equal priority unicode small f x equal priority unicode small g x equal priority unicode small h x equal priority unicode small i x equal priority unicode small j x equal priority unicode small k x equal priority unicode small l x equal priority unicode small m x equal priority unicode small n x equal priority unicode small o x equal priority unicode small p x equal priority unicode small q x equal priority unicode small r x equal priority unicode small s x equal priority unicode small t x equal priority unicode small u x equal priority unicode small v x equal priority unicode small w x equal priority unicode small x x equal priority unicode small y x equal priority unicode small z x equal priority unicode left brace x equal priority unicode vertical line x equal priority unicode right brace x equal priority unicode tilde x equal priority preassociative x greater than x equal priority postassociative x greater than x equal priority priority x equal x equal priority priority x end priority equal priority newline x equal priority macro newline x end priority greater than preassociative priority x bit nil equal priority x bit one equal priority binary equal priority x color x end color equal priority x color star x end color end priority greater than preassociative priority x apply x equal priority x tagged apply x end priority greater than preassociative priority x raw head equal priority x raw tail equal priority x cardinal untag equal priority x head equal priority x tail equal priority x is singular equal priority x is cardinal equal priority x is data equal priority x is atomic equal priority x cardinal retract equal priority x tagged retract equal priority x boolean retract equal priority x ref equal priority x id equal priority x debug equal priority x root equal priority x zeroth equal priority x first equal priority x second equal priority x third equal priority x fourth equal priority x fifth equal priority x sixth equal priority x seventh equal priority x eighth equal priority x ninth equal priority x is error equal priority x is metavar equal priority x is metaclosed equal priority x is metaclosed star equal priority x peano succ end priority greater than preassociative priority x times x equal priority x times zero x equal priority x peano times x end priority greater than preassociative priority x plus x equal priority x plus zero x equal priority x plus one x equal priority x minus x equal priority x minus zero x equal priority x minus one x equal priority x peano plus x end priority greater than preassociative priority x term plus x end plus equal priority x term union x equal priority x term minus x end minus end priority greater than postassociative priority x raw pair x equal priority x eager pair x equal priority x tagged pair x equal priority x untagged double x equal priority x pair x equal priority x double x end priority greater than postassociative priority x comma x end priority greater than preassociative priority x boolean equal x equal priority x data equal x equal priority x cardinal equal x equal priority x peano equal x equal priority x tagged equal x equal priority x math equal x equal priority x reduce to x equal priority x term equal x equal priority x term list equal x equal priority x term root equal x equal priority x term in x equal priority x term subset x equal priority x term set equal x equal priority x sequent equal x equal priority x free in x equal priority x free in star x equal priority x free for x in x equal priority x free for star x in x equal priority x claim in x equal priority x less x equal priority x less zero x equal priority x less one x equal priority x peano is x equal priority x is peano var end priority greater than preassociative priority not x equal priority peano not x end priority greater than preassociative priority x and x equal priority x macro and x equal priority x simple and x equal priority x claim and x equal priority x peano and x end priority greater than preassociative priority x or x equal priority x parallel x equal priority x macro or x equal priority x peano or x end priority greater than preassociative priority peano all x indeed x equal priority peano exist x indeed x end priority greater than postassociative priority x macro imply x equal priority x peano imply x equal priority x peano iff x end priority greater than postassociative priority x guard x equal priority x tagged guard x end priority greater than preassociative priority x select x else x end select end priority greater than preassociative priority lambda x dot x equal priority tagging x equal priority open if x then x else x equal priority let x be x in x equal priority let x abbreviate x in x end priority greater than preassociative priority x init equal priority x modus equal priority x verify equal priority x curry plus equal priority x curry minus equal priority x dereference end priority greater than preassociative priority x at x equal priority x modus ponens x equal priority x modus probans x equal priority x conclude x equal priority x macro modus ponens x equal priority x macro first modus ponens x macro second modus ponens x equal priority x hypothetical macro modus ponens x equal priority x hypothetical macro first modus ponens x hypothetical macro second modus ponens var x end priority greater than postassociative priority x infer x equal priority x endorse x equal priority x id est x end priority greater than preassociative priority all x indeed x end priority greater than postassociative priority x rule plus x end priority greater than postassociative priority x cut x end priority greater than preassociative priority x proves x end priority greater than preassociative priority x proof of x reads x equal priority line x because x indeed x end line x equal priority because x indeed x qed equal priority line x premise x end line x equal priority line x side condition x end line x equal priority arbitrary x end line x equal priority locally define x as x end line x equal priority line x hypothesis modus ponens x modus ponens x indeed x end line x equal priority line x hypothesis first modus ponens x modus ponens x indeed x end line x equal priority line x hypothesis second modus ponens x modus ponens x indeed x end line x equal priority line x hypothesis double modus ponens x modus ponens x modus ponens x indeed x end line x equal priority line x hypothesis indeed x end line x equal priority line x hypothesis because x indeed x end line x equal priority line x hypothesis raw because x indeed x end line x end priority greater than postassociative priority x
then x equal priority x
begin x
end x end priority greater than preassociative priority x tab x end priority greater than preassociative priority x row
x end priority greater than unicode end of text end define end math end left
end "
\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"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,