\documentclass[a4paper, norsk, 11 pt]{article}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{babel, mathpple, textcomp, varioref, amsmath, amsfonts, amssymb, amsthm, proof, latexsym}

\newcommand{\seq}{\ensuremath{\vdash}}
\newcommand{\Ga}{\ensuremath{\Gamma}}
\newcommand{\De}{\ensuremath{\Delta}}
\newcommand{\AX }{{ AX} } 
\newcommand{\LT }{{ LW} } 
\newcommand{\RT }{{ RW} } 
\newcommand{\LW }{{ LW} } 
\newcommand{\LC }{{ LC} } 
\newcommand{\RC }{{ RC} } 
\newcommand{\Lneg }{{ L\neg }}
\newcommand{\imp}{\rightarrow}
\newcommand{\Lim}{L\imp}
\newcommand{\Rneg }{ { R\neg }}
\newcommand{\LBOT }{ { L\bot }}
\newcommand{\Land }{ { L\wedge   }}

\newcommand{\Rand }{ { R\wedge  }}

\newcommand{\Lor }{ { L\vee  }}
\newcommand{\Ror }{ { R\vee   }}

\newcommand{\Snitt }{\mbox{ Snitt} }

\newcommand{\lukket}[1]{\deduce{#1}{\times}}

\title{Løsningsforslag obligatorisk oppgave 2 \\ inf 3170 våren 2006}

\date {\today}

\begin{document}
\maketitle


\begin{tabular}{p{0.6\textwidth}p{0.32\textwidth}}
{\bf(1)} 
$$\infer[\Snitt]{\Ga,A\seq\De}{  
  \infer[\LW]{\Ga,A \seq\fbox{$\neg A$},\De}{\Ga\seq\neg A,\De} &
  \infer[\Lneg]{\Ga,A,\fbox{$\neg A$}\seq \De }{\lukket{\Ga ,A \seq A, \De }}
}$$ &
\vspace{2ex}
Snittformlene er merket med firkant.
\end{tabular}

\begin{tabular}{p{0.6\textwidth}p{0.32\textwidth}}
{\bf(2)} 
$$\infer[\Rneg]{ \Ga \seq \De ,\neg \neg A}{\infer[\Lneg]{\Ga, \neg A \seq \De}{\quad \Ga  \seq \De, A}}$$ &
\vspace{2ex} Denne er grei. Vi er ikke nødt til å bruke snitt her.
\end{tabular}

\begin{tabular}{p{0.6\textwidth}p{0.32\textwidth}}
{\bf(3)}
$$\infer[\Rneg]{\Ga\seq \neg (A \land B),\De} {\infer[\Land]{\Ga , A \land B \seq\De}
{\infer[(1)]{\Ga , A, B \seq \De} {\infer[(1)]{\Ga , A \seq\neg B ,\De}
{\quad \Ga \seq \neg A, \neg B, \De}}}}$$ &
\vspace{2ex} Her bruker vi den avledede regelen fra (1).
\end{tabular}


Uten bruk av de avledede reglene ville {\bf(3)} sett slik ut:

\[\infer[\Rneg]{\Ga \seq \neg (A \land B), \De}
{\infer[\Rand]{\Ga, A \land B \seq \De}
  {\infer[\Snitt]{\Ga, A, B \seq \De}
    {\infer[\LW]{\Ga, A, B \seq \fbox{$\neg B$}, \De }
      {\infer[\Snitt]{\Ga, A \seq \neg B,\De}
        {\infer[\LW]{\Ga, A \seq\fbox{$\neg A$},\neg B, \De}
          {\Ga \seq\neg A,\neg B,\De}
          &
          \infer[\Lneg]{\Ga, A,\fbox{$\neg A$}\seq \neg B,\De}
          {\lukket{\Ga, A \seq  A, \neg B,\De}}}}
      & \infer[\Lneg]{\Ga, A, B, \fbox{$\neg B$} \seq \De}
      {\lukket{\Ga, A, B \seq B, \De}}}}}
\]



{\bf(4)}
$$
\infer[\Snitt]{\Ga, A\imp B\seq\De}
	{\infer[\Ror]{\Ga, A\imp B\seq\fbox{$\neg A\lor B$},\De}
  		{\infer[\Rneg]{\Ga, A\imp B\seq\neg A, B,\De}
    			{\infer[\Lim]{\Ga, A\imp B, A\seq B,\De}
      				{\lukket{\Ga, A\seq A, B,\De}
        			&
        			\lukket{\Ga,A, B\seq B,\De}
        		}
        	}
        }
  &
  \infer[\LW]{\Ga,A\imp B,\fbox{$\neg A\lor B$}\seq\De}
  	{\Ga, \neg A\lor B \seq\De}
  }
$$ 

\end{document}