"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}
%\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=A Logiweb base page}
\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}
\title{Formelt bevis for den kommutative lov for addition i peano-aritmetik}
\author{Ole Hyldahl Hansen 260579}
\begin {document}
\maketitle
\tableofcontents
\newpage
\addtolength{\parskip}{1.0\baselineskip}
\section{Indledning}
Det skal bevises, at den kommutative lov for addition g{\ae}lder i Peano-aritmetik. Dette er p{\aa} ingen m{\aa}de et nyt resultat, s{\aa} rapporten skal ses som en opgave i at arbejde med formelle beviser i en logisk teori. S{\ae}rlig interessent er det, at rapporten er skrevet i systemet Logiweb. Dette tillader en maskine at verificere de givne beviser ud fra de definerede axiomer og inferensregler, men stiller om muligt endnu h{\o}jere krav til stringens i beviserne end traditionelle beviser inden for logikken. Der vil blive taget udgangspunkt i Mendelson \cite{mendelson}, s{\aa} det meste af arbejdet vil best{\aa} i, at tilpasse beviserne s{\aa} de kan forst{\aa}s af Logiweb, og s{\o}rge for at alle n{\o}dvendige hj{\ae}lpes{\ae}tninger er bevist i mindste detalje.
\section{Logiweb}
Denne rapport er lavet i systemet Logiweb \cite{logiweb}. Systemet giver dels mulighed for at lave pr{\ae}sentable formelle beviser, men dets vigtigste form{\aa}l er nok at kunne verificere korrekt skrevne beviser. I mods{\ae}tning til mere traditionelle beviser i den matematiske litteratur kan beviser inden for logikken ofte skrives s{\aa} tilstr{\ae}kkeligt formelt op, at de kan verificeres ved en rent mekanisk procedure.
I Logiweb-forstand er denne rapport en \emph{side}. Sider kan definere et antel logiske \emph{teorier} og kan publiseres, referere andre sider og selv refereres p{\aa} en m{\aa}de meget lig dokumenter p{\aa} WWW, hvilket skulle g{\o}re det muligt at skabe komplekse logiske teorier ved at basere nye teorier p{\aa} allerede eksisterende og formelt beviste teorier. Peano-aritmetik er dog en relativt simpel teori, og derfor baserer denne rapport sig kun p{\aa} de helt basale sider \texttt{base} og \texttt{check}.
Alle matematiske konstruktioner som Logiweb-systemet g{\o}res bekendt med, vises i kantede parenteser, som f.eks. denne reference til et lemma "
begin bracket mendelson one seven end bracket
end ". L{\ae}seren er hermed klar over, at konstruktionen er passende defineret p{\aa} den p{\aa}g{\ae}ldende side. Lemmaer kan dog stadig postuleres uden beviser, men hvis et bevis er tilstede, vil bevis-checkeren p{\aa} siden \texttt{check} have verificeret dette og evt. fejl vil blive rapporteret p{\aa} en s{\ae}rlig \emph{diagnose}-side.
Under udarbejdelsen er denne rapport l{\o}bende blevet checket, og den endelige udgave meldes fri for formelle fejl af Logiweb, hvilket l{\ae}seren selv kan kontrollere ved at bes{\o}ge rapportens hjemsted \cite{this} p{\aa} internettet, hvor ogs{\aa} al kildekode er tilg{\ae}ngelig.
N{\aa}r en konstruktion defineres i logiweb skal b{\aa}de gramatikken og en r{\ae}kke \emph{aspekter} defineres, der tilsammen beskriver for Logiweb hvordan konstruktionen skal bruges, og hvordan den skal optr{\ae}de i det f{\ae}rdige dokument. Hvordan dette maskineri pr{\ae}cist fungerer er omfattende, og her henvises til \texttt{base}-siden \cite{basepage}. Her skal blot n{\ae}vnes, at introduktionen af nye konstruktioner giver anledning til \emph{pyk}-fodnoter, der automatisk inds{\ae}ttes af Logiweb. Disse beskriver sammenh{\ae}ngen mellem en konstruktions navn i kildeteksten og i den f{\ae}rdigtformaterede tekst, og kan uden videre ignoreres, hvis man ikke {\o}nsker at l{\ae}se kildeteksten.
\section{Peano-aritmetik}
Peano-aritmetik er en formel teori for de naturlige tal, og egner sig godt til behandling i Logiweb. Teorien er relativt enkel at definere, men der kan alligvel bevises en meget stor m{\ae}ngde interessante s{\ae}tninger. Fordi n{\ae}sten enhver har regnet med naturlige tal siden barndommen, er Logiweb's uvilje mod at acceptere andet end strengt formelt korrekte beviser en vigtig egenskab, da man ellers nemt kommer til at benytte ubeviste antagelser, der virker fuldst{\ae}ndigt oplagte.
\subsection{Grammatik}
Ved en term "
begin math meta t end math
end " i peano-aritmetik forst{\aa}s en af f{\o}lgende konstruktioner: konstanten nul "
begin intro peano zero pyk "peano zero" tex "
\dot{0}" end intro
end ", efterf{\o}lgeroperatoren "
begin intro var x peano succ pyk "* peano succ" tex "#1.'" end intro
end ", plus "
begin intro var x peano plus var y pyk "* peano plus *" tex "#1.
\mathop{\dot{+}} #2." end intro
end " og gange "
begin intro var x peano times var y pyk "* peano times *" tex "#1.
\mathop{\dot{\cdot}} #2." end intro
end ". Alle konstruktioner h{\o}rende til Peano-aritmetik er i denne rapport markeret med en prik\footnote{Lighed skrives dog "
begin bracket var x peano is var y end bracket
end ", da lighed med en prik over betyder ``defineres som'' i Logiweb.}, for at kunne skelne dem fra lignende konstruktioner defineret p{\aa} \texttt{base}-siden. Teorien g{\o}r ogs{\aa} brug af de \emph{konkrete variabler} "
begin intro peano a index "a" pyk "peano a" tex "
\dot{\mathit{a}}" end intro
end ", "
begin intro peano b index "b" pyk "peano b" tex "
\dot{\mathit{b}}" end intro
end ", ..., der varierer over konstante termer.
Formler "
begin math meta p end math
end " kan bygges op af lighed "
begin intro var x peano is var y index "p" pyk "* peano is *" tex "#1.
\stackrel{p}{=} #2." end intro
end ", negation "
begin intro peano not var x pyk "peano not *" tex "
\dot{\neg}\, #1." end intro
end ", implikation "
begin intro var x peano imply var y pyk "* peano imply *" tex "#1.
\mathrel{\dot{\Rightarrow}} #2." end intro
end " og al-kvantoren "
begin intro peano all var x indeed var y pyk "peano all * indeed *" tex "
\dot{\forall} #1.
\colon #2." end intro
end ".
Kort kan grammatikken skrives som:
\begin{eqnarray*}
{\cal T} & ::= & \dot{0} \; | \; {{\cal T}}' \; | \; {\cal T} \mathop{\dot{+}} {\cal T} \; | \; {\cal T} \mathop{\dot{\cdot}} {\cal T} \; | \; \dot{\texttt{var}} \\
{\cal F} & ::= & {\cal T} \mathop{\dot{=}} {\cal T} \; | \; \dot{\neg} {\cal F} \; | \; {\cal F} \mathrel{\dot{\Rightarrow}} {\cal F} \; | \;
\dot{\forall} \dot{\texttt{var}} \colon {\cal F}
\end{eqnarray*}
hvor $\dot{\texttt{var}}$ er en vilk{\aa}rlig konkret variabel. Plus og gange er venstreassociative mens implikation er h{\o}jreassociativ. Operatorenes pr{\ae}cedens er i faldende orden $'$, $\dot{\cdot}$, $\dot{+}$, $\dot{\neg}$, $\dot{\forall}$, $\dot{\Rightarrow}$. Der er ingen andre konstanter end "
begin math peano zero end math
end ", men de {\o}vrige naturlige tal "
begin intro peano one pyk "peano one" tex "
\dot{1}" end intro
end ", "
begin intro peano two pyk "peano two" tex "
\dot{2}" end intro
end " ..., kan makrodefineres s{\aa}ledes: "
begin math macro define peano one as peano zero peano succ end define end math
end ", "
begin math macro define peano two as peano one peano succ end define end math
end ", ... . I denne rapport vil der dog ikke blive brug for andre tal end "
begin bracket peano zero end bracket
end ", ligesom gange og negation heller ikke vil blive set mere.
\subsection{Meta- og konkrete variabler}
Det er vigtigt at skelne skarpt mellem \emph{metavariabler} og konkrete variabler "
begin intro var x peano var pyk "* peano var" tex "
\dot{#1.
}" end intro
end ". I Logiweb vil metavariabler blive skrevet store og kursiverede, mens konkrete variabler i Peano-aritmetik f{\aa}r en prik over. Eksempelvis er "
begin bracket meta t end bracket
end " en metavariabel, mens "
begin bracket peano t end bracket
end " er den tilsvarende konkrete variabel.
Som udgangspunkt er s{\ae}tninger omhandlende metavariabler at fortr{\ae}kke fremfor samme s{\ae}tning involverende konkrete variabler. Med metavariabler kommer Logiweb's unificeringssystem til sin ret, og man kan frit udskifte variabler med vilk{\aa}rlige (lovlige) konstruktioner. Visse beviser (specielt beviser involverende induktion) lader sig dog ikke gennemf{\o}re for metavariabler i Logiweb, s{\aa} konkrete variabler vil blive brugt, hvor det er n{\o}dvendigt.
Nogle af axiomerne i Peano-aritmetik stiller krav om, at der ved substitution af termer for en variabel ikke fejlagtigt bliver bundet variabler af kvantorer (det s{\aa}kaldte ``$T$ er fri for $x$ i $S$''-begreb i Mendelson). Eftersom Logiweb ikke har nogen ide om, hvilke regler vores Peano-variabler skal adlyde, m{\aa} disse regler defineres eksplicit. Dette g{\o}res herunder \footnote{Disse definitioner er taget u{\ae}ndret fra \cite{peanopage}.}:
Der introduceres en operator "
begin intro var x is peano var index "P" pyk "* is peano var" tex "#1.
{} ^ {\cal P}" end intro
end ", der er sand netop hvis "
begin bracket var x end bracket
end " er en Peano-variabel.
\display{"
begin math value define var x is peano var as var x term root equal quote var x peano var end quote end define end math
end "}
"
begin intro peano nonfree var x in var y end nonfree index "nonfree" pyk "peano nonfree * in * end nonfree" tex "
\dot{nonfree}(#1.
,#2.
)" end intro
end " er sand netop hvis Peano-variablen "
begin bracket var x end bracket
end " ikke forekommer frit i "
begin bracket var y end bracket
end ". "
begin intro peano nonfree star var x in var y end nonfree index "nonfree*" pyk "peano nonfree star * in * end nonfree" tex "
\dot{nonfree}^*(#1.
,#2.
)" end intro
end " er sand netop hvis Peano-variablen "
begin bracket var x end bracket
end " ikke forekommer frit i en liste "
begin bracket var y end bracket
end " af termer og/eller formler.
\display{"
begin math value define peano nonfree var x in var y end nonfree as newline open if var y is peano var then not var x term equal var y else newline open if not var y term root equal quote peano all var x indeed var y end quote then peano nonfree star var x in var y tail end nonfree else newline open if var x term equal var y first then true else peano nonfree var x in var y second end nonfree end define end math
end "}
\display{"
begin math value define peano nonfree star var x in var y end nonfree as var x tagged guard tagged if var y then true else peano nonfree var x in var y head end nonfree macro and peano nonfree star var x in var y tail end nonfree end if end define end math
end "}%
%
\test{"
begin math test peano nonfree quote peano x end quote in quote peano y peano is peano z peano imply peano all peano x indeed peano x peano is peano y end quote end nonfree end test end math
end "}%
%
\test{"
begin math false test peano nonfree quote peano x end quote in quote peano x peano is peano z peano imply peano all peano x indeed peano x peano is peano y end quote end nonfree end test end math
end "}%
%
\test{"
begin math false test peano nonfree quote peano x end quote in quote peano y peano is peano x peano imply peano all peano x indeed peano x peano is peano y end quote end nonfree end test end math
end "}%
%
\test{"
begin math false test peano nonfree quote peano x end quote in quote peano y peano is peano z peano imply peano all peano y indeed peano x peano is peano y end quote end nonfree end test end math
end "}%
"
begin intro peano free var a set var x to var b end free index "free" pyk "peano free * set * to * end free" tex "
\dot{free}\langle #1.
| #2.
:= #3.
\rangle" end intro
end " er sand n{\aa}r substitutionen "
begin bracket substitute var a set var x to var b end substitute end bracket
end " er \emph{fri}. "
begin intro peano free star var a set var x to var b end free index "free*" pyk "peano free star * set * to * end free" tex "
\dot{free}{}^*\langle #1.
| #2.
:= #3.
\rangle" end intro
end " har samme betydning for en liste af termer "
begin bracket var a end bracket
end ".
\display{"
begin math value define peano free var a set var x to var b end free as var x tagged guard var b tagged guard newline open if var a is peano var then true else newline open if not var a term root equal quote peano all var u indeed var v end quote then peano free star var a tail set var x to var b end free else newline open if var a first term equal var x then true else newline open if peano nonfree var x in var a second end nonfree then true else newline open if not peano nonfree var a first in var b end nonfree then false else newline peano free var a second set var x to var b end free end define end math
end "}
\display{"
begin math value define peano free star var a set var x to var b end free as var x tagged guard var b tagged guard tagged if var a then true else peano free var a head set var x to var b end free macro and peano free star var a tail set var x to var b end free end if end define end math
end "}%
%
\test{"
begin math test peano free quote peano all peano x indeed var b pair peano x pair var c end quote set quote peano x end quote to quote var x pair peano y pair var z end quote end free end test end math
end "}%
%
\test{"
begin math false test peano free quote peano all peano y indeed var b pair peano x pair var c end quote set quote peano x end quote to quote var x pair peano y pair var z end quote end free end test end math
end "}%
%
\test{"
begin math test peano free quote peano all peano x indeed var b pair peano x pair var c end quote set quote peano y end quote to quote var x pair peano y pair var z end quote end free end test end math
end "}%
%
\test{"
begin math test peano free quote peano all peano y indeed var b pair peano x pair var c end quote set quote peano y end quote to quote var x pair peano y pair var z end quote end free end test end math
end "}%
%
"
begin intro peano sub var a is var b where var x is var c end sub pyk "peano sub * is * where * is * end sub" tex "#1.
{\equiv}\langle #2.
|#3.
:=#4.
\rangle" end intro
end " er sand n{\aa}r "
begin bracket var a end bracket
end " er "
begin bracket substitute var b set var x to var c end substitute end bracket
end ". "
begin intro peano sub star var a is var b where var x is var c end sub pyk "peano sub star * is * where * is * end sub" tex "#1.
{\equiv}\langle^* #2.
|#3.
:=#4.
\rangle" end intro
end " har samme betydning for lister "
begin bracket var a end bracket
end " og "
begin bracket var b end bracket
end ".
\display{"
begin math value define peano sub var a is var b where var x is var c end sub as var a tagged guard var x tagged guard var c tagged guard newline open if var b term root equal quote peano all var u indeed var v end quote macro and var b first term equal var x then var a term equal var b else newline open if var b is peano var and var b term equal var x then var a term equal var c else newline var a term root equal var b macro and peano sub star var a tail is var b tail where var x is var c end sub end define end math
end "}
\display{"
begin math value define peano sub star var a is var b where var x is var c end sub as var b tagged guard var x tagged guard var c tagged guard tagged if var a then true else peano sub var a head is var b head where var x is var c end sub macro and peano sub star var a tail is var b tail where var x is var c end sub end if end define end math
end "}%
%
\test{"
begin math test peano sub peano a is peano a where peano b is peano c end sub end test end math
end "}%
%
\test{"
begin math test peano sub peano c is peano b where peano b is peano c end sub end test end math
end "}%
%
\test{"
begin math test peano sub all peano a indeed peano a peano is peano b is all peano a indeed peano a peano is peano b where peano a is peano c end sub end test end math
end "}%
%
\test{"
begin math test peano sub all peano a indeed peano a peano is peano c is all peano a indeed peano a peano is peano b where peano b is peano c end sub end test end math
end "}%
%
\test{"
begin math test peano sub peano all peano a indeed peano a peano is peano zero peano plus peano a peano imply peano c peano times peano d peano is peano zero peano plus peano c peano times peano d is peano all peano a indeed peano a peano is peano zero peano plus peano a peano imply peano b peano is peano zero peano plus peano b where peano b is peano c peano times peano d end sub end test end math
end "}%
%
\test{"
begin math test peano sub peano all peano a indeed peano a peano is peano zero peano plus peano a peano imply peano b peano is peano zero peano plus peano b is peano all peano a indeed peano a peano is peano zero peano plus peano a peano imply peano b peano is peano zero peano plus peano b where peano a is peano c end sub end test end math
end "}%
%
\subsection{Teorien S'}
Den formelle teori, som vil danne grundlag for denne rapport, vil blive betegnet
"
begin intro system prime s index "S'" pyk "system prime s" tex "
S'" end intro
end ", og er n{\ae}sten identisk med teorien $S$, som defineres i Mendelson. Teorien indeholder de 5 axiomer\footnote{Strengt taget er der tale om axiomsskemaer, men denne forskel er ikke v{\ae}sentlig i denne sammenh{\ae}ng.} fra f{\o}rsteordens pr{\ae}dikatkalkulen
"
begin intro axiom prime a one index "A1'" pyk "axiom prime a one" tex "
A1'" end intro
end ",
"
begin intro axiom prime a two index "A2'" pyk "axiom prime a two" tex "
A2'" end intro
end ",
"
begin intro axiom prime a three index "A3'" pyk "axiom prime a three" tex "
A3'" end intro
end ",
"
begin intro axiom prime a four index "A4'" pyk "axiom prime a four" tex "
A4'" end intro
end ", og
"
begin intro axiom prime a five index "A5'" pyk "axiom prime a five" tex "
A5'" end intro
end ", samt de 2 inferensregler
"
begin intro rule prime mp index "MP'" pyk "rule prime mp" tex "
MP'" end intro
end " og
"
begin intro rule prime gen index "Gen'" pyk "rule prime gen" tex "
Gen'" end intro
end ":
\display{"
begin math theory system prime s end theory end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a one says all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a two says 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 rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a three says 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 rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a four says 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 rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a five says 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 rule end math
end "}
\display{"
begin math in theory system prime s rule rule prime mp says all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule rule prime gen says all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end rule end math
end "}
Derudover er der ogs{\aa} de egentlige axiomer fra Peano-aritmetik "
begin intro axiom prime s one index "S1'" pyk "axiom prime s one" tex "
S1'" end intro
end ",
"
begin intro axiom prime s two index "S2'" pyk "axiom prime s two" tex "
S2'" end intro
end ",
"
begin intro axiom prime s three index "S3'" pyk "axiom prime s three" tex "
S3'" end intro
end ",
"
begin intro axiom prime s four index "S4'" pyk "axiom prime s four" tex "
S4'" end intro
end ",
"
begin intro axiom prime s five index "S5'" pyk "axiom prime s five" tex "
S5'" end intro
end ",
"
begin intro axiom prime s six index "S6'" pyk "axiom prime s six" tex "
S6'" end intro
end ",
"
begin intro axiom prime s seven index "S7'" pyk "axiom prime s seven" tex "
S7'" end intro
end ",
"
begin intro axiom prime s eight index "S8'" pyk "axiom prime s eight" tex "
S8'" end intro
end ", og
"
begin intro axiom prime s nine index "S9'" pyk "axiom prime s nine" tex "
S9'" end intro
end ":
\display{"
begin math in theory system prime s rule axiom prime s one says 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 rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s two says 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 rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s three says all meta a indeed not peano zero peano is meta a peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s four says 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 rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s five says all meta a indeed meta a peano plus peano zero peano is meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s six says 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 rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s seven says all meta a indeed meta a peano times peano zero peano is peano zero end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s eight says 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 rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s nine says 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 rule end math
end "}
Bortset fra de Logiweb-specifikke tilf{\o}jelser, adskiller teorien "
begin bracket system prime s end bracket
end " sig fra teorien $S$ i Mendelson ved, at axiomerne "
begin bracket axiom prime s one end bracket
end "-"
begin bracket axiom prime s nine end bracket
end " prim{\ae}rt er angivet med metavariabler i stedet for konkrete variabler, og dermed svarer axiomerne til lemma 3.2(1-9) i Mendelson. Teorien kunne sagtens v{\ae}re formuleret p{\aa} samme m{\aa}de som i Mendelson, men dette havde blot gjort beviser meget l{\ae}ngere pga. omfattende brug af "
begin bracket axiom prime a four end bracket
end " og generaliseringer. Den pr{\ae}senterede formulering viser sig meget mere anvendelig i praksis, og vil derfor blive benyttet.
\section{Den kommutative lov for addition}
Nu da grundlaget er p{\aa} plads, er det tid til at l{\o}se den stillede opgave. Der skal leveres et bevis for, at den den kommutative lov g{\ae}lder for addition i Peano-aritmetik, dvs. at $t + r = r + t$ for to vilk{\aa}rlige ikke-negative heltal $t$ og $r$. Skrevet i Logiweb's notation skal "
begin math peano all peano t indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end math
end " bevises\footnote{I denne sammenh{\ae}ng spiller kvantorene ingen rolle, da de kan tilf{\o}jes eller fjernes efter behag.}.
Mendelson leverer et bevis for denne s{\ae}tning, men for at kunne komme s{\aa} langt skal der bevises en del forskellige hj{\ae}lpes{\ae}tninger. Ser man i Mendelson indser man hurtigt, at beviset for kommutativitet "
begin intro lemma prime three two h pyk "lemma prime three two h" tex "L3.2 (h)'" end intro
end " afh{\ae}nger af de foreg{\aa}ende lemmaer
"
begin intro lemma prime three two a pyk "lemma prime three two a" tex "L3.2 (a)'" end intro
end ",
"
begin intro lemma prime three two b pyk "lemma prime three two b" tex "L3.2 (b)'" end intro
end ",
"
begin intro lemma prime three two c pyk "lemma prime three two c" tex "L3.2 (c)'" end intro
end ",
"
begin intro lemma prime three two d pyk "lemma prime three two d" tex "L3.2 (d)'" end intro
end ",
"
begin intro lemma prime three two f pyk "lemma prime three two f" tex "L3.2 (f)'" end intro
end " og
"
begin intro lemma prime three two g pyk "lemma prime three two g" tex "L3.2 (g)'" end intro
end ". Derudover vil det v{\ae}re praktisk at bevise at antal tautologier, som vil kunne spare en del gentagelser af bevislinier. Der vil som udgangspunkt ikke blive bevist flere s{\ae}tninger end strengt n{\o}dvendigt for at kunne gennemf{\o}re beviset for "
begin math lemma prime three two h end math
end ".
\subsection{Hj{\ae}lpes{\ae}tninger}
Der vil nu blive fremsat og bevist en r{\ae}kke forskellige tautologier, der er meget nyttige at have ved h{\aa}nden. Disse hj{\ae}lpes{\ae}tninger bruger kun begreber fra den rene pr{\ae}dikatkalkule, og vil derfor kunne bevises i mange andre teorier end Peano-aritmetik.
\subsubsection{MPTwice}
I beviser har man af og til linier af formen "
begin bracket meta a peano imply meta b peano imply meta c end bracket
end ", og man {\o}nsker at konkludere "
begin bracket meta c end bracket
end " ud fra "
begin bracket meta a end bracket
end " og "
begin bracket meta b end bracket
end ". Dette kan naturligvis let klares med to anvendelser af modus ponens, men der kan i disse situationer spares en bevislinie ved at benytte det enkle lemma "
begin intro lemma mp twice pyk "lemma mp twice" tex "MPTwice" end intro
end ":
\statement {"
begin math in theory system prime s lemma lemma mp twice 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 "}
Beviset for lemmaet er naturligvis blot at benytte modus ponens to gange, men man vil bem{\ae}rke at der alligevel kr{\ae}ves 8 bevislinier pga. nogle Logiweb-teknikaliteter. Det skulle dog v{\ae}re rimeligt enkelt at forst{\aa} meningen med disse liner, idet de simpethen blot remser lemmaets pr{\ae}misser op igen.
\statement{"
begin math system prime s proof of lemma mp twice 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 rule prime mp modus ponens ell a modus ponens ell b indeed meta b peano imply meta c end line because rule prime mp modus ponens ell d modus ponens ell c indeed meta c qed end math
end "}
\subsubsection{Lemma M1.7}
Fra Mendelson tages lemma 1.7 "
begin intro mendelson one seven index "M1.7" pyk "mendelson one seven" tex "
M1.7" end intro
end ":
\statement{"
begin math in theory system prime s lemma mendelson one seven says all meta b indeed meta b peano imply meta b end lemma end math
end "}
\statement{"
begin math system prime s proof of mendelson one seven reads arbitrary meta b end line line ell a because axiom prime a one indeed meta b peano imply parenthesis meta b peano imply meta b end parenthesis peano imply meta b end line line ell c because axiom prime a two indeed parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis peano imply meta b end parenthesis peano imply macro newline parenthesis meta b peano imply meta b peano imply meta b end parenthesis peano imply meta b peano imply meta b end line line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed parenthesis meta b peano imply meta b peano imply meta b end parenthesis peano imply meta b peano imply meta b end line line ell b because axiom prime a one indeed meta b peano imply meta b peano imply meta b end line because rule prime mp modus ponens ell d modus ponens ell b indeed meta b peano imply meta b qed end math
end "}
\subsubsection{Lemma Weaken}
Det vil blive n{\o}dvendigt at g{\o}re et udsagn ``svagere'', dvs. g{\o}re det betinget af et nyt udsagn, hvilket naturligvis altid er tilladt. Dette udtrykkes i lemmaet "
begin intro lemma weaken pyk "lemma weaken" tex "Weaken" end intro
end ":
\statement{
"
begin math in theory system prime s lemma lemma weaken says all meta a indeed all meta b indeed meta a infer meta b peano imply meta a end lemma end math
end "}
Beviset er helt enkelt:
\statement{
"
begin math system prime s proof of lemma weaken 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 rule prime mp modus ponens ell b modus ponens ell a indeed meta b peano imply meta a qed end math
end "}
\subsubsection {Tautologi 1}
"
begin intro lemma tautology one pyk "lemma tautology one" tex "Taut 1" end intro
end " er det f{\o}rste af fire tautologier, der er en smule mere komplicerede end de hidtil sete. Disse tautologier har ikke nogle oplagte navne, hvorfor de blot vil blive nummereret. Dette f{\o}ste lemma tillader, om man ombytter r{\ae}kkef{\o}lgen af visse pr{\ae}misser i en implikation:
\statement{
"
begin math in theory system prime s lemma lemma tautology one 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 "}
Beviset er ikke langt, men demonstrerer alligvel, at man naturligvis kan referere tilbage til tidligere beviste lemmaer. Logiweb checker, at alle refererede lemmaer ogs{\aa} er beviste, og at der ikke er cykliske afh{\ae}ngigheder mellem beviser.
\statement{
"
begin math system prime s proof of lemma tautology one 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 parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end line line ell c because rule prime mp modus ponens ell b modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end line line ell d because lemma weaken modus ponens ell c indeed meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end line line ell e because axiom prime a two indeed parenthesis meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis peano imply parenthesis parenthesis meta b peano imply meta a peano imply meta b end parenthesis peano imply parenthesis meta b peano imply meta a peano imply meta c end parenthesis end parenthesis end line line ell f because axiom prime a one indeed meta b peano imply meta a peano imply meta b end line because lemma mp twice modus ponens ell e modus ponens ell d modus ponens ell f indeed meta b peano imply meta a peano imply meta c qed end math
end "
}
\subsubsection{Tautologi 2}
Lemma "
begin intro lemma tautology two pyk "lemma tautology two" tex "Taut 2" end intro
end " udtrykker en form for transitivitet af implikationsoperatoren.
\statement{
"
begin math in theory system prime s lemma lemma tautology two says all meta d indeed all meta e indeed all meta f indeed parenthesis meta d peano imply meta e end parenthesis infer parenthesis meta e peano imply meta f end parenthesis infer parenthesis meta d peano imply meta f end parenthesis end lemma end math
end "}
\statement{"
begin math system prime s proof of lemma tautology two reads arbitrary meta d end line arbitrary meta e end line arbitrary meta f end line line ell a premise meta d peano imply meta e end line line ell b premise meta e peano imply meta f end line line ell c because axiom prime a one indeed parenthesis meta e peano imply meta f end parenthesis peano imply meta d peano imply parenthesis meta e peano imply meta f end parenthesis end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed meta d peano imply meta e peano imply meta f end line line ell e because axiom prime a two indeed parenthesis meta d peano imply meta e peano imply meta f end parenthesis peano imply parenthesis parenthesis meta d peano imply meta e end parenthesis peano imply parenthesis meta d peano imply meta f end parenthesis end parenthesis end line because lemma mp twice modus ponens ell e modus ponens ell d modus ponens ell a indeed meta d peano imply meta f qed end math
end "
}
\subsubsection{Tautologi 3}
Med lemma "
begin intro lemma tautology three pyk "lemma tautology three" tex "Taut 3" end intro
end " kan man eliminere en betingelse fra en dobbeltimplikation, s{\aa}fremt det kan bevises, at betingelsen altid er opfyldt.
\statement{"
begin math in theory system prime s lemma lemma tautology three says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b infer meta a peano imply meta b peano imply meta c infer meta a peano imply meta c end lemma end math
end "}
\statement{"
begin math system prime s proof of lemma tautology three 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 a peano imply meta b peano imply meta c end line line ell c because axiom prime a two indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis parenthesis meta a peano imply meta b end parenthesis peano imply parenthesis meta a peano imply meta c end parenthesis end parenthesis end line because lemma mp twice modus ponens ell c modus ponens ell b modus ponens ell a indeed meta a peano imply meta c qed end math
end "}
\subsubsection{Tautologi 4}
Tautologi "
begin intro lemma tautology four pyk "lemma tautology four" tex "Taut 4" end intro
end " er en svagere variant af forrige tautologi.
\statement{
"
begin math in theory system prime s lemma lemma tautology four says all meta a indeed all meta b indeed all meta c indeed meta a infer meta b peano imply meta a peano imply meta c infer meta b peano imply meta c end lemma end math
end "}
\statement{
"
begin math system prime s proof of lemma tautology four reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a end line line ell b premise meta b peano imply meta a peano imply meta c end line line ell c because lemma tautology one modus ponens ell b indeed meta a peano imply meta b peano imply meta c end line because rule prime mp modus ponens ell c modus ponens ell a indeed meta b peano imply meta c qed end math
end "
}
\subsection{Lemmaer fra Peanoaritmetik}
\subsubsection{Lemma 3.2 (a)}
Det f{\o}rste lemma fra Mendelson udtrykker at lighedstegnet er refleksivt:
\statement{
"
begin math in theory system prime s lemma lemma prime three two a says all meta t indeed meta t peano is meta t end lemma end math
end "
}
Beviset er kort, og benytter addition med nul som ``trick'':
\statement{
"
begin math system prime s proof of lemma prime three two a reads arbitrary meta t end line line ell a because axiom prime s five indeed meta t peano plus peano zero peano is meta t end line line ell b because axiom prime s one indeed parenthesis meta t peano plus peano zero peano is meta t end parenthesis peano imply parenthesis meta t peano plus peano zero peano is meta t peano imply meta t peano is meta t end parenthesis end line because lemma mp twice modus ponens ell b modus ponens ell a modus ponens ell a indeed meta t peano is meta t qed end math
end "}
\subsubsection {Lemma 3.2 (b)}
Lemma "
begin bracket lemma prime three two b end bracket
end " siger, at lighedstegnet er symmetrisk:
\statement{"
begin math in theory system prime s lemma lemma prime three two b says all meta t indeed all meta r indeed meta t peano is meta r peano imply meta r peano is meta t end lemma end math
end "}
\statement{
"
begin math system prime s proof of lemma prime three two b reads arbitrary meta t end line arbitrary meta r end line line ell a because axiom prime s one indeed meta t peano is meta r peano imply parenthesis meta t peano is meta t peano imply meta r peano is meta t end parenthesis end line line ell b because lemma tautology one modus ponens ell a indeed meta t peano is meta t peano imply parenthesis meta t peano is meta r peano imply meta r peano is meta t end parenthesis end line line ell c because lemma prime three two a indeed meta t peano is meta t end line because rule prime mp modus ponens ell b modus ponens ell c indeed meta t peano is meta r peano imply meta r peano is meta t qed end math
end "}
\subsubsection{Lemma 3.2 (c)}
Dette lemma siger, at lighedstegnet er transitivt. Med dette lemma er det nu bevist, at lighedstegnet er en {\ae}kvivalensrelation.
\statement{"
begin math in theory system prime s lemma lemma prime three two c says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r peano imply parenthesis meta r peano is meta s peano imply meta t peano is meta s end parenthesis end lemma end math
end "}
Med de allerede beviste lemmaer er dette bevis helt enkelt:
\statement{
"
begin math system prime s proof of lemma prime three two c reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because axiom prime s one indeed meta r peano is meta t peano imply parenthesis meta r peano is meta s peano imply meta t peano is meta s end parenthesis end line line ell b because lemma prime three two b indeed meta t peano is meta r peano imply meta r peano is meta t end line because lemma tautology two modus ponens ell b modus ponens ell a indeed meta t peano is meta r peano imply parenthesis meta r peano is meta s peano imply meta t peano is meta s end parenthesis qed end math
end "}
\subsubsection{Lemma 3.2 (d)}
Dette lemma er lidt besv{\ae}rligt at beskrive med ord, men dets mening skulle v{\ae}re klar og det vil vise sig s{\ae}rdeles nyttigt i flere af de kommende beviser
\statement{"
begin math in theory system prime s lemma lemma prime three two d says all meta t indeed all meta r indeed all meta s indeed meta r peano is meta t peano imply parenthesis meta s peano is meta t peano imply meta r peano is meta s end parenthesis end lemma end math
end "}
\statement{"
begin math system prime s proof of lemma prime three two d reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because lemma prime three two c indeed meta r peano is meta t peano imply parenthesis meta t peano is meta s peano imply meta r peano is meta s end parenthesis end line line ell c because lemma tautology one modus ponens ell a indeed meta t peano is meta s peano imply parenthesis meta r peano is meta t peano imply meta r peano is meta s end parenthesis end line line ell d because lemma prime three two b indeed meta s peano is meta t peano imply meta t peano is meta s end line line ell e because lemma tautology two modus ponens ell d modus ponens ell c indeed meta s peano is meta t peano imply parenthesis meta r peano is meta t peano imply meta r peano is meta s end parenthesis end line because lemma tautology one modus ponens ell e indeed meta r peano is meta t peano imply parenthesis meta s peano is meta t peano imply meta r peano is meta s end parenthesis qed end math
end "}
\subsubsection{Lemma 3.2 (f)}
Lemma "
begin math lemma prime three two f end math
end " er det f{\o}rste lemma, der kr{\ae}ver et induktivt bevis. Dette bevirker, at lemmaet m{\aa} formuleres med konkrete variabler i stedet for metavariabler som de tidligere lemmaer har benyttet. Der bevises en version, hvor den frie variabel er kvantoriseret, da denne denne form er nemmere at arbejde med i senere beviser.
\statement{"
begin math in theory system prime s lemma lemma prime three two f says peano all peano t indeed peano t peano is peano zero peano plus peano t end lemma end math
end "}
Som ved enhver induktion skal der b{\aa}de bevises et basistilf{\ae}lde og et induktionsskridt for at axiom "
begin math axiom prime s nine end math
end " kan bruges til at konkludere det {\o}nskede. Beviset er dog ikke l{\ae}ngere, end at begge dele uden problemer kan bevises i samme lemma. Var beviset blevet langt, ville det nok have v{\ae}ret mere overskueligt, at dele lemmaet op i flere dele.
\statement{
"
begin math system prime s proof of lemma prime three two f reads line ell a because axiom prime s five indeed peano zero peano plus peano zero peano is peano zero end line line ell b because lemma prime three two b indeed peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero end line line ell c because rule prime mp modus ponens ell b modus ponens ell a indeed peano zero peano is peano zero peano plus peano zero end line line ell d because axiom prime s six indeed peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell e because axiom prime a one indeed peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano is peano zero peano plus peano t peano imply peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell f because rule prime mp modus ponens ell e modus ponens ell d indeed peano t peano is peano zero peano plus peano t peano imply peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell g because mendelson one seven indeed peano t peano is peano zero peano plus peano t peano imply peano t peano is peano zero peano plus peano t end line line ell h because axiom prime s two indeed peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell i because lemma tautology two modus ponens ell g modus ponens ell h indeed peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell j because lemma prime three two d indeed peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply parenthesis peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell k because lemma tautology two modus ponens ell h modus ponens ell j indeed peano t peano is peano zero peano plus peano t peano imply parenthesis peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell l because lemma tautology three modus ponens ell f modus ponens ell k indeed peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end line line ell m because rule prime gen modus ponens ell l indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell n because axiom prime s nine indeed peano zero peano is peano zero peano plus peano zero peano imply peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis peano imply peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t end parenthesis end line because lemma mp twice modus ponens ell n modus ponens ell c modus ponens ell m indeed peano all peano t indeed peano t peano is peano zero peano plus peano t qed end math
end "
}
\subsubsection{Lemma 3.2 (g)}
Dette sidste lemma inden "
begin math lemma prime three two h end math
end " er i sig selv ikke specielt interessant, men er n{\o}dvendigt for at det endelige induktive argument kan gives.
\statement{
"
begin math in theory system prime s lemma lemma prime three two g says peano all peano t indeed peano all peano r indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end lemma end math
end "}
Beviset er l{\ae}ngere og mere komplekst end nogen af de tidligere beviser. Igen er det et bevis ved induktion, og fremgangsm{\aa}den er i vid udstr{\ae}kning den samme som i Mendelson. Beviset er gjort en anelse kortere ved at anvende en makro "
begin math meta h end math
end ".
\statement{"
begin math system prime s proof of lemma prime three two g reads line ell a because axiom prime s five indeed peano t peano succ peano plus peano zero peano is peano t peano succ end line line ell b because axiom prime s five indeed peano t peano plus peano zero peano is peano t end line line ell c because axiom prime s two indeed peano t peano plus peano zero peano is peano t peano imply parenthesis peano t peano plus peano zero end parenthesis peano succ peano is peano t peano succ end line line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed parenthesis peano t peano plus peano zero end parenthesis peano succ peano is peano t peano succ end line line ell e because lemma prime three two d indeed peano t peano succ peano plus peano zero peano is peano t peano succ peano imply parenthesis peano t peano plus peano zero end parenthesis peano succ peano is peano t peano succ peano imply peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end line line ell g because lemma mp twice modus ponens ell e modus ponens ell a modus ponens ell d indeed peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ end line locally define meta h as peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell h because axiom prime s six indeed peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ end line line ell i because lemma weaken modus ponens ell h indeed meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ end line line ell j because axiom prime s two indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ end line line ell k because lemma prime three two c indeed peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano imply parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ end line line ell l because rule prime mp modus ponens ell k modus ponens ell h indeed parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ end line line ell m because lemma tautology two modus ponens ell j modus ponens ell l indeed meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ end line line ell n because axiom prime s six indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell o because axiom prime s two indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ end line line ell p because rule prime mp modus ponens ell o modus ponens ell n indeed parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ end line line ell q because lemma prime three two d indeed peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ peano imply parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end line line ell r because lemma tautology two modus ponens ell m modus ponens ell q indeed meta h peano imply parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end line line ell t because lemma tautology one modus ponens ell r indeed parenthesis peano t peano plus peano r peano succ end parenthesis peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano succ peano imply meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end line line ell u because rule prime mp modus ponens ell t modus ponens ell p indeed meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end line line ell x because rule prime gen modus ponens ell u indeed peano all peano r indeed parenthesis meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end line line ell v because axiom prime s nine indeed peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ peano imply parenthesis peano all peano r indeed parenthesis meta h peano imply peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ end parenthesis end parenthesis peano imply peano all peano r indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell y because lemma mp twice modus ponens ell v modus ponens ell g modus ponens ell x indeed peano all peano r indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line because rule prime gen modus ponens ell y indeed peano all peano t indeed peano all peano r indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ qed end math
end "
}
\subsubsection{Lemma 3.2 (g) II}
I beviset for "
begin math lemma prime three two h end math
end " skal "
begin math lemma prime three two g end math
end " benyttes, men netop fordi der skal bevises kommutativitet, skal variablerne "
begin math peano t end math
end " og "
begin math peano r end math
end " benyttes i omvendt r{\ae}kkef{\o}lge. At denne ombytning er tilladt er intuitivt oplagt for en menneskelig l{\ae}ser, men Logiweb kr{\ae}ver dette bevist i pinagtig detalje. For at g{\o}re beviset for "
begin math lemma prime three two h end math
end " kortere, er her en udgave af "
begin math lemma prime three two g end math
end " kaldet "
begin intro lemma prime three two g rev pyk "lemma prime three two g rev" tex "L3.2 (g)' II" end intro
end ", der passer perfekt til senere brug.
Hj{\ae}lpes{\ae}tningen har tre umiddelbart meget komplicerede sidebetingelser. Disse betingelser siger tilsammen, at det er tilladt at udskifte "
begin math peano t end math
end " med "
begin math peano r end math
end " og omvendt. Fordi disse udskiftninger ikke kan foretages samtidigt, er det n{\o}dvendigt at benytte en midlertidig tredie variabel "
begin math peano s end math
end ". Det endelige lemma er ikke kvantoriseret, hvilket er godt, da det netop er skrevet med samme konkrete variabler, som skal bruges senere.
\statement{
"
begin math in theory system prime s lemma lemma prime three two g rev says peano sub quote peano all peano r indeed peano s peano succ peano plus peano r peano is parenthesis peano s peano plus peano r end parenthesis peano succ end quote is quote peano all peano r indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end quote where quote peano t end quote is quote peano s end quote end sub endorse peano sub quote peano s peano succ peano plus peano t peano is parenthesis peano s peano plus peano t end parenthesis peano succ end quote is quote peano s peano succ peano plus peano r peano is parenthesis peano s peano plus peano r end parenthesis peano succ end quote where quote peano r end quote is quote peano t end quote end sub endorse peano sub quote peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end quote is quote peano s peano succ peano plus peano t peano is parenthesis peano s peano plus peano t end parenthesis peano succ end quote where quote peano s end quote is quote peano r end quote end sub endorse peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end lemma end math
end "}
Beviset udskifter f{\o}rst "
begin math peano t end math
end " med "
begin math peano s end math
end ", derefter "
begin math peano r end math
end " med "
begin math peano t end math
end " og til sidst "
begin math peano s end math
end " med "
begin math peano r end math
end " ved hj{\ae}lp af axiom "
begin math axiom prime a four end math
end ". Sidebetingelserne skal explicit angives, fot at Logiweb kan kontrollere, at substitutionerne er legale.
\statement{
"
begin math system prime s proof of lemma prime three two g rev reads line ell a because lemma prime three two g indeed peano all peano t indeed peano all peano r indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell b side condition peano sub quote peano all peano r indeed peano s peano succ peano plus peano r peano is parenthesis peano s peano plus peano r end parenthesis peano succ end quote is quote peano all peano r indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end quote where quote peano t end quote is quote peano s end quote end sub end line line ell c because axiom prime a four modus probans ell b indeed parenthesis peano all peano t indeed peano all peano r indeed peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano imply peano all peano r indeed peano s peano succ peano plus peano r peano is parenthesis peano s peano plus peano r end parenthesis peano succ end line line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed peano all peano r indeed peano s peano succ peano plus peano r peano is parenthesis peano s peano plus peano r end parenthesis peano succ end line line ell e side condition peano sub quote peano s peano succ peano plus peano t peano is parenthesis peano s peano plus peano t end parenthesis peano succ end quote is quote peano s peano succ peano plus peano r peano is parenthesis peano s peano plus peano r end parenthesis peano succ end quote where quote peano r end quote is quote peano t end quote end sub end line line ell f because axiom prime a four modus probans ell e indeed parenthesis peano all peano r indeed peano s peano succ peano plus peano r peano is parenthesis peano s peano plus peano r end parenthesis peano succ end parenthesis peano imply peano s peano succ peano plus peano t peano is parenthesis peano s peano plus peano t end parenthesis peano succ end line line ell g because rule prime mp modus ponens ell f modus ponens ell d indeed peano s peano succ peano plus peano t peano is parenthesis peano s peano plus peano t end parenthesis peano succ end line line ell h because rule prime gen modus ponens ell g indeed peano all peano s indeed peano s peano succ peano plus peano t peano is parenthesis peano s peano plus peano t end parenthesis peano succ end line line ell i side condition peano sub quote peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end quote is quote peano s peano succ peano plus peano t peano is parenthesis peano s peano plus peano t end parenthesis peano succ end quote where quote peano s end quote is quote peano r end quote end sub end line line ell j because axiom prime a four modus probans ell i indeed parenthesis peano all peano s indeed peano s peano succ peano plus peano t peano is parenthesis peano s peano plus peano t end parenthesis peano succ end parenthesis peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line because rule prime mp modus ponens ell j modus ponens ell h indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ qed end math
end "
}
\subsubsection{Lemma 3.2 (h) basis}
Beviset for "
begin bracket lemma prime three two h end bracket
end " er tilpas langt til, at det b{\o}r deles op i flere bidder. Derudover anvendes i beviset en instans af axiom "
begin math axiom prime a four end math
end " som kr{\ae}ver at en (triviel) sidebetingelse er opfyldt. Denne sidebetingelse skal s{\aa} ogs{\aa} angives i selve lemmaet, og ser dels ikke p{\ae}nt ud og kunne dels forlede l{\ae}seren til at tro, at kun en svagere variant af lemma 3.2 var blevet bevist, s{\aa} derfor pakkes denne sidebetingelse v{\ae}k i den f{\o}rste halvdel af beviset for "
begin bracket lemma prime three two h end bracket
end ". Derfor bevises f{\o}rst en del af "
begin bracket lemma prime three two h end bracket
end " kaldet "
begin intro lemma prime three two h base pyk "lemma prime three two h base" tex "L3.2 (h)' basis" end intro
end ".
Denne f{\o}rste del tager sig ogs{\aa} af selve induktionsargumentet, og beviser basistilf{\ae}ldet. "
begin bracket lemma prime three two h end bracket
end " vil s{\aa} v{\ae}re bevist ud fra dette lemma "
begin bracket lemma prime three two h base end bracket
end ", hvis selve induktionsskridtet kan bevises.
\statement{"
begin math in theory system prime s lemma lemma prime three two h base says peano sub quote peano t peano is peano zero peano plus peano t end quote is quote peano t peano is peano zero peano plus peano t end quote where quote peano t end quote is quote peano t end quote end sub endorse parenthesis peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis peano imply peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end parenthesis end lemma end math
end "
}
\statement{
"
begin math system prime s proof of lemma prime three two h base reads line ell a because axiom prime s five indeed peano t peano plus peano zero peano is peano t end line line ell b because lemma prime three two f indeed peano all peano t indeed peano t peano is peano zero peano plus peano t end line line ell c side condition peano sub quote peano t peano is peano zero peano plus peano t end quote is quote peano t peano is peano zero peano plus peano t end quote where quote peano t end quote is quote peano t end quote end sub end line line ell d because axiom prime a four modus probans ell c indeed parenthesis peano all peano t indeed peano t peano is peano zero peano plus peano t end parenthesis peano imply peano t peano is peano zero peano plus peano t end line line ell e because rule prime mp modus ponens ell d modus ponens ell b indeed peano t peano is peano zero peano plus peano t end line line ell f because lemma prime three two c indeed peano t peano plus peano zero peano is peano t peano imply peano t peano is peano zero peano plus peano t peano imply peano t peano plus peano zero peano is peano zero peano plus peano t end line line ell h because lemma mp twice modus ponens ell f modus ponens ell a modus ponens ell e indeed peano t peano plus peano zero peano is peano zero peano plus peano t end line line ell i because axiom prime s nine indeed peano t peano plus peano zero peano is peano zero peano plus peano t peano imply parenthesis peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis peano imply peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end parenthesis end line because rule prime mp modus ponens ell i modus ponens ell h indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis peano imply peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t qed end math
end "
}
\subsection{Kommutativitet - Lemma 3.2 (h)}
Med alt det gjorte forarbejde er beviset for "
begin bracket lemma prime three two h end bracket
end " nu ret enkelt.
\statement{"
begin math in theory system prime s lemma lemma prime three two h says peano all peano t indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end lemma end math
end "
}
Beviset er naturligvis et induktionsbevis, men eftersom selve induktionsargumentet er pakket v{\ae}k i "
begin bracket lemma prime three two h base end bracket
end ", har dette bevis mest til opgave at samle tr{\aa}dene fra forg{\aa}ende lemmaer.
\statement{
"
begin math system prime s proof of lemma prime three two h reads line ell a because axiom prime s six indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell b because lemma prime three two g rev indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line locally define meta h as peano t peano plus peano r peano is peano r peano plus peano t end line line ell c because axiom prime s two indeed peano t peano plus peano r peano is peano r peano plus peano t peano imply parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell d because lemma prime three two c indeed peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ peano imply parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell e because rule prime mp modus ponens ell d modus ponens ell a indeed parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell f because lemma tautology two modus ponens ell c modus ponens ell e indeed meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell g because lemma prime three two d indeed peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end line line ell h because lemma tautology two modus ponens ell f modus ponens ell g indeed meta h peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end line line ell i because lemma tautology four modus ponens ell b modus ponens ell h indeed meta h peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end line line ell j because rule prime gen modus ponens ell i indeed peano all peano r indeed parenthesis meta h peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end line line ell k because lemma prime three two h base indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis peano imply peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end line line ell l because rule prime mp modus ponens ell k modus ponens ell j indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end line because rule prime gen modus ponens ell l indeed peano all peano t indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t qed end math
end "
}
\section{Konklusion}
Det er lykkedes at bevise den kommutative lov for addition formelt i systemet Logiweb, der b{\aa}de kan verificere beviser i logiske systemer, og samtidigt kan pr{\ae}sentere disse p{\aa} en p{\ae}n m{\aa}de for l{\ae}seren. Brug af konkrete variabler gjorde flere af beviserne overraskende komplekse, men ellers var Logiweb et fornuftigt system at udarbejde beviser i.
\clearpage
\appendix
\section{Definitioner}
\subsection{Denne sides navn}
Denne rapport er ogs{\aa} en Logiweb-side, og skal derfor have et navn. Dette defineres til:
\display{"
begin math pyk define peanorapport as "peanorapport" end define end math
end "}
\subsection{Variabler i Peano-aritmetik}\label{section:VariablesOfPeanoArithmetic}
F{\o}lgende kan v{\ae}re konkrete variabler i Peano-aritmetik
"
begin intro peano a index "a" pyk "peano a" tex "
\dot{\mathit{a}}" end intro
end ",
"
begin intro peano b index "b" pyk "peano b" tex "
\dot{\mathit{b}}" end intro
end ",
"
begin intro peano c index "c" pyk "peano c" tex "
\dot{\mathit{c}}" end intro
end ",
"
begin intro peano d index "d" pyk "peano d" tex "
\dot{\mathit{d}}" end intro
end ",
"
begin intro peano e index "e" pyk "peano e" tex "
\dot{\mathit{e}}" end intro
end ",
"
begin intro peano f index "f" pyk "peano f" tex "
\dot{\mathit{f}}" end intro
end ",
"
begin intro peano g index "g" pyk "peano g" tex "
\dot{\mathit{g}}" end intro
end ",
"
begin intro peano h index "h" pyk "peano h" tex "
\dot{\mathit{h}}" end intro
end ",
"
begin intro peano i index "i" pyk "peano i" tex "
\dot{\mathit{i}}" end intro
end ",
"
begin intro peano j index "j" pyk "peano j" tex "
\dot{\mathit{j}}" end intro
end ",
"
begin intro peano k index "k" pyk "peano k" tex "
\dot{\mathit{k}}" end intro
end ",
"
begin intro peano l index "l" pyk "peano l" tex "
\dot{\mathit{l}}" end intro
end ",
"
begin intro peano m index "m" pyk "peano m" tex "
\dot{\mathit{m}}" end intro
end ",
"
begin intro peano n index "n" pyk "peano n" tex "
\dot{\mathit{n}}" end intro
end ",
"
begin intro peano o index "o" pyk "peano o" tex "
\dot{\mathit{o}}" end intro
end ",
"
begin intro peano p index "p" pyk "peano p" tex "
\dot{\mathit{p}}" end intro
end ",
"
begin intro peano q index "q" pyk "peano q" tex "
\dot{\mathit{q}}" end intro
end ",
"
begin intro peano r index "r" pyk "peano r" tex "
\dot{\mathit{r}}" end intro
end ",
"
begin intro peano s index "s" pyk "peano s" tex "
\dot{\mathit{s}}" end intro
end ",
"
begin intro peano t index "t" pyk "peano t" tex "
\dot{\mathit{t}}" end intro
end ",
"
begin intro peano u index "u" pyk "peano u" tex "
\dot{\mathit{u}}" end intro
end ",
"
begin intro peano v index "v" pyk "peano v" tex "
\dot{\mathit{v}}" end intro
end ",
"
begin intro peano w index "w" pyk "peano w" tex "
\dot{\mathit{w}}" end intro
end ",
"
begin intro peano x index "x" pyk "peano x" tex "
\dot{\mathit{x}}" end intro
end ",
"
begin intro peano y index "y" pyk "peano y" tex "
\dot{\mathit{y}}" end intro
end ", and
"
begin intro peano z index "z" pyk "peano z" tex "
\dot{\mathit{z}}" end intro
end ".
Disse variabler makrodefineres som
"
begin math macro define peano a as var a peano var end define end math
end ",
"
begin math macro define peano b as var b peano var end define end math
end ",
"
begin math macro define peano c as var c peano var end define end math
end ",
"
begin math macro define peano d as var d peano var end define end math
end ",
"
begin math macro define peano e as var e peano var end define end math
end ",
"
begin math macro define peano f as var f peano var end define end math
end ",
"
begin math macro define peano g as var g peano var end define end math
end ",
"
begin math macro define peano h as var h peano var end define end math
end ",
"
begin math macro define peano i as var i peano var end define end math
end ",
"
begin math macro define peano j as var j peano var end define end math
end ",
"
begin math macro define peano k as var k peano var end define end math
end ",
"
begin math macro define peano l as var l peano var end define end math
end ",
"
begin math macro define peano m as var m peano var end define end math
end ",
"
begin math macro define peano n as var n peano var end define end math
end ",
"
begin math macro define peano o as var o peano var end define end math
end ",
"
begin math macro define peano p as var p peano var end define end math
end ",
"
begin math macro define peano q as var q peano var end define end math
end ",
"
begin math macro define peano r as var r peano var end define end math
end ",
"
begin math macro define peano s as var s peano var end define end math
end ",
"
begin math macro define peano t as var t peano var end define end math
end ",
"
begin math macro define peano u as var u peano var end define end math
end ",
"
begin math macro define peano v as var v peano var end define end math
end ",
"
begin math macro define peano w as var w peano var end define end math
end ",
"
begin math macro define peano x as var x peano var end define end math
end ",
"
begin math macro define peano y as var y peano var end define end math
end ", og
"
begin math macro define peano z as var z peano var end define end math
end ".
\section{Litteraturliste}
\bibliography{./page}
\end{document}
End of file
File page.bib
@Misc{logiweb,
title ={Logiweb},
howpublished = {\url{http://yoa.dk}}
}
@book {mendelson,
author = {E. Mendelson},
title = {Introduction to Mathematical Logic, fourth edition},
publisher = {Chapman \& Hall},
year = {1997}}
@Misc{this,
title = {Formelt bevis for den kommutative lov for addition i peano-aritmetik},
howpublished = {\url{http://www.diku.dk/~grue/logiweb/20050502/home/hyldahl/peanorapport/fixed/}
}}
@Misc{basepage,
title = {Logiweb Base page},
howpublished = {\url{http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/latest/}
}}
@Misc{peanopage,
title = {Peano},
howpublished = {\url{http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/latest/}}
}
End of file
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
latex page
makeindex page
bibtex page
latex page
makeindex page
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,