"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 intro hmpeano pyk "hmpeano" tex "HMpeano" end intro
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 meta x 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 meta t
end " & ::= "
begin peano zero
end " \;|\; "
begin meta t peano succ
end " \;|\; "
begin meta t peano plus meta t
end " \;|\; "
begin meta t peano times meta t
end " \;|\; "
begin meta x
end "\\
"
begin meta f
end " & ::= "
begin meta t peano is meta t
end " \;|\; "
begin peano not meta f
end " \;|\; "
begin meta f peano imply meta f
end " \;|\; "
begin peano all meta x indeed meta f
end "\\
"
begin meta x
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 peano a end math
end " til "
begin math peano z 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 theory system prime s end theory end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a one says all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a two says all meta a indeed all meta b indeed all meta c indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a three says all meta a indeed all meta b indeed parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a four says all meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub endorse peano all meta x indeed meta b peano imply meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime a five says all meta x indeed all meta a indeed all meta b indeed peano nonfree quote meta x end quote in quote meta a end quote end nonfree endorse peano all meta x indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply peano all meta x indeed meta b end rule end math
end "}
"
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 meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub end math
end " betyder at "
begin math meta a end math
end " er syntaktisk {\ae}kvivalent med "
begin math meta b end math
end " hvor alle frie forekomster af "
begin math meta x end math
end " er substitueret med "
begin math meta c end math
end ". "
begin math peano nonfree quote meta x end quote in quote meta a end quote end nonfree end math
end " betyder det oplagte: "
begin math meta a end math
end " indeholder ingen frie forekomster af "
begin math meta x 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 in theory system prime s rule rule prime mp says all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule rule prime gen says all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end rule end math
end "}
Disse er de velkendte inferensregler, \emph{modus ponens} og \emph{generalisering}.
\display{"
begin math in theory system prime s rule axiom prime s one says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s two says all meta a indeed all meta b indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s three says all meta a indeed not peano zero peano is meta a peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s four says all meta a indeed all meta b indeed meta a peano succ peano is meta b peano succ peano imply meta a peano is meta b end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s five says all meta a indeed meta a peano plus peano zero peano is meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s six says all meta a indeed all meta b indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s seven says all meta a indeed meta a peano times peano zero peano is peano zero end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s eight says all meta a indeed all meta b indeed meta a peano times parenthesis meta b peano succ end parenthesis peano is parenthesis meta a peano times meta b end parenthesis peano plus meta a end rule end math
end "}
\display{"
begin math in theory system prime s rule axiom prime s nine says all meta a indeed all meta b indeed all meta c indeed all meta x indeed macro newline peano sub meta b is meta a where meta x is peano zero end sub endorse peano sub meta c is meta a where meta x is meta x peano succ end sub endorse macro newline meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end rule end math
end "}
"
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 meta a infer meta b end math
end " om til et bevis for "
begin math meta a peano imply meta b 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 meta a infer meta b end math
end " kan transformeres til et bevis "
begin math meta a peano imply meta b 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 meta a peano imply meta b end math
end " b{\o}r basere sig p{\aa} beviset for "
begin math meta a infer meta b end math
end ", og derfor st{\aa}r vi overfor f{\o}lgende valg:
\begin{itemize}
\item[1.] Udfold beviset for "
begin math meta a infer meta b 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 meta d infer meta e end math
end " findes et tilsvarende \emph{hypotetisk} lemma "
begin math meta h peano imply meta d infer meta h peano imply meta e 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 meta a infer meta b end math
end ", s{\aa} kan vi trivielt overs{\ae}tte beviset til et bevis for "
begin math meta a peano imply meta b 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 in theory system prime s lemma hypothetical rule prime mp says all meta h indeed all meta a indeed all meta b indeed meta h peano imply meta a peano imply meta b infer meta h peano imply meta a infer meta h peano imply meta b end lemma 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 in theory system prime s lemma hypothesize says all meta h indeed all meta a indeed meta a infer meta h peano imply meta a end lemma 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 meta a infer meta b end math
end " til at lave et bevis for "
begin math meta a peano imply meta b 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 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 math
end "
"
begin math macro define var x macro modus ponens var y as rule prime mp modus ponens var x modus ponens var y end define end math
end "
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 intro prop three two h pyk "prop three two h" tex "\mathit{Mendelson \; 3.2(h)}" end intro
end "), som vist i [3], s.156-159.
\display{
"
begin math in theory system prime s lemma prop three two h says peano all peano t indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end lemma end math
end "
}
Betragtes beviset i [3], ses det at vi ogs\aa{} har brug for f\o{}lgende lemmaer fra samme afsnit:\\
\\
"
begin intro prop three two a pyk "prop three two a" tex "\mathit{Mendelson \; 3.2(a)}" end intro
end ", "
begin intro prop three two b pyk "prop three two b" tex "\mathit{Mendelson \; 3.2(b)}" end intro
end ", "
begin intro prop three two c pyk "prop three two c" tex "\mathit{Mendelson \; 3.2(c)}" end intro
end ",\\"
begin intro prop three two d pyk "prop three two d" tex "\mathit{Mendelson \; 3.2(d)}" end intro
end ", "
begin intro prop three two f pyk "prop three two f" tex "\mathit{Mendelson \; 3.2(f)}" end intro
end " og "
begin intro prop three two g pyk "prop three two g" tex "\mathit{Mendelson \; 3.2(g)}" end intro
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 intro permute premises pyk "permute premises" tex "\mathit{Lemma \; 1}" end intro
end " og "
begin intro no middle man pyk "no middle man" tex "\mathit{Lemma \; 2}" end intro
end "
\subsubsection*{Bevis for "
begin math permute premises end math
end "}
\display{
"
begin math in theory system prime s lemma permute premises says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b peano imply meta c infer meta b peano imply meta a peano imply meta c end lemma end math
end "
}
"
begin math system prime s proof of permute premises reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b peano imply meta c end line line ell b because axiom prime a two indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line line ell c because ell b macro modus ponens ell a indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line line ell d because hypothesize modus ponens ell c indeed meta b peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end line line ell e because axiom prime a one indeed meta b peano imply meta a peano imply meta b end line because ell d hypothetical modus ponens ell e indeed meta b peano imply meta a peano imply meta c qed end math
end "
\subsubsection*{Bevis for "
begin math no middle man end math
end "}
\display{
"
begin math in theory system prime s lemma no middle man says all meta a indeed all meta b indeed all meta c indeed meta a peano imply meta b infer meta b peano imply meta c infer meta a peano imply meta c end lemma end math
end "
}
"
begin math system prime s proof of no middle man reads arbitrary meta a end line arbitrary meta b end line arbitrary meta c end line line ell a premise meta a peano imply meta b end line line ell b premise meta b peano imply meta c end line line ell c because hypothesize modus ponens ell b indeed meta a peano imply meta b peano imply meta c end line because ell c hypothetical modus ponens ell a indeed meta a peano imply meta c qed 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 in theory system prime s lemma prop three two a says all meta t indeed meta t peano is meta t end lemma end math
end "
}
"
begin math system prime s proof of prop three two a reads arbitrary meta t end line line ell a because axiom prime s five indeed meta t peano plus peano zero peano is meta t end line line ell b because axiom prime s one indeed meta t peano plus peano zero peano is meta t peano imply macro newline meta t peano plus peano zero peano is meta t peano imply meta t peano is meta t end line line ell c because ell b macro modus ponens ell a indeed meta t peano plus peano zero peano is meta t peano imply meta t peano is meta t end line because ell c macro modus ponens ell a indeed meta t peano is meta t qed end math
end "
\subsubsection{Bevis for "
begin math prop three two b end math
end "}
\display{
"
begin math in theory system prime s lemma prop three two b says all meta t indeed all meta r indeed meta t peano is meta r peano imply meta r peano is meta t end lemma end math
end "
}
"
begin math system prime s proof of prop three two b reads arbitrary meta t end line arbitrary meta r end line line ell a because axiom prime s one indeed meta t peano is meta r peano imply meta t peano is meta t peano imply meta r peano is meta t end line line ell b because permute premises modus ponens ell a indeed meta t peano is meta t peano imply meta t peano is meta r peano imply meta r peano is meta t end line line ell c because prop three two a indeed meta t peano is meta t end line because ell b macro modus ponens ell c indeed meta t peano is meta r peano imply meta r peano is meta t qed end math
end "
\subsubsection{Bevis for "
begin math prop three two c end math
end "}
\display{
"
begin math in theory system prime s lemma prop three two c says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end lemma end math
end "
}
"
begin math system prime s proof of prop three two c reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because axiom prime s one indeed meta r peano is meta t peano imply meta r peano is meta s peano imply meta t peano is meta s end line line ell b because prop three two b indeed meta t peano is meta r peano imply meta r peano is meta t end line because no middle man modus ponens ell b modus ponens ell a indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s qed end math
end "
\subsubsection{Bevis for "
begin math prop three two d end math
end "}
\display{
"
begin math in theory system prime s lemma prop three two d says all meta t indeed all meta r indeed all meta s indeed meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s end lemma end math
end "
}
"
begin math system prime s proof of prop three two d reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a because prop three two c indeed meta r peano is meta t peano imply meta t peano is meta s peano imply meta r peano is meta s end line line ell b because permute premises modus ponens ell a indeed meta t peano is meta s peano imply meta r peano is meta t peano imply meta r peano is meta s end line line ell c because prop three two b indeed meta s peano is meta t peano imply meta t peano is meta s end line line ell d because no middle man modus ponens ell c modus ponens ell b indeed meta s peano is meta t peano imply meta r peano is meta t peano imply meta r peano is meta s end line because permute premises modus ponens ell d indeed meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s qed 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 in theory system prime s lemma prop three two f says peano all peano t indeed peano t peano is peano zero peano plus peano t end lemma end math
end "
}
Vi splitter "
begin math prop three two f end math
end " i et basistil{\ae}lde "
begin intro prop three two f base pyk "prop three two f base" tex "\mathit{Mendelson\;3.2(f)_0}" end intro
end ", og et induktionsskridt "
begin intro prop three two f ind pyk "prop three two f ind" tex "\mathit{Mendelson\;3.2(f)_n}" end intro
end ".
\subsubsection*{
"
begin math in theory system prime s lemma prop three two f base says peano zero peano is peano zero peano plus peano zero end lemma end math
end "
}
"
begin math system prime s proof of prop three two f base reads line ell a because axiom prime s five indeed peano zero peano plus peano zero peano is peano zero end line because prop three two b rule modus ponens ell a indeed peano zero peano is peano zero peano plus peano zero qed end math
end "
\subsubsection*{
"
begin math in theory system prime s lemma prop three two f ind says peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end lemma end math
end "
}
"
begin math system prime s proof of prop three two f ind reads locally define meta h as peano t peano is peano zero peano plus peano t end line line ell a because axiom prime s six hyp indeed meta h peano imply peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell b because axiom prime s two indeed meta h peano imply peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ end line line ell c because prop three two d hyp rule modus ponens ell b modus ponens ell a indeed meta h peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end line because rule prime gen modus ponens ell c indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis qed end math
end "
\subsubsection*{Induktionsbeviset for "
begin math prop three two f end math
end " }
"
begin math system prime s proof of prop three two f reads line ell a because prop three two f base indeed peano zero peano is peano zero peano plus peano zero end line line ell b because prop three two f ind indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis end line line ell c because axiom prime s nine indeed peano zero peano is peano zero peano plus peano zero peano imply macro newline peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis peano imply peano all peano t indeed peano t peano is peano zero peano plus peano t end line line ell d because ell c macro modus ponens ell a indeed peano all peano t indeed parenthesis peano t peano is peano zero peano plus peano t peano imply peano t peano succ peano is peano zero peano plus peano t peano succ end parenthesis peano imply peano all peano t indeed peano t peano is peano zero peano plus peano t end line because ell d macro modus ponens ell b indeed peano all peano t indeed peano t peano is peano zero peano plus peano t qed end math
end "
\subsubsection{Bevis for "
begin math prop three two g end math
end ".}
\display{
"
begin math in theory system prime s lemma prop three two g says peano all peano r indeed peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end lemma end math
end "
}
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 intro prop three two g base pyk "prop three two g base" tex "\mathit{Mendelson\;3.2(g)_0}" end intro
end ", og et induktionsskridt "
begin intro prop three two g ind pyk "prop three two g ind" tex "\mathit{Mendelson\;3.2(g)_n}" end intro
end ".
\subsubsection*{
"
begin math in theory system prime s lemma prop three two g base says peano r peano succ peano plus peano zero peano is parenthesis peano r peano plus peano zero end parenthesis peano succ end lemma end math
end "
}
"
begin math system prime s proof of prop three two g base reads line ell a because axiom prime s five indeed peano r peano succ peano plus peano zero peano is peano r peano succ end line line ell b because axiom prime s five indeed peano r peano plus peano zero peano is peano r end line line ell c because axiom prime s two indeed peano r peano plus peano zero peano is peano r peano imply parenthesis peano r peano plus peano zero end parenthesis peano succ peano is peano r peano succ end line line ell d because ell c macro modus ponens ell b indeed parenthesis peano r peano plus peano zero end parenthesis peano succ peano is peano r peano succ end line because prop three two d rule modus ponens ell a modus ponens ell d indeed peano r peano succ peano plus peano zero peano is parenthesis peano r peano plus peano zero end parenthesis peano succ qed end math
end "
\subsubsection*{
"
begin math in theory system prime s lemma prop three two g ind says peano all peano t indeed parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end parenthesis end lemma end math
end "
}
"
begin math system prime s proof of prop three two g ind reads locally define meta h as peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell a because axiom prime s six hyp indeed meta h peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano succ peano plus peano t end parenthesis peano succ end line line ell b because axiom prime s two indeed meta h peano imply parenthesis peano r peano succ peano plus peano t end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line line ell c because prop three two c hyp rule modus ponens ell a modus ponens ell b indeed meta h peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line line ell d because axiom prime s six hyp indeed meta h peano imply peano r peano plus peano t peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell e because axiom prime s two indeed peano r peano plus peano t peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply macro newline parenthesis peano r peano plus peano t peano succ end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line line ell f because no middle man modus ponens ell d modus ponens ell e indeed meta h peano imply parenthesis peano r peano plus peano t peano succ end parenthesis peano succ peano is parenthesis parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano succ end line line ell g because prop three two d hyp rule modus ponens ell c modus ponens ell f indeed meta h peano imply peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end line because rule prime gen modus ponens ell g indeed peano all peano t indeed parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply macro newline peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end parenthesis qed end math
end "
\subsubsection*{Induktionsbeviset for "
begin math prop three two g end math
end "
}
"
begin math system prime s proof of prop three two g reads line ell a because prop three two g base indeed peano r peano succ peano plus peano zero peano is parenthesis peano r peano plus peano zero end parenthesis peano succ end line line ell b because prop three two g ind indeed peano all peano t indeed parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply macro newline peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end parenthesis end line line ell c because axiom prime s nine indeed peano r peano succ peano plus peano zero peano is parenthesis peano r peano plus peano zero end parenthesis peano succ peano imply macro newline peano all peano t indeed parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply macro newline peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end parenthesis peano imply macro newline peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell d because ell c macro modus ponens ell a indeed peano all peano t indeed parenthesis peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply macro newline peano r peano succ peano plus peano t peano succ peano is parenthesis peano r peano plus peano t peano succ end parenthesis peano succ end parenthesis peano imply macro newline peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell e because ell d macro modus ponens ell b indeed peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line because rule prime gen modus ponens ell e indeed peano all peano r indeed peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ qed end math
end "
\subsubsection{Bevis for "
begin math prop three two h end math
end ".}
\display{
"
begin math in theory system prime s lemma prop three two h says peano all peano t indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end lemma end math
end "
}
Ligeledes opdeler vi "
begin math prop three two h end math
end " i et basistil{\ae}lde "
begin intro prop three two h base pyk "prop three two h base" tex "\mathit{Mendelson\;3.2(h)_0}" end intro
end ", og et induktionsskridt "
begin intro prop three two h ind pyk "prop three two h ind" tex "\mathit{Mendelson\;3.2(h)_n}" end intro
end ".
\subsubsection*{
"
begin math in theory system prime s lemma prop three two h base says peano t peano plus peano zero peano is peano zero peano plus peano t end lemma end math
end "
}
"
begin math system prime s proof of prop three two h base reads line ell a because axiom prime s five indeed peano t peano plus peano zero peano is peano t end line line ell b because prop three two f t indeed peano t peano is peano zero peano plus peano t end line because prop three two c rule modus ponens ell a modus ponens ell b indeed peano t peano plus peano zero peano is peano zero peano plus peano t qed end math
end "
\subsubsection*{
"
begin math in theory system prime s lemma prop three two h ind says peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end lemma end math
end "
}
"
begin math system prime s proof of prop three two h ind reads locally define meta h as peano t peano plus peano r peano is peano r peano plus peano t end line line ell a because axiom prime s six hyp indeed meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ end line line ell b because prop three two g rt hyp indeed meta h peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell c because axiom prime s two indeed meta h peano imply parenthesis peano t peano plus peano r end parenthesis peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell d because prop three two c hyp rule modus ponens ell a modus ponens ell c indeed meta h peano imply peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell e because prop three two d hyp rule modus ponens ell d modus ponens ell b indeed meta h peano imply peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end line because rule prime gen modus ponens ell e indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply macro newline peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis qed end math
end "
\subsubsection*{Induktionsbeviset for "
begin math prop three two h end math
end " }
"
begin math system prime s proof of prop three two h reads line ell a because prop three two h base indeed peano t peano plus peano zero peano is peano zero peano plus peano t end line line ell b because prop three two h ind indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply macro newline peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis end line line ell c because axiom prime s nine indeed peano t peano plus peano zero peano is peano zero peano plus peano t peano imply macro newline peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply macro newline peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis peano imply macro newline peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end line line ell d because ell c macro modus ponens ell a indeed peano all peano r indeed parenthesis peano t peano plus peano r peano is peano r peano plus peano t peano imply macro newline peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t end parenthesis peano imply macro newline peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end line line ell e because ell d macro modus ponens ell b indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t end line because rule prime gen modus ponens ell e indeed peano all peano t indeed peano all peano r indeed peano t peano plus peano r peano is peano r peano plus peano t qed end math
end "
\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 intro axiom prime s six hyp pyk "axiom prime s six hyp" tex "S6'_h" end intro
end " fungerer som "
begin math axiom prime s six end math
end " men har en betingelse "
begin math meta h end math
end ".
\subsubsection*{
"
begin math in theory system prime s lemma axiom prime s six hyp says all meta h indeed all meta a indeed all meta b indeed meta h peano imply meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end lemma end math
end "
}
"
begin math system prime s proof of axiom prime s six hyp reads arbitrary meta h end line arbitrary meta a end line arbitrary meta b end line line ell a because axiom prime s six indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end line because hypothesize modus ponens ell a indeed meta h peano imply meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ qed end math
end "
\subsection{"
begin math prop three two b end math
end " som regellemma}
"
begin intro prop three two b rule pyk "prop three two b rule" tex "\mathit{Mendelson \; 3.2(b)^R}" end intro
end " er "
begin math prop three two b end math
end " som regellemma, dvs. med beting\-elsen som pr{\ae}mis.
\subsubsection*{
"
begin math in theory system prime s lemma prop three two b rule says all meta t indeed all meta r indeed meta t peano is meta r infer meta r peano is meta t end lemma end math
end "
}
"
begin math system prime s proof of prop three two b rule reads arbitrary meta t end line arbitrary meta r end line line ell a premise meta t peano is meta r end line line ell b because prop three two b indeed meta t peano is meta r peano imply meta r peano is meta t end line because ell b macro modus ponens ell a indeed meta r peano is meta t qed end math
end "
\subsection{"
begin math prop three two c end math
end " som regellemma}
"
begin intro prop three two c rule pyk "prop three two c rule" tex "\mathit{Mendelson \; 3.2(c)^R}" end intro
end " er "
begin math prop three two c end math
end " men hvor betingelserne er pr{\ae}mis\-ser.
\subsubsection*{
"
begin math in theory system prime s lemma prop three two c rule says all meta t indeed all meta r indeed all meta s indeed meta t peano is meta r infer meta r peano is meta s infer meta t peano is meta s end lemma end math
end "
}
"
begin math system prime s proof of prop three two c rule reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta t peano is meta r end line line ell b premise meta r peano is meta s end line line ell c because prop three two c indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end line line ell d because ell c macro modus ponens ell a indeed meta r peano is meta s peano imply meta t peano is meta s end line because ell d macro modus ponens ell b indeed meta t peano is meta s qed end math
end "
\subsection{"
begin math prop three two c end math
end " som hypotetisk regellemma}
Lemma "
begin intro prop three two c hyp rule pyk "prop three two c hyp rule" tex "\mathit{Mendelson \; 3.2(c)_h^R}" end intro
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 meta h end math
end ".
\subsubsection*{
"
begin math in theory system prime s lemma prop three two c hyp rule says macro newline all meta h indeed all meta t indeed all meta r indeed all meta s indeed meta h peano imply meta t peano is meta r infer meta h peano imply meta r peano is meta s infer meta h peano imply meta t peano is meta s end lemma end math
end "
}
"
begin math system prime s proof of prop three two c hyp rule reads arbitrary meta h end line arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta h peano imply meta t peano is meta r end line line ell b premise meta h peano imply meta r peano is meta s end line line ell c because prop three two c indeed meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end line line ell d because hypothesize modus ponens ell c indeed meta h peano imply meta t peano is meta r peano imply meta r peano is meta s peano imply meta t peano is meta s end line line ell e because ell d hypothetical modus ponens ell a indeed meta h peano imply meta r peano is meta s peano imply meta t peano is meta s end line because ell e hypothetical modus ponens ell b indeed meta h peano imply meta t peano is meta s qed end math
end "
\subsection{"
begin math prop three two d end math
end " som regellemma}
"
begin intro prop three two d rule pyk "prop three two d rule" tex "\mathit{Mendelson \; 3.2(d)^R}" end intro
end " er "
begin math prop three two d end math
end " med betingelserne som pr{\ae}misser.
\subsubsection*{
"
begin math in theory system prime s lemma prop three two d rule says all meta t indeed all meta r indeed all meta s indeed meta r peano is meta t infer meta s peano is meta t infer meta r peano is meta s end lemma end math
end "
}
"
begin math system prime s proof of prop three two d rule reads arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta r peano is meta t end line line ell b premise meta s peano is meta t end line line ell c because prop three two d indeed meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s end line line ell d because ell c macro modus ponens ell a indeed meta s peano is meta t peano imply meta r peano is meta s end line because ell d macro modus ponens ell b indeed meta r peano is meta s qed end math
end "
\subsection{"
begin math prop three two d end math
end " som hypotetisk regellemma}
Lemma "
begin intro prop three two d hyp rule pyk "prop three two d hyp rule" tex "\mathit{Mendelson \; 3.2(d)_h^R}" end intro
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 meta h end math
end ".
\subsubsection*{
"
begin math in theory system prime s lemma prop three two d hyp rule says all meta h indeed all meta t indeed all meta r indeed all meta s indeed meta h peano imply meta r peano is meta t infer meta h peano imply meta s peano is meta t infer meta h peano imply meta r peano is meta s end lemma end math
end "
}
"
begin math system prime s proof of prop three two d hyp rule reads arbitrary meta h end line arbitrary meta t end line arbitrary meta r end line arbitrary meta s end line line ell a premise meta h peano imply meta r peano is meta t end line line ell b premise meta h peano imply meta s peano is meta t end line line ell c because prop three two d indeed meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s end line line ell d because hypothesize modus ponens ell c indeed meta h peano imply meta r peano is meta t peano imply meta s peano is meta t peano imply meta r peano is meta s end line line ell e because ell d hypothetical modus ponens ell a indeed meta h peano imply meta s peano is meta t peano imply meta r peano is meta s end line because ell e hypothetical modus ponens ell b indeed meta h peano imply meta r peano is meta s qed end math
end "
\section{Specialicerede lemmaer}
\label{appendix b}
\subsection{"
begin math prop three two f end math
end " specialiseret}
Lemma "
begin intro prop three two f t pyk "prop three two f t" tex "\mathit{Mendelson \; 3.2(f)(\dot{t})}" end intro
end " er "
begin math prop three two f end math
end " specialiseret til "
begin math peano t end math
end ".
\subsubsection*{
"
begin math in theory system prime s lemma prop three two f t says peano t peano is peano zero peano plus peano t end lemma end math
end "
}
"
begin math system prime s proof of prop three two f t reads line ell a because prop three two f indeed peano all peano t indeed peano t peano is peano zero peano plus peano t end line line ell b because axiom prime a four at peano t indeed peano all peano t indeed peano t peano is peano zero peano plus peano t peano imply peano t peano is peano zero peano plus peano t end line because ell b macro modus ponens ell a indeed peano t peano is peano zero peano plus peano t qed end math
end "
\subsection{"
begin math prop three two g end math
end " specialiseret og hypotiseret.}
Lemma "
begin intro prop three two g rt hyp pyk "prop three two g rt hyp " tex "\mathit{Mendelson \; 3.2(g)_h(\dot{r},\dot{t})}" end intro
end " er "
begin math prop three two g end math
end " specialiseret til "
begin math peano r end math
end " og "
begin math peano t end math
end " og hypotiseret (med betingelsen "
begin math meta h end math
end ").
\subsubsection*{
"
begin math in theory system prime s lemma prop three two g rt hyp says all meta h indeed meta h peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end lemma end math
end "
}
"
begin math system prime s proof of prop three two g rt hyp reads arbitrary meta h end line line ell a because prop three two g indeed peano all peano r indeed peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell b because axiom prime a four at peano r indeed peano all peano r indeed parenthesis peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis peano imply parenthesis peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end parenthesis end line line ell c because ell b macro modus ponens ell a indeed peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell d because axiom prime a four at peano t indeed peano all peano t indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line line ell e because ell d macro modus ponens ell c indeed peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ end line because hypothesize modus ponens ell e indeed meta h peano imply peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ qed 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,