\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