"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{amsmath}
%\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{Logik Rapport}
\author{Holger Bock Axelsen\\Michael Kirkedal Thomsen}
%%%%%%%%%%%HER BEGYNDER DOKUMENTET%%%%%%%%%%%%%%%%
\begin {document}
\maketitle
\newpage
\tableofcontents
\newpage
\section{Introduktion til Logiweb}
Denne rapport er skrevet med henblik p{\aa} publikation i Logiweb-systemet, og er hvad der kaldes en Logiweb-\emph{side}. Logiweb er ikke kun lavet for at kunne fremvise rapporter og matematiske formler p\aa{} en p\ae{}n m\aa{}de\footnote{Der er mange systemer der er god til at fremvise rapporter og is\ae{}r matematiske formler. \TeX{} (og herunder \LaTeX{}) er et meget godt eksempel herp\aa{}.};
Logiweb skal ogs\aa{} kunne forst\aa{} (dele af) den matematik, der bliver skrevet p\aa{} siden. Med denne forst\aa{}else gives der mulighed for at definere en bevischecker og k\o{}re programmer, som defineret p\aa{} Logiweb sider, og formelt verificere korrekthed. Logiweb-sider kan ogs{\aa} publiceres p{\aa} en Logiweb-server, s\aa{} andre nemt kan henvise til siden og benytte beviser og lignende fra publicerede sider p{\aa} en nem, men formel og korrekt m{\aa}de.
\subsection{Logiweb-siden}
Til at generere Logiweb sider er der designet et sprog kaldet \textit{pyk}, der p{\aa} mange m{\aa}der minder om andre mark-up sprog: F\o{}rst defineres sidens navn, derefter de sider der refereres til, og bagefter de \emph{pyk}-konstruktioner, der benyttes p\aa{} siden (ogs\aa{} dem som er defineret p\aa{} referencesider). En konstruktion kan v\ae{}re alt fra formler og relationer til variabler og programmer. Alle konstruktioner introduceres med en \textit{pyk}-(reference) og en \textit{tex}-definition af deres udseende p{\aa} papiret. Dette er et eksempel p{\aa} forskellige \emph{aspekter} af den samme konstruktion, et begreb der er meget vigtigt for \emph{pyk}-compileren: F.eks. vil \emph{pyk}-aspektet af en definition blive brugt i den formelle verifikation af en side, og \emph{tex}-aspektet blive brugt i generering af den l{\ae}sbare tekst.
Vi bruger alts{\aa} en \emph{pyk}-compiler i samarbejde med en Logiweb-server til at f{\aa} en reel Logiweb-side. En \emph{pyk}-kildetekst best{\aa}r s{\aa}ledes groft sagt af nogle s\ae{}tninger og beviser skrevet i \textit{pyk} sammensat med br{\o}dtekst, der skal v{\ae}re formateret i \LaTeX{} kode. Udseendet af den formelle matematik og Logiwebs forst{\aa}else af dem afh\ae{}nger af de konstruktioner der er defineret p\aa{} siden og i bibliografien. For den formelle verifikation af matematikken skal \textit{pyk}-konstruktion\-er alts{\aa} benyttes.
Som uddata giver Logiweb-serveren et system af html-sider, tilg{\ae}ngeligt via internettet, med f\o{}lgende indhold:
\begin{itemize}
\item \textit{Reference} - Unik reference til siden s\aa{} andre kan benytte indholdet.
\item \textit{Vector} - Den del af en Logiweb side der bliver indl\ae{}st af andre sider.
\item \textit{Body} - Selve siden i ``papir''. Denne rapport er \textit{body} til denne Logiweb side.
\item \textit{Bibliography } - Liste med de Logiweb-sider som siden refererer til, inkl. siden selv.
\item \textit{Dictionary} - Liste med alle Logiweb-konstruktioner der er introduceret p\aa{} siden.
\item \textit{Codex} - Liste med alt som er defineret p\aa{} denne side, samt deres definitioner.
\item \textit{Expansion} - Version af \textit{body} som er makro ekspanderet fuldt ud.
\item \textit{Diagnose} - Hvis matematikken ikke kunne verificeres gives her en fejlmeddelelse.
\item \textit{Source} - Sidens kildekode (i \textit{pyk}).
\end{itemize}
Indholdet i hvert af afsnittene (undtagen \textit{Source}, som er den r\aa{} \emph{pyk} kodetekst) kan ses i en r{\ae}kke formater, bl.a. PDF\footnote{Portable Document Format}.
For den interesserede l{\ae}ser er der (meget) mere om Logiweb i (base reference) -- det vigtigste at f{\aa} ud af den meget korte introduktion til Logiweb ovenfor er at sider publiceret i Logiweb-systemet er checket af en automatisk bevischecker (der i sig selv er defineret i \emph{pyk}).
\subsection{Denne Logiweb side.}
Til eksempel kan vi gennemg{\aa} denne side i Logiweb-forstand:
Denne Logiweb side hedder "
begin math define pyk of hmpeano as text "hmpeano" end text end define end math
then math define tex of hmpeano as text "HMpeano" end text end define end math
end ". I fodnoten ses den f\o{}rst introduktion p\aa{} denne side, som er en \emph{pyk}-definition af selve siden.
Denne sides bibliografi er bestemt af referencen til to andre sider:
\begin{itemize}
\item \textbf{base}\footnote{Se [1].} - indeholder bevischecker, makroudfoldelse, aritmetik og meget mere.
\item \textbf{peano}\footnote{Se [2].} - definerer Peano aritmetik som benyttes p\aa{} denne side.
\end{itemize}
Dens Logiweb homepage er\\
\verb+http://www.diku.dk/~grue/logiweb/20050502/home/funkstar/hmpeano+
Dens kana reference er
\display{\tt\lgwHmpeanoKana}
\subsubsection{Ops\ae{}tning af beviser.}
Ops\ae{}tningen af beviser og definitioner bliver fastlagt p\aa{} Logiweb-siderne selv -- i vores tilf{\ae}lde benytter vi bevis-konstruktet fra [1]. Men alle lemmaer p\aa{} siden skal introduceres, defineres og bevises. L{\ae}g m{\ae}rke til at papirops{\ae}tningen, \emph{tex}-aspektet, er uafh{\ae}ngigt af bevis-checkeren. S{\aa}ledes kan et bevis v{\ae}re forkert, men sat op p{\aa} samme m{\aa}de som andre beviser. Kun ved at konsultere Logiweb-systemet kan man reelt verificere at beviset er korrekt\footnote{Med det caveat at beviset skal v{\ae}re genereret udfra et \emph{pyk}-bevis. Med \LaTeX{} kan man naturligvis emulere de generede beviser, hvorfor skeptikeren b{\o}r inspicere kildekoden.}.
Et bevis vil p{\aa} denne side fremst{\aa} som en r{\ae}kke linier, der definerer argumentationen for beviset. Et eksempel p{\aa} et bevis is systemet System for propositionen Lemma ser s\aa{}ledes ud:\\
\\
System
$\mathbf {\ proof\ of\ }$Lemma$
\colon
\newline $
\makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{
$L01$:}$
Argument
{}\gg {}$}
\quad
\parbox [t]{0.4\textwidth }{$
Konklusion
$\hfill \makebox [0mm][l]{\quad ;}}
$\newline $
\makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{
$L02$:}$
Keyword
{}\gg {}$}
\quad
\parbox [t]{0.4\textwidth }{$
Formel/Term
$\hfill \makebox [0mm][l]{\quad \makebox[0mm]{$\Box$}}}\\
Et Argument kan v{\ae}re et axiom eller et lemma, og inludere linienumre, variable eller andre konstruktioner i argumentationen, og en formel underst{\o}ttet af denne argumentation kan skrives som Konklusion (en sand formel, givet foruds{\ae}tningerne for beviset). Mao. er ops{\ae}tningen \emph{ikke} t{\ae}nkt som i en bevis-\emph{assistent}, der generer en formel udfra en given argumentation, men som linier med tilh{\o}rende argumentation. Dette svarer ogs{\aa} til \emph{pyk}-koden, og formatet brugt i (Mendelson reference). Argumenter har udforming som f{\o}lgende eksempel, "
begin math rule mp modus ponens ell a modus ponens ell b end math
end ", der skal forst{\aa}s p{\aa} den m{\aa}de at Lemma/Axiom "
begin math rule mp end math
end " benyttet med linierne "
begin math ell a end math
end " og "
begin math ell b end math
end " som pre{\ae}misser, underst{\o}tter den givne konklusion. Den eneste anden form for argumentation vil vi se i denne rapport, er "
begin math axiom prime a four at var x peano var end math
end " der siger at "
begin math axiom prime a four end math
end "'s substitutions variabel (meta-kvantiseret som "
begin math metavar var x end metavar end math
end ") er "
begin math var x peano var end math
end " i konklusionen.
Et Keyword er et de f{\o}lgende fire:
\begin{itemize}
\item Arbitrary, hvor konklusionen er en meta-variabel (skrevet med kalligrafisk skrifttype). Hvad meta-variablen rangerer over (formler, termer, Peano variable) vil v{\ae}re klart af konteksten. Hvis vi har introduceret en variabel som Arbitrary, vil en konklusion automatisk v{\ae}re generaliseret (med al-kvantoren $\forall$).
\item Premise, hvor konklusion er en af de givne pr{\ae}misser.
\item Side-condition, hvor konklusionen er en given sidebetingelse.
\item Local, hvor konklusion er bindingen af en frisk meta-variabel til en given formel/term.
\end{itemize}
Vi vil ikke direkte benytte Side-condition, men bem{\ae}rker at der er forskel p{\aa} at kr{\ae}ve noget som side-betingelse i forhold til at kr{\ae}ve det som pr{\ae}mis: I Peano aritmetik, som defineret nedenfor, har flere af axiomerne side-betingelser.
Endelig vil den sidste linie i beviset v{\ae}re afsluttet med $\Box$ (klassisk forkortelse for \emph{quod erat demontrandum}), og konklusionen vil v{\ae}re identisk med Lemmaets proposition.
\subsection{Hvorfor benytte Logiweb?}
Denne rapport er som betingelse skrevet i Logiweb, men det er ikke sv{\ae}rt at se Logiwebs styrker:
\begin{itemize}
\item Globalt. Sider publiceret p{\aa} Logiweb er tilg{\ae}ngelige for alle, hvilket motiverer kode-deling, og f{\ae}lles udvikling.
\item Modul{\ae}rt. Sider (som) denne kan opbygges af eksisterende bestandele.
\item Selvindeholdt. Selvom vi har benyttet grunddefinitioner fra en bestemt side, er dette ikke mandatorisk, og andre formuleringer kan t{\ae}nkes.
\item P{\ae}nt. For l{\ae}seren genereres et l{\ae}sbart stykke tekst der svarer til de formelle definitioner.
\item Frit. N{\ae}sten alt kan tilpasses, og specielle konstruktioner kan introduceres efter behov.
\end{itemize}
\section{Peano-aritmetik}
Det logiske system system vi benytter er Peano aritmetik (PA), som defineret i systemet "
begin system prime s
end " defineret p{\aa} siden [2], svarende til Mendelson Lemma 3.1. Vi giver her en kort gennemgang af dette system, og henviser l{\ae}seren til [2] for yderligere detaljer.
PA termer og formler er opbygget af en r{\ae}kke konstruktorer, beskrevet ved f{\o}lgende BNF:
\begin{align*}
"
begin metavar var t end metavar
end " & ::= "
begin peano zero
end " \;|\; "
begin metavar var t end metavar peano succ
end " \;|\; "
begin metavar var t end metavar peano plus metavar var t end metavar
end " \;|\; "
begin metavar var t end metavar peano times metavar var t end metavar
end " \;|\; "
begin metavar var x end metavar
end "\\
"
begin metavar var f end metavar
end " & ::= "
begin metavar var t end metavar peano is metavar var t end metavar
end " \;|\; "
begin peano not metavar var f end metavar
end " \;|\; "
begin metavar var f end metavar peano imply metavar var f end metavar
end " \;|\; "
begin peano all metavar var x end metavar indeed metavar var f end metavar
end "\\
"
begin metavar var x end metavar
end " & ::= "
begin var x peano var
end "\\
\end{align*}
hvor "
begin math var x peano var end math
end " er navnet p{\aa} en konkret Peano variabel. Tilg{\ae}ngelige navne er "
begin math var a peano var end math
end " til "
begin math var z peano var end math
end ". De resterende logiske konnektiver kan defineret udfra de her givne, hvilket er gjort i [2], men i denne rapport er de originale kontruktioner nok. N{\aa}r vi skriver formler i PA bruges pr{\ae}cedens regler til at udflade syntakstr{\ae}et, og eliminere parenteser. De brugte operatorer i denne rapport har pr{\ae}cedensorden $\dot{\Rightarrow}$, $\dot{\forall}$, $\dot{+}$, $'$, hvor $'$ binder st{\ae}rkest. Til forskel fra Mendelson er $\dot{\Rightarrow}$ h{\o}jreassociativ.
Til formel r{\ae}ssonering om PA termer og formler har vi brug for axiomer og inferensregler.
\display{"
begin math define statement of system prime s as var x 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 "}
"
begin math axiom prime a one end math
end " til "
begin math axiom prime a five end math
end " er de velkendte axiomer for f{\o}rste ordens pr{\ae}dikat-kalkyle (Mendelson, s.69). Bem{\ae}rk formalisering af Mendelsons ``free for'' begreb i side\-be\-ting\-el\-ser\-ne for "
begin math axiom prime a four end math
end " og "
begin math axiom prime a five end math
end ": "
begin math 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 end math
end " betyder at "
begin math metavar var a end metavar end math
end " er syntaktisk {\ae}kvivalent med "
begin math metavar var b end metavar end math
end " hvor alle frie forekomster af "
begin math metavar var x end metavar end math
end " er substitueret med "
begin math metavar var c end metavar end math
end ". "
begin math peano nonfree quote metavar var x end metavar end quote in quote metavar var a end metavar end quote end nonfree end math
end " betyder det oplagte: "
begin math metavar var a end metavar end math
end " indeholder ingen frie forekomster af "
begin math metavar var x end metavar end math
end ". Den pr{\ae}cise formalisering som disse konstrukter d{\ae}kker over kan ses p{\aa} siden (peano reference).
Det er desuden vigtigt at bem{\ae}rke forskellen p{\aa} kvantisering over formler (well-forms) hvor notationen benytter den almindelige al-kvantor, og kvantisering over Peano variable, hvor notationen benytter en al-kvantor med en prik, $\dot{\forall}$. I PA er disse to distinkte konstruktioner. Dette vil v{\ae}re relevant senere i rapporten, men det allerede nu burde konventionen v{\ae}re klar: Variable med prik er Peano variable, konstruktioner (funktioner, relationer) med en prik er Peano konstruktioner. Logiweb-systemet har ingen intrinsisk viden om semantikken for disse konstruktioner, dvs. vil man argumentere med f.eks. DeMorgans love, skal disse formuleres med de tilsvarende Peano konstruktioner og bevises vha. ovenst{\aa}ende axiomer. Mao. er Logiweb-systemet syntaktisk.
\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 "}
Disse er de velkendte inferensregler, \emph{modus ponens} og \emph{generalisering}.
\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 "}
"
begin math axiom prime s one end math
end " til "
begin math axiom prime s nine end math
end " er de egentlige axiomer i PA, og giver logikken lighed, rekursive definitioner af to funktioner (addition og multiplikation), samt induktion. Igen, for at skelne lighed i PA med lighed defineret andetsteds i Logiweb bibliografien for denne side (specifikt, lighed som defineret p{\aa} siden [1]), har lighedstegnet f{\aa}et et ``p'' (for Peano.) Bem{\ae}rk ogs{\aa} brugen af side-betingelser i induktionsprincippet. Brugen af Peano al-kvantoren betyder ogs{\aa} at induktion kun kan foreg{\aa} over Peano variable.
\section{Hypotetisk deduktion}
Beviser der g{\o}r brug af induktionsprincippet giver os et glimrende eksempel p{\aa} en klassisk problemstilling i logik: forholdet mellem praktisk anvendelighed og parsimoni. Ofte vil det v{\ae}re muligt at komprimere en teori til meget f{\aa} og pr{\ae}cise grundelementer, men p{\aa} bekostning af brugervenlighed. Et eksempel med h{\o}j relevans for dataloger er NAND-gates: De velkendte logiske konnektiver kan repr{\ae}senteres ved blot et enkelt, bin{\ae}rt symbol. Tilg{\ae}ndg{\ae}ld bliver alt udover de allersimpleste udtryk uoverskuelige at l{\ae}se for mennesker. En tilsvarende situation g{\o}r sig g{\ae}ldende for axiomatiske systemer: M{\ae}ngden af axiomer kan g{\o}res lille, men samtidig bliver systemet sv{\ae}rere at bruge.
Specifikt skal vi i denne rapport benytte induktion, og i induktionsskridtet bevise en implikation. Havde vi arbejdet i et andet system end PA, f.eks. naturlig deduktion (se [4]) ville fremgangsm{\aa}den havde v{\ae}ret oplagt: naturlig deduktion inkluderer en regel der direkte laver et bevis for "
begin math metavar var a end metavar infer metavar var b end metavar end math
end " om til et bevis for "
begin math metavar var a end metavar peano imply metavar var b end metavar end math
end ". Det ``tynde'' (men {\ae}kvivalente) axiomatiske system, har \emph{ikke} en s{\aa}dan regel, da det kan indses ved et meta-argument at ethvert bevis for "
begin math metavar var a end metavar infer metavar var b end metavar end math
end " kan transformeres til et bevis "
begin math metavar var a end metavar peano imply metavar var b end metavar end math
end " rent mekanisk. Mendelson gennemg{\aa}r argumentet i [3] s.37, og benytter derfra argumentet som ``Deduction theorem'' i teksten. Dette er en luksus vi ikke kan tillade os i et strengt formelt system som Logiweb. Alligevel er det oplagt at et bevis for "
begin math metavar var a end metavar peano imply metavar var b end metavar end math
end " b{\o}r basere sig p{\aa} beviset for "
begin math metavar var a end metavar infer metavar var b end metavar end math
end ", og derfor st{\aa}r vi overfor f{\o}lgende valg:
\begin{itemize}
\item[1.] Udfold beviset for "
begin math metavar var a end metavar infer metavar var b end metavar end math
end " i h{\aa}nden.
\item[2.] Implementer deduktionsalgoritmen i pyk.
\end{itemize}
1. er den oplagte mulighed. Det er nemt og velkendt, men det giver lange, ofte uoverskuelige, beviser i praksis. 2. blev frar{\aa}det os i forel{\ae}sningerne, og selvom det absolut ville v{\ae}re den mest elegante l{\o}sning er det formodentlig ogs{\aa} urealistisk givet vores erfaring med pyk og Logiweb-systemet. Men der er faktisk en l{\o}sning der kombiner begge l{\o}sningers styrker:
\begin{itemize}
\item[3.] Sv{\ae}k de benyttede lemmaer og arbejd \emph{bag} implikationspilen.
\end{itemize}
Hvad menes der s{\aa} med det? Jo, det er velkendt at vi kan sv{\ae}kke en vilk{\aa}rlig sand proposition med en vilk{\aa}rlig betingelse. Dette g{\ae}lder s{\aa}ledes ogs{\aa} for lemmaer uden pr{\ae}misser. Vi kan generalisere dette p{\aa} f{\o}lgende m{\aa}de: Givet et beviseligt lemma "
begin math metavar var d end metavar infer metavar var e end metavar end math
end " findes et tilsvarende \emph{hypotetisk} lemma "
begin math metavar var h end metavar peano imply metavar var d end metavar infer metavar var h end metavar peano imply metavar var e end metavar end math
end ". Den hypotetiske udgave af et lemma tillader os at springe implikationspilen over, s{\aa} at sige. Dette medf{\o}rer at givet hypotetiske versioner af de lemmaer og axiomer der indg{\aa}r i beviset for "
begin math metavar var a end metavar infer metavar var b end metavar end math
end ", s{\aa} kan vi trivielt overs{\ae}tte beviset til et bevis for "
begin math metavar var a end metavar peano imply metavar var b end metavar end math
end ". Den opm{\ae}rksomme l{\ae}ser vil indvende at dette reelt set er {\ae}kvivalent til at udfolde beviset, men med udfoldningen lagt ud i lemmaer. Dette er korrekt, men overser de motiverende faktorer:
\begin{itemize}
\item Hypotetiske lemmaer kan genbruges i andre beviser.
\item Det nye bevis har samme l{\ae}ngde og struktur som det originale bevis.
\end{itemize}
Disse faktorer er lovende nok til at vi har benyttet denne bevis strategi. Hypotetiske lemmaer vil fremover blive angivet med et s{\ae}nket ``h'', f.eks. er "
begin math hypothetical rule prime mp end math
end " den hypotetiske udgave af \emph{modus ponens}, dvs. et lemma der siger\\
\\
"
begin math define statement of hypothetical rule prime mp as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar infer metavar var h end metavar peano imply metavar var a end metavar infer metavar var h end metavar peano imply metavar var b end metavar end define end math
end "\\
\\
Denne definition er direkte taget fra siden [2], hvor lemmaet ogs{\aa} er bevist. Fra denne side tager vi ogs{\aa} lemmaet "
begin math hypothesize end math
end " der siger\\
\\
"
begin math define statement of hypothesize as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer metavar var h end metavar peano imply metavar var a end metavar end define end math
end "\\
\\
Normalt ville vi have kaldt et s{\aa}dant lemma for ``Weaken'' eller noget lignende, men med den ovenst{\aa}ende diskussion giver "
begin math hypothesize end math
end " bedre mening.
\subsection{Forkortende notation}
Ovenst{\aa}ende har vi gennemg{\aa}et hvorledes vi kan benytte argumentationen i et bevis for "
begin math metavar var a end metavar infer metavar var b end metavar end math
end " til at lave et bevis for "
begin math metavar var a end metavar peano imply metavar var b end metavar end math
end ". Det modsatte kan naturligvis ogs{\aa} lade sig g{\o}re, ved en simpel anvendelse af modus ponens. Et s{\aa}dant lemma vil vi kalde et \emph{regel}--lemma, og v{\ae}re indikere med et h{\ae}vet ``R'', f.eks. er "
begin math prop three two b rule end math
end " regel-udgaven af "
begin math prop three two b end math
end ". Vi vil benytter lemmaer der b{\aa}de er regel- og hypotetiske lemmaer. Dette skal forst{\aa}s som ``den hypotetiske udgave af regel-lemmaet''.
Derudover vil vi tillade os at l{\ae}gge instantiering af lemmaer med udtryk kvantiseret over Peano variable ud i seperate lemmaer. Dette vil blive noteret som lemmaet's navn efter fulgt at den konkrete variabel (i parentes) der instantieres med. Dette er n{\o}dvendigt da al-kvantoren for peano-variable, $\dot{\forall}$, \emph{ikke} er identisk med al-kvantoren for meta-variable, $\forall$, og bevischeckeren fra [1] ved ikke at al-kvantiserede PA udtryk kan instantieres. For at f{\aa} en konkret instantiering ud af et peano-kvatiseret udtryk skal vi derfor igennem lidt teknisk fifleri med axiom "
begin math axiom prime a four end math
end ", men dette er uinteressant for de beviser hvori instantiering bruges.
Endelig benytter vi lokale makro-definitioner i induktions-skridtet, for at komprimere det visuelle plads-forbrug: (N{\ae}sten) alt interessant forg{\aa}r bag implikations-pilen, s{\aa} en metavariabel reserveres til den f{\ae}lles pr{\ae}mis. Vi f{\o}lger eksemplet fra [2] og makrodefinerer desuden anvendelser "
begin math rule prime mp end math
end " og "
begin math hypothetical rule prime mp end math
end " med f{\o}lgende:
"
begin math define macro of var x hypothetical modus ponens var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x hypothetical modus ponens var y as hypothetical rule prime mp modus ponens var x modus ponens var y end define end quote end define end define end math
end "
"
begin math define macro of var x macro modus ponens var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x macro modus ponens var y as rule prime mp modus ponens var x modus ponens var y end define end quote end define end define end math
end "
Dette g{\o}res b{\aa}de af {\ae}stetiske hensyn, samt for at lette \emph{pyk}-kodningen.
V{\ae}rdien af den fremlagte strategi er {\aa}benlys n{\aa}r vi betragter de resulterende beviser (nedenfor): Intet bevis er l{\ae}ngere end 10 linier, og argumentationen er klart {\ae}kvivalent til Mendelsons.
\newpage
\section{Beviser}
Form\aa{}let med denne rapport er at bevise kommutativitet for addition\\ ("
begin math define pyk of prop three two h as text "prop three two h" end text end define end math
then math define tex of prop three two h as text "\mathit{Mendelson \; 3.2(h)}" end text end define end math
end "), som vist i [3], s.156-159.
\display{
"
begin math define statement of prop 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 "
}
Betragtes beviset i [3], ses det at vi ogs\aa{} har brug for f\o{}lgende lemmaer fra samme afsnit:\\
\\
"
begin math define pyk of prop three two a as text "prop three two a" end text end define end math
then math define tex of prop three two a as text "\mathit{Mendelson \; 3.2(a)}" end text end define end math
end ", "
begin math define pyk of prop three two b as text "prop three two b" end text end define end math
then math define tex of prop three two b as text "\mathit{Mendelson \; 3.2(b)}" end text end define end math
end ", "
begin math define pyk of prop three two c as text "prop three two c" end text end define end math
then math define tex of prop three two c as text "\mathit{Mendelson \; 3.2(c)}" end text end define end math
end ",\\"
begin math define pyk of prop three two d as text "prop three two d" end text end define end math
then math define tex of prop three two d as text "\mathit{Mendelson \; 3.2(d)}" end text end define end math
end ", "
begin math define pyk of prop three two f as text "prop three two f" end text end define end math
then math define tex of prop three two f as text "\mathit{Mendelson \; 3.2(f)}" end text end define end math
end " og "
begin math define pyk of prop three two g as text "prop three two g" end text end define end math
then math define tex of prop three two g as text "\mathit{Mendelson \; 3.2(g)}" end text end define end math
end ".\\
\\
For at g\o{}re beviserne overskuelige \ae{}ndres nogle af lemmaerne (og et enkelt axiom) til regellemmaer og/eller hypotetiske lemmaer samt specialisering til en konkret Peano varial. Notationen forklaret i afsnit 3 benyttes i alle tilf\ae{}lde. Se bilag A \& B for s\ae{}tninger og beviser for disse.
\subsection{Tautologier}
Der ses desuden at der er brug for to unavngivne tautologier, "
begin math define pyk of permute premises as text "permute premises" end text end define end math
then math define tex of permute premises as text "\mathit{Lemma \; 1}" end text end define end math
end " og "
begin math define pyk of no middle man as text "no middle man" end text end define end math
then math define tex of no middle man as text "\mathit{Lemma \; 2}" end text end define end math
end "
\subsubsection*{Bevis for "
begin math permute premises end math
end "}
\display{
"
begin math define statement of permute premises 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 "
}
"
begin math define proof of permute premises 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 hypothesize modus ponens metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar cut axiom prime a one conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar cut hypothetical rule prime mp modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar modus ponens metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var b end metavar conclude metavar var b end metavar peano imply metavar var a end metavar peano imply metavar var c end metavar end quote state proof state cache var c end expand end define end math
end "
\subsubsection*{Bevis for "
begin math no middle man end math
end "}
\display{
"
begin math define statement of no middle man as system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer metavar var a end metavar peano imply metavar var c end metavar end define end math
end "
}
"
begin math define proof of no middle man as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar peano imply metavar var b end metavar infer metavar var b end metavar peano imply metavar var c end metavar infer hypothesize modus ponens metavar var b end metavar peano imply metavar var c end metavar conclude metavar var a end metavar peano imply metavar var b end metavar peano imply metavar var c end metavar cut hypothetical 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 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 "
\subsection{Beviser for hovedlemmaer}
De tre f\o{}rste lemmaer udsiger at $\stackrel{p}{=}$ er en {\ae}kvivalensrelation. Bem{\ae}rk at hvor Mendelson rask v{\ae}k springer flere skridt over, og benytter uidentificerede tautologier, m{\aa} vi i Logiweb holde os strengt til reglerne for at vise korrekthed.
\subsubsection{Bevis for "
begin math prop three two a end math
end "}
\display{
"
begin math define statement of prop 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 "
}
"
begin math define proof of prop 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 rule prime mp 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 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 is metavar var t end metavar cut rule prime mp 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 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{Bevis for "
begin math prop three two b end math
end "}
\display{
"
begin math define statement of prop 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 "
}
"
begin math define proof of prop 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 permute premises 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 prop 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{Bevis for "
begin math prop three two c end math
end "}
\display{
"
begin math define statement of prop 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 "
}
"
begin math define proof of prop 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 prop 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 no middle man 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{Bevis for "
begin math prop three two d end math
end "}
\display{
"
begin math define statement of prop 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 "
}
"
begin math define proof of prop 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 prop 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 permute premises 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 prop 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 no middle man 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 permute premises 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 "
\\
\\
Hvis det ovenst{\aa}ende bevis samlignes med det givet i [3], ses det at Mendelson mangler den sidste linie, og har s{\aa}ledes ikke bevist det {\o}nskede! Selv en st{\ae}rk formel beskrivelse kan s{\aa}ledes falde igennem hvis den bliver checket af en bevis checker. Disse sm{\aa}, trivielle lemmaer viser med al {\o}nskelig t{\ae}nkelighed at automatiske bevis checkere er relevante, ogs{\aa} selvom de identificerede fejl er nemme at rette. Dette g{\ae}lder specielt i logik, der priser formalisme meget h{\o}jt.
\subsection{Induktive beviser for resterende hovedlemmaer}
De sidste tre lemmaer bevises ved induktion. Hvis vi ser p{\aa} axiom "
begin axiom prime s nine
end " ser vi at vi skal vise en implikation, for at vise induktionskridtet.
Bem{\ae}rk desuden at f,g,h bruger forskellige kvantorer!!!
\subsubsection{Bevis for "
begin math prop three two f end math
end " }
\display{
"
begin math define statement of prop 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 "
}
Vi splitter "
begin math prop three two f end math
end " i et basistil{\ae}lde "
begin math define pyk of prop three two f base as text "prop three two f base" end text end define end math
then math define tex of prop three two f base as text "\mathit{Mendelson\;3.2(f)_0}" end text end define end math
end ", og et induktionsskridt "
begin math define pyk of prop three two f ind as text "prop three two f ind" end text end define end math
then math define tex of prop three two f ind as text "\mathit{Mendelson\;3.2(f)_n}" end text end define end math
end ".
\subsubsection*{
"
begin math define statement of prop three two f base as system prime s infer peano zero peano is peano zero peano plus peano zero end define end math
end "
}
"
begin math define proof of prop three two f base 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 prop three two b rule modus ponens peano zero peano plus peano zero peano is peano zero conclude peano zero peano is peano zero peano plus peano zero end quote state proof state cache var c end expand end define end math
end "
\subsubsection*{
"
begin math define statement of prop three two f ind 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 peano imply var t peano var peano succ peano is peano zero peano plus var t peano var peano succ end define end math
end "
}
"
begin math define proof of prop three two f ind as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six hyp 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 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 prop three two d hyp rule 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 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 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 end quote state proof state cache var c end expand end define end math
end "
\subsubsection*{Induktionsbeviset for "
begin math prop three two f end math
end " }
"
begin math define proof of prop three two f as lambda var c dot lambda var x dot proof expand quote system prime s infer prop three two f base conclude peano zero peano is peano zero peano plus peano zero cut prop three two f ind 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 rule prime mp 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 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 peano imply peano all var t peano var indeed 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 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 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{Bevis for "
begin math prop three two g end math
end ".}
\display{
"
begin math define statement of prop three two g as system prime s infer peano all var r peano var indeed peano all var t peano var indeed 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 "
}
Ligesom med "
begin math prop three two f end math
end " splitter vi "
begin math prop three two g end math
end " i et basistil{\ae}lde "
begin math define pyk of prop three two g base as text "prop three two g base" end text end define end math
then math define tex of prop three two g base as text "\mathit{Mendelson\;3.2(g)_0}" end text end define end math
end ", og et induktionsskridt "
begin math define pyk of prop three two g ind as text "prop three two g ind" end text end define end math
then math define tex of prop three two g ind as text "\mathit{Mendelson\;3.2(g)_n}" end text end define end math
end ".
\subsubsection*{
"
begin math define statement of prop three two g base as system prime s infer var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ end define end math
end "
}
"
begin math define proof of prop three two g base as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s five conclude var r peano var peano succ peano plus peano zero peano is var r peano var peano succ cut axiom prime s five conclude var r peano var peano plus peano zero peano is var r peano var cut axiom prime s two conclude var r peano var peano plus peano zero peano is var r peano var peano imply var r peano var peano plus peano zero peano succ peano is var r peano var peano succ cut rule prime mp modus ponens var r peano var peano plus peano zero peano is var r peano var peano imply var r peano var peano plus peano zero peano succ peano is var r peano var peano succ modus ponens var r peano var peano plus peano zero peano is var r peano var conclude var r peano var peano plus peano zero peano succ peano is var r peano var peano succ cut prop three two d rule modus ponens var r peano var peano succ peano plus peano zero peano is var r peano var peano succ modus ponens var r peano var peano plus peano zero peano succ peano is var r peano var peano succ conclude var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ end quote state proof state cache var c end expand end define end math
end "
\subsubsection*{
"
begin math define statement of prop three two g ind as system prime s infer peano all var t peano var indeed 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 r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ end define end math
end "
}
"
begin math define proof of prop three two g ind as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six hyp 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 peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano succ cut axiom prime s two 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 peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut prop three two c hyp rule 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 peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano succ peano plus var t peano var peano succ 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 peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ 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 peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut axiom prime s six hyp 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 peano imply var r peano var peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ cut axiom prime s two conclude var r peano var peano plus var t 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 plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut no middle man 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 peano imply var r peano var peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ modus ponens var r peano var peano plus var t 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 plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ 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 peano imply var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut prop three two d hyp rule 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 peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ 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 peano imply var r peano var peano plus var t peano var peano succ peano succ peano is var r peano var peano plus var t peano var peano succ 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 peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut rule prime gen 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 peano imply var r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ conclude peano all var t peano var indeed 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 r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ end quote state proof state cache var c end expand end define end math
end "
\subsubsection*{Induktionsbeviset for "
begin math prop three two g end math
end "
}
"
begin math define proof of prop three two g as lambda var c dot lambda var x dot proof expand quote system prime s infer prop three two g base conclude var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ cut prop three two g ind conclude peano all var t peano var indeed 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 r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ cut axiom prime s nine conclude var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ peano imply peano all var t peano var indeed 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 r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply peano all var t peano var indeed 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 var r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ peano imply peano all var t peano var indeed 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 r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply peano all var t peano var indeed 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 r peano var peano succ peano plus peano zero peano is var r peano var peano plus peano zero peano succ conclude peano all var t peano var indeed 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 r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply peano all var t peano var indeed 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 t peano var indeed 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 r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ peano imply peano all var t peano var indeed 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 t peano var indeed 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 r peano var peano succ peano plus var t peano var peano succ peano is var r peano var peano plus var t peano var peano succ peano succ conclude peano all var t peano var indeed 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 gen modus ponens peano all var t peano var indeed 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 conclude peano all var r peano var indeed peano all var t peano var indeed 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{Bevis for "
begin math prop three two h end math
end ".}
\display{
"
begin math define statement of prop 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 "
}
Ligeledes opdeler vi "
begin math prop three two h end math
end " i et basistil{\ae}lde "
begin math define pyk of prop three two h base as text "prop three two h base" end text end define end math
then math define tex of prop three two h base as text "\mathit{Mendelson\;3.2(h)_0}" end text end define end math
end ", og et induktionsskridt "
begin math define pyk of prop three two h ind as text "prop three two h ind" end text end define end math
then math define tex of prop three two h ind as text "\mathit{Mendelson\;3.2(h)_n}" end text end define end math
end ".
\subsubsection*{
"
begin math define statement of prop three two h base as system prime s infer var t peano var peano plus peano zero peano is peano zero peano plus var t peano var end define end math
end "
}
"
begin math define proof of prop 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 prop three two f t conclude var t peano var peano is peano zero peano plus var t peano var cut prop three two c rule 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 end quote state proof state cache var c end expand end define end math
end "
\subsubsection*{
"
begin math define statement of prop three two h ind as system prime s infer 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 end define end math
end "
}
"
begin math define proof of prop three two h ind as lambda var c dot lambda var x dot proof expand quote system prime s infer axiom prime s six hyp 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 t peano var peano plus var r peano var peano succ cut prop three two g rt hyp 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 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 prop three two c hyp rule 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 t peano var peano plus var r 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 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 prop three two d hyp rule 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 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 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 end quote state proof state cache var c end expand end define end math
end "
\subsubsection*{Induktionsbeviset for "
begin math prop three two h end math
end " }
"
begin math define proof of prop three two h as lambda var c dot lambda var x dot proof expand quote system prime s infer prop three two h base conclude var t peano var peano plus peano zero peano is peano zero peano plus var t peano var cut prop three two h ind 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 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 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 "
\newpage
\appendix
\section{Regellemmaer og hypotetiske lemmaer}
\label{appendix a}
I det f\o{}lgende er flere af de eksisterende lemmaer og axiomer omskrevet til regellemmaer og/eller hypotetiske lemmaer. Dette g\o{}res for at de \o{}vrige beviser bliver kortere og ser mere overskuelige ud, som detaljeret i bevis-strategien.
\subsection{"
begin math axiom prime s six end math
end " som hypotetisk lemma}
"
begin math define pyk of axiom prime s six hyp as text "axiom prime s six hyp" end text end define end math
then math define tex of axiom prime s six hyp as text "S6'_h" end text end define end math
end " fungerer som "
begin math axiom prime s six end math
end " men har en betingelse "
begin math metavar var h end metavar end math
end ".
\subsubsection*{
"
begin math define statement of axiom prime s six hyp as system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var h end metavar peano imply metavar var a end metavar peano 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 end math
end "
}
"
begin math define proof of axiom prime s six hyp as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed axiom prime s six conclude 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 cut hypothesize modus ponens 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 conclude metavar var h end metavar peano imply 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 quote state proof state cache var c end expand end define end math
end "
\subsection{"
begin math prop three two b end math
end " som regellemma}
"
begin math define pyk of prop three two b rule as text "prop three two b rule" end text end define end math
then math define tex of prop three two b rule as text "\mathit{Mendelson \; 3.2(b)^R}" end text end define end math
end " er "
begin math prop three two b end math
end " som regellemma, dvs. med beting\-elsen som pr{\ae}mis.
\subsubsection*{
"
begin math define statement of prop three two b rule 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 infer metavar var r end metavar peano is metavar var t end metavar end define end math
end "
}
"
begin math define proof of prop three two b rule 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 metavar var t end metavar peano is metavar var r end metavar infer prop 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 rule prime mp 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 t end metavar peano is metavar var r end metavar conclude 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 "
\subsection{"
begin math prop three two c end math
end " som regellemma}
"
begin math define pyk of prop three two c rule as text "prop three two c rule" end text end define end math
then math define tex of prop three two c rule as text "\mathit{Mendelson \; 3.2(c)^R}" end text end define end math
end " er "
begin math prop three two c end math
end " men hvor betingelserne er pr{\ae}mis\-ser.
\subsubsection*{
"
begin math define statement of prop three two c rule 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 infer metavar var r end metavar peano is metavar var s end metavar infer metavar var t end metavar peano is metavar var s end metavar end define end math
end "
}
"
begin math define proof of prop three two c rule 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 metavar var t end metavar peano is metavar var r end metavar infer metavar var r end metavar peano is metavar var s end metavar infer prop three two c 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 cut rule prime mp 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 s 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 r end metavar conclude 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 rule prime mp modus ponens 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 modus ponens 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 end quote state proof state cache var c end expand end define end math
end "
\subsection{"
begin math prop three two c end math
end " som hypotetisk regellemma}
Lemma "
begin math define pyk of prop three two c hyp rule as text "prop three two c hyp rule" end text end define end math
then math define tex of prop three two c hyp rule as text "\mathit{Mendelson \; 3.2(c)_h^R}" end text end define end math
end " er "
begin math prop three two c end math
end " hvor betingelserne er \ae{}ndret til pr{\ae}misser og som derefter er sv\ae{}kkaet med en betingelse "
begin math metavar var h end metavar end math
end ".
\subsubsection*{
"
begin math define statement of prop three two c hyp rule as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar infer metavar var h end metavar peano imply metavar var t end metavar peano is metavar var s end metavar end define end math
end "
}
"
begin math define proof of prop three two c hyp rule as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar infer prop three two c 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 cut hypothesize 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 s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar conclude metavar var h 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 s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar cut hypothetical rule prime mp modus ponens metavar var h 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 s end metavar peano imply metavar var t end metavar peano is metavar var s end metavar modus ponens metavar var h end metavar peano imply metavar var t end metavar peano is metavar var r end metavar conclude metavar var h 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 hypothetical rule prime mp modus ponens metavar var h 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 modus ponens metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar conclude metavar var h 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 "
\subsection{"
begin math prop three two d end math
end " som regellemma}
"
begin math define pyk of prop three two d rule as text "prop three two d rule" end text end define end math
then math define tex of prop three two d rule as text "\mathit{Mendelson \; 3.2(d)^R}" end text end define end math
end " er "
begin math prop three two d end math
end " med betingelserne som pr{\ae}misser.
\subsubsection*{
"
begin math define statement of prop three two d rule 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 infer metavar var s end metavar peano is metavar var t end metavar infer metavar var r end metavar peano is metavar var s end metavar end define end math
end "
}
"
begin math define proof of prop three two d rule 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 metavar var r end metavar peano is metavar var t end metavar infer metavar var s end metavar peano is metavar var t end metavar infer prop three two d 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 cut rule prime mp modus ponens 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 modus ponens metavar var r end metavar peano is metavar var t 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 s end metavar cut rule prime mp 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 s end metavar modus ponens metavar var s end metavar peano is metavar var t end metavar conclude 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 "
\subsection{"
begin math prop three two d end math
end " som hypotetisk regellemma}
Lemma "
begin math define pyk of prop three two d hyp rule as text "prop three two d hyp rule" end text end define end math
then math define tex of prop three two d hyp rule as text "\mathit{Mendelson \; 3.2(d)_h^R}" end text end define end math
end " er "
begin math prop three two d end math
end " hvor betingelserne er \ae{}ndret til pr{\ae}misser og som derefter er sv\ae{}kkaet med en betingelse "
begin math metavar var h end metavar end math
end ".
\subsubsection*{
"
begin math define statement of prop three two d hyp rule as system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar infer metavar var h end metavar peano imply metavar var s end metavar peano is metavar var t end metavar infer metavar var h end metavar peano imply metavar var r end metavar peano is metavar var s end metavar end define end math
end "
}
"
begin math define proof of prop three two d hyp rule as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed all metavar var t end metavar indeed all metavar var r end metavar indeed all metavar var s end metavar indeed metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar infer metavar var h end metavar peano imply metavar var s end metavar peano is metavar var t end metavar infer prop three two d 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 cut hypothesize modus ponens 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 conclude metavar var h end metavar peano imply 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 cut hypothetical rule prime mp modus ponens metavar var h end metavar peano imply 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 modus ponens metavar var h end metavar peano imply metavar var r end metavar peano is metavar var t end metavar conclude metavar var h 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 cut hypothetical rule prime mp modus ponens metavar var h 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 modus ponens metavar var h end metavar peano imply metavar var s end metavar peano is metavar var t end metavar conclude metavar var h 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 "
\section{Specialicerede lemmaer}
\label{appendix b}
\subsection{"
begin math prop three two f end math
end " specialiseret}
Lemma "
begin math define pyk of prop three two f t as text "prop three two f t" end text end define end math
then math define tex of prop three two f t as text "\mathit{Mendelson \; 3.2(f)(\dot{t})}" end text end define end math
end " er "
begin math prop three two f end math
end " specialiseret til "
begin math var t peano var end math
end ".
\subsubsection*{
"
begin math define statement of prop three two f t as system prime s infer var t peano var peano is peano zero peano plus var t peano var end define end math
end "
}
"
begin math define proof of prop three two f t as lambda var c dot lambda var x dot proof expand quote system prime s infer prop 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 axiom prime a four at var t peano var 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 end quote state proof state cache var c end expand end define end math
end "
\subsection{"
begin math prop three two g end math
end " specialiseret og hypotiseret.}
Lemma "
begin math define pyk of prop three two g rt hyp as text "prop three two g rt hyp " end text end define end math
then math define tex of prop three two g rt hyp as text "\mathit{Mendelson \; 3.2(g)_h(\dot{r},\dot{t})}" end text end define end math
end " er "
begin math prop three two g end math
end " specialiseret til "
begin math var r peano var end math
end " og "
begin math var t peano var end math
end " og hypotiseret (med betingelsen "
begin math metavar var h end metavar end math
end ").
\subsubsection*{
"
begin math define statement of prop three two g rt hyp as system prime s infer all metavar var h end metavar indeed metavar var h end metavar 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 end define end math
end "
}
"
begin math define proof of prop three two g rt hyp as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed prop three two g conclude peano all var r peano var indeed peano all var t peano var indeed 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 a four at var r peano var conclude peano all var r peano var indeed peano all var t peano var indeed 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 peano all var t peano var indeed 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 r peano var indeed peano all var t peano var indeed 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 peano all var t peano var indeed 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 r peano var indeed peano all var t peano var indeed 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 conclude peano all var t peano var indeed 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 a four at var t peano var conclude peano all var t peano var indeed 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 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 t peano var indeed 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 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 t peano var indeed 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 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 hypothesize 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 conclude metavar var h end metavar 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 end quote state proof state cache var c end expand end define end math
end "
\newpage
\section{Litteraturliste}
[1] Klaus Grue, \emph{A Logiweb base page}, Juni 2005\newline
\footnotesize\verb+ http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/+\newline
\verb+ GRD-2005-06-22-UTC-06-58-05-413682/body/tex/page.pdf+\normalsize\newline
\newline
[2] Klaus Grue, \emph{Peano arithmetic}, Juni 2005\newline
\footnotesize\verb+ http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/+\newline
\verb+ GRD-2005-06-22-UTC-07-23-31-271829/body/tex/page.pdf+\normalsize\newline
\newline
[3] Elliott Mendelson, \textit{Introduction to Mathematical Logic, Fourth Edition},\\ Chapman \& Hall, 1997\newline
\newline
[4] Michael R. A. Huth \& Mark D. Ryan, \textit{Logic in Computer Science: Modelling and reasoning about systems}, Cambrige University Press, 2003
\end{document}
End of file
latex page
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,