"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 expansion
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 meta t
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 meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end math
end "}
\display{$A2':$ "
begin math all meta a indeed all meta b indeed all meta c indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end math
end "}
\display{$A3':$ "
begin math all meta a indeed all meta b indeed parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end math
end "}
Samt en enkelt inferens regel:
\display{$MP':$ "
begin math all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b 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 intro var x macro modus ponens var y pyk "* macro modus ponens *" tex "#1.
\unrhd #2." end intro
end "
, som bliver makrodefinert til
"
begin math macro define var x macro modus ponens var y as rule prime mp modus ponens var x modus ponens var y end define end math
end ".
\subsubsection{Bevis $MP'_{d}$}
Det f\o{}rste bevis er
"
begin intro double rule prime mp pyk "double rule prime mp" tex "MP'_{d}" end intro
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 in theory system prime s lemma double rule prime mp says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta a infer meta b infer meta c end lemma end math
end "}
"
begin math system prime s proof of double rule prime mp reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b premise meta a end line line ell c premise meta b end line line ell d because ell a macro modus ponens ell b indeed meta b peano imply meta c end line because ell d macro modus ponens ell c indeed meta c qed end math
end " \\
Idet "
begin math double rule prime mp end math
end " er bevist, f\o{}lges eksemplet fra f\o{}r og
"
begin intro var x macro first modus ponens var y macro second modus ponens var z pyk "* macro first modus ponens * macro second modus ponens *" tex "#1.
\unrhd #2.
\unrhd #3." end intro
end "
introduceres, der p\aa{} samme m\aa{}de er makrodefineret til den dobbelte anvendelse
"
begin math macro define var x macro first modus ponens var y macro second modus ponens var z as double rule prime mp modus ponens var x modus ponens var y modus ponens var z end define end math
end "
.
\subsubsection{Bevis $A1'_{i}$}
Lemmaet
"
begin intro inference axiom prime a one pyk "inference axiom prime a one" tex "A1'_{i}" end intro
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 in theory system prime s lemma inference axiom prime a one says all meta a indeed all meta b indeed meta a infer meta b peano imply meta a end lemma end math
end "}
Beviset f\o{}leger: \\
"
begin math system prime s proof of inference axiom prime a one reads arbitrary meta a end line arbitrary meta b end line line ell a premise meta a end line line ell b because axiom prime a one indeed meta a peano imply meta b peano imply meta a end line because ell b macro modus ponens ell a indeed meta b peano imply meta a qed end math
end " \\
Da denne s\ae{}tning er essentiel i nogle af de f\o{}lgende afsnit, gives den navnet
"
begin intro rule hypothesize pyk "rule hypothesize" tex "Hypothesize" end intro
end "
, der er makrodefineret til s\ae{}tningen selv
"
begin math macro define rule hypothesize as inference axiom prime a one end define end math
end "
\subsubsection{Bevis $A2'_{i}$}
"
begin intro inference axiom prime a two pyk "inference axiom prime a two" tex "A2'_{i}" end intro
end "
er endnu en inferens version af et aksiom. Lemmaet og beviset er som nedenst\aa{}ende:
\display{
"
begin math in theory system prime s lemma inference axiom prime a two says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end lemma end math
end "}
"
begin math system prime s proof of inference axiom prime a two reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b because axiom prime a two indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line because ell b macro modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c qed end math
end "
\subsubsection{Bevis $A2'_{ii}$}
"
begin intro inference inference axiom prime a two pyk "inference inference axiom prime a two" tex "A2'_{ii}" end intro
end "
er den f\o{}rste dobbelte inferens version af et lemma, som det ses i
\display{
"
begin math in theory system prime s lemma inference inference axiom prime a two says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta a peano imply meta b infer meta a peano imply meta c end lemma end math
end "}
udskiftes to implikations-operatorer - heraf de to \textit{i}er. I beviset kan den foreg\aa{}ende s\ae{}tning udnyttes: \\
"
begin math system prime s proof of inference inference axiom prime a two reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b premise meta a peano imply meta b end line line ell c because inference axiom prime a two modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line because ell c macro modus ponens ell b indeed meta a peano imply meta c qed end math
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 intro hypothetical rule prime mp pyk "hypothetical rule prime mp" tex "MP'_{h}" end intro
end "
defineret til
"
begin math macro define hypothetical rule prime mp as inference inference axiom prime a two end define end math
end "
. Modus ponens blev f\o{}r defineret med $\unrhd{}$, herefter vil den hypotetiske version af denne (
"
begin intro var x hypothetical macro modus ponens var y pyk "* hypothetical macro modus ponens *" tex "#1.
\unrhd_h #2." end intro
end "
) blive defineret til
"
begin math macro define var x hypothetical macro modus ponens var y as hypothetical rule prime mp modus ponens var x modus ponens var y end define end math
end "
.
\subsubsection{Bevis $A2'_{iid}$}
Den f\o{}rste brug af dobbelt-navnet ses af
"
begin intro double inference inference axiom prime a two pyk "double inference inference axiom prime a two" tex "A2'_{iid}" end intro
end "
. S\ae{}tningen
\display{
"
begin math in theory system prime s lemma double inference inference axiom prime a two says all meta a indeed all meta b indeed all meta c indeed all meta d indeed meta a peano imply meta b peano imply meta c peano imply meta d infer meta a peano imply meta b infer meta a peano imply meta c infer meta a peano imply meta d end lemma end math
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 system prime s proof of double inference inference axiom prime a two reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line arbitrary meta d end line line ell a premise meta a peano imply meta b peano imply meta c peano imply meta d end line line ell b premise meta a peano imply meta b end line line ell c premise meta a peano imply meta c end line line ell d because inference inference axiom prime a two modus ponens ell a modus ponens ell b indeed meta a peano imply meta c peano imply meta d end line because inference inference axiom prime a two modus ponens ell d modus ponens ell c indeed meta a peano imply meta d qed end math
end " \\
Forholdes lemmaet til "
begin math double hypothetical rule prime mp end math
end ", ses det at dette er en dobbelt hypotetisk modus ponens.
"
begin intro double hypothetical rule prime mp pyk "double hypothetical rule prime mp" tex "MP'_{hd}" end intro
end "
bliver derfor makrodefineret til
"
begin math macro define double hypothetical rule prime mp as double inference inference axiom prime a two end define end math
end "
. P\aa{} samme m\aa{}de som f\o{}r bliver
"
begin intro var x hypothetical macro first modus ponens var y hypothetical macro second modus ponens var var z pyk "* hypothetical macro first modus ponens * hypothetical macro second modus ponens var *" tex "#1.
\unrhd_h #2.
\unrhd_h #3." end intro
end "
defineret
"
begin math 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 math
end "
.
\subsubsection{Bevis $1.8$}
"
begin intro mendelson lemma one eight pyk "mendelson lemma one eight" tex "Mendelson\ \textbf{1.8}" end intro
end "
er et grundl\ae{}ggende bevis i \cite{mendelson}. S\ae{}tningen -
\display{
"
begin math in theory system prime s lemma mendelson lemma one eight says all meta a indeed meta a peano imply meta a end lemma end math
end "}
- siger at noget medf\o{}rer sig selv. \\
"
begin math system prime s proof of mendelson lemma one eight reads arbitrary meta a end line line ell a because axiom prime a one indeed meta a peano imply parenthesis meta a peano imply meta a end parenthesis peano imply meta a end line line ell b because axiom prime a one indeed meta a peano imply meta a peano imply meta a end line because inference inference axiom prime a two modus ponens ell a modus ponens ell b indeed meta a peano imply meta a qed end math
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 intro inference mendelson lemma one eight pyk "inference mendelson lemma one eight" tex "Mendelson\ \textbf{1.8}_{i}" end intro
end "
som siger
"
begin math in theory system prime s lemma inference mendelson lemma one eight says all meta a indeed meta a infer meta a end lemma end math
end "
, kan virke besynderligt, men efterf\o{}lgende vil dette vise sig nyttigt: \\
"
begin math system prime s proof of inference mendelson lemma one eight reads arbitrary meta a end line line ell a premise meta a end line line ell b because mendelson lemma one eight indeed meta a peano imply meta a end line because ell b macro modus ponens ell a indeed meta a qed end math
end " \\
Beviet navngives
"
begin intro rule repetition pyk "rule repetition" tex "Repetition" end intro
end "
via makrodefinitionen \linebreak[4]
"
begin math macro define rule repetition as inference mendelson lemma one eight end define end math
end "
.
\subsubsection{Bevis $1.47\ b$}
"
begin intro mendelson exercise one fourtyseven b pyk "mendelson exercise one fourtyseven b" tex "Mendelson\ \textbf{1.47}\ b" end intro
end "
er en form for transitivets lemma p\aa{} implikation:
\display{
"
begin math in theory system prime s lemma mendelson exercise one fourtyseven b says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b infer meta b peano imply meta c infer meta a peano imply meta c end lemma end math
end "}
Beviset udnytter flere af de foreg\aa{}ende lemmaer: \\
"
begin math system prime s proof of mendelson exercise one fourtyseven b reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b end line line ell b premise meta b peano imply meta c end line line ell c because inference axiom prime a one modus ponens ell b indeed meta a peano imply meta b peano imply meta c end line because inference inference axiom prime a two modus ponens ell c modus ponens ell a indeed meta a peano imply meta c qed end math
end "
\subsubsection{Bevis $1.47\ c$}
"
begin intro mendelson exercise one fourtyseven c pyk "mendelson exercise one fourtyseven c" tex "Mendelson\ \textbf{1.47}\ c" end intro
end "
permutere r\ae{}kkef\o{}lgen af bestemte termer:
\display{
"
begin math in theory system prime s lemma mendelson exercise one fourtyseven c says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b peano imply meta a peano imply meta c end lemma end math
end "}
For f\o{}rste gang benyttes den hypotetiske version af modus ponens: \\
"
begin math system prime s proof of mendelson exercise one fourtyseven c reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b because inference axiom prime a two modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line line ell c because inference axiom prime a one modus ponens ell b indeed meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line line ell d because axiom prime a one indeed meta b peano imply meta a peano imply meta b end line because ell c hypothetical macro modus ponens ell d indeed meta b peano imply meta a peano imply meta c qed end math
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 intro mendelson exercise one fourtyseven e pyk "mendelson exercise one fourtyseven e" tex "Mendelson\ \textbf{1.47}\ e" end intro
end "
siger f\o{}lgende:
\display{
"
begin math in theory system prime s lemma mendelson exercise one fourtyseven e says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b infer meta a peano imply meta c end lemma end math
end "}
Nedenst\aa{}ende beviser "
begin math mendelson exercise one fourtyseven e end math
end ": \\
"
begin math system prime s proof of mendelson exercise one fourtyseven e reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b premise meta b end line line ell c because mendelson exercise one fourtyseven c modus ponens ell a indeed meta b peano imply meta a peano imply meta c end line because ell c macro modus ponens ell b indeed meta a peano imply meta c qed end math
end "
\section{Deduktion}
\subsection{Definitioner}
Proposition 1.9 i \cite{mendelson} beviser, at man fra "
begin math meta a infer meta b 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 meta b peano imply meta c infer meta c peano imply meta d infer meta b peano imply meta d end math
end "}
Hvor "
begin math meta b peano imply meta c end math
end " er den f\o{}rste pr\ae{}misse, "
begin math meta c peano imply meta d end math
end " den anden, "
begin math meta b end math
end " er hypotesen og "
begin math meta d 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 intro hypothesis pyk "hypothesis" tex "\mathsf{hyp}" end intro
end "
v\ae{}re en pladsholder for en given hypotese,
"
begin intro instance pyk "instance" tex "\mathsf{instance}" end intro
end "
for en instanciering af et aksiom eller lemma og
"
begin intro conclusion pyk "conclusion" tex "\mathsf{conclusion}" end intro
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 intro mendelson lemma one eleven d pyk "mendelson lemma one eleven d" tex "Mendelson\ \textbf{1.11}\ d" end intro
end "
vil herefter v\ae{}re navnet p\aa{} eksemplet, hvor s\ae{}tningen siger:
\display{
"
begin math in theory system prime s lemma mendelson lemma one eleven d says all meta a indeed all meta b indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply meta a end lemma end math
end "}
Idet udf\o{}relsen af beviset gennemg\aa{}s linje for linje, opn\aa{}s en enkelt anskuelse: \\
"
begin math system prime s proof of mendelson lemma one eleven d reads arbitrary meta a end line arbitrary meta b end line line ell a because mendelson lemma one eight indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply peano not meta a peano imply peano not meta b end line line ell b because axiom prime a three indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line line ell c because axiom prime a one indeed parenthesis parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line line ell d because ell c macro modus ponens ell b indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line line ell e because axiom prime a one indeed meta b peano imply peano not meta a peano imply meta b end line line ell f because axiom prime a one indeed parenthesis meta b peano imply peano not meta a peano imply meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply peano not meta a peano imply meta b end line line ell g because ell f macro modus ponens ell e indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply peano not meta a peano imply meta b end line line ell h because axiom prime a two indeed parenthesis parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end parenthesis peano imply parenthesis parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line line ell i because ell h macro modus ponens ell d indeed parenthesis parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line line ell j because ell i macro modus ponens ell a indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line because hypothetical mendelson exercise one fourtyseven b modus ponens ell g modus ponens ell j indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply meta a qed end math
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 system prime s proof of mendelson lemma one eleven d reads arbitrary meta a end line arbitrary meta b end line line ell a because mendelson lemma one eight indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply peano not meta a peano imply peano not meta b end line line ell b because axiom prime a three indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line line ell c because rule hypothesize modus ponens ell b indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line line ell d because axiom prime a one indeed meta b peano imply peano not meta a peano imply meta b end line line ell e because rule hypothesize modus ponens ell d indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply peano not meta a peano imply meta b end line line ell f because ell c hypothetical macro modus ponens ell a indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line because hypothetical mendelson exercise one fourtyseven b modus ponens ell e modus ponens ell f indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply meta a qed end math
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 rule hypothesize 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 intro line var l hypothesis indeed var i end line var p pyk "line * hypothesis indeed * end line *" tex "
\newline \makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}\makebox [0.4\textwidth ][l]{$Hypothesis{}
\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$#2.
$\hfill \makebox [0mm][l]{\quad ;}}#3." end intro
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 macro define line var l hypothesis indeed var i end line var p as parenthesis mendelson lemma one eight conclude var i peano imply var i cut let hypothesis abbreviate var i in let var l abbreviate var i peano imply var i in var p end parenthesis end define end math
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 rule repetition end math
end " til at 'udfylde' den sidste linje.
\tex{
"
begin math tex name define line var l hypothesis indeed var i end line var p as "
Line \, #1.
:\bullet{}\ Hypothesis
\gg #2.
; #3." end define end math
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 rule hypothesize 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 intro line var l hypothesis because var a indeed var i end line var p pyk "line * hypothesis because * indeed * end line *" tex "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$#2.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#3.
$\hfill \makebox [0mm][l]{\quad ;}}#4." end intro
end "
laver automatisk en "
begin math rule hypothesize end math
end " p\aa{} en instancering af en regel.
\display{
"
begin math macro define line var l hypothesis because var a indeed var i end line var p as parenthesis var a conclude var i cut rule hypothesize modus ponens var i conclude hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p end parenthesis end define end math
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 rule hypothesize end math
end " - bem\ae{}rk brugen af "
begin math hypothesis end math
end ", der opretholder proposition 1.9.
\tex{
"
begin math tex name define line var l hypothesis because var a indeed var i end line var p as "
Line \, #1.
:\bullet{}\ #2.
\gg #3.
; #4." end define end math
end "}
Til instanciering af en regel med brug af modus ponens, kan konstruktionen
"
begin intro line var l hypothesis raw because var a indeed var i end line var p pyk "line * hypothesis raw because * indeed * end line *" tex "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$#2.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#3.
$\hfill \makebox [0mm][l]{\quad ;}}#4." end intro
end "
bruges. Selve makrodefinitionen:
\display{
"
begin math macro define line var l hypothesis raw because var a indeed var i end line var p as parenthesis var a conclude hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p end parenthesis end define end math
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 tex name define line var l hypothesis raw because var a indeed var i end line var p as "
Line \, #1.
:\bullet{}\ #2.
\gg #3.
; #4." end define end math
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 intro line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p pyk "line * hypothesis modus ponens * modus ponens * indeed * end line *" tex "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$#2.
\unrhd{} #3.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#4.
$\hfill \makebox [0mm][l]{\quad ;}}#5." end intro
end "
er blot en hypotetisk brug af modus ponens:
\display{
"
begin math macro define line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p as parenthesis var u hypothetical macro modus ponens var v conclude hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p end parenthesis end define end math
end "}
\tex{
"
begin math tex name define line var l hypothesis modus ponens var u modus ponens var v indeed var i end line var p as "
Line \, #1.
:\bullet{}\ #2.
\unrhd{} #3.
\gg #4.
; #5." end define end math
end "}
"
begin intro line var l hypothesis double modus ponens var u modus ponens var v modus ponens var z indeed var i end line var p pyk "line * hypothesis double modus ponens * modus ponens * modus ponens * indeed * end line *" tex "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$ #2.
\unrhd{} #3.
\unrhd{} #4.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#5.
$\hfill \makebox [0mm][l]{\quad ;}}#6." end intro
end "
definere den dobbelte brug af modus ponens:
\display{
"
begin math macro define line var l hypothesis double modus ponens var u modus ponens var v modus ponens var z indeed var i end line var p as parenthesis var u hypothetical macro first modus ponens var v hypothetical macro second modus ponens var var z conclude hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p end parenthesis end define end math
end "}
\tex{
"
begin math tex name define line var l hypothesis double modus ponens var u modus ponens var v modus ponens var z indeed var i end line var p as "
Line \, #1.
:\bullet{}\ #2.
\unrhd{} #3.
\unrhd{} #4.
\gg #5.
; #6." end define end math
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 intro line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p pyk "line * hypothesis first modus ponens * modus ponens * indeed * end line *" tex "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$ #2.
\circ{} \unrhd{} #3.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#4.
$\hfill \makebox [0mm][l]{\quad ;}}#5." end intro
end "
benyttes - cirklen angiver hvilket argument der er eksternt.
\display{
"
begin math macro define line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p as parenthesis mendelson exercise one fourtyseven b modus ponens var v modus ponens var u conclude hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p end parenthesis end define end math
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 tex name define line var l hypothesis first modus ponens var u modus ponens var v indeed var i end line var p as "
Line \, #1.
:\bullet{}\ #2.
\circ{} \unrhd{} #3.
\gg #4.
; #5." end define end math
end "}
Ved modus ponens med reference eksternt i 2. argument, kan
"
begin intro line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p pyk "line * hypothesis second modus ponens * modus ponens * indeed * end line *" tex "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:$\bullet$}$ #2.
\unrhd{} #3.
\circ{} {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#4.
$\hfill \makebox [0mm][l]{\quad ;}}#5." end intro
end "
udnyttes. Makrodefinitionen er igen simpel:
\display{
"
begin math macro define line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p as parenthesis mendelson exercise one fourtyseven e modus ponens var u modus ponens var v conclude hypothesis peano imply var i cut let var l abbreviate hypothesis peano imply var i in var p end parenthesis end define end math
end "}
\tex{
"
begin math tex name define line var l hypothesis second modus ponens var u modus ponens var v indeed var i end line var p as "
Line \, #1.
:\bullet{}\ #2.
\unrhd{} #3.
\circ{} \gg #4.
; #5." end define end math
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 system prime s proof of mendelson lemma one eleven d reads arbitrary meta a end line arbitrary meta b end line line ell a hypothesis indeed peano not meta a peano imply peano not meta b end line line ell b hypothesis because axiom prime a three indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line line ell c hypothesis because axiom prime a one indeed meta b peano imply peano not meta a peano imply meta b end line line ell d hypothesis modus ponens ell b modus ponens ell a indeed parenthesis peano not meta a peano imply meta b end parenthesis peano imply meta a end line line ell e hypothesis raw because hypothetical mendelson exercise one fourtyseven b modus ponens ell c modus ponens ell d indeed meta b peano imply meta a end line because rule repetition modus ponens ell e indeed parenthesis peano not meta a peano imply peano not meta b end parenthesis peano imply meta b peano imply meta a qed end math
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 intro hypothetical inference axiom prime a one pyk "hypothetical inference axiom prime a one" tex "A1'_{ih}" end intro
end "
\display{
"
begin math in theory system prime s lemma hypothetical inference axiom prime a one says all meta h indeed all meta a indeed all meta b indeed meta h peano imply meta a infer meta h peano imply meta b peano imply meta a end lemma end math
end "}
"
begin math system prime s proof of hypothetical inference axiom prime a one reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line line ell a premise meta h peano imply meta a end line line ell b hypothesis indeed meta h end line line ell c hypothesis because axiom prime a one indeed meta a peano imply meta b peano imply meta a end line line ell e hypothesis modus ponens ell c modus ponens ell a indeed meta b peano imply meta a end line because rule repetition modus ponens ell e indeed meta h peano imply meta b peano imply meta a qed end math
end "
\subsubsection{Bevis $A2'_{ih}$}
"
begin intro hypothetical inference axiom prime a two pyk "hypothetical inference axiom prime a two" tex "A2'_{ih}" end intro
end "
\display{
"
begin math in theory system prime s lemma hypothetical inference axiom prime a two says all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano imply meta b peano imply meta c infer meta h peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end lemma end math
end "}
"
begin math system prime s proof of hypothetical inference axiom prime a two reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta h peano imply meta a peano imply meta b peano imply meta c end line line ell c hypothesis indeed meta h end line line ell d hypothesis because axiom prime a two indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line line ell e hypothesis modus ponens ell d modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line because rule repetition modus ponens ell e indeed meta h peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c qed end math
end "
\subsubsection{Bevis $A2'_{iih}$}
"
begin intro hypothetical inference inference axiom prime a two pyk "hypothetical inference inference axiom prime a two" tex "A2'_{iih}" end intro
end "
\display{
"
begin math in theory system prime s lemma hypothetical inference inference axiom prime a two says all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano imply meta b peano imply meta c infer meta h peano imply meta a peano imply meta b infer meta h peano imply meta a peano imply meta c end lemma end math
end "}
"
begin math system prime s proof of hypothetical inference inference axiom prime a two reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta h peano imply meta a peano imply meta b peano imply meta c end line line ell b premise meta h peano imply meta a peano imply meta b end line line ell c hypothesis indeed meta h end line line ell d hypothesis because axiom prime a two indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line line ell e hypothesis double modus ponens ell d modus ponens ell a modus ponens ell b indeed meta a peano imply meta c end line because rule repetition modus ponens ell e indeed meta h peano imply meta a peano imply meta c qed end math
end "
\subsubsection{Bevis $1.47\ b_{h}$}
\label{sssec:hyp_one_ fourtyseven_b}
"
begin intro hypothetical mendelson exercise one fourtyseven b pyk "hypothetical mendelson exercise one fourtyseven b" tex "Mendelson\ \textbf{1.47}\ b_{h}" end intro
end "
\display{
"
begin math in theory system prime s lemma hypothetical mendelson exercise one fourtyseven b says all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano imply meta b infer meta h peano imply meta b peano imply meta c infer meta h peano imply meta a peano imply meta c end lemma end math
end "}
"
begin math system prime s proof of hypothetical mendelson exercise one fourtyseven b reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta h peano imply meta a peano imply meta b end line line ell b premise meta h peano imply meta b peano imply meta c end line line ell c hypothesis indeed meta h end line line ell d hypothesis raw because hypothetical inference axiom prime a one modus ponens ell b indeed meta a peano imply meta b peano imply meta c end line line ell e hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell d modus ponens ell a indeed meta a peano imply meta c end line because rule repetition modus ponens ell e indeed meta h peano imply meta a peano imply meta c qed end math
end "
\subsubsection{Bevis $1.47\ c_{h}$}
"
begin intro hypothetical mendelson exercise one fourtyseven c pyk "hypothetical mendelson exercise one fourtyseven c" tex "Mendelson\ \textbf{1.47}\ c_{h}" end intro
end "
\display{
"
begin math in theory system prime s lemma hypothetical mendelson exercise one fourtyseven c says all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano imply meta b peano imply meta c infer meta h peano imply meta b peano imply meta a peano imply meta c end lemma end math
end "}
"
begin math system prime s proof of hypothetical mendelson exercise one fourtyseven c reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta h peano imply meta a peano imply meta b peano imply meta c end line line ell b hypothesis indeed meta h end line line ell c hypothesis raw because hypothetical inference axiom prime a two modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line line ell e hypothesis raw because hypothetical inference axiom prime a one modus ponens ell c indeed meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line line ell f hypothesis because axiom prime a one indeed meta b peano imply meta a peano imply meta b end line line ell g hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell e modus ponens ell f indeed meta b peano imply meta a peano imply meta c end line because rule repetition modus ponens ell g indeed meta h peano imply meta b peano imply meta a peano imply meta c qed end math
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 intro mendelson lemma one eleven c pyk "mendelson lemma one eleven c" tex "Mendelson\ \textbf{1.11}\ c" end intro
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 in theory system prime s lemma mendelson lemma one eleven c says all meta a indeed all meta b indeed peano not meta a peano imply meta a peano imply meta b end lemma end math
end "}
Nedenst\aa{}ende viser beviset af eksemplet: \\
"
begin math system prime s proof of mendelson lemma one eleven c reads arbitrary meta a end line arbitrary meta b end line line ell a hypothesis indeed peano not meta a end line line ell b hypothesis because mendelson lemma one eight indeed meta a peano imply meta a end line line ell c hypothesis because axiom prime a one indeed meta a peano imply peano not meta b peano imply meta a end line line ell d hypothesis raw because hypothetical inference axiom prime a one modus ponens ell c indeed meta a peano imply meta a peano imply peano not meta b peano imply meta a end line line ell e hypothesis because axiom prime a one indeed peano not meta a peano imply peano not meta b peano imply peano not meta a end line line ell f hypothesis raw because hypothetical inference axiom prime a one modus ponens ell e indeed meta a peano imply peano not meta a peano imply peano not meta b peano imply peano not meta a end line line ell g hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell d modus ponens ell b indeed meta a peano imply peano not meta b peano imply meta a end line line ell h hypothesis modus ponens ell e modus ponens ell a indeed peano not meta b peano imply peano not meta a end line line ell i hypothesis raw because hypothetical inference axiom prime a one modus ponens ell h indeed meta a peano imply peano not meta b peano imply peano not meta a end line line ell j hypothesis because axiom prime a three indeed parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end line line ell k hypothesis raw because hypothetical inference axiom prime a one modus ponens ell j indeed meta a peano imply parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end line line ell l hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell k modus ponens ell i indeed meta a peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end line line ell m hypothesis raw because hypothetical inference inference axiom prime a two modus ponens ell l modus ponens ell g indeed meta a peano imply meta b end line because rule repetition modus ponens ell m indeed peano not meta a peano imply meta a peano imply meta b qed end math
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 hypothesis peano and 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 intro mendelson exercise one fourtyeight d pyk "mendelson exercise one fourtyeight d" tex "Mendelson\ \textbf{1.48}\ d" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson exercise one fourtyeight d says all meta a indeed all meta b indeed meta a peano and meta b peano imply meta a end lemma end math
end "}
"
begin intro mendelson exercise one fourtyeight e pyk "mendelson exercise one fourtyeight e" tex "Mendelson\ \textbf{1.48}\ e" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson exercise one fourtyeight e says all meta a indeed all meta b indeed meta a peano and meta b peano imply meta b end lemma end math
end "}
"
begin intro mendelson exercise one fourtyeight h pyk "mendelson exercise one fourtyeight h" tex "Mendelson\ \textbf{1.48}\ h" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson exercise one fourtyeight h says all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a peano and meta b end lemma end math
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 intro mendelson corollary one ten a pyk "mendelson corollary one ten a" tex "Mendelson\ \textbf{1.10}\ a" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson corollary one ten a says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b infer meta b peano imply meta c infer meta a peano imply meta c end lemma end math
end "}
"
begin math system prime s proof of mendelson corollary one ten a reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b end line line ell b premise meta b peano imply meta c end line line ell c hypothesis indeed meta a end line line ell d hypothesis first modus ponens ell a modus ponens ell c indeed meta b end line line ell e hypothesis first modus ponens ell b modus ponens ell d indeed meta c end line because rule repetition modus ponens ell e indeed meta a peano imply meta c qed end math
end "
\subsubsection{Bevis $1.10\ b$}
"
begin intro mendelson corollary one ten b pyk "mendelson corollary one ten b" tex "Mendelson\ \textbf{1.10}\ b" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson corollary one ten b says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b infer meta a peano imply meta c end lemma end math
end "}
"
begin math system prime s proof of mendelson corollary one ten b reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b premise meta b end line line ell c hypothesis indeed meta a end line line ell d hypothesis first modus ponens ell a modus ponens ell c indeed meta b peano imply meta c end line line ell e hypothesis second modus ponens ell d modus ponens ell b indeed meta c end line because rule repetition modus ponens ell e indeed meta a peano imply meta c qed end math
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 meta f
end "\ ;\ "
begin meta f
end " \Rightarrow{} "
begin meta f
end "\ ;\ "
begin all meta v indeed meta f
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 meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub endorse peano all meta x indeed meta b peano imply meta a end math
end "}
\display{$A5':$ "
begin math all meta x indeed all meta a indeed all meta b indeed peano nonfree quote meta x end quote in quote meta a end quote end nonfree endorse peano all meta x indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply peano all meta x indeed meta b end math
end "}
\display{$Gen':$ "
begin math all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a 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 meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end math
end "}
\display{$S2':$ "
begin math all meta a indeed all meta b indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end math
end "}
\display{$S3':$ "
begin math all meta a indeed not peano zero peano is meta a peano succ end math
end "}
\display{$S4':$ "
begin math all meta a indeed all meta b indeed meta a peano succ peano is meta b peano succ peano imply meta a peano is meta b end math
end "}
\display{$S5':$ "
begin math all meta a indeed meta a peano plus peano zero peano is meta a end math
end "}
\display{$S6':$ "
begin math all meta a indeed all meta b indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end math
end "}
\display{$S7':$ "
begin math all meta a indeed meta a peano times peano zero peano is peano zero end math
end "}
\display{$S8':$ "
begin math all meta a indeed all meta b indeed meta a peano times parenthesis meta b peano succ end parenthesis peano is parenthesis meta a peano times meta b end parenthesis peano plus meta a end math
end "}
\display{$S9':$ "
begin math all meta a indeed all meta b indeed all meta c indeed all meta x indeed macro newline peano sub meta b is meta a where meta x is peano zero end sub endorse peano sub meta c is meta a where meta x is meta x peano succ end sub endorse macro newline meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end math
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 intro inference axiom prime s one pyk "inference axiom prime s one" tex "S1'_{i}" end intro
end "
\display{
"
begin math in theory system prime s lemma inference axiom prime s one says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b infer meta a peano is meta c peano imply meta b peano is meta c end lemma end math
end "}
"
begin math system prime s proof of inference axiom prime s one reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano is meta b end line line ell b because axiom prime s one indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end line because ell b macro modus ponens ell a indeed meta a peano is meta c peano imply meta b peano is meta c qed end math
end "
\subsubsection{Bevis $S1'_{ii}$}
"
begin intro inference inference axiom prime s one pyk "inference inference axiom prime s one" tex "S1'_{ii}" end intro
end "
\display{
"
begin math in theory system prime s lemma inference inference axiom prime s one says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b infer meta a peano is meta c infer meta b peano is meta c end lemma end math
end "}
"
begin math system prime s proof of inference inference axiom prime s one reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano is meta b end line line ell b premise meta a peano is meta c end line line ell c because inference axiom prime s one modus ponens ell a indeed meta a peano is meta c peano imply meta b peano is meta c end line because ell c macro modus ponens ell b indeed meta b peano is meta c qed end math
end "
\subsubsection{Bevis $S2'_{i}$}
"
begin intro inference axiom prime s two pyk "inference axiom prime s two" tex "S2'_{i}" end intro
end "
\display{
"
begin math in theory system prime s lemma inference axiom prime s two says all meta a indeed all meta b indeed meta a peano is meta b infer meta a peano succ peano is meta b peano succ end lemma end math
end "}
"
begin math system prime s proof of inference axiom prime s two reads arbitrary meta a end line arbitrary meta b end line line ell a premise meta a peano is meta b end line line ell b because axiom prime s two indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end line because ell b macro modus ponens ell a indeed meta a peano succ peano is meta b peano succ qed end math
end "
\subsubsection{Bevis $S2'_{ih}$}
"
begin intro hypothetical inference axiom prime s two pyk "hypothetical inference axiom prime s two" tex "S2'_{ih}" end intro
end "
\display{
"
begin math in theory system prime s lemma hypothetical inference axiom prime s two says all meta h indeed all meta a indeed all meta b indeed meta h peano imply meta a peano is meta b infer meta h peano imply meta a peano succ peano is meta b peano succ end lemma end math
end "}
"
begin math system prime s proof of hypothetical inference axiom prime s two reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line line ell a premise meta h peano imply meta a peano is meta b end line line ell b hypothesis indeed meta h end line line ell c hypothesis because axiom prime s two indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end line line ell d hypothesis modus ponens ell c modus ponens ell a indeed meta a peano succ peano is meta b peano succ end line because rule repetition modus ponens ell d indeed meta h peano imply meta a peano succ peano is meta b peano succ qed end math
end "
\subsubsection{Bevis $S9'_{ii}$}
"
begin intro inference inference axiom prime s nine pyk "inference inference axiom prime s nine" tex "S9'_{ii}" end intro
end "
er en inferens-version af induktions-aksiomet. I selve s\ae{}tningen, er to implikationsoperatoere blevet udskiftet:
\display{
"
begin math in theory system prime s lemma inference inference axiom prime s nine says all meta a indeed all meta b indeed all meta c indeed all meta y indeed peano sub meta b is meta a where meta y is peano zero end sub endorse peano sub meta c is meta a where meta y is meta y peano succ end sub endorse macro newline meta b infer peano all meta y indeed parenthesis meta a peano imply meta c end parenthesis infer peano all meta y indeed meta a end lemma end math
end "}
Selve beviset er ligefrem, det skal dog bem\ae{}rkes hvordan sidebetingelser kan elimineres: \\
"
begin math system prime s proof of inference inference axiom prime s nine reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line arbitrary meta y end line line ell a side condition peano sub meta b is meta a where meta y is peano zero end sub end line line ell b side condition peano sub meta c is meta a where meta y is meta y peano succ end sub end line line ell c premise meta b end line line ell d premise peano all meta y indeed parenthesis meta a peano imply meta c end parenthesis end line line ell e because axiom prime s nine modus probans ell a modus probans ell b indeed meta b peano imply peano all meta y indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta y indeed meta a end line because ell e macro first modus ponens ell c macro second modus ponens ell d indeed peano all meta y indeed meta a qed end math
end "
\subsubsection{Bevis $Induction$}
For at lette anvendelsen af induktion er s\ae{}tningen
"
begin intro rule induction pyk "rule induction" tex "Induction" end intro
end "
blevet lavet, s\ae{}tningen siger f\o{}lgende:
\display{
"
begin math in theory system prime s lemma rule induction says all meta a indeed all meta b indeed all meta c indeed all meta y indeed peano sub meta b is meta a where meta y is peano zero end sub endorse peano sub meta c is meta a where meta y is meta y peano succ end sub endorse macro newline peano sub quote meta a end quote is quote meta a end quote where quote meta y end quote is quote meta y end quote end sub endorse meta b infer meta a peano imply meta c infer meta a end lemma end math
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 system prime s proof of rule induction reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line arbitrary meta y end line line ell a side condition peano sub meta b is meta a where meta y is peano zero end sub end line line ell b side condition peano sub meta c is meta a where meta y is meta y peano succ end sub end line line ell w side condition peano sub quote meta a end quote is quote meta a end quote where quote meta y end quote is quote meta y end quote end sub end line line ell c premise meta b end line line ell d premise meta a peano imply meta c end line line ell e because rule prime gen modus ponens ell d indeed peano all meta y indeed parenthesis meta a peano imply meta c end parenthesis end line line ell f because inference inference axiom prime s nine modus probans ell a modus probans ell b modus ponens ell c modus ponens ell e indeed peano all meta y indeed meta a end line line ell g because axiom prime a four modus probans ell w indeed peano all meta y indeed meta a peano imply meta a end line because ell g macro modus ponens ell f indeed meta a qed end math
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 intro mendelson proposition three two a pyk "mendelson proposition three two a" tex "Mendelson\ \textbf{3.2}\ a" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two a says all meta a indeed meta a peano is meta a end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two a reads arbitrary meta a end line line ell a because axiom prime s five indeed meta a peano plus peano zero peano is meta a end line because inference inference axiom prime s one modus ponens ell a modus ponens ell a indeed meta a peano is meta a qed end math
end "
\subsubsection{Bevis $3.2\ b$}
"
begin intro mendelson proposition three two b pyk "mendelson proposition three two b" tex "Mendelson\ \textbf{3.2}\ b" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two b says all meta a indeed all meta b indeed meta a peano is meta b peano imply meta b peano is meta a end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two b reads arbitrary meta a end line arbitrary meta b end line line ell a because axiom prime s one indeed meta a peano is meta b peano imply meta a peano is meta a peano imply meta b peano is meta a end line line ell b because mendelson proposition three two a indeed meta a peano is meta a end line because mendelson corollary one ten b modus ponens ell a modus ponens ell b indeed meta a peano is meta b peano imply meta b peano is meta a qed end math
end "
\subsubsection{Bevis $3.2\ b_{i}$}
"
begin intro inference mendelson proposition three two b pyk "inference mendelson proposition three two b" tex "Mendelson\ \textbf{3.2}\ b_{i}" end intro
end "
"
begin math in theory system prime s lemma inference mendelson proposition three two b says all meta a indeed all meta b indeed meta a peano is meta b infer meta b peano is meta a end lemma end math
end "
"
begin math system prime s proof of inference mendelson proposition three two b reads arbitrary meta a end line arbitrary meta b end line line ell a premise meta a peano is meta b end line line ell b because mendelson proposition three two b indeed meta a peano is meta b peano imply meta b peano is meta a end line because ell b macro modus ponens ell a indeed meta b peano is meta a qed end math
end "
\subsubsection{Bevis $3.2\ c$}
"
begin intro mendelson proposition three two c pyk "mendelson proposition three two c" tex "Mendelson\ \textbf{3.2}\ c" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two c says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two c reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a because axiom prime s one indeed meta b peano is meta a peano imply meta b peano is meta c peano imply meta a peano is meta c end line line ell b because mendelson proposition three two b indeed meta a peano is meta b peano imply meta b peano is meta a end line because mendelson corollary one ten a modus ponens ell b modus ponens ell a indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c qed end math
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 intro inference inference mendelson proposition three two c pyk "inference inference mendelson proposition three two c" tex "Mendelson\ \textbf{3.2}\ c_{ii}" end intro
end "
\display{
"
begin math in theory system prime s lemma inference inference mendelson proposition three two c says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b infer meta b peano is meta c infer meta a peano is meta c end lemma end math
end "}
"
begin math system prime s proof of inference inference mendelson proposition three two c reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano is meta b end line line ell b premise meta b peano is meta c end line line ell c because mendelson proposition three two c indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c end line because ell c macro first modus ponens ell a macro second modus ponens ell b indeed meta a peano is meta c qed end math
end "
\subsubsection{Bevis $3.2\ c_{iih}$}
"
begin intro hypothetical inference inference mendelson proposition three two c pyk "hypothetical inference inference mendelson proposition three two c" tex "Mendelson\ \textbf{3.2}\ c_{iih}" end intro
end "
\display{
"
begin math in theory system prime s lemma hypothetical inference inference mendelson proposition three two c says all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano is meta b infer meta h peano imply meta b peano is meta c infer meta h peano imply meta a peano is meta c end lemma end math
end "}
"
begin math system prime s proof of hypothetical inference inference mendelson proposition three two c reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta h peano imply meta a peano is meta b end line line ell b premise meta h peano imply meta b peano is meta c end line line ell c hypothesis indeed meta h end line line ell d hypothesis because mendelson proposition three two c indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c end line line ell e hypothesis double modus ponens ell d modus ponens ell a modus ponens ell b indeed meta a peano is meta c end line because rule repetition modus ponens ell e indeed meta h peano imply meta a peano is meta c qed end math
end "
\subsubsection{Bevis $3.2\ d$}
"
begin intro mendelson proposition three two d pyk "mendelson proposition three two d" tex "Mendelson\ \textbf{3.2}\ d" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two d says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta c peano is meta b peano imply meta a peano is meta c end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two d reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a because mendelson proposition three two c indeed meta a peano is meta b peano imply meta b peano is meta c peano imply meta a peano is meta c end line line ell b because mendelson exercise one fourtyseven c modus ponens ell a indeed meta b peano is meta c peano imply meta a peano is meta b peano imply meta a peano is meta c end line line ell c because mendelson proposition three two b indeed meta c peano is meta b peano imply meta b peano is meta c end line line ell d because mendelson corollary one ten a modus ponens ell c modus ponens ell b indeed meta c peano is meta b peano imply meta a peano is meta b peano imply meta a peano is meta c end line because mendelson exercise one fourtyseven c modus ponens ell d indeed meta a peano is meta b peano imply meta c peano is meta b peano imply meta a peano is meta c qed end math
end "
\subsubsection{Bevis $3.2\ d_{ii}$}
"
begin intro inference inference mendelson proposition three two d pyk "inference inference mendelson proposition three two d" tex "Mendelson\ \textbf{3.2}\ d_{ii}" end intro
end "
\display{
"
begin math in theory system prime s lemma inference inference mendelson proposition three two d says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b infer meta c peano is meta b infer meta a peano is meta c end lemma end math
end "}
"
begin math system prime s proof of inference inference mendelson proposition three two d reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano is meta b end line line ell b premise meta c peano is meta b end line line ell c because mendelson proposition three two d indeed meta a peano is meta b peano imply meta c peano is meta b peano imply meta a peano is meta c end line because ell c macro first modus ponens ell a macro second modus ponens ell b indeed meta a peano is meta c qed end math
end "
\subsubsection{Bevis $3.2\ d_{iih}$}
"
begin intro hypothetical inference inference mendelson proposition three two d pyk "hypothetical inference inference mendelson proposition three two d" tex "Mendelson\ \textbf{3.2}\ d_{iih}" end intro
end "
\display{
"
begin math in theory system prime s lemma hypothetical inference inference mendelson proposition three two d says all meta h indeed all meta a indeed all meta b indeed all meta c indeed meta h peano imply meta a peano is meta b infer meta h peano imply meta c peano is meta b infer meta h peano imply meta a peano is meta c end lemma end math
end "}
"
begin math system prime s proof of hypothetical inference inference mendelson proposition three two d reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta h peano imply meta a peano is meta b end line line ell b premise meta h peano imply meta c peano is meta b end line line ell c hypothesis indeed meta h end line line ell d hypothesis because mendelson proposition three two d indeed meta a peano is meta b peano imply meta c peano is meta b peano imply meta a peano is meta c end line line ell e hypothesis double modus ponens ell d modus ponens ell a modus ponens ell b indeed meta a peano is meta c end line because rule repetition modus ponens ell e indeed meta h peano imply meta a peano is meta c qed end math
end "
\subsubsection{Bevis $3.2\ f$}
"
begin intro mendelson proposition three two f i pyk "mendelson proposition three two f i" tex "Mendelson\ \textbf{3.2}\ f\ i" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two f i says peano zero peano is peano zero peano plus peano zero end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two f i reads line ell a because axiom prime s five indeed peano zero peano plus peano zero peano is peano zero end line because inference mendelson proposition three two b modus ponens ell a indeed peano zero peano is peano zero peano plus peano zero qed end math
end " \\
"
begin intro mendelson proposition three two f ii pyk "mendelson proposition three two f ii" tex "Mendelson\ \textbf{3.2}\ f\ ii" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two f ii says peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two f ii reads line ell a hypothesis indeed peano x peano is peano zero peano plus peano x end line line ell b hypothesis because axiom prime s six indeed peano zero peano plus peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ end line line ell c hypothesis raw because hypothetical inference axiom prime s two modus ponens ell a indeed peano x peano succ peano is parenthesis peano zero peano plus peano x end parenthesis peano succ end line line ell d hypothesis raw because hypothetical inference inference mendelson proposition three two d modus ponens ell c modus ponens ell b indeed peano x peano succ peano is peano zero peano plus peano x peano succ end line because rule repetition modus ponens ell d indeed peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ qed end math
end " \\
"
begin intro mendelson proposition three two f pyk "mendelson proposition three two f" tex "Mendelson\ \textbf{3.2}\ f" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two f says peano x peano is peano zero peano plus peano x end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two f reads line ell a because mendelson proposition three two f i indeed peano zero peano is peano zero peano plus peano zero end line line ell b because mendelson proposition three two f ii indeed peano x peano is peano zero peano plus peano x peano imply peano x peano succ peano is peano zero peano plus peano x peano succ end line because rule induction modus ponens ell a modus ponens ell b indeed peano x peano is peano zero peano plus peano x qed end math
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 intro mendelson proposition three two g i pyk "mendelson proposition three two g i" tex "Mendelson\ \textbf{3.2}\ g\ i" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two g i says peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two g i reads line ell a because axiom prime s five indeed peano y peano succ peano plus peano zero peano is peano y peano succ end line line ell b because axiom prime s five indeed peano y peano plus peano zero peano is peano y end line line ell c because inference axiom prime s two modus ponens ell b indeed parenthesis peano y peano plus peano zero end parenthesis peano succ peano is peano y peano succ end line because inference inference mendelson proposition three two d modus ponens ell a modus ponens ell c indeed peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ qed end math
end "
"
begin intro mendelson proposition three two g ii pyk "mendelson proposition three two g ii" tex "Mendelson\ \textbf{3.2}\ g\ ii" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two g ii says peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two g ii reads line ell a hypothesis indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell b hypothesis because axiom prime s six indeed peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano succ peano plus peano x end parenthesis peano succ end line line ell c hypothesis raw because hypothetical inference axiom prime s two modus ponens ell a indeed parenthesis peano y peano succ peano plus peano x end parenthesis peano succ peano is parenthesis parenthesis peano y peano plus peano x end parenthesis peano succ end parenthesis peano succ end line line ell e hypothesis raw because hypothetical inference inference mendelson proposition three two c modus ponens ell b modus ponens ell c indeed peano y peano succ peano plus peano x peano succ peano is parenthesis parenthesis peano y peano plus peano x end parenthesis peano succ end parenthesis peano succ end line line ell g hypothesis because axiom prime s six indeed peano y peano plus peano x peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell h hypothesis raw because hypothetical inference axiom prime s two modus ponens ell g indeed parenthesis peano y peano plus peano x peano succ end parenthesis peano succ peano is parenthesis parenthesis peano y peano plus peano x end parenthesis peano succ end parenthesis peano succ end line line ell j hypothesis raw because hypothetical inference inference mendelson proposition three two d modus ponens ell e modus ponens ell h indeed peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ end line because rule repetition modus ponens ell j indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ qed end math
end "
"
begin intro mendelson proposition three two g pyk "mendelson proposition three two g" tex "Mendelson\ \textbf{3.2}\ g" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two g says peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two g reads line ell a because mendelson proposition three two g i indeed peano y peano succ peano plus peano zero peano is parenthesis peano y peano plus peano zero end parenthesis peano succ end line line ell b because mendelson proposition three two g ii indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ peano imply peano y peano succ peano plus peano x peano succ peano is parenthesis peano y peano plus peano x peano succ end parenthesis peano succ end line because rule induction modus ponens ell a modus ponens ell b indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ qed end math
end "
\subsubsection{Bevis $3.2\ h$}
\label{ssec:peano_three_two_h}
"
begin intro mendelson proposition three two h i pyk "mendelson proposition three two h i" tex "Mendelson\ \textbf{3.2}\ h\ i" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two h i says peano x peano plus peano zero peano is peano zero peano plus peano x end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two h i reads line ell a because axiom prime s five indeed peano x peano plus peano zero peano is peano x end line line ell b because mendelson proposition three two f indeed peano x peano is peano zero peano plus peano x end line because inference inference mendelson proposition three two c modus ponens ell a modus ponens ell b indeed peano x peano plus peano zero peano is peano zero peano plus peano x qed end math
end "
"
begin intro mendelson proposition three two h ii pyk "mendelson proposition three two h ii" tex "Mendelson\ \textbf{3.2}\ h\ ii" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two h ii says peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two h ii reads line ell a hypothesis indeed peano x peano plus peano y peano is peano y peano plus peano x end line line ell b hypothesis because axiom prime s six indeed peano x peano plus peano y peano succ peano is parenthesis peano x peano plus peano y end parenthesis peano succ end line line ell c hypothesis because mendelson proposition three two g indeed peano y peano succ peano plus peano x peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell d hypothesis raw because hypothetical inference axiom prime s two modus ponens ell a indeed parenthesis peano x peano plus peano y end parenthesis peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell f hypothesis raw because hypothetical inference inference mendelson proposition three two c modus ponens ell b modus ponens ell d indeed peano x peano plus peano y peano succ peano is parenthesis peano y peano plus peano x end parenthesis peano succ end line line ell h hypothesis raw because hypothetical inference inference mendelson proposition three two d modus ponens ell f modus ponens ell c indeed peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end line because rule repetition modus ponens ell h indeed peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x qed end math
end "
"
begin intro mendelson proposition three two h pyk "mendelson proposition three two h" tex "Mendelson\ \textbf{3.2}\ h" end intro
end "
\display{
"
begin math in theory system prime s lemma mendelson proposition three two h says peano x peano plus peano y peano is peano y peano plus peano x end lemma end math
end "}
"
begin math system prime s proof of mendelson proposition three two h reads line ell a because mendelson proposition three two h i indeed peano x peano plus peano zero peano is peano zero peano plus peano x end line line ell b because mendelson proposition three two h ii indeed peano x peano plus peano y peano is peano y peano plus peano x peano imply peano x peano plus peano y peano succ peano is peano y peano succ peano plus peano x end line because rule induction modus ponens ell a modus ponens ell b indeed peano x peano plus peano y peano is peano y peano plus peano x qed end math
end "
\appendix
\section{Diverse}
"
begin math pyk define logic as "logic" 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 priority table 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 table 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,