\documentclass [fleqn]{article}

\everymath{\rm}
\everydisplay{\rm}
\usepackage{latexsym}
\setlength {\overfullrule }{0mm}
\input{lgwinclude}
\usepackage[danish]{babel}
\usepackage{url}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=Logiweb sequent calculus}
\hypersetup{colorlinks=true}

% Save current \parindent (used by e.g. pyk display ... end display)
\newlength{\docparindent}
\setlength{\docparindent}{\parindent}

\newcommand{\liberalUrlBreak}[1]{{%
\mathcode`\/="202F%
\mathcode`\0="2030%
\mathcode`\1="2031%
\mathcode`\2="2032%
\mathcode`\3="2033%
\mathcode`\4="2034%
\mathcode`\5="2035%
\mathcode`\6="2036%
\mathcode`\7="2037%
\mathcode`\8="2038%
\mathcode`\9="2039%
\mathcode`\:="203A%
\mathcode`\A="2041%
\mathcode`\B="2042%
\mathcode`\C="2043%
\mathcode`\D="2044%
\mathcode`\E="2045%
\mathcode`\F="2046%
%\thinmuskip=0mu%
\medmuskip=0mu plus 2mu minus 0mu%
%\thickmuskip=0mu%
%\def\thinspace{\kern 0em}%
$#1$}}

\begin {document}
\title {projekt i logik}
\author {Maja Hanne T\o nnesen, Rune Kildetoft Andresen \\ \& Niels Peter Meyn Milthers}
\date {\today}
\maketitle
\tableofcontents





\begin{abstract}

\end{abstract}




\section{Introduction}\label{sec:Introduction}
In this paper we will prove the propositions regarding $
S$ starting with proposition $
Prop\ 3.2i$. continuing to 3.4, bevise 3.5,
%tilf\o je aksiomet %$ x < y <=> E z : z 0 \& z + x = y$, bevise 3.7, tilf\o je
aksiomer, der definerer x|y, bevise 3.10, og bevise 3.11.


We chose to prove chapter 3 from mendelson, starting with Lemma 3.2, since the first ten wfs' are proved in Mendelson, we will
start with Lemma 3.2.i.


\section{}


A modified version of Mendelsons system $
S$ (Peano arithmetic) \cite{mendelson} may be formulated thus:

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}

\item \makebox[0.45\textwidth][l]{$
[ \mathbf{Theory\ } 
S
]$}$
[ 
S
\mathbf{\ rule\ } 
MP
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
\Rightarrow {\cal B}
\vdash {\cal A}
\vdash {\cal B}
]$

\item \makebox[0.45\textwidth][l]{$
[ 
S
\mathbf{\ rule\ } 
Gen
\colon 
\Pi {\cal X}
,\linebreak [0] {\cal A}
\colon {\cal A}
\vdash 
\forall {\cal X}
\colon {\cal A}
]$}$
[ 
S
\mathbf{\ rule\ } 
Ded
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon 
Ded({\cal A}
,{\cal B}
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} {\cal A}
\vdash {\cal B}
]$

\item \makebox[0.45\textwidth][l]{}$
[ 
S
\mathbf{\ rule\ } 
S2
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
= {\cal B}
\vdash {\cal A}
{}'
= {\cal B}
{}'
]$

\item \makebox[0.45\textwidth][l]{$
[ 
S
\mathbf{\ rule\ } 
S3
\colon 
\Pi {\cal A}
\colon 
{\neg }
0
= {\cal A}
{}'
]$}$
[ 
S
\mathbf{\ rule\ } 
S4
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
{}'
= {\cal B}
{}'
\vdash {\cal A}
= {\cal B}
]$

\item \makebox[0.45\textwidth][l]{$
[ 
S
\mathbf{\ rule\ } 
S5
\colon 
\Pi {\cal A}
\colon {\cal A}
+ 
0
= {\cal A}
]$}$
[ 
S
\mathbf{\ rule\ } 
S6
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
+ {\cal B}
{}'
= 
({\cal A}
+ {\cal B}
)
{}'
]$

\item \makebox[0.45\textwidth][l]{$
[ 
S
\mathbf{\ rule\ } 
S7
\colon 
\Pi {\cal A}
\colon {\cal A}
\cdot 
0
= 
0
]$}$
[ 
S
\mathbf{\ rule\ } 
S8
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
\cdot 
({\cal B}
{}'
)
= 
({\cal A}
\cdot {\cal B}
)
+ {\cal A}
]$

\item $
[ 
S
\mathbf{\ rule\ } 
Neg
\colon 
\Pi {\cal A}
\colon 
\Pi {\cal B}
\colon 
{\neg }{\cal B}
\Rightarrow 
{\neg }{\cal A}
\vdash 
{\neg }{\cal B}
\Rightarrow {\cal A}
\vdash {\cal B}
]$

\item $
[ 
S
\mathbf{\ rule\ } 
S1
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A}
= {\cal B}
\vdash {\cal A}
= {\cal C}
\vdash {\cal B}
= {\cal C}
]$

\item $
[ 
S
\mathbf{\ rule\ } 
S9
\colon 
\Pi {\cal X}
,\linebreak [0] {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon 
\langle {\cal B}
{\equiv} {\cal A}
| {\cal X}
{:=} 
0
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle {\cal C}
{\equiv} {\cal A}
| {\cal X}
{:=} {\cal X}
{}'
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} {\cal B}
\vdash {\cal A}
\Rightarrow {\cal C}
\vdash {\cal A}
]$


\end{list}


\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}

\item $
[ 
S
\mathbf{\ rule\ } 
Prop\ 3.2a
\colon 
\Pi {\cal A}
\colon {\cal A}
= {\cal A}
]$

\item $
[ 
S
\mathbf{\ rule\ } 
Prop\ 3.2b
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
= {\cal B}
\vdash {\cal B}
= {\cal A}
]$

\item $
[ 
S
\mathbf{\ rule\ } 
Prop\ 3.2c
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A}
= {\cal B}
\vdash {\cal B}
= {\cal C}
\vdash {\cal A}
= {\cal C}
]$

\item $
[ 
S
\mathbf{\ rule\ } 
Prop\ 3.2d
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A}
= {\cal C}
\vdash {\cal B}
= {\cal C}
\vdash {\cal A}
= {\cal B}
]$

\item $
[ 
S
\mathbf{\ rule\ } 
Prop\ 3.2e
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A}
= {\cal B}
\vdash {\cal A}
+ {\cal C}
= {\cal B}
+ {\cal C}
]$

\item $
[ 
S
\mathbf{\ rule\ } 
Prop\ 3.2f
\colon 
\Pi {\cal A}
\colon {\cal A}
= 
0
+ {\cal A}
]$

\item $
[ 
S
\mathbf{\ rule\ } 
Prop\ 3.2g
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
{}'
+ {\cal B}
= 
({\cal A}
+ {\cal B}
)
{}'
]$

\item $
[ 
S
\mathbf{\ rule\ } 
Prop\ 3.2h
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
+ {\cal B}
= {\cal B}
+ {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.2i
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A}
= {\cal B}
\vdash {\cal C}
+ {\cal A}
= {\cal C}
+ {\cal B}
]$



\end{list}

we will start by  doing $
Prop\ 3.2i$

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item $
\if\relax\csname lgwprooflinep\endcsname
\def\lgwprooflinep{x}
\newcount\lgwproofline
\fi
\begingroup
\def\insideproof{x}
\lgwproofline=0 
S
\mathbf {\ proof\ of\ } 
Prop\ 3.2i
\colon 
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{${\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
$\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]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}$Block {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$Begin
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
${\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_d \else
\if \relax \csname lgwelld\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelld {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelld \fi 
$:}\makebox [0.4\textwidth ][l]{$Premise{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
${\cal A}
= {\cal B}
$\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]{$
\if \relax \csname lgwprooflinep\endcsname L_a \else
\if \relax \csname lgwella\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwella {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwella \fi 
$:}$
Prop\ 3.2e
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_d \else
\if \relax \csname lgwelld\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelld {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelld \fi 
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
${\cal A}
+ {\cal C}
= {\cal B}
+ {\cal C}
$\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]{$
\if \relax \csname lgwprooflinep\endcsname L_b \else
\if \relax \csname lgwellb\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellb {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellb \fi 
$:}$
Prop\ 3.2h
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
${\cal A}
+ {\cal C}
= {\cal C}
+ {\cal A}
$\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]{$
\if \relax \csname lgwprooflinep\endcsname L_c \else
\if \relax \csname lgwellc\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellc {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellc \fi 
$:}$
Prop\ 3.2h
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
${\cal B}
+ {\cal C}
= {\cal C}
+ {\cal B}
$\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]{$
\if \relax \csname lgwprooflinep\endcsname L_h \else
\if \relax \csname lgwellh\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellh {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellh \fi 
$:}$
S1
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_a \else
\if \relax \csname lgwella\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwella {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwella \fi 
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_b \else
\if \relax \csname lgwellb\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellb {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellb \fi 
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
${\cal B}
+ {\cal C}
= {\cal C}
+ {\cal A}
$\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]{$
\if \relax \csname lgwprooflinep\endcsname L_j \else
\if \relax \csname lgwellj\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellj {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellj \fi 
$:}$
Prop\ 3.2b
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_h \else
\if \relax \csname lgwellh\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellh {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellh \fi 
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
${\cal C}
+ {\cal A}
= {\cal B}
+ {\cal C}
$\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]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}$
Prop\ 3.2c
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_j \else
\if \relax \csname lgwellj\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellj {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellj \fi 
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_c \else
\if \relax \csname lgwellc\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellc {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellc \fi 
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
${\cal C}
+ {\cal A}
= {\cal C}
+ {\cal B}
$\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]{$
\if \relax \csname lgwprooflinep\endcsname L_g \else
\if \relax \csname lgwellg\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellg {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellg \fi 
$:}$Block {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$End
$\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]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}$
Ded
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_g \else
\if \relax \csname lgwellg\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellg {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellg \fi 
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{${\cal A}
= {\cal B}
\vdash {\cal C}
+ {\cal A}
= {\cal C}
+ {\cal B}
$\hfill \makebox [0mm][l]{\quad \makebox[0mm]{$\Box$}}}
\gdef\lgwella{\relax}
\gdef\lgwellb{\relax}
\gdef\lgwellc{\relax}
\gdef\lgwelld{\relax}
\gdef\lgwelle{\relax}
\gdef\lgwellf{\relax}
\gdef\lgwellg{\relax}
\gdef\lgwellh{\relax}
\gdef\lgwelli{\relax}
\gdef\lgwellj{\relax}
\gdef\lgwellk{\relax}
\gdef\lgwelll{\relax}
\gdef\lgwellm{\relax}
\gdef\lgwelln{\relax}
\gdef\lgwello{\relax}
\gdef\lgwellp{\relax}
\gdef\lgwellq{\relax}
\gdef\lgwellr{\relax}
\gdef\lgwells{\relax}
\gdef\lgwellt{\relax}
\gdef\lgwellu{\relax}
\gdef\lgwellv{\relax}
\gdef\lgwellw{\relax}
\gdef\lgwellx{\relax}
\gdef\lgwelly{\relax}
\gdef\lgwellz{\relax}
\gdef\lgwellbiga{\relax}
\gdef\lgwellbigb{\relax}
\gdef\lgwellbigc{\relax}
\gdef\lgwellbigd{\relax}
\gdef\lgwellbige{\relax}
\gdef\lgwellbigf{\relax}
\gdef\lgwellbigg{\relax}
\gdef\lgwellbigh{\relax}
\gdef\lgwellbigi{\relax}
\gdef\lgwellbigj{\relax}
\gdef\lgwellbigk{\relax}
\gdef\lgwellbigl{\relax}
\gdef\lgwellbigm{\relax}
\gdef\lgwellbign{\relax}
\gdef\lgwellbigo{\relax}
\gdef\lgwellbigp{\relax}
\gdef\lgwellbigq{\relax}
\gdef\lgwellbigr{\relax}
\gdef\lgwellbigs{\relax}
\gdef\lgwellbigt{\relax}
\gdef\lgwellbigu{\relax}
\gdef\lgwellbigv{\relax}
\gdef\lgwellbigw{\relax}
\gdef\lgwellbigx{\relax}
\gdef\lgwellbigy{\relax}
\gdef\lgwellbigz{\relax}
\endgroup $

\end{list}


%------------------------------------------------------------------------------
\bibliographystyle{alpha}
\bibliography{./page}
%------------------------------------------------------------------------------
\everymath{}
\everydisplay{}

\end{document}
