\documentclass[12pt]{book}



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

\textheight=28cm
\textwidth=18cm

\pagestyle{empty}

\topmargin=-2.5cm
\leftmargin=-5cm
\oddsidemargin=-1cm
\evensidemargin=-1cm

\begin{document}



\centerline{\huge\bf ND1750PRED} 

\vspace{1cm}

\centerline{\large\bf 
består av reglene/aksiomene i ND1750 pluss følgende}

\vspace{1cm}

\noindent 
\begin{tabular}{|c|c|c|} \hline
\begin{minipage}{2.4in}\vspace*{5pt} \hspace{1cm} {\bf Regel} \vspace*{5pt}\end{minipage} & 
\begin{minipage}{1.4in}\vspace*{5pt} \hspace{1cm} {\bf Mønster} \vspace*{5pt}\end{minipage} & 
\begin{minipage}{2.8in}\vspace*{5pt} \hspace{1cm} {\bf Betingelser} \vspace*{5pt}\end{minipage} 
\\ \hline 
Universell instansiering (UI) & 
$\displaystyle \frac{\forall x\ W}{\displaystyle \therefore W(x/t)}$ & 
\begin{minipage}{2.4in} \vskip 10pt  $x$ har ingen fri forekomst i $W$ innenfor skopet til en kvantor som binder en variabel i $t$. \vspace*{10pt}  \end{minipage} \\ \hline 
Eksistensiell generalisering (EG) & 
$\frac{\displaystyle W(x/t)}{\displaystyle \therefore   \exists x\ W} $ & 
\begin{minipage}{2.4in} \vskip 10pt  $x$ har ingen fri forekomst i $W$ innenfor skopet til en kvantor som binder en variabel i $t$.\vspace*{10pt}    \end{minipage}
\\ \hline
Eksistensiell instansiering (EI) & 
$\frac{\displaystyle \exists x\ W}{\displaystyle \therefore W(x/c)}$ & 
\begin{minipage}{2.4in} \vskip 10pt  $c$ er en konstant som til nå ikke har vært brukt i beviset\vspace{8pt} \\ 
$c$ forekommer ikke i konklusjonen (det vil si siste linje av beviset) \vspace*{10pt}     \end{minipage}   \\ \hline
Universiell generalisering (UG) & 
$\frac{\displaystyle W}{\displaystyle \therefore   \forall x\ W} $ & \begin{minipage}{2.4in}\vskip 10pt  
$x$ er ikke fri i noen premiss som $W$ avhegner av \vspace{8pt} \\ 
$W$ inneholder ikke noen konstant innført ved bruk av EI på en formel der $x$ er fri \vspace*{10pt}   
\end{minipage} \\
\hline
\end{tabular}

\vspace{1cm}

\hspace{1cm}

\noindent {\bf Eksempel:} La  $a$ og $b$ være konstanter mens $x,y,z,v,w$ er variabler, og la videre $W$ og $t$ være $$\forall z\ (P(z) \rightarrow \exists w\ (R(z,w)\land R(z,x) \land \forall y\ R(y,w)\land \forall x\ R(w,x)))\ \ \ \  {\rm og}\ \ \ \ 
f(a,g(y,f(b,v),f(y,v))).$$  

Betingelsen i de to første reglene kan leses slik:

\begin{enumerate}
\item  Finn alle kvantorer i $W$ som har skop som inneholder frie forekomster av $x$. (Vi får i dette tilfellet $\forall z$ og  $\exists w$.)  Finn mengden av variabler som brukes i disse kvantorene.  (Vi får i dette tilfellet $\{ z,w\}$.)
\item Finn mengden av variabler som forekommer i $t$.  (Vi får i dette tilfellet  $\{ y,v\}$.)
\item Kontroller at de to mengdene ikke har felles elementer. (OK i dette tilfellet.)
\end{enumerate}





\vfil\break

\centerline{\huge Et lovlig bevis} 


\vspace{1cm}

\centerline{\large\bf 
(Siste kolonne angir hvilke premisser hver linje avhenger av.)}

\vspace{1cm}


\begin{equation*}
\begin{fitch}
\fa  \forall x\ \forall y\ (R(x,y)\rightarrow R(y,x)) & P & 1\\
\fa  \forall y (R(x,y)\rightarrow R(y,x)) & 1,UI & 1\\
\fa \fa \exists y\ R(x,y) & P & 3\\
\fa \fa R(x,c) & 3,EI & 3 \\
\fa \fa R(x,c)\rightarrow R(c,x) & 2,UI & 1\\
\fa \fa R(c,x) & 4,5,MP & 1,3 \\
\fa \fa \exists y\ R(y,x) & 6,EG & 1,3\\
\fa \exists y\ R(x,y) \rightarrow \exists y\ R(y,x) & 3,7,CP & 1\\
\fa \forall x(\exists y\ R(x,y) \rightarrow \exists y\ R(y,x)) & 8,UG & 1\\
\forall x\ \forall y\ (R(x,y)\rightarrow R(y,x)) \rightarrow \forall x(\exists y\ R(x,y) \rightarrow \exists y\ R(y,x)) & 1,9,CP 
\end{fitch}
\end{equation*}

\vspace{1cm}

Alle betingelser er oppfylt:

\vspace{.5cm}

\begin{itemize}
\item UI i linje 2 er OK.  (Mengdene for ``$W$'' og ``$t$'' er her $\{ y\}$ og $\{ x\}$, som ikke har felles elementer.)
\item EI i linje 4 er OK fordi $c$ ikke forekommer før linje 4, og fordi $c$ ikke forekommer i linje 10.
\item UI i linje 5 er OK.  (Mengdene for ``$W$'' og ``$t$'' er i dette tilfellet begge tomme, og har derfor selvsagt ikke felles elementer.)
\item EG i linje 7 er OK.  (Også her er mengdene for ``$W$'' og ``$t$'' begge tomme.)
\item UG i linje 9 er OK, siden $x$ ikke forekommer fri i linje 1 (det vil si premisset som 8 avhenger av) {\bf og} fordi linje 8 ikke inneholder noen konstant innført ved hjelp av EI.\\  {\bf (Men OBS:  Denne anvendelsen av UG er ikke OK slik boken har formulert det.  Det bryr vi oss ikke om---boken tar feil.)}
\end{itemize}



\vfil\break

\centerline{\huge Noen ulovlige bevis} 

\vspace{1cm}



\begin{tabular}{l|p{6cm}}
\begin{minipage}{10cm}
\begin{equation*}
\begin{fitch}
\fa \forall x\ \exists y\ x<y & P & 1\\
\fa \exists y \ y<y & 1,UI & 1 
\end{fitch}
\end{equation*}
\vspace*{12pt}
\end{minipage} & Ulovlig bruk av UI i linje 2: For $x$ settes inn $y$, som ``fanges inn'' av $\exists y$. \\ \hline
\begin{minipage}{10cm}
\vspace{12pt}
\begin{equation*}
\begin{fitch}
\fa \forall  y\ y\leq y & P & 1\\
\fa \exists x\ \forall y\  y\leq x & 1,EG & 1 \\
\end{fitch}
\end{equation*}
\vspace*{12pt}

\end{minipage} & Ulovlig bruk av EG i linje 2:
Formelen i linje 1 svarer til at vi for $x$ har satt inn $y$, som ``fanges inn'' av $\forall y$. \\ \hline
\begin{minipage}{10cm}
\vspace{12pt}

\begin{equation*}
\begin{fitch}
\fa \exists x\ P(x) \land \exists y\ R(y) & P & 1\\
\fa \exists x\ P(x) & 1,Simp & 1\\
\fa \exists y\ R(y) & 1,Simp & 1\\
\fa R(c) & 3,EI & 1\\
\fa P(c) & 2,EI & 1\\
\fa P(c)\land R(c) &4,5,Conj & 1\\
\fa \exists x\ (P(x)\land R(x)) & 6, EG & 1\\
\end{fitch}
\end{equation*}
\vspace*{12pt}

\end{minipage} & 
Ulovlig bruk av EI i linje 5: Konstanten $c$ forekommer ovenfor. \\ \hline
\begin{minipage}{10cm}
\vspace{12pt}

\begin{equation*}
\begin{fitch}
\fa \exists x\ P(x)  & P & 1 \\
\fa P(c) & 1,EI & 1\\
 \exists x\ P(x)\rightarrow P(c) & 1,2,CP \\
\end{fitch}
\end{equation*}
\vspace*{12pt}


\end{minipage} & 
Ulovlig bruk av EI: Konstanten $c$ forkommer i konklusjonen, det vil si linje 3.\\ \hline
\begin{minipage}{10cm}
\vspace{12pt}

\begin{equation*}
\begin{fitch}
\fa P(x) & P & 1\\
\fa  P(x)\lor R(x) & 1,Add & 1\\
\fa  \forall x\ (P(x)\lor R(x)) & 2,UG & 1 \\
P(x)\rightarrow \forall x\ (P(x)\lor R(x)) & 1,3,CP \\
\end{fitch}
\end{equation*}
\vspace*{12pt}

\end{minipage} & 
Ulovlig bruk av UG i linje 3:  $x$ er fri i premisset 1, som linje 2 (og 3) avhenger av. \\ \hline
\begin{minipage}{10cm}
\vspace{12pt}

\begin{equation*}
\begin{fitch}
\fa \forall x\ \exists y\ R(x,y)  & P & 1 \\
\fa  \exists y\ R(x,y)  & 1,UI & 1 \\
\fa   R(x,c)  & 2,EI & 1 \\
\fa  \forall x\ R(x,c)  & 3,UG & 1 \\
\fa  \exists y\ \forall x\ R(x,y)  & 4,EG & 1 \\
\end{fitch}
\end{equation*}
\vspace*{12pt}

\end{minipage} & 
Ulovlig bruk av UG i linje 4: Linje 3 inneholder konstanten $c$, som ble innf?rt  ved EI i en formel der $x$ er fri.
\end{tabular}






\end{document}

