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

\newcommand{\proves}{\ensuremath{\vdash}}
\newcommand{\nproves}{\ensuremath{\nvdash}}
\renewcommand{\models}{\ensuremath{\vDash}}
\newcommand{\nmodels}{\ensuremath{\nvDash}}

\title{Løsningsforslag oblig 1}

\date {\today}

\begin{document}
\maketitle{}

\section*{Oppgave 1}
\subsection*{a.}
\begin{displaymath}
\infer{\proves (A \rightarrow B) \rightarrow ((A \rightarrow (B \rightarrow C)) \rightarrow (A \rightarrow C))}
	{\infer{A \rightarrow B \proves ((A \rightarrow (B \rightarrow C)) \rightarrow (A \rightarrow C))}
		{\infer{A \rightarrow B, A \rightarrow (B \rightarrow C) \proves A \rightarrow C}
			{\infer{A \rightarrow B, A \rightarrow (B \rightarrow C), A \proves C}
				{\deduce{A \rightarrow (B \rightarrow C), A \proves A, C}
					{\times}
				&
				\infer{B, A \rightarrow (B \rightarrow C), A \proves C}
					{\deduce{B, A \proves A, C}
						{\times}
					&
					\infer{B, B \rightarrow C, A \proves C}
						{\deduce{B, A \proves B, C}
							{\times}
						&
						\deduce{B, C, A \proves C}
							{\times}
						}
					}
				}
			}
		}
	}
\end{displaymath}
Alle løvsekventer lukkes. Vi har et bevis.



\subsection*{b.}

\begin{displaymath}
\infer{ \proves (A \rightarrow B) \rightarrow ((A \rightarrow \neg B) \rightarrow \neg A)}
	{\infer{ A \rightarrow B \proves (A \rightarrow \neg B) \rightarrow \neg A}
		{\infer{ A \rightarrow B, A \rightarrow \neg B \proves  \neg A}
			{\infer{ A \rightarrow B, A \rightarrow \neg B, A \proves}
				{\deduce{ A \rightarrow \neg B, A \proves A}
					{\times}
				&
				\infer{ B, A \rightarrow \neg B, A \proves}
					{\deduce{ B, A \proves A}
						{\times}						
					&	
					\infer{ B, \neg B, A \proves}
						{\deduce{ B, A \proves B}
							{\times}
						}
					}
				}
			}
		}
	}
\end{displaymath}
Alle løvsekventer lukkes. Vi har et bevis.

\subsection*{c.}

\begin{displaymath}
\infer{ \proves (A \lor B) \rightarrow ((\neg A \land B) \lor (A \land \neg B))}
	{\infer{ A \lor B \proves (\neg A \land B) \lor (A \land \neg B)}
		{\infer{ A \lor B \proves \neg A \land B, A \land \neg B}
			{\infer{ A \proves \neg A \land B, A \land \neg B}
				{\infer{ A \proves \neg A, A \land \neg B}
					{\infer{ A, A \proves A \land \neg B}
						{\deduce{ A, A \proves A}
							{\times}
						&
						\infer{ A, A \proves \neg B}
							{\deduce{ A, A, B \proves}
								{\circ}
							}
						}
					}
					&
					\infer{ A \proves B, A \land \neg B}
						{\deduce{ A \proves B, A}
							{\times}
						&
						\infer{ A \proves B, \neg B}
							{\deduce{ A, B \proves B}
								{\times}
							}
						}
					}
				&
				\infer{ B \proves \neg A \land B, A \land \neg B}
					{\infer{ B \proves \neg A, A \land \neg B}
						{\infer{ B, A \proves A \land \neg B}
							{\deduce{ B, A \proves A}
								{\times}
							&
							\infer{ B, A \proves \neg B}
								{\deduce{ B, A, B \proves}
									{\circ}
								}
							}
						}
					&										
					\infer{ B \proves B, A \land \neg B}
						{\deduce{ B \proves B, A}
							{\times}
						&
						\infer{ B \proves B, \neg B}
							{\deduce{ B, B \proves B}
								{\times}
							}
						}
					}
				}
			}
		}
\end{displaymath}
Av de åpne løvsekventene ser vi at valuasjonen $v$ slik at $v(A) = v(B) = 1$ er en motmodell til rotsekventen.

\subsection*{d.}

\begin{displaymath}
\infer{ \proves (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow ((A \lor B) \rightarrow C))}
	{\infer{ A \rightarrow B \proves (B \rightarrow C) \rightarrow ((A \lor B) \rightarrow C)}
		{\infer{ A \rightarrow B, B \rightarrow C \proves (A \lor B) \rightarrow C}
			{\infer{ A \rightarrow B, B \rightarrow C, A \lor B \proves C}
				{\infer{ A \rightarrow B, A \lor B \proves C, B}
					{\infer{ A \rightarrow B, A \proves C, B}
						{\deduce{A \proves C, B, A}
							{\times}
						&
						\deduce{B, A \proves C, B}
							{\times}
						}
					&
					\deduce{ A \rightarrow B, B \proves C, B}
						{\times}
					}
				&
				\deduce{ A \rightarrow B, C, A \lor B \proves C}
					{\times}
				}
			}
		}
	}		
\end{displaymath}
Alle løvsekventer lukkes. Vi har et bevis.


\section*{Oppgave 2}
Bevis i to steg. Viser først at dersom $A$ er en tautologi, må sekventen $\proves A$ være gyldig ($\Rightarrow$)), deretter i motsatt retning ($\Leftarrow$)).

$\Rightarrow$) Anta at $A$ er en tautologi, $\models A$, dvs. $v(A) = 1$ for alle valuasjoner $v$. Alle valuasjoner oppfyller trivielt antecentenen i $\proves A$ siden denne mengden er tom, og siden alle valuasjoner oppfyller $A$ da $A$ er en tautologi, så oppfyller de minst en formel i succedenten av $\proves A$. $\proves A$ er gyldig.

$\Leftarrow$) Anta at $\proves A$ er gyldig. Siden alle valuasjoner oppfyller en tom mengde formler, oppfyller de antecendenten i $\proves A$. Siden $\proves A$ ved antagelse er gyldig må dermed alle valuasjoner oppfylle $A$. Da er $v(A)=1$ for alle $v$ og $A$ er en tautologi.

\section*{Oppgave 3}
En sannhetsverditabell er et semantisk argument.

\begin{displaymath}
\begin{array}{c|c||c|c}
A & \bot & \neg A & A \rightarrow \bot  \\ \hline
1 & 0	 &   0    & 0			\\
0 & 0	 &   1	  & 1			\\
\end{array}
\end{displaymath}
Vi ser av tabellen at $\neg A$ og $A \rightarrow \bot$ har like verdier i hver rad. Da vet vi at $v(\neg A) = v(A \rightarrow \bot)$ for alle valuasjoner $v$.

\section*{Oppgave 4}
\subsection*{a.}
Anta at premissene er gyldige. La $v$ være en valuasjon som oppfyller alle formlene i antecedenten av konklusjonen, dvs. alle formelene i $\Gamma$ og $A \lor B$. Målet er nå å vise at $v$ også oppfyller minst en formel i $\Delta$. Da har vi vist at enhver valuasjon som oppfyller antecedenten også oppfyller en formel i succedenten av konklusjonen---og konklusjonen må være gyldig.

Vi vet at $v$ oppfyller alle formelene i $\Gamma$ og at $v(A \lor B) = 1$. Ved definisjonen av en boolsk valuasjon vet vi da at $v(A) = 1$ eller $v(B) = 1$. Hvis $v$ oppfyller $A$, så har vi ved antakelsen om at venstre premiss er gyldig, at $v$ oppfyller en formel i $\Delta$. Hvis $v$ oppfyller $B$, så har vi ved antakelsen om at høyre premiss er gyldig, at $v$ oppfyller en formel i $\Delta$. I begge tilfeller får vi at en $v$ oppfyller en formel i $\Delta$, og vi er ferdige.

\subsection*{b.}
\emph{En sekventkalkyleregel er gyldighetsbevarende hvis og bare hvis regelen er falsifikasjonsbevarende.}

$\Rightarrow$) 
Anta at $v$ falsifiserer konklusjonen i en regel som er gyldighetsbevarende. Da kan ikke begge premissene være gyldige, for da må konklusjonen også være gyldig. Derfor er minst ett av premissene ikke gyldige, og da er minst et av premissene falsifiserbare.

$\Leftarrow$)
Anta at $v$ gjør alle premissene gyldige i en regel som er falsifikasjonsbevarende. Da kan ikke konklusjonen være falsifiserbar, for da ville et av premissene være falsifisert. Derfor er ikke konklusjonen falsifiserbar, men konklusjonen må være gyldig.

\section*{Oppgave 5}

\subsection*{a.}

\begin{itemize}
\item Anta at $\Gamma \proves \Delta$ er gyldig og at $\Gamma \cup \Delta^\bot$ er oppfyllbar. Da fins en valuasjon $v$ slik at $v \models A$
for alle $A\in \Gamma \cup \Delta^\bot$. Antakelsen (om at
$\Gamma \proves \Delta$ er gyldig) gir at det fins en formel $B \in
\Delta$ slik at $v \models B$. Men siden $\neg B \in \Delta^\bot$,
så må også $v \nmodels \neg B$. Motsigelse.

\item Anta at $\Gamma \cup \Delta^\bot$ ikke er oppfyllbar og for en vilkårlig valuasjon $v$ at $v \models A$ for alle $A \in \Gamma$. Antakelsen
(om at $\Gamma \cup \Delta^\bot$ ikke er oppfyllbar) gir at det fins en formel $B \in \Delta^\bot$ slik at $v \nmodels B$ (hvis ikke en slik $B$ fantes ville $\Gamma \cup \Delta^\bot$ være oppfyllbar). $B$ må være på formen $\neg C$ for en $C \in \Delta$ og $v \nmodels \neg C \Leftrightarrow v \models C$. Da er vi fremme, for vi har vist at alle modeller som gjør alle formlene i $\Gamma$ sanne må gjøre minst èn formel i $\Delta$ sann.
\end{itemize}

\subsection*{b.}
\begin{itemize}
\item Anta at $\Gamma \proves \Delta$  er gyldig og at det fins en valuasjon $v$ slik at $v \nmodels A$ for alle $A \in \Gamma^\bot \cup \Delta$. Denne modellen vil gjøre alle formlene i $\Gamma$ sanne, siden alle formler i $\Gamma^\bot$ er på formen $\neg B$ for $B \in \Gamma$ og     $v \models \neg B \Leftrightarrow v \models B$. Antakelsen gir at $v$ gjør minst èn formel i $\Delta$ sann, men vi har at $v \nmodels A$ for alle $A\in \Delta$. Motsigelse.

\item Anta at det ikke fins en modell $v$ slik at $v \nmodels A$ for alle $A \in \Gamma^\bot \cup \Delta$. Anta videre for en vilkårlig modell $v$ at $v \models A$ for alle $A \in \Gamma$. Denne valuasjonen gjør alle formlene i $\Gamma^\bot$ usanne. Antakelsen gir at det fins en formel $B \in \Delta$ slik at $v \models B$ (hvis ikke ville vi hatt en $v$ slik at $v \nmodels A$ for alle $A \in \Gamma^\bot \cup \Delta$). Men da har vi at $\Gamma \proves \Delta$  er gyldig.
    \end{itemize} 

\end{document}