"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 metavar var t end metavar end math
end " i peano-aritmetik forst{\aa}s en af f{\o}lgende konstruktioner: konstanten nul "
begin math define pyk of peano zero as text "peano zero" end text end define end math
then math define tex of peano zero as text "
\dot{0}" end text end define end math
end ", efterf{\o}lgeroperatoren "
begin math define pyk of var x peano succ as text "* peano succ" end text end define end math
then math define tex of var x peano succ as text "#1.'" end text end define end math
end ", plus "
begin math define pyk of var x peano plus var y as text "* peano plus *" end text end define end math
then math define tex of var x peano plus var y as text "#1.
\mathop{\dot{+}} #2." end text end define end math
end " og gange "
begin math define pyk of var x peano times var y as text "* peano times *" end text end define end math
then math define tex of var x peano times var y as text "#1.
\mathop{\dot{\cdot}} #2." end text end define end math
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 math define pyk of peano a as text "peano a" end text end define end math
then math define tex of peano a as text "
\dot{\mathit{a}}" end text end define end math
end ", "
begin math define pyk of peano b as text "peano b" end text end define end math
then math define tex of peano b as text "
\dot{\mathit{b}}" end text end define end math
end ", ..., der varierer over konstante termer.
Formler "
begin math metavar var p end metavar end math
end " kan bygges op af lighed "
begin math define pyk of var x peano is var y as text "* peano is *" end text end define end math
then math define tex of var x peano is var y as text "#1.
\stackrel{p}{=} #2." end text end define end math
end ", negation "
begin math define pyk of peano not var x as text "peano not *" end text end define end math
then math define tex of peano not var x as text "
\dot{\neg}\, #1." end text end define end math
end ", implikation "
begin math define pyk of var x peano imply var y as text "* peano imply *" end text end define end math
then math define tex of var x peano imply var y as text "#1.
\mathrel{\dot{\Rightarrow}} #2." end text end define end math
end " og al-kvantoren "
begin math define pyk of peano all var x indeed var y as text "peano all * indeed *" end text end define end math
then math define tex of peano all var x indeed var y as text "
\dot{\forall} #1.
\colon #2." end text end define end math
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 math define pyk of peano one as text "peano one" end text end define end math
then math define tex of peano one as text "
\dot{1}" end text end define end math
end ", "
begin math define pyk of peano two as text "peano two" end text end define end math
then math define tex of peano two as text "
\dot{2}" end text end define end math
end " ..., kan makrodefineres s{\aa}ledes: "
begin math define macro of peano one as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano one as peano zero peano succ end define end quote end define end define end math
end ", "
begin math define macro of peano two as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano two as peano one peano succ end define end quote end define 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 math define pyk of var x peano var as text "* peano var" end text end define end math
then math define tex of var x peano var as text "
\dot{#1.
}" end text end define end math
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 metavar var t end metavar end bracket
end " en metavariabel, mens "
begin bracket var t peano var 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 math define pyk of var x is peano var as text "* is peano var" end text end define end math
then math define tex of var x is peano var as text "#1.
{} ^ {\cal P}" end text end define end math
end ", der er sand netop hvis "
begin bracket var x end bracket
end " er en Peano-variabel.
\display{"
begin math define value of var x is peano var as var x term root equal quote var x peano var end quote end define end math
end "}
"
begin math define pyk of peano nonfree var x in var y end nonfree as text "peano nonfree * in * end nonfree" end text end define end math
then math define tex of peano nonfree var x in var y end nonfree as text "
\dot{nonfree}(#1.
,#2.
)" end text end define end math
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 math define pyk of peano nonfree star var x in var y end nonfree as text "peano nonfree star * in * end nonfree" end text end define end math
then math define tex of peano nonfree star var x in var y end nonfree as text "
\dot{nonfree}^*(#1.
,#2.
)" end text end define end math
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 define value of peano nonfree var x in var y end nonfree as newline tagged if var y is peano var then not var x term equal var y else newline tagged 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 tagged if var x term equal var y first then true else peano nonfree var x in var y second end nonfree end if end if end if end define end math
end "}
\display{"
begin math define value of peano nonfree star var x in var y end nonfree as var x tagged guard tagged if var y then true else tagged if peano nonfree var x in var y head end nonfree then peano nonfree star var x in var y tail end nonfree else false end if end if end define end math
end "}%
%
\test{"
begin math test peano nonfree quote var x peano var end quote in quote var y peano var peano is var z peano var peano imply peano all var x peano var indeed var x peano var peano is var y peano var end quote end nonfree end test end math
end "}%
%
\test{"
begin math false test peano nonfree quote var x peano var end quote in quote var x peano var peano is var z peano var peano imply peano all var x peano var indeed var x peano var peano is var y peano var end quote end nonfree end test end math
end "}%
%
\test{"
begin math false test peano nonfree quote var x peano var end quote in quote var y peano var peano is var x peano var peano imply peano all var x peano var indeed var x peano var peano is var y peano var end quote end nonfree end test end math
end "}%
%
\test{"
begin math false test peano nonfree quote var x peano var end quote in quote var y peano var peano is var z peano var peano imply peano all var y peano var indeed var x peano var peano is var y peano var end quote end nonfree end test end math
end "}%
"
begin math define pyk of peano free var a set var x to var b end free as text "peano free * set * to * end free" end text end define end math
then math define tex of peano free var a set var x to var b end free as text "
\dot{free}\langle #1.
| #2.
:= #3.
\rangle" end text end define end math
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 math define pyk of peano free star var a set var x to var b end free as text "peano free star * set * to * end free" end text end define end math
then math define tex of peano free star var a set var x to var b end free as text "
\dot{free}{}^*\langle #1.
| #2.
:= #3.
\rangle" end text end define end math
end " har samme betydning for en liste af termer "
begin bracket var a end bracket
end ".
\display{"
begin math define value of peano free var a set var x to var b end free as var x tagged guard var b tagged guard newline tagged if var a is peano var then true else newline tagged 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 tagged if var a first term equal var x then true else newline tagged if peano nonfree var x in var a second end nonfree then true else newline tagged 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 if end if end if end if end if end define end math
end "}
\display{"
begin math define value of 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 tagged if peano free var a head set var x to var b end free then peano free star var a tail set var x to var b end free else false end if end if end define end math
end "}%
%
\test{"
begin math test peano free quote peano all var x peano var indeed var b pair var x peano var pair var c end quote set quote var x peano var end quote to quote var x pair var y peano var pair var z end quote end free end test end math
end "}%
%
\test{"
begin math false test peano free quote peano all var y peano var indeed var b pair var x peano var pair var c end quote set quote var x peano var end quote to quote var x pair var y peano var pair var z end quote end free end test end math
end "}%
%
\test{"
begin math test peano free quote peano all var x peano var indeed var b pair var x peano var pair var c end quote set quote var y peano var end quote to quote var x pair var y peano var pair var z end quote end free end test end math
end "}%
%
\test{"
begin math test peano free quote peano all var y peano var indeed var b pair var x peano var pair var c end quote set quote var y peano var end quote to quote var x pair var y peano var pair var z end quote end free end test end math
end "}%
%
"
begin math define pyk of peano sub var a is var b where var x is var c end sub as text "peano sub * is * where * is * end sub" end text end define end math
then math define tex of peano sub var a is var b where var x is var c end sub as text "#1.
{\equiv}\langle #2.
|#3.
:=#4.
\rangle" end text end define end math
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 math define pyk of peano sub star var a is var b where var x is var c end sub as text "peano sub star * is * where * is * end sub" end text end define end math
then math define tex of peano sub star var a is var b where var x is var c end sub as text "#1.
{\equiv}\langle^* #2.
|#3.
:=#4.
\rangle" end text end define end math
end " har samme betydning for lister "
begin bracket var a end bracket
end " og "
begin bracket var b end bracket
end ".
\display{"
begin math define value of 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 tagged if tagged if var b term root equal quote peano all var u indeed var v end quote then var b first term equal var x else false end if then var a term equal var b else newline tagged if var b is peano var and var b term equal var x then var a term equal var c else tagged if newline var a term root equal var b then peano sub star var a tail is var b tail where var x is var c end sub else false end if end if end if end define end math
end "}
\display{"
begin math define value of 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 tagged if peano sub var a head is var b head where var x is var c end sub then peano sub star var a tail is var b tail where var x is var c end sub else false end if end if end define end math
end "}%
%
\test{"
begin math test peano sub var a peano var is var a peano var where var b peano var is var c peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub var c peano var is var b peano var where var b peano var is var c peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub all var a peano var indeed var a peano var peano is var b peano var is all var a peano var indeed var a peano var peano is var b peano var where var a peano var is var c peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub all var a peano var indeed var a peano var peano is var c peano var is all var a peano var indeed var a peano var peano is var b peano var where var b peano var is var c peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub peano all var a peano var indeed var a peano var peano is peano zero peano plus var a peano var peano imply var c peano var peano times var d peano var peano is peano zero peano plus var c peano var peano times var d peano var is peano all var a peano var indeed var a peano var peano is peano zero peano plus var a peano var peano imply var b peano var peano is peano zero peano plus var b peano var where var b peano var is var c peano var peano times var d peano var end sub end test end math
end "}%
%
\test{"
begin math test peano sub peano all var a peano var indeed var a peano var peano is peano zero peano plus var a peano var peano imply var b peano var peano is peano zero peano plus var b peano var is peano all var a peano var indeed var a peano var peano is peano zero peano plus var a peano var peano imply var b peano var peano is peano zero peano plus var b peano var where var a peano var is var c peano var end sub end test end math
end "}%
%
\subsection{Teorien S'}
Den formelle teori, som vil danne grundlag for denne rapport, vil blive betegnet
"
begin math define pyk of system prime s as text "system prime s" end text end define end math
then math define tex of system prime s as text "
S'" end text end define end math
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 math define pyk of axiom prime a one as text "axiom prime a one" end text end define end math
then math define tex of axiom prime a one as text "
A1'" end text end define end math
end ",
"
begin math define pyk of axiom prime a two as text "axiom prime a two" end text end define end math
then math define tex of axiom prime a two as text "
A2'" end text end define end math
end ",
"
begin math define pyk of axiom prime a three as text "axiom prime a three" end text end define end math
then math define tex of axiom prime a three as text "
A3'" end text end define end math
end ",
"
begin math define pyk of axiom prime a four as text "axiom prime a four" end text end define end math
then math define tex of axiom prime a four as text "
A4'" end text end define end math
end ", og
"
begin math define pyk of axiom prime a five as text "axiom prime a five" end text end define end math
then math define tex of axiom prime a five as text "
A5'" end text end define end math
end ", samt de 2 inferensregler
"
begin math define pyk of rule prime mp as text "rule prime mp" end text end define end math
then math define tex of rule prime mp as text "
MP'" end text end define end math
end " og
"
begin math define pyk of rule prime gen as text "rule prime gen" end text end define end math
then math define tex of rule prime gen as text "
Gen'" end text end define end math
end ":
\display{"
begin math define statement of system prime s as all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano plus metavar var b end metavar peano succ peano is metavar var a end metavar peano plus metavar var b end metavar peano succ rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano succ peano is metavar var b end metavar peano succ peano imply metavar var a end metavar peano is metavar var b end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var a end metavar end quote end nonfree endorse peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano times metavar var b end metavar peano succ peano is metavar var a end metavar peano times metavar var b end metavar peano plus metavar var a end metavar rule plus all metavar var a end metavar indeed metavar var a end metavar peano plus peano zero peano is metavar var a end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse metavar var b end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar rule plus all metavar var a end metavar indeed not peano zero peano is metavar var a end metavar peano succ rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar rule plus all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar rule plus all metavar var a end metavar indeed metavar var a end metavar peano times peano zero peano is peano zero end define end math
end "}
\display{"
begin math define statement of axiom prime a one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom prime a one as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define
then define proof of axiom prime a two as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a three as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed peano not metavar var b end metavar peano imply peano not metavar var a end metavar peano imply peano not metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar end define
then define proof of axiom prime a three as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a four as system prime s infer all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse peano all metavar var x end metavar indeed metavar var b end metavar peano imply metavar var a end metavar end define
then define proof of axiom prime a four as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime a five as system prime s infer all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed peano nonfree quote metavar var x end metavar end quote in quote metavar var a end metavar end quote end nonfree endorse peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar end define
then define proof of axiom prime a five as rule tactic end define end math
end "}
\display{"
begin math define statement of rule prime mp as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar end define
then define proof of rule prime mp as rule tactic end define end math
end "}
\display{"
begin math define statement of rule prime gen as system prime s infer all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar end define
then define proof of rule prime gen as rule tactic end define end math
end "}
Derudover er der ogs{\aa} de egentlige axiomer fra Peano-aritmetik "
begin math define pyk of axiom prime s one as text "axiom prime s one" end text end define end math
then math define tex of axiom prime s one as text "
S1'" end text end define end math
end ",
"
begin math define pyk of axiom prime s two as text "axiom prime s two" end text end define end math
then math define tex of axiom prime s two as text "
S2'" end text end define end math
end ",
"
begin math define pyk of axiom prime s three as text "axiom prime s three" end text end define end math
then math define tex of axiom prime s three as text "
S3'" end text end define end math
end ",
"
begin math define pyk of axiom prime s four as text "axiom prime s four" end text end define end math
then math define tex of axiom prime s four as text "
S4'" end text end define end math
end ",
"
begin math define pyk of axiom prime s five as text "axiom prime s five" end text end define end math
then math define tex of axiom prime s five as text "
S5'" end text end define end math
end ",
"
begin math define pyk of axiom prime s six as text "axiom prime s six" end text end define end math
then math define tex of axiom prime s six as text "
S6'" end text end define end math
end ",
"
begin math define pyk of axiom prime s seven as text "axiom prime s seven" end text end define end math
then math define tex of axiom prime s seven as text "
S7'" end text end define end math
end ",
"
begin math define pyk of axiom prime s eight as text "axiom prime s eight" end text end define end math
then math define tex of axiom prime s eight as text "
S8'" end text end define end math
end ", og
"
begin math define pyk of axiom prime s nine as text "axiom prime s nine" end text end define end math
then math define tex of axiom prime s nine as text "
S9'" end text end define end math
end ":
\display{"
begin math define statement of axiom prime s one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano is metavar var c end metavar peano imply metavar var b end metavar peano is metavar var c end metavar end define
then define proof of axiom prime s one as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s two as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano is metavar var b end metavar peano imply metavar var a end metavar peano succ peano is metavar var b end metavar peano succ end define
then define proof of axiom prime s two as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s three as system prime s infer all metavar var a end metavar indeed not peano zero peano is metavar var a end metavar peano succ end define
then define proof of axiom prime s three as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s four as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano succ peano is metavar var b end metavar peano succ peano imply metavar var a end metavar peano is metavar var b end metavar end define
then define proof of axiom prime s four as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s five as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano plus peano zero peano is metavar var a end metavar end define
then define proof of axiom prime s five as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s six as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano plus metavar var b end metavar peano succ peano is metavar var a end metavar peano plus metavar var b end metavar peano succ end define
then define proof of axiom prime s six as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s seven as system prime s infer all metavar var a end metavar indeed metavar var a end metavar peano times peano zero peano is peano zero end define
then define proof of axiom prime s seven as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s eight as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar peano times metavar var b end metavar peano succ peano is metavar var a end metavar peano times metavar var b end metavar peano plus metavar var a end metavar end define
then define proof of axiom prime s eight as rule tactic end define end math
end "}
\display{"
begin math define statement of axiom prime s nine as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse metavar var b end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar peano imply metavar var c end metavar peano imply peano all metavar var x end metavar indeed metavar var a end metavar end define
then define proof of axiom prime s nine as rule tactic end define 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 var t peano var indeed peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var 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 math define pyk of lemma prime three two h as text "lemma prime three two h" end text end define end math
then math define tex of lemma prime three two h as text "L3.2 (h)'" end text end define end math
end " afh{\ae}nger af de foreg{\aa}ende lemmaer
"
begin math define pyk of lemma prime three two a as text "lemma prime three two a" end text end define end math
then math define tex of lemma prime three two a as text "L3.2 (a)'" end text end define end math
end ",
"
begin math define pyk of lemma prime three two b as text "lemma prime three two b" end text end define end math
then math define tex of lemma prime three two b as text "L3.2 (b)'" end text end define end math
end ",
"
begin math define pyk of lemma prime three two c as text "lemma prime three two c" end text end define end math
then math define tex of lemma prime three two c as text "L3.2 (c)'" end text end define end math
end ",
"
begin math define pyk of lemma prime three two d as text "lemma prime three two d" end text end define end math
then math define tex of lemma prime three two d as text "L3.2 (d)'" end text end define end math
end ",
"
begin math define pyk of lemma prime three two f as text "lemma prime three two f" end text end define end math
then math define tex of lemma prime three two f as text "L3.2 (f)'" end text end define end math
end " og
"
begin math define pyk of lemma prime three two g as text "lemma prime three two g" end text end define end math
then math define tex of lemma prime three two g as text "L3.2 (g)'" end text end define end math
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 metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar end bracket
end ", og man {\o}nsker at konkludere "
begin bracket metavar var c end metavar end bracket
end " ud fra "
begin bracket metavar var a end metavar end bracket
end " og "
begin bracket metavar var b end metavar 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 math define pyk of lemma mp twice as text "lemma mp twice" end text end define end math
then math define tex of lemma mp twice as text "MPTwice" end text end define end math
end ":
\statement {"
begin math define statement of lemma mp twice as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar infer metavar var b end metavar infer metavar var c end metavar end define end math
end "}
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 define proof of lemma mp twice as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar infer metavar var b end metavar infer rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar conclude metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "}
\subsubsection{Lemma M1.7}
Fra Mendelson tages lemma 1.7 "
begin math define pyk of mendelson one seven as text "mendelson one seven" end text end define end math
then math define tex of mendelson one seven as text "
M1.7" end text end define end math
end ":
\statement{"
begin math define statement of mendelson one seven as system prime s infer all metavar var b end metavar indeed metavar var b end metavar peano imply metavar var b end metavar end define end math
end "}
\statement{"
begin math define proof of mendelson one seven as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var b end metavar indeed axiom prime a one conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut axiom prime a two conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar cut rule prime mp modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar modus ponens metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var b end metavar end quote state proof state cache var c end expand end define 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 math define pyk of lemma weaken as text "lemma weaken" end text end define end math
then math define tex of lemma weaken as text "Weaken" end text end define end math
end ":
\statement{
"
begin math define statement of lemma weaken as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer metavar var b end metavar peano imply metavar var a end metavar end define end math
end "}
Beviset er helt enkelt:
\statement{
"
begin math define proof of lemma weaken as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer axiom prime a one conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar peano imply metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "}
\subsubsection {Tautologi 1}
"
begin math define pyk of lemma tautology one as text "lemma tautology one" end text end define end math
then math define tex of lemma tautology one as text "Taut 1" end text end define end math
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 define statement of lemma tautology one as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
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 define proof of lemma tautology one as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer axiom prime a two conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut lemma weaken modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut axiom prime a two conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut lemma mp twice modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
}
\subsubsection{Tautologi 2}
Lemma "
begin math define pyk of lemma tautology two as text "lemma tautology two" end text end define end math
then math define tex of lemma tautology two as text "Taut 2" end text end define end math
end " udtrykker en form for transitivitet af implikationsoperatoren.
\statement{
"
begin math define statement of lemma tautology two as system prime s infer all metavar var d end metavar indeed all metavar var e end metavar indeed all metavar var f end metavar indeed metavar var d end metavar peano imply metavar var e end metavar infer metavar var e end metavar peano imply metavar var f end metavar infer metavar var d end metavar peano imply metavar var f end metavar end define end math
end "}
\statement{"
begin math define proof of lemma tautology two as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var d end metavar indeed all metavar var e end metavar indeed all metavar var f end metavar indeed metavar var d end metavar peano imply metavar var e end metavar infer metavar var e end metavar peano imply metavar var f end metavar infer axiom prime a one conclude metavar var e end metavar peano imply metavar var f end metavar peano imply metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar cut rule prime mp modus ponens metavar var e end metavar peano imply metavar var f end metavar peano imply metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar modus ponens metavar var e end metavar peano imply metavar var f end metavar conclude metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar cut axiom prime a two conclude metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar peano imply metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var d end metavar peano imply metavar var f end metavar cut lemma mp twice modus ponens metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar peano imply metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var d end metavar peano imply metavar var f end metavar modus ponens metavar var d end metavar peano imply metavar var e end metavar peano imply metavar var f end metavar modus ponens metavar var d end metavar peano imply metavar var e end metavar conclude metavar var d end metavar peano imply metavar var f end metavar end quote state proof state cache var c end expand end define end math
end "
}
\subsubsection{Tautologi 3}
Med lemma "
begin math define pyk of lemma tautology three as text "lemma tautology three" end text end define end math
then math define tex of lemma tautology three as text "Taut 3" end text end define end math
end " kan man eliminere en betingelse fra en dobbeltimplikation, s{\aa}fremt det kan bevises, at betingelsen altid er opfyldt.
\statement{"
begin math define statement of lemma tautology three as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "}
\statement{"
begin math define proof of lemma tautology three as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar infer axiom prime a two conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut lemma mp twice modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar peano imply metavar var b end metavar conclude metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "}
\subsubsection{Tautologi 4}
Tautologi "
begin math define pyk of lemma tautology four as text "lemma tautology four" end text end define end math
then math define tex of lemma tautology four as text "Taut 4" end text end define end math
end " er en svagere variant af forrige tautologi.
\statement{
"
begin math define statement of lemma tautology four as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar infer metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar infer metavar var b end metavar peano imply metavar var c end metavar end define end math
end "}
\statement{
"
begin math define proof of lemma tautology four as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar infer metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar infer lemma tautology one modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut rule prime mp modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define 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 define statement of lemma prime three two a as system prime s infer all metavar var t end metavar indeed metavar var t end metavar peano is metavar var t end metavar end define end math
end "
}
Beviset er kort, og benytter addition med nul som ``trick'':
\statement{
"
begin math define proof of lemma prime three two a as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed axiom prime s five conclude metavar var t end metavar peano plus peano zero peano is metavar var t end metavar cut axiom prime s one conclude metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar cut lemma mp twice modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano plus peano zero peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var t end metavar modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar modus ponens metavar var t end metavar peano plus peano zero peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define 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 define statement of lemma prime three two b as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end define end math
end "}
\statement{
"
begin math define proof of lemma prime three two b as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed axiom prime s one conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut lemma tautology one modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var t end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut lemma prime three two a conclude metavar var t end metavar peano is metavar var t end metavar cut rule prime mp modus ponens metavar var t end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var t end metavar peano is metavar var t end metavar conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar end quote state proof state cache var c end expand end define 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 define statement of lemma prime three two c as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end define end math
end "}
Med de allerede beviste lemmaer er dette bevis helt enkelt:
\statement{
"
begin math define proof of lemma prime three two c as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed axiom prime s one conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut lemma prime three two b conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar cut lemma tautology two modus ponens metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var t end metavar modus ponens metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar conclude metavar var t end metavar peano is metavar var r end metavar peano imply metavar var r end metavar peano is metavar var s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define 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 define statement of lemma prime three two d as system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define end math
end "}
\statement{"
begin math define proof of lemma prime three two d as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed lemma prime three two c conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut lemma tautology one modus ponens metavar var r end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut lemma prime three two b conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut lemma tautology two modus ponens metavar var s end metavar peano is metavar var t end metavar peano imply metavar var t end metavar peano is metavar var s end metavar modus ponens metavar var t end metavar peano is metavar var s end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar cut lemma tautology one modus ponens metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var r end metavar peano is metavar var t end metavar peano imply metavar var s end metavar peano is metavar var t end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end quote state proof state cache var c end expand end define 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 define statement of lemma prime three two f as system prime s infer peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var end define 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 define proof of lemma prime three two f as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude peano zero peano plus peano zero peano is peano zero cut lemma prime three two b conclude peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero cut rule prime mp modus ponens peano zero peano plus peano zero peano is peano zero peano imply peano zero peano is peano zero peano plus peano zero modus ponens peano zero peano plus peano zero peano is peano zero conclude peano zero peano is peano zero peano plus peano zero cut axiom prime s six conclude peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut axiom prime a one conclude peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime mp modus ponens peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ modus ponens peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut mendelson one seven conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var cut axiom prime s two conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut lemma tautology two modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut lemma prime three two d conclude var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut lemma tautology two modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ modus ponens var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut lemma tautology three modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply peano zero peano plus var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut rule prime gen modus ponens var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ cut axiom prime s nine conclude peano zero peano is peano zero peano plus peano zero peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut lemma mp twice modus ponens peano zero peano is peano zero peano plus peano zero peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ peano imply peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var modus ponens peano zero peano is peano zero peano plus peano zero modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var end quote state proof state cache var c end expand end define 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 define statement of lemma prime three two g as system prime s infer peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ end define 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 metavar var h end metavar end math
end ".
\statement{"
begin math define proof of lemma prime three two g as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var t peano var peano succ peano plus peano zero peano is var t peano var peano succ cut axiom prime s five conclude var t peano var peano plus peano zero peano is var t peano var cut axiom prime s two conclude var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano plus peano zero peano succ peano is var t peano var peano succ cut rule prime mp modus ponens var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano plus peano zero peano succ peano is var t peano var peano succ modus ponens var t peano var peano plus peano zero peano is var t peano var conclude var t peano var peano plus peano zero peano succ peano is var t peano var peano succ cut lemma prime three two d conclude var t peano var peano succ peano plus peano zero peano is var t peano var peano succ peano imply var t peano var peano plus peano zero peano succ peano is var t peano var peano succ peano imply var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ cut lemma mp twice modus ponens var t peano var peano succ peano plus peano zero peano is var t peano var peano succ peano imply var t peano var peano plus peano zero peano succ peano is var t peano var peano succ peano imply var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ modus ponens var t peano var peano succ peano plus peano zero peano is var t peano var peano succ modus ponens var t peano var peano plus peano zero peano succ peano is var t peano var peano succ conclude var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ cut axiom prime s six conclude var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ cut lemma weaken modus ponens var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ cut axiom prime s two conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime three two c conclude var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime mp modus ponens var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano succ peano plus var r peano var peano succ conclude var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma tautology two modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut axiom prime s six conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ cut axiom prime s two conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime mp modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ conclude var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma prime three two d conclude var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma tautology two modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut lemma tautology one modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime mp modus ponens var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ modus ponens var t peano var peano plus var r peano var peano succ peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut rule prime gen modus ponens var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ cut axiom prime s nine conclude var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut lemma mp twice modus ponens var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ peano imply peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ modus ponens var t peano var peano succ peano plus peano zero peano is var t peano var peano plus peano zero peano succ modus ponens peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano succ peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano succ conclude peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut rule prime gen modus ponens peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ conclude peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ end quote state proof state cache var c end expand end define 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 var t peano var end math
end " og "
begin math var r peano var 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 math define pyk of lemma prime three two g rev as text "lemma prime three two g rev" end text end define end math
then math define tex of lemma prime three two g rev as text "L3.2 (g)' II" end text end define end math
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 var t peano var end math
end " med "
begin math var r peano var 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 var s peano var 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 define statement of lemma prime three two g rev as system prime s infer peano sub quote peano all var r peano var indeed var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ end quote is quote peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ end quote where quote var t peano var end quote is quote var s peano var end quote end sub endorse peano sub quote var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ end quote is quote var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ end quote where quote var r peano var end quote is quote var t peano var end quote end sub endorse peano sub quote var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end quote is quote var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ end quote where quote var s peano var end quote is quote var r peano var end quote end sub endorse var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end define end math
end "}
Beviset udskifter f{\o}rst "
begin math var t peano var end math
end " med "
begin math var s peano var end math
end ", derefter "
begin math var r peano var end math
end " med "
begin math var t peano var end math
end " og til sidst "
begin math var s peano var end math
end " med "
begin math var r peano var 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 define proof of lemma prime three two g rev as lambda var c dot lambda var x dot proof expand quote system prime s infer lemma prime three two g conclude peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ cut peano sub quote peano all var r peano var indeed var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ end quote is quote peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ end quote where quote var t peano var end quote is quote var s peano var end quote end sub endorse axiom prime a four modus probans peano sub quote peano all var r peano var indeed var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ end quote is quote peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ end quote where quote var t peano var end quote is quote var s peano var end quote end sub conclude peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply peano all var r peano var indeed var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ cut rule prime mp modus ponens peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ peano imply peano all var r peano var indeed var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ modus ponens peano all var t peano var indeed peano all var r peano var indeed var t peano var peano succ peano plus var r peano var peano is var t peano var peano plus var r peano var peano succ conclude peano all var r peano var indeed var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ cut peano sub quote var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ end quote is quote var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ end quote where quote var r peano var end quote is quote var t peano var end quote end sub endorse axiom prime a four modus probans peano sub quote var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ end quote is quote var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ end quote where quote var r peano var end quote is quote var t peano var end quote end sub conclude peano all var r peano var indeed var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ peano imply var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ cut rule prime mp modus ponens peano all var r peano var indeed var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ peano imply var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ modus ponens peano all var r peano var indeed var s peano var peano succ peano plus var r peano var peano is var s peano var peano plus var r peano var peano succ conclude var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ cut rule prime gen modus ponens var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ conclude peano all var s peano var indeed var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ cut peano sub quote var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end quote is quote var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ end quote where quote var s peano var end quote is quote var r peano var end quote end sub endorse axiom prime a four modus probans peano sub quote var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end quote is quote var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ end quote where quote var s peano var end quote is quote var r peano var end quote end sub conclude peano all var s peano var indeed var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut rule prime mp modus ponens peano all var s peano var indeed var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ modus ponens peano all var s peano var indeed var s peano var peano succ peano plus var t peano var peano is var s peano var peano plus var t peano var peano succ conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ end quote state proof state cache var c end expand end define 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 math define pyk of lemma prime three two h base as text "lemma prime three two h base" end text end define end math
then math define tex of lemma prime three two h base as text "L3.2 (h)' basis" end text end define end math
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 define statement of lemma prime three two h base as system prime s infer peano sub quote var t peano var peano is peano zero peano plus var t peano var end quote is quote var t peano var peano is peano zero peano plus var t peano var end quote where quote var t peano var end quote is quote var t peano var end quote end sub endorse peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end define end math
end "
}
\statement{
"
begin math define proof of lemma prime three two h base as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var t peano var peano plus peano zero peano is var t peano var cut lemma prime three two f conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var cut peano sub quote var t peano var peano is peano zero peano plus var t peano var end quote is quote var t peano var peano is peano zero peano plus var t peano var end quote where quote var t peano var end quote is quote var t peano var end quote end sub endorse axiom prime a four modus probans peano sub quote var t peano var peano is peano zero peano plus var t peano var end quote is quote var t peano var peano is peano zero peano plus var t peano var end quote where quote var t peano var end quote is quote var t peano var end quote end sub conclude peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var cut rule prime mp modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var modus ponens peano all var t peano var indeed var t peano var peano is peano zero peano plus var t peano var conclude var t peano var peano is peano zero peano plus var t peano var cut lemma prime three two c conclude var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano plus peano zero peano is peano zero peano plus var t peano var cut lemma mp twice modus ponens var t peano var peano plus peano zero peano is var t peano var peano imply var t peano var peano is peano zero peano plus var t peano var peano imply var t peano var peano plus peano zero peano is peano zero peano plus var t peano var modus ponens var t peano var peano plus peano zero peano is var t peano var modus ponens var t peano var peano is peano zero peano plus var t peano var conclude var t peano var peano plus peano zero peano is peano zero peano plus var t peano var cut axiom prime s nine conclude var t peano var peano plus peano zero peano is peano zero peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut rule prime mp modus ponens var t peano var peano plus peano zero peano is peano zero peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var modus ponens var t peano var peano plus peano zero peano is peano zero peano plus var t peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end quote state proof state cache var c end expand end define 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 define statement of lemma prime three two h as system prime s infer peano all var t peano var indeed peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end define 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 define proof of lemma prime three two h as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ cut lemma prime three two g rev conclude var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ cut axiom prime s two conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut lemma prime three two c conclude var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut rule prime mp modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano succ peano is var t peano var peano plus var r peano var peano succ conclude var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut lemma tautology two modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut lemma prime three two d conclude var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut lemma tautology two modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut lemma tautology four modus ponens var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var r peano var peano succ peano plus var t peano var peano is var r peano var peano plus var t peano var peano succ peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut rule prime gen modus ponens var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var cut lemma prime three two h base conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut rule prime mp modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano imply peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var peano imply var t peano var peano plus var r peano var peano succ peano is var r peano var peano succ peano plus var t peano var conclude peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var cut rule prime gen modus ponens peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var conclude peano all var t peano var indeed peano all var r peano var indeed var t peano var peano plus var r peano var peano is var r peano var peano plus var t peano var end quote state proof state cache var c end expand end define 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 define pyk of peanorapport as text "peanorapport" end text 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 math define pyk of peano a as text "peano a" end text end define end math
then math define tex of peano a as text "
\dot{\mathit{a}}" end text end define end math
end ",
"
begin math define pyk of peano b as text "peano b" end text end define end math
then math define tex of peano b as text "
\dot{\mathit{b}}" end text end define end math
end ",
"
begin math define pyk of peano c as text "peano c" end text end define end math
then math define tex of peano c as text "
\dot{\mathit{c}}" end text end define end math
end ",
"
begin math define pyk of peano d as text "peano d" end text end define end math
then math define tex of peano d as text "
\dot{\mathit{d}}" end text end define end math
end ",
"
begin math define pyk of peano e as text "peano e" end text end define end math
then math define tex of peano e as text "
\dot{\mathit{e}}" end text end define end math
end ",
"
begin math define pyk of peano f as text "peano f" end text end define end math
then math define tex of peano f as text "
\dot{\mathit{f}}" end text end define end math
end ",
"
begin math define pyk of peano g as text "peano g" end text end define end math
then math define tex of peano g as text "
\dot{\mathit{g}}" end text end define end math
end ",
"
begin math define pyk of peano h as text "peano h" end text end define end math
then math define tex of peano h as text "
\dot{\mathit{h}}" end text end define end math
end ",
"
begin math define pyk of peano i as text "peano i" end text end define end math
then math define tex of peano i as text "
\dot{\mathit{i}}" end text end define end math
end ",
"
begin math define pyk of peano j as text "peano j" end text end define end math
then math define tex of peano j as text "
\dot{\mathit{j}}" end text end define end math
end ",
"
begin math define pyk of peano k as text "peano k" end text end define end math
then math define tex of peano k as text "
\dot{\mathit{k}}" end text end define end math
end ",
"
begin math define pyk of peano l as text "peano l" end text end define end math
then math define tex of peano l as text "
\dot{\mathit{l}}" end text end define end math
end ",
"
begin math define pyk of peano m as text "peano m" end text end define end math
then math define tex of peano m as text "
\dot{\mathit{m}}" end text end define end math
end ",
"
begin math define pyk of peano n as text "peano n" end text end define end math
then math define tex of peano n as text "
\dot{\mathit{n}}" end text end define end math
end ",
"
begin math define pyk of peano o as text "peano o" end text end define end math
then math define tex of peano o as text "
\dot{\mathit{o}}" end text end define end math
end ",
"
begin math define pyk of peano p as text "peano p" end text end define end math
then math define tex of peano p as text "
\dot{\mathit{p}}" end text end define end math
end ",
"
begin math define pyk of peano q as text "peano q" end text end define end math
then math define tex of peano q as text "
\dot{\mathit{q}}" end text end define end math
end ",
"
begin math define pyk of peano r as text "peano r" end text end define end math
then math define tex of peano r as text "
\dot{\mathit{r}}" end text end define end math
end ",
"
begin math define pyk of peano s as text "peano s" end text end define end math
then math define tex of peano s as text "
\dot{\mathit{s}}" end text end define end math
end ",
"
begin math define pyk of peano t as text "peano t" end text end define end math
then math define tex of peano t as text "
\dot{\mathit{t}}" end text end define end math
end ",
"
begin math define pyk of peano u as text "peano u" end text end define end math
then math define tex of peano u as text "
\dot{\mathit{u}}" end text end define end math
end ",
"
begin math define pyk of peano v as text "peano v" end text end define end math
then math define tex of peano v as text "
\dot{\mathit{v}}" end text end define end math
end ",
"
begin math define pyk of peano w as text "peano w" end text end define end math
then math define tex of peano w as text "
\dot{\mathit{w}}" end text end define end math
end ",
"
begin math define pyk of peano x as text "peano x" end text end define end math
then math define tex of peano x as text "
\dot{\mathit{x}}" end text end define end math
end ",
"
begin math define pyk of peano y as text "peano y" end text end define end math
then math define tex of peano y as text "
\dot{\mathit{y}}" end text end define end math
end ", and
"
begin math define pyk of peano z as text "peano z" end text end define end math
then math define tex of peano z as text "
\dot{\mathit{z}}" end text end define end math
end ".
Disse variabler makrodefineres som
"
begin math define macro of peano a as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano a as var a peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano b as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano b as var b peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano c as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano c as var c peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano d as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano d as var d peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano e as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano e as var e peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano f as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano f as var f peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano g as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano g as var g peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano h as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano h as var h peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano i as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano i as var i peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano j as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano j as var j peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano k as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano k as var k peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano l as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano l as var l peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano m as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano m as var m peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano n as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano n as var n peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano o as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano o as var o peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano p as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano p as var p peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano q as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano q as var q peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano r as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano r as var r peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano s as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano s as var s peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano t as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano t as var t peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano u as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano u as var u peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano v as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano v as var v peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano w as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano w as var w peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano x as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano x as var x peano var end define end quote end define end define end math
end ",
"
begin math define macro of peano y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano y as var y peano var end define end quote end define end define end math
end ", og
"
begin math define macro of peano z as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define peano z as var z peano var end define end quote end define 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,