\documentclass{book}

\usepackage[english]{babel}
\usepackage{amssymb,latexsym}
\usepackage[latin1]{inputenc}
\usepackage{dratex,aldratex}
\usepackage{ndplus}


\newtheorem{oppgave}{Oppgave}


\newenvironment{hint}{\bigskip\textbf{Hint: }\em}{   \bigskip}
\newenvironment{proof}{\bigskip\textbf{Proof: }}{$\blacksquare$\bigskip}

\newcommand{\prob}[1]
{\bigskip\noindent \fbox{
\begin{minipage}{11.5cm}
\begin{problem}
#1
\end{problem}
\end{minipage}
}\bigskip}

\newcommand{\tes}[2]
{\bigskip\noindent \fbox{
\begin{minipage}{11.5cm}
\begin{thesis}[#1]
#2
\end{thesis}
\end{minipage}
}\bigskip}

\newcommand{\defin}[1]
{\bigskip\noindent \fbox{
\begin{minipage}{11.5cm}
\begin{definition}
#1
\end{definition}
\end{minipage}
}\bigskip}

\newcommand{\backgr}[1]
{\bigskip\noindent \fbox{
\begin{minipage}{11.5cm}
\begin{background}
#1
\end{background}
\end{minipage}
}\bigskip}

\pagestyle{empty}

%\topmargin=-1cm
%\textheight=27cm

\begin{document}

\chapter*{Om premisser i bevis}

Indentering i beviser brukes for å skille ut det boken kaller {\it delbeviser (subproofs)}; det vil si at man for en stund gjør en ekstra antakelse og ser hvor den fører hen. Den ekstra premissen og formlene man får fra den står på linje under hverandre i beviset med samme indentering.  Avhengigheten av premisset kan fjernes ved bruk av den spesielle regelen CP.  At avhengigheten er borte, angis ved at den nye formelen ikke får samme indentering.

Av og til, og kanskje spesielt i forbindelse med kvantorregelen UG, kan det være nyttig å ha en mer eksplisitt oversikt over hvilke premisser de enkelte formlene i beviset avhenger av.  Bevisene på de neste sidene har fått en ekstra kolonne til høyre hvor vi holder greie på hvilke premisser formelen i hver linje avhenger av.  (Premissene identifiseres ved sine linjenumre.)

Reglene for hvilke premisser som skal oppgis i denne kolonnen er enkle:

\begin{itemize}
\item Premisser oppgir seg selv
\item Aksiomer oppgir ingenting
\item Hvis formelen i linje $n$ er avledet fra formelen i linje $m$ ved hjelp av en regel med nøyaktig en formel over streken, da skal $n$ oppgi de samme premissene som $m$ gjør.
\item Hvis formelen i linje $n$ er avledet fra formlene i linjene $k$ og ($\ldots$ og) $m$ ved bruk av en annen regel enn CP (eller IP), da skal $n$ oppgi summen (altså unionen) av premisser som er oppgitt i linjene $k$ og ($\ldots$ og) $m$.
\item Hvis  formelen i linje $n$  er avledet fra formlene i linjene $k$ (premiss) og $m$ ved hjelp av CP, da skal $n$ føre opp alle premissene som $m$ avhenger av, unntatt $k$.
\end{itemize}

Altså, hvis formelen i linje 20 er avledet fra formlene i linjene 10, 15 og 19 ved hjelp av CD, og linjene 10, 15 og 19 oppgir henholdsvis 1,2,5 og 2,5,11,14 og 19, da skal vi føre opp 1,2,5,11,14,19 i linje 20.

IP-regelen er spesiell på samme måte som CP.  Hvis den blir brukt, skal premisser tas vekk i høyre kolonne på tilsvarende måte.

På de neste sidene følger en del eksempler på beviser som har denne ekstra kolonnen til høyre.  Eksemplene er alle fra utsagnslogikk, men burde være illustrerende nok; formler avledet ved hjelp av kvantorreglene arver premisser på akkurat samme måte som gjennom de vanlige reglene i utsagnslogikk.

\section*{(1) $\ \ A\rightarrow A$}

\begin{equation*}
\begin{fitch}
\fa A & P & 1 \\
 A\rightarrow A & 1,1,CP &
\end{fitch}
\end{equation*}

\section*{(2) $\ \ A\land\neg A\rightarrow {\bf false}$}

\begin{equation*}
\begin{fitch}
\fa A\land\neg A & P & 1 \\
\fa  A & 1,Simp & 1 \\
\fa \neg A & 1,Simp & 1  \\
\fa {\bf false}\lor A & 2,Add & 1 \\
\fa {\bf false} & 4,3,DS & 1 \\
A\land\neg A\rightarrow {\bf false} & 1,5,CP & 
\end{fitch}
\end{equation*}




\section*{(3) $\ \  \neg\neg A\rightarrow A$}

\begin{equation*}
\begin{fitch}
\fa \neg\neg A & P & 1  \\
\fa  A\lor \neg A & XM&   \\
\fa A & 2,1,DS & 1 \\      
\neg\neg A\rightarrow A & 1,3,CP &
\end{fitch}
\end{equation*}



\section*{(4) $\ \  A\rightarrow \neg\neg A$}

\begin{equation*}
\begin{fitch}
\neg\neg A\rightarrow\neg\neg A & T fra (1) over & \\
A\land\neg A\rightarrow {\bf false} & T fra (2) over & \\
\fa  A & P  & 3 \\
\fa \fa \neg A & P & 4 \\
\fa \fa A\land \neg A & 3,4,Conj & 3,4  \\
\fa \fa {\bf false} & 2,5,MP & 3,4  \\
\fa \fa \neg \neg A & 6,FE & 3,4  \\
\fa \neg A\rightarrow \neg\neg A & 4,7,CP & 3  \\
\fa \neg A\lor \neg \neg A & XM  & \\
\fa \neg \neg A\lor \neg\neg A & 9,8,1,CD & 3  \\
\fa \neg\neg A & 10,Contr & 3  \\
A\rightarrow\neg\neg A& 3,11,CP  &
\end{fitch}
\end{equation*}


\section*{Flere beviser}

\begin{equation*}
\begin{fitch}
\fa  A\rightarrow B & P   & 1  \\
\fa \fa \neg A\rightarrow B & P & 2 \\
\fa \fa A\lor  \neg A & XM & \\
\fa \fa B\lor B & 3,1,2 CD & 1,2\\
\fa \fa B  & 4,Contr & 1,2\\
\fa (\neg A\rightarrow B)\rightarrow B & 2,5,CP & 1\\
(A\rightarrow B)\rightarrow ((\neg A\rightarrow B)\rightarrow B) & 1,6,CP & 
\end{fitch}
\end{equation*}

\vskip 30pt

\begin{equation*}
\begin{fitch}
\fa  A & P & 1 \\
\fa \fa B & P & 2\\
\fa \fa A\land B   & 1,2,Conj & 1,2 \\
\fa  B\rightarrow (A\land B) & 2,3  CP & 1 \\
A\rightarrow (B\rightarrow (A\land B)) & 1,4,CP &
\end{fitch}
\end{equation*}

\vskip 30pt

\begin{equation*}
\begin{fitch}
\fa  A\land B & P  & 1\\
\fa A & 1,Simp & 1\\
 A\land B  \rightarrow A & 1,2,CP & \\
\fa \neg A & P & 2 \\
\fa \neg (A\land B) & 3,4,MT & 2 \\
\neg A\rightarrow \neg (A\land B) & 1,5,CP &
\end{fitch}
\end{equation*}

\vskip 30pt

\begin{equation*}
\begin{fitch}
\fa  A\land B & P  & 1\\
\fa B & 1,Simp & 1\\
 A\land B  \rightarrow B & 1,2,CP & \\
\fa \neg B & P & 4\\
\fa \neg (A\land B) & 3,4,MT & 4\\
\neg B\rightarrow \neg (A\land B) & 1,5,CP &
\end{fitch}
\end{equation*}

\vskip 30pt

\begin{equation*}
\begin{fitch}
  {\bf true} & TI & 
\end{fitch}
\end{equation*}

\vskip 30pt

\begin{equation*}
\begin{fitch}
\neg {\bf false} \rightarrow\neg {\bf false} & T fra (1) over & \\
\fa  {\bf false} & P  & 2\\
\fa \neg {\bf false} & 2,FE & 2\\
{\bf false}\rightarrow \neg {\bf false} & 2,3,CP & \\
{\bf false}\lor \neg {\bf false} & XM & \\
\neg {\bf false} \lor \neg {\bf false} & 5,4,1,CD & \\
\neg {\bf false} & 6,Contr  & 
\end{fitch}
\end{equation*}

\vskip 30pt

\begin{equation*}
\begin{fitch}
A\land\neg A\rightarrow {\bf false} & T fra (2) over & \\
\fa  \neg A & P  & 2\\
\fa \fa  A & P & 3 \\
\fa \fa A\land \neg A & 3,2,Conj & 2,3 \\
\fa \fa {\bf false} & 1,4,MP & 2,3 \\
\fa \fa B & 5,FE & 2,3\\
\fa  A\rightarrow B & 3,6,CP & 2\\
 \neg A\rightarrow (A\rightarrow B) & 2,7,CP &
\end{fitch}
\end{equation*}

\vskip 30pt


\begin{equation*}
\begin{fitch}
\fa   B & P  & 1\\
\fa \fa  A & P & 2\\
\fa \fa B\lor B & 1,Add & 1\\
\fa \fa  B & 3,Contr & 1\\
\fa  A\rightarrow B & 2,4,CP & 1\\
B\rightarrow (A\rightarrow B) & 1,5,CP &
\end{fitch}
\end{equation*}


\vskip 30pt


\begin{equation*}
\begin{fitch}
\fa A & P & 1\\
\fa \fa  A\rightarrow B & P  & 2\\
\fa \fa  B & MP & 1,2\\
\fa  (A\rightarrow B)\rightarrow B & 2,3,CP & 1\\
\fa \fa \neg B  & P & 5\\
\fa \fa \neg (A\rightarrow B) & 4,5,MT & 1,5\\
\fa \neg B\rightarrow \neg (A\rightarrow B) & 5,6,CP & 1\\
A\rightarrow (\neg B\rightarrow \neg (A\rightarrow B)) & 1,7,CP &
\end{fitch}
\end{equation*}


\vskip 30pt


\begin{equation*}
\begin{fitch}
\fa   A & P & 1 \\
\fa   A\lor B & 1,Add & 1\\
A\rightarrow (A\lor B) & 1,2,CP &
\end{fitch}
\end{equation*}

\vskip 30pt


\begin{equation*}
\begin{fitch}
\fa   B & P  & 1\\
\fa   A\lor B & 1,Add & 1\\
B\rightarrow (A\lor B) & 1,2,CP &
\end{fitch}
\end{equation*}

\vskip30pt

\begin{equation*}
\begin{fitch}
\fa \neg A & P & 1\\
\fa \fa  A\lor B & P & 2 \\
\fa \fa  B & 2,1,DS & 1,2\\
\fa  (A\lor B)\rightarrow B & 2,3,CP & 1\\
\fa \fa \neg B  & P & 5\\
\fa \fa \neg (A\lor B) & 4,5,MT & 1,5\\
\fa \neg B\rightarrow \neg (A\lor B) & 5,6,CP & 1\\
\neg A\rightarrow (\neg B\rightarrow \neg (A\lor B)) & 1,7,CP &
\end{fitch}
\end{equation*}


\vskip 30pt



\end{document}

