Intuitionistic Logic

Soundness and Completeness

content/intuitionistic-logic/soundness-completeness/soundness-completeness.tex

% part: intuitionistic-logic% chapter: soundness-completeness\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{int}{sc}{Soundness and Completeness}\begin{editorial}  This chapter collects soundness and completeness results for  propositional intuitionistic logic. It needs an introduction. The  completeness proof makes use of facts about provability that should  be stated and proved explicitly somewhere.\end{editorial}\olimport{soundness-axd}\olimport{soundness-nd}\olimport{lindenbaum}\olimport{canonical-model}\olimport{truth-lemma}\olimport{completeness-thm}\olimport{decidability}\OLEndChapterHook\end{document}

content/intuitionistic-logic/soundness-completeness/soundness-axd.tex

% part: intuitionistic-logic% chapter: soundness-completeness% section: soundness-axd\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sc}{sax}\olsection{Soundness of Axiomatic \usetoken{P}{derivation}}\begin{editorial}  The soundness proof relies on the fact that all axioms are  intuitionistically valid; this still needs to be proved, e.g., in  the Semantics chapter.\end{editorial}\begin{thm}[Soundness]  \ollabel{thm:soundness}  If $\Gamma \Proves !A$, then $ \Gamma \Entails !A$.\end{thm}\begin{proof}  We prove that if $\Gamma \Proves !A$, then $\Gamma \Entails !A$.  The proof is by induction on the number~$n$ of !!{formula}s in the  !!{derivation} of~$!A$ from~$\Gamma$.  We show that if $!A_1$,  \dots, $!A_n = !A$ is !!a{derivation} from~$\Gamma$, then $\Gamma  \Entails !A_n$. Note that if $!A_1$, \dots, $!A_n$ is  !!a{derivation}, so is $!A_1$, \dots, $!A_k$ for any $k<n$.  There are no !!{derivation}s of length~$0$, so for $n=0$ the claim  holds vacuously. So the claim holds for all !!{derivation}s of  length~$<n$. We distinguish cases according to the justification  of~$!A_n$.    \begin{enumerate}  \item $!A_n$ is an axiom. All axioms are valid, so $\Gamma \Entails    !A_n$ for any~$\Gamma$.  \item $!A_n \in \Gamma$. Then for any $\mModel{M}$ and $w$, if    $\mSat{M}{\Gamma}[w]$, obviously $\mSat{M}{\Gamma}{!A_n}[w]$,    i.e., $\Gamma \Entails !A$.  \item $!A_n$ follows by \MP{} from $!A_i$ and $!A_j \ident !A_i \lif    !A_n$. $!A_1$, \dots, $!A_i$ and $!A_1$, \dots, $!A_j$ are    !!{derivation}s from~$\Gamma$, so by inductive hypothesis, $\Gamma    \Entails !A_i$ and $\Gamma \Entails !A_i \lif !A_n$.        Suppose $\mSat{M}{\Gamma}[w]$. Since $\mSat{M}{\Gamma}[w]$ and    $\Gamma \Entails !A_i \lif !A_n$, $\mSat{M}{!A_i \lif      !A_n}[w]$. By definition, this means that for all $w'$ such that    $Rww'$, if $\mSat{M}{!A_i}[w']$ then $\mSat{M}{!A_n}[w']$. Since    $R$ is reflexive, $w$ is among the $w'$ such that $Rww'$, i.e., we    have that if $\mSat{M}{!A_i}[w]$ then $\mSat{M}{!A_n}[w]$. Since    $\Gamma \Entails !A_i$, $\mSat{M}{!A_i}[w]$. So,    $\mSat{M}{!A_n}[w]$, as we wanted to show.  \end{enumerate}\end{proof}\end{document}

content/intuitionistic-logic/soundness-completeness/soundness-nd.tex

% part: intuitionistic-logic% chapter: soundness-completeness% section: soundness-nd\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sc}{snd}\olsection{Soundness of Natural Deduction}We will now prove soundness of natural deduction with regards to therelational semantics, that is, showing that if !!a{formula} is !!{derivable}from a set of assumptions then the set of assumptions entails the!!{formula}.\begin{thm}[Soundness]  \ollabel{thm:soundness}  If $\Gamma \Proves !A$, then $ \Gamma \Entails !A$.\end{thm}\begin{proof}  We prove that if $\Gamma \Proves !A$, then $\Gamma \Entails !A$.  The proof is by induction on the !!{derivation} of~$!A$  from~$\Gamma$.    \begin{enumerate}  \item If the !!{derivation} consists of just the assumption~$!A$, we    have $!A \Proves !A$, and want to show that $!A \Entails !A$.    Suppose that $\mSat{M}{!A}[w]$. Then trivially $\mSat{M}{!A}[w]$.  \item The !!{derivation} ends in $\Intro{\land}$:    \iftag{probAnd}{Exercise.}{The !!{derivation}s of the premises      $!B$ from !!{undischarged} assumptions~$\Gamma$ and of~$!C$ from      !!{undischarged} assumptions~$\Delta$ show that $\Gamma \Proves      !B$ and $\Delta \Proves !C$. By induction hypothesis we have      that $\Gamma \Entails !B$ and $\Delta \Entails !C$. We have to      show that $\Gamma \cup \Delta \Entails !A \land !B$, since the      !!{undischarged} assumptions of the entire !!{derivation} are      $\Gamma$ together with $\Delta$.  So suppose $\mSat{M}{\Gamma        \cup \Delta}[w]$. Then also $\mSat{M}{\Gamma}[w]$. Since $\Gamma      \Entails !B$, $\mSat{M}{!B}[w]$. Similarly, $\mSat{M}{!C}[w]$. So      $\mSat{M}{!B \land !C}[w]$.}  \item The !!{derivation} ends in $\Elim{\land}$:    \iftag{probAnd}{Exercise.}{The !!{derivation} of the premise $!B        \land !C$ from !!{undischarged} assumptions $\Gamma$ shows        that $\Gamma \Proves !B \land !C$. By induction hypothesis,        $\Gamma \Entails !B \land !C$. We have to show that $\Gamma        \Entails !B$. So suppose $\mSat{M}{\Gamma}[w]$. Since $\Gamma        \Entails !B \land !C$, $\mSat{M}{!B \land !C}[w]$. Then also        $\mSat{M}{!B}[w]$. Similarly if $\Elim\land$ ends in~$!C$, then        $\Gamma \Entails !C$.}  \item The !!{derivation} ends in $\Intro{\lor}$:    \iftag{probOr}{Exercise.}{Suppose the premise is $!B$, and the      !!{undischarged} assumptions of the !!{derivation} ending      in~$!B$ are $\Gamma$. Then we have $\Gamma \Proves !B$ and by      inductive hypothesis, $\Gamma \Entails !B$. We have to show that      $\Gamma \Entails !B \lor !C$. Suppose $\mSat{M}{\Gamma}[w]$. Since      $\Gamma \Entails !B$, $\mSat{M}{!B}[w]$. But then also $\mSat{M}{!B        \lor !C}[w]$. Similarly, if the premise is~$!C$, we have that      $\Gamma \Entails !C$.}      \item The !!{derivation} ends in~$\Elim{\lor}$:    \iftag{probOr}{Exercise.}{The !!{derivation}s ending in the      premises are of $!B \lor !C$ from !!{undischarged}      assumptions~$\Gamma$, of $!D$ from !!{undischarged} assumptions      $\Delta_1 \cup \{!B\}$, and of $!D$ from !!{undischarged}      assumptions~$\Delta_2 \cup \{!C\}$. So we have $\Gamma \Proves      !B \lor !C$, $\Delta_1 \cup \{!B\} \Proves !D$, and $\Delta_2      \cup \{!C\} \Proves !D$.  By induction hypothesis, $\Gamma      \Entails !B \lor !C$, $\Delta_1 \cup \{!B\} \Entails !D$, and      $\Delta_2 \cup \{!C\} \Entails !D$.  We have to prove that      $\Gamma \cup \Delta_1 \cup \Delta_2 \Entails !D$.    Suppose $\mSat{M}{\Gamma \cup \Delta_1 \cup \Delta_2}[w]$. Then    $\mSat{M}{\Gamma}[w]$ and since $\Gamma \Entails !B \lor !C$,    $\mSat{M}{!B \lor !C}[w]$. By definition of $\mSat{M}{}$, either    $\mSat{M}{!B}[w]$ or $\mSat{M}{!C}[w]$. So we distinguish cases:    (a)~$\mSat{M}{!B}$[w]. Then $\mSat{M}{\Delta_1 \cup \{!B\}}[w]$.    Since $\Delta_1 \cup !B \Entails !D$, we have $\mSat{M}{!D}[w]$.    (b)~$\mSat{M}{!C}[w]$. Then $\mSat{M}{\Delta_2 \cup \{!C\}}[w]$.    Since $\Delta_2 \cup !C \Entails !D$, we have $\mSat{M}{!D}[w]$. So    in either case, $\mSat{M}{!D}[w]$, as we wanted to show.}  \item The !!{derivation} ends with $\Intro{\lif}$ concluding~$!B\lif    !C$. Then the premise is~$!C$, and the !!{derivation} ending in    the premise has !!{undischarged} assumptions~$\Gamma \cup    \{!B\}$. So we have that $\Gamma \cup \{!B\} \Proves !C$, and by    induction hypothesis that $\Gamma \cup \{!B\} \Entails !C$. We    have to show that $\Gamma \Entails !B \lif !C$.    Suppose $\mSat{M}{\Gamma}[w]$. We want to show that for all    $w'$ such that $Rww'$, if $\mSat{M}{!B}[w']$, then    $\mSat{M}{!C}[w']$. So assume that $Rww'$ and    $\mSat{M}{!B}[w']$. By \olref[sem][rel]{prop:true-monotonic},    $\mSat{M}{\Gamma}[w']$. Since $\Gamma \cup \{!B\} \Entails !C$,    $\mSat{M}{!C}[w']$, which is what we wanted to show.   \item The !!{derivation} ends in $\Elim{\lif}$ and    conclusion~$!C$. The premises are $!B \lif !C$ and $!B$, with    !!{derivation}s from !!{undischarged} assumptions $\Gamma$,    $\Delta$. So we have $\Gamma \Proves !B \lif !C$ and $\Delta    \Proves !B$. By inductive hypothesis, $\Gamma \Entails !B \lif !C$    and $\Delta \Entails !B$. We have to show that $\Gamma \cup \Delta    \Entails !C$.    Suppose $\mSat{M}{\Gamma \cup \Delta}[w]$. Since    $\mSat{M}{\Gamma}[w]$ and $\Gamma \Entails !B \lif !C$,    $\mSat{M}{!B \lif !C}[w]$. By definition, this means that for all    $w'$ such that $Rww'$, if $\mSat{M}{!B}[w']$ then    $\mSat{M}{!C}[w']$. Since $R$ is reflexive, $w$ is among the $w'$    such that $Rww'$, i.e., we have that if $\mSat{M}{!B}[w]$ then    $\mSat{M}{!C}[w]$. Since $\mSat{M}{\Delta}[w]$ and $\Delta    \Entails !B$, $\mSat{M}{!B}[w]$. So, $\mSat{M}{!C}[w]$, as we    wanted to show.  \item The !!{derivation} ends in $\FalseInt$, concluding~$!A$. The    premise is $\lfalse$ and the !!{undischarged} assumptions of the    !!{derivation} of the premise are~$\Gamma$. Then $\Gamma \Proves    \lfalse$. By inductive hypothesis, $\Gamma \Entails \lfalse$. We    have to show $\Gamma \Entails !A$.    We proceed indirectly. If $\Gamma \Entails/ !A$ there is a    model~$\mModel{M}$ and world~$w$ such that $\mSat{M}{\Gamma}[w]$    and $\mSat/{M}{!A}[w]$.  Since $\Gamma \Entails \lfalse$,    $\mSat{M}{\lfalse}[w]$. But that's impossible, since by    definition, $\mSat/{M}{\lfalse}[w]$. So $\Gamma \Entails !A$.  \item The !!{derivation} ends in $\Intro\lnot$: Exercise.  \item The !!{derivation} ends in $\Elim\lnot$: Exercise.  \end{enumerate}\end{proof}\begin{prob}  Complete the proof of \olref[int][sc][snd]{thm:soundness}. For the  cases for $\Intro\lnot$ and $\Elim\lnot$, use the definition of  $\mSat{M}{\lnot !A}[w]$ in \olref[int][sem][rel]{defn:true-at-w}, i.e.,  don't treat $\lnot !A$ as defined by $!A \lif \lfalse$.\end{prob}\begin{prob}  Show that the following !!{formula}s are not !!{derivable} in  intuitionistic logic:  \begin{enumerate}    \item $(!A \lif !B) \lor (!B \lif !A)$    \item $(\lnot\lnot !A \lif !A) \lif (!A \lor \lnot !A)$    \item $(!A \lif !B \lor !C) \lif \bigl((!A \lif !B)\lor(!A \lif !C)\bigr)$  \end{enumerate}\end{prob}\end{document}

content/intuitionistic-logic/soundness-completeness/lindenbaum.tex

% part: intuitionistic-logic% chapter: soundness-completeness% section: lindenbaum\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sc}{lin}\olsection{Lindenbaum's Lemma}The completeness theorem for intuitionistic logic is proved by assuming$\Gamma \Proves/ !A$ and constructing a model $\mSat{M}{\Gamma}$ and~$\mSat/{M}{!A}$.In classical logic the relation of !!{derivability} can be reduced tothe notion of consistency since !!a{formula}~$!A$ is !!{derivable}from a set of !!{formula}s iff the set together with the negationof~$!A$ is inconsistent. This is not possible in intuitionistic logic.In intuitionistic logic, if $\lnot!A$ is inconsistent, we only getthat $\Proves \lnot\lnot !A$. Since $\lnot\lnot!A \lif !A$ does nothold intuitionistically in general, we cannot conclude that~$\Proves!A$.Thus, when constructing the model~$\mModel{M}$, we will need to keep track of the non-!!{derivability} of the !!{formula}~$!A$ and thus we will not be able to use a complete set $\Gamma^* \supseteq \Gamma$ to build the model$\mModel{M}$, as in every complete set $\Gamma^*$, we have$\Gamma^* \Proves !A \lor \lnot !A$.Instead of using a complete set~$\Gamma^*$, we will us the notion ofa prime set of formulas:\begin{defn}\ollabel{defn:prime}  A set of !!{formula}s~$\Gamma$ is \emph{prime} iff   \begin{enumerate}  \item\ollabel{defn:prime1} $\Gamma$ is consistent, i.e., $\Gamma \Proves/ \lfalse$;  \item\ollabel{defn:prime2} if $\Gamma \Proves !A$ then $!A \in \Gamma$; and  \item\ollabel{defn:prime3} if $!A \lor !B \in \Gamma$ then $!A \in    \Gamma$ or $!B \in \Gamma$.  \end{enumerate}\end{defn}\begin{lem}[Lindenbaum's Lemma]  \ollabel{lem:lindenbaum} If $\Gamma \Proves/ !A$, there is a  $\Gamma^* \supseteq \Gamma$ such that $\Gamma^*$ is prime and  $\Gamma^* \Proves/ !A$.\end{lem}\begin{proof}  Let $!B_1 \lor !C_1$, $!B_2 \lor !C_2$, \dots, be an enumeration of  all !!{formula}s of the form~$!B \lor !C$.  We'll define an  increasing sequence of sets of !!{formula}s~$\Gamma_n$, where each  $\Gamma_{n+1}$ is defined as $\Gamma_n$ together with one new  !!{formula}. $\Gamma^*$ will be the union of all~$\Gamma_n$. The new  !!{formula}s are selected so as to ensure that $\Gamma^*$ is prime  and still $\Gamma^* \Proves/ !A$. This means that at each step we  should find the first disjunction~$!B_i \lor !C_i$ such that:  \begin{enumerate}  \item\ollabel{gamma-1} $\Gamma_n \Proves !B_i \lor !C_i$  \item\ollabel{gamma-2} $!B_i \notin \Gamma_n$ and $!C_i \notin \Gamma_n$  \end{enumerate}  We add to $\Gamma_n$ either $!B_i$ if $\Gamma_n \cup \{!B_i\}  \Proves/ !A$, or $!C_i$ otherwise. We'll have to show that this  works. For now, let's define $i(n)$ as the least $i$ such that  \olref{gamma-1} and~\olref{gamma-2} hold.    Define $\Gamma_0 = \Gamma$ and  \[  \Gamma_{n+1} = \begin{cases}    \Gamma_n \cup \{!B_{i(n)}\} &    \text{if $\Gamma_n \cup \{!B_{i(n)}\} \Proves/ !A$} \\    \Gamma_n \cup \{!C_{i(n)}\} & \text{otherwise}    \end{cases}  \]  If $i(n)$ is undefined, i.e., whenever $\Gamma_n \Proves !B \lor !C$,  either $!B \in \Gamma_n$ or $!C \in \Gamma_n$, we let $\Gamma_{n+1}  = \Gamma_n$.  Now let $\Gamma^* = \bigcup_{n=0}^\infty \Gamma_n$  First we show that for all $n$, $\Gamma_n \Proves/ !A$. We proceed  by induction on~$n$. For $n = 0$ the claim holds by the hypothesis  of the theorem, i.e., $\Gamma \Proves/ !A$. If $n>0$, we have to  show that if $\Gamma_n \Proves/ !A$ then $\Gamma_{n+1} \Proves/ !A$. If  $i(n)$ is undefined, $\Gamma_{n+1} = \Gamma_n$ and there is nothing  to prove. So suppose $i(n)$ is defined. For simplicity, let $i =  i(n)$.    We'll prove the contrapositive of the claim. Suppose $\Gamma_{n+1}  \Proves !A$. By construction, $\Gamma_{n+1} = \Gamma_n \cup  \{!B_i\}$ if $\Gamma_n \cup \{!B_i\} \Proves/ !A$, or else  $\Gamma_{n+1} = \Gamma_n \cup \{!C_i\}$. It clearly can't be the  first, since then $\Gamma_{n+1} \Proves/ !A$.  Hence, $\Gamma_n \cup  \{!B_i\} \Proves !A$ and $\Gamma_{n+1} = \Gamma_n \cup \{!C_i\}$.  By definition of $i(n)$, we have that $\Gamma _n \Proves !B_i \lor  !C_i$. We have $\Gamma_n \cup \{!B_i\} \Proves !A$. We also have  $\Gamma_{n+1} = \Gamma_n \cup \{!C_i\} \Proves !A$. Hence, $\Gamma_n  \Proves !A$, which is what we wanted to show.  If $\Gamma^* \Proves !A$, there would be some finite subset $\Gamma'  \subseteq \Gamma^*$ such that $\Gamma' \Proves !A$. Each $!D \in  \Gamma'$ must be in $\Gamma_i$ for some~$i$.  Let $n$ be the largest  of these. Since $\Gamma_i \subseteq \Gamma_n$ if $i \le n$, $\Gamma'  \subseteq \Gamma_n$. But then $\Gamma_n \Proves !A$, contrary to our  proof above that $\Gamma_n \Proves/ !A$.  Lastly, we show that $\Gamma^*$ is prime, i.e., satisfies conditions  \olref{defn:prime1}, \olref{defn:prime2}, and~\olref{defn:prime3} of  \olref{defn:prime}.  First, $\Gamma^* \Proves/ !A$, so $\Gamma^*$ is  consistent, so \olref{defn:prime1} holds.  We now show that if $\Gamma^* \Proves !B \lor !C$, then either $!B  \in \Gamma^*$ or $!C \in \Gamma^*$. This proves \olref{defn:prime3},  since if $!B \lor !C \in \Gamma^*$ then also $\Gamma^* \Proves !B   \lor !C$. So assume $\Gamma^* \Proves !B \lor !C$ but $!B  \notin \Gamma^*$ and $!C \notin \Gamma^*$. Since $\Gamma^* \Proves  !B \lor !C$, $\Gamma_n \Proves !B \lor !C$ for some~$n$. $!B \lor  !C$ appears on the enumeration of all disjunctions, say, as $!B_j  \lor !C_j$. $!B_j \lor !C_j$ satisfies the properties in the  definition of $i(n)$, namely we have $\Gamma_n \Proves !B_j  \lor !C_j$, while $!B_j \notin \Gamma_n$ and $!C_j \notin \Gamma_n$. At  each stage, at least one fewer disjunction $!B_i \lor !C_i$  satisfies the conditions (since at each stage we add either $!B_i$  or $!C_i$), so at some stage~$m$ we will have $j = i(m)$. But  then either $!B \in \Gamma_{m+1}$ or $!C \in \Gamma_{m+1}$, contrary  to the assumption that $!B \notin \Gamma^*$ and $!C \notin  \Gamma^*$.  Now suppose $\Gamma^* \Proves !B$. Then $\Gamma^* \Proves !B \lor  !B$. But we've just proved that if $\Gamma^* \Proves !B \lor !B$  then $!B \in \Gamma^*$. Hence, $\Gamma^*$  satisfies~\olref{defn:prime2} of~\olref{defn:prime}.\end{proof}\begin{prob}Show that if $\Gamma \Proves/ \bot$ then $\Gamma$ is consistent in classical logic, i.e., there is a valuation making all formulas in~$\Gamma$ true.\end{prob}\end{document}

content/intuitionistic-logic/soundness-completeness/canonical-model.tex

% part: intuitionistic-logic% chapter: soundness-completeness% section: canonical-model\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sc}{mod}\olsection{The Canonical Model}The worlds in our model will be finite sequences~$\sigma$ of naturalnumbers, i.e., $\sigma \in \Nat^*$. Note that $\Nat^*$ is inductivelydefined by:\begin{enumerate}\item $\emptyseq \in \Nat^*$.\item If $\sigma \in \Nat^*$ and $n \in \Nat$, then $\sigma.n \in  \Nat^*$ (where $\sigma.n$ is $\sigma \concat \tuple{n}$ and $\sigma \concat \sigma'$ is the concatenation if $\sigma$ and $\sigma'$).\item Nothing else is in $\Nat^*$.\end{enumerate}So we can use $\Nat^*$ to give inductive definitions.Let $\tuple{!B_1, !C_1}$, $\tuple{!B_2, !C_2}$, \dots, be anenumeration of all pairs of !!{formula}s. Given a set of!!{formula}s~$\Delta$, define $\Delta(\sigma)$ by induction asfollows:\begin{enumerate}\item $\Delta(\emptyseq) = \Delta$\item $\Delta(\sigma.n) = {}$  \[  \begin{cases}    (\Delta(\sigma) \cup \{!B_n\})^* &    \text{if $\Delta(\sigma) \cup \{!B_n\} \Proves/ !C_n$} \\    \Delta(\sigma) & \text{otherwise}  \end{cases}  \]\end{enumerate}Here by $(\Delta(\sigma) \cup \{!B_n\})^*$ we mean the prime set of!!{formula}s which exists by \olref[lin]{lem:lindenbaum} applied to theset $\Delta(\sigma) \cup \{!B_n\}$ and the !!{formula}~$!C_n$. Note that by this definition, if$\Delta(\sigma) \cup \{!B_n\} \Proves/ !C_n$, then $\Delta(\sigma.n)\Proves !B_n$ and $\Delta(\sigma.n) \Proves/ !C_n$.  Note also that$\Delta(\sigma) \subseteq \Delta(\sigma.n)$ for any~$n$. If $\Delta$is prime, then $\Delta(\sigma)$ is prime for all~$\sigma$.\begin{defn}\ollabel{defn:canonical-model}  Suppose $\Delta$ is prime.  Then the \emph{canonical model} $\mModel{M(\Delta)}$ for  $\Delta$ is defined by:  \begin{enumerate}  \item $W = \Nat^*$, the set of finite sequences of natural numbers.  \item $R$ is the partial order according to which $R\sigma\sigma'$    iff $\sigma$ is an initial segment of~$\sigma'$ (i.e., $\sigma' =    \sigma \concat \sigma''$ for some sequence~$\sigma''$).  \item $V(p) = \Setabs{\sigma}{p \in \Delta(\sigma)}$.  \end{enumerate}\end{defn}It is easy to verify that $R$ is indeed a partial order. Also, themonotonicity condition on~$V$ is satisfied.  Since $\Delta(\sigma)\subseteq \Delta(\sigma.n)$ we get $\Delta(\sigma)\subseteq \Delta(\sigma')$ whenever $R\sigma\sigma'$ by inductionon~$\sigma$.\end{document}

content/intuitionistic-logic/soundness-completeness/truth-lemma.tex

% part: intuitionistic-logic% chapter: soundness-completeness% section: truth-lemma\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sc}{tru}\olsection{The Truth Lemma}The following lemma connects satisfaction in the canonical model withwhich !!{formula}s are !!{element}s of the prime set $\Delta$.\begin{lem}\ollabel{lem:truth}  If $\Delta$ is prime, then $\mSat{M(\Delta)}{!A}[\sigma]$ iff  $\Delta(\sigma) \Proves !A$.\end{lem}\begin{proof}  By induction on~$!A$.  \begin{enumerate}    \item \indcase{!A}{\lfalse}{Since $\Delta(\sigma)$ is prime, it      is consistent, so $\Delta(\sigma) \Proves/ \indfrm$. By      definition, $\mSat/{M(\Delta)}{\indfrm}[\sigma]$.}      \item \indcase{!A}{p}{By definition of $\mSat{{}}{}$,        $\mSat{M(\Delta)}{\indfrm}[\sigma]$ iff $\sigma \in V(p)$,        i.e., $\Delta(\sigma) \Proves \indfrm$.}      \item \indcase!{!A}{\lnot !B}{}      \item \indcase{!A}{!B \land        !C}{$\mSat{M(\Delta)}{\indfrm}[\sigma]$ iff        $\mSat{M(\Delta)}{!B}[\sigma]$ and        $\mSat{M(\Delta)}{!C}[\sigma]$. By induction hypothesis,        $\mSat{M(\Delta)}{!B}[\sigma]$ iff $\Delta(\sigma) \Proves        !B$, and similarly for~$!C$. But $\Delta(\sigma) \Proves !B$        and $\Delta(\sigma) \Proves !C$ iff $\Delta(\sigma)        \Proves \indfrm$.}      \item \indcase{!A}{!B \lor        !C}{$\mSat{M(\Delta)}{\indfrm}[\sigma]$ iff        $\mSat{M(\Delta)}{!B}[\sigma]$ or        $\mSat{M(\Delta)}{!C}[\sigma]$. By induction hypothesis,        this holds iff $\Delta(\sigma) \Proves !B$ or        $\Delta(\sigma) \Proves !C$. We have to show that this in        turn holds iff $\Delta(\sigma) \Proves \indfrm$. The        left-to-right direction is clear. The right-to-left direction        follows since $\Delta(\sigma)$ is prime.}      \item \indcase{!A}{!B \lif !C}{First the contrapositive of the        left-to-right direction: Assume $\Delta(\sigma) \Proves/ !B        \lif !C$. Then also $\Delta(\sigma) \cup \{!B\} \Proves/        !C$. Since $\tuple{!B, !C}$ is $\tuple{!B_n, !C_n}$ for        some~$n$, we have $\Delta(\sigma.n) = (\Delta(\sigma) \cup        \{!B\})^*$, and $\Delta(\sigma.n) \Proves !B$ but $\Delta(\sigma.n) \Proves/        !C$. By inductive hypothesis, $\mSat{M(\Delta)}{!B}[\sigma.n]$        and $\mSat/{M(\Delta)}{!C}[\sigma.n]$. Since        $R\sigma(\sigma.n)$, this means that        $\mSat/{M(\Delta)}{\indfrm}[\sigma]$.        Now assume $\Delta(\sigma) \Proves !B \lif !C$, and let        $R\sigma\sigma'$. Since $\Delta(\sigma) \subseteq        \Delta(\sigma')$, we have: if $\Delta(\sigma') \Proves        !B$, then $\Delta(\sigma') \Proves !C$. In other words, for        every $\sigma'$ such that $R\sigma\sigma'$, either        $\Delta(\sigma') \Proves/ !B$ or $\Delta(\sigma') \Proves        !C$. By induction hypothesis, this means that whenever        $R\sigma\sigma'$, either $\mSat/{M(\Delta)}{!B}[\sigma']$ or        $\mSat{M(\Delta)}{!C}[\sigma']$, i.e.,        $\mSat{M(\Delta)}{\indfrm}[\sigma]$.}  \end{enumerate}\end{proof}\end{document}

content/intuitionistic-logic/soundness-completeness/completeness-thm.tex

% part: intuitionistic-logic% chapter: soundness-completeness% section: completeness-thm\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sc}{cpl}\olsection{The Completeness Theorem}\begin{thm}\ollabel{thm:completeness}  If $\Gamma \Entails !A$ then $\Gamma \Proves !A$.\end{thm}\begin{proof}  We prove the contrapositive: Suppose $\Gamma \Proves/ !A$. Then by  \olref[lin]{lem:lindenbaum}, there is a prime set~$\Gamma^*  \supseteq \Gamma$ such that $\Gamma^* \Proves/ !A$. Consider the  canonical model~$\mModel{M(\Gamma^*)}$ for $\Gamma^*$ as defined in  \olref[mod]{defn:canonical-model}. For any $!B \in \Gamma$, $\Gamma^*  \Proves !B$. Note that $\Gamma^*(\emptyseq) = \Gamma^*$. By the Truth  Lemma (\olref[tru]{lem:truth}), we have  $\mSat{M(\Gamma^*)}{!B}[\emptyseq]$ for all $!B \in \Gamma$ and  $\mSat/{M(\Gamma^*)}{!A}[\emptyseq]$. This shows that $\Gamma  \Entails/ !A$.\end{proof}\begin{prob}  Show that if $!A$ only contains !!{propositional variable}s, $\lor$,  and~$\land$, then $\Entails/ !A$. Use this to conclude that $\lif$ is  not definable in intuitionistic logic from $\lor$ and~$\land$. \end{prob}  \begin{prob}  By using the completeness theorem prove that if $\Proves !A \lor !B$ then  $\Proves !A$ or $\Proves !B$. (Hint: Assume $\mSat/{M_1}{!A}$ and  $\mSat/{M_2}{!B}$ and construct a new model $\mModel{M}$ such that  $\mSat/{M}{!A \lor !B}$.)\end{prob}  \begin{prob}   Show that if $\mModel{M}$ is a relational model using a linear order then  $\mSat{M}{(!A \lif !B)\lor(!B \lif !A)}$.\end{prob}\end{document}

content/intuitionistic-logic/soundness-completeness/decidability.tex

% part: intuitionistic-logic% chapter: soundness-completeness% section: decidability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sc}{dec}\olsection{Decidability}Observe that the proof of the completeness theorem gives us for every$\Gamma \Proves/ !A$ a model with an infinite number of worldswitnessing the fact that $\Gamma \Entails/ !A$. The followingproposition shows that to prove $\Entails !A$ it is enough to provethat $\mSat{M}{!A}$ for all finite models (i.e., models with a finiteset of worlds).\begin{thm}\ollabel{thm:decidability}  If $\Entails/ !A$ then there is a finite model $\mSat/{M'}{!A}$.\end{thm}\begin{proof}  Assume $\mModel{M}=\tuple{W, R, V}$ is such that $\mSat/{M}{!A}$ and $P$   is the set of !!{propositional variable}s occurring in~$!A$. Define  $\mModel{M'}=\tuple{W', R', V'}$ by letting $W' = \Setabs{[w]}{w \in W}$   where $[w] = \Setabs{p \in P}{w \in V(p)}$, $R'$ be the subset relation,   and $V'(p)=\Setabs{[w]}{p \in [w]}$. It should be clear that $W'$ is a   finite set and that $\mModel{M'}$ is !!a{relational model}.  It can be shown, by induction on~$!A$, that   \[    \mSat{M}{!A}[w] \text{ iff } \mSat{M'}{!A}[{[w]}]  \]  for all !!{formula}s $!A$ with only !!{propositional variable}s  from~$P$. This is left as an exercise for the reader.\end{proof}\begin{prob}Finish the proof of \olref[int][sc][dec]{thm:decidability} by showingthat $\mSat{M,w}{!A}$ iff $\mSat{M',[w]}{!A}$ for all !!{formula}s~$!A$with only propositional variables from~$P$. \end{prob}From \olref{thm:decidability} it follows that there is an algorithm todecide whether~$\Entails !A$.\end{document}