Intuitionistic Logic

Intuitionistic Tableaux

content/intuitionistic-logic/tableaux/tableaux.tex

% Part: intuitionistic-logic% Chapter: tableaux\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{int}{tab}{Intuitionistic \usetoken{P}{tableau}}\begin{editorial}  Draft chapter on prefixed tableaux for intuitionistic logic. Needs more  examples, completeness proofs, and discussion of how one can find  countermodels from unsuccessful searches for closed tableaux.\end{editorial}\olimport{introduction}\olimport{rules}\olimport{proofs}\olimport{soundness}%\olimport{completeness}%\olimport{countermodels}\OLEndChapterHook\end{document}

content/intuitionistic-logic/tableaux/introduction.tex

% Part: intuitionistic-logic% Chapter: tableaux% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{tab}{int}\olsection{Introduction}!!^{tableau}s are certain (downward-branching) trees of !!{signed  formula}s, i.e., pairs consisting of a truth value sign ($\True$ or$\False$) and !!a{sentence}\[\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.\]!!^a{tableau} begins with a number of \emph{assumptions}. Each further!!{signed formula} is generated by applying one of the inferencerules. Some inference rules add one or more !!{signed formula}s to atip of the tree; others add two new tips, resulting in two branches.Rules result in !!{signed formula}s where the !!{formula} isless complex than that of the !!{signed formula} to which it wasapplied. When a branch contains both $\sFmla{\True}{!A}$ and$\sFmla{\False}{!A}$, we say the branch is \emph{closed}. If everybranch in !!a{tableau} is closed, the entire !!{tableau} is closed. Aclosed !!{tableau} constitutes !!a{derivation} that shows that the setof !!{signed formula}s which were used to begin the !!{tableau} areunsatisfiable.  This can be used to define a $\Proves$ relation:$\Gamma \Proves !A$ iff there is some finite set~$\Gamma_0 = \{!B_1,\dots, !B_n\} \subseteq \Gamma$ such that there is a closed!!{tableau} for the assumptions\[\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}.\]For intuitionistic logic, we have to both extend the notion of!!{signed formula} and adjust the rules for the connectives. Inaddition to a sign($\True$ or $\False$), !!{formula}s in modal!!{tableau}s also have \emph{prefixes}~$\sigma$. The prefixes arenon-empty sequences of positive integers, i.e., $\sigma \in(\PosInt)^* \setminus \{\emptyseq\}$. When we write such prefixeswithout the surrounding $\tuple{\ }$, and separate the individual!!{element}s by~$.$'s instead of $,$'s. If $\sigma$ is a prefix, then$\sigma.n$ is $\sigma \concat \tuple{n}$; e.g., if $\sigma = 1.2.1$,then $\sigma.3$ is $1.2.1.3$. So for instance,\[\sFmla{\True}{!A \lif (!B \lif !C)}[1.2]\]is a \emph{prefixed !!{signed formula}} (or just a \emph{prefixed  !!{formula}} for short).Intuitively, the prefix names a world in a model that might satisfythe !!{formula}s on a branch of !!a{tableau}, and if $\sigma$ namessome world, then $\sigma.n$ names a world accessible from (the worldnamed by)~$\sigma$.In intuitionistic models, the accessibility relation is reflexive andtransitive. In terms of prefixes, this means that $\sigma$ isaccessible from $\sigma$ itself, and so is any prefix thatextends~$\sigma$, i.e., any prefix of the form$\sigma.n_1.\cdots.n_k$. Let's introduce the notation $\sigma.*$ toindicate $\sigma$ itself and any extension of it. In other words, theprefixes $\sigma.*$ are all and only the prefixes accessiblefrom~$\sigma$.\end{document}

content/intuitionistic-logic/tableaux/rules.tex

% Part: intuitionistic-logic% Chapter: tableaux% Section: rules\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{tab}{rul}\olsection{Rules for Intuitionistic Logic}The rules for the connectives $\land$ and $\lor$ are the same as forregular propositional signed !!{tableau}s, just with prefixes added.In each case, the rule applied to a signed !!{formula}$\sFmla{S}{!A}[\sigma]$ produces new !!{formula}s that are alsoprefixed by~$\sigma$. This should be intuitively clear: e.g., if $!A\land !B$ is true at (a world named by)~$\sigma$, then $!A$ and $!B$are true at~$\sigma$ (and not at any other world). We collect therules for $\land$ and $\lor$ in \olref{tab:prop-rules}.\begin{table}  \[\def\arraystretch{3}\begin{array}{|c|c|}    \hline    \AxiomC{\sFmla{\True}{!A \land !B}[\sigma]}    \RightLabel{\TRule{\True}{\land}}    \UnaryInfC{\sFmla{\True}{!A}[\sigma]}    \noLine    \UnaryInfC{\sFmla{\True}{!B}[\sigma]}    \DisplayProof    &    \AxiomC{\sFmla{\False}{!A \land !B}[\sigma]}    \RightLabel{\TRule{\False}{\land}}    \UnaryInfC{$\sFmla{\False}{!A}[\sigma] \quad \mid \quad      \sFmla{\False}{!B}[\sigma]$}    \DisplayProof    \\[2ex]    \hline    \AxiomC{\sFmla{\True}{!A \lor !B}[\sigma]}    \RightLabel{\TRule{\True}{\lor}}    \UnaryInfC{$\sFmla{\True}{!A}[\sigma] \quad \mid \quad      \sFmla{\True}{!B}[\sigma]$}    \DisplayProof    &    \AxiomC{\sFmla{\False}{!A \lor !B}[\sigma]}    \RightLabel{\TRule{\False}{\lor}}    \UnaryInfC{\sFmla{\False}{!A}[\sigma]}    \noLine    \UnaryInfC{\sFmla{\False}{!B}[\sigma]}    \DisplayProof    \\[2ex]    \hline  \end{array}\]  \caption{Prefixed !!{tableau} rules for $\land$ and $\lor$}  \ollabel{tab:prop-rules}\end{table}The closure condition is similar to that for ordinary !!{tableau}s,although we require that not just the !!{formula}s, but also that theprefixes must match. In fact, we can be somewhat more liberal: Sincein intuitionistic models, !!{formula}s, once true, remain true, it isimpossible that $!A$ is true at~$\sigma$ but false at any accessibleprefix~$\sigma.{*}$. So a branch is closed if it contains both\[\sFmla{\True}{!A}[\sigma] \quad\text{and}\quad \sFmla{\False}{!A}[\sigma.{*}]\]for some prefix $\sigma$ and !!{formula}~$!A$. Note that if the signsare reversed, i.e., if it contains\[\sFmla{\False}{!A}[\sigma] \quad\text{and}\quad \sFmla{\True}{!A}[\sigma.{*}]\]the branch is closed only if $*$ is the empty sequence.In addition, a branch is closed if it contains~$\sFmla{\True}{\bot}[\sigma]$.The rules for setting up assumptions is also as for ordinary!!{tableau}s, except that for assumptions we always use theprefix~$1$. (It does not matter which prefix we use, as long as it'sthe same for all assumptions.) So, e.g., we say that\[!B_1, \dots, !B_n \Proves !A\]iff there is a closed tableau for the assumptions\[\sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1],\sFmla{\False}{!A}[1].\]For the conditional~$\lif$, the rules differ from the classical andmodal cases. The $\TRule{\lif}{\True}$ rule extends a branchcontaining $\sFmla{\True}{!A \lif !B}[\sigma]$ by$\sFmla{\True}{!A}[\sigma.{*}]$ and $\sFmla{\False}{!B}[\sigma.{*}]$ on twodifferent branches. It can only be applied for a prefix~$\sigma.{*}$which \emph{already} occurs on the branch in which it is applied.Let's call such a prefix ``used'' (on the branch). (Since $\sigma.{*}$includes $\sigma$ itself, the rule can always be applied by adding theprefixed signed formulas $\sFmla{\True}{!A}[\sigma]$ and$\sFmla{\False}{!B}[\sigma]$ on separate branches.)The $\TRule{\lif}{\False}$ rule extends a branch containing$\sFmla{\False}{!A \lif !B}[\sigma]$ by both$\sFmla{\True}{!A}[\sigma.n]$ and $\sFmla{\False}{!B}[\sigma.n]$ onthe same branch, with $\sigma.n$ a prefix new to the branch. The rules for $\lnot$ are defined analogously (using the definition of$\lnot !A$ as $!A \lif \lfalse$).The rules are given in \olref{tab:rules-lif-lnot}.\begin{table}  \[\def\arraystretch{3}\begin{array}{|c|c|}    \hline    \AxiomC{\sFmla{\True}{\lnot !A}[\sigma]}    \RightLabel{\TRule{\True}{\lnot}}    \UnaryInfC{$\sFmla{\False}{!A}[\sigma.{*}]$}    \DisplayProof    &    \AxiomC{\sFmla{\False}{\lnot !A}[\sigma]}    \RightLabel{\TRule{\False}{\lnot}}    \UnaryInfC{\sFmla{\True}{!A}[\sigma.n]}    \DisplayProof    \\[1ex]    \text{$\sigma.{*}$ is used} & \text{$\sigma.n$ is new}\\    \hline    \AxiomC{\sFmla{\True}{!A \lif !B}[\sigma]}    \RightLabel{\TRule{\True}{\lif}}    \UnaryInfC{$\sFmla{\False}{!A}[\sigma.{*}] \quad \mid \quad      \sFmla{\True}{!B}[\sigma.{*}]$}    \DisplayProof    &    \AxiomC{\sFmla{\False}{!A \lif !B}[\sigma]}    \RightLabel{\TRule{\False}{\lif}}    \UnaryInfC{\sFmla{\True}{!A}[\sigma.n]}    \noLine    \UnaryInfC{\sFmla{\False}{!B}[\sigma.n]}    \DisplayProof    \\[1ex]    \text{$\sigma.{*}$ is used} & \text{$\sigma.n$ is new}\\    \hline  \end{array}\]  \caption{Prefixed !!{tableau} rules for $\lnot$ and $\lif$}  \ollabel{tab:rules-lif-lnot}\end{table}\end{document}

content/intuitionistic-logic/tableaux/proofs.tex

% Part: intuitionistic-logic% Chapter: tableaux% Section: proofs\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{tab}{prf}\olsection{\usetoken{P}{tableau} for Intuitionistic Logic}\begin{ex}  We give a closed tableau that shows $(!A \land !B) \lif !C \Proves   !A \lif (!B \lif !C)$.  \begin{oltableau}    [\pFmla{\True}{(\formula{A} \land \formula{B}) \lif \formula{C}}{1},      just =\TAss      [\pFmla{\False}{\formula{A} \lif (\formula{B} \lif \formula{C})}{1},        just =\TAss        [\pFmla{\True}{\formula{A}}{1.1},          just = {\TRule{\False}{\lif}[2]}          [\pFmla{\False}{\formula{B} \lif \formula{C}}{1.1},            just = {\TRule{\False}{\lif}[2]}            [\pFmla{\True}{\formula{B}}{1.1.1},              just = {\TRule{\False}{\lif}[4]}              [\pFmla{\False}{\formula{C}}{1.1.1},                just = {\TRule{\False}{\lif}[4]}                [\pFmla{\False}{\formula{A} \land \formula{B}}{1.1.1},                  just = {\TRule{\True}{\lif}[1]}                  [\pFmla{\False}{\formula{A}}{1.1.1},                    just= {\TRule{\False}{\land}[4]}, close]                  [\pFmla{\False}{\formula{B}}{1.1.1},                    just= {\TRule{\False}{\land}[4]}, close]]                [\pFmla{\True}{\formula{C}}{1.1.1},                  just = {\TRule{\True}{\lif}[1]}, close]]            ]          ]        ]      ]    ]  \end{oltableau}\end{ex}\begin{prob}  Find closed intuitionistic !!{tableau}s to show the following:  \begin{enumerate}    \item $\Proves !A \lif (!B \lif !A)$    \item $\Proves \lnot(!A \land \lnot !A)$    \item $!A \lif (!B \lif !C) \Proves (!A \land !B) \lif !C$    \item $\lnot !A \lor \lnot !B \Proves \lnot(!A \land !B)$  \end{enumerate}\end{prob}\end{document}

content/intuitionistic-logic/tableaux/soundness.tex

% Part: intuitionistic-logic% Chapter: tableaux% Section: soundness\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{tab}{sou}\olsection{Soundness for Intuitionistic \usetoken{P}{tableau}}\begin{explain}  In order to show that intuitionistic !!{tableau}s are sound, we have to  show that if  \[  \sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1], \sFmla{\False}{!A}[1]  \]  has a closed !!{tableau} then $!B_1, \dots, !B_n \Entails !A$. It is  easier to prove the contrapositive: if for some $\mModel{M}$ and  world~$w$, $\mSat{M}{!B_i}[w]$ for all $i=1$, \dots,~$n$ but  $\mSat{M}{!A}[w]$, then no !!{tableau} can close. Such a  countermodel shows that the initial assumptions of the !!{tableau}  are satisfiable. The strategy of the proof is to show that whenever  all the prefixed !!{formula}s on !!a{tableau} branch are  satisfiable, any application of a rule results in at least one  extended branch that is also satisfiable. Since closed branches are  unsatisfiable, any !!{tableau} for a satisfiable set of prefixed  !!{formula}s must have at least one open branch.  In order to apply this strategy in the modal case, we have to extend  our definition of ``satisfiable'' to relational and prefixes. With  that in hand, however, the proof is straightforward.\end{explain}\begin{defn}  Let $P$ be some set of prefixes, i.e., $P \subseteq (\PosInt)^*  \setminus \{\emptyseq\}$ and let $\mModel{M}$ be a model.  A  function~$f\colon P \to W$ is an \emph{interpretation of}~$P$  in~$\mModel{M}$ if, whenever $\sigma$ and $\sigma.n$ are both  in~$P$, then $Rf(\sigma)f(\sigma.n)$.  Relative to an interpretation of prefixes~$P$ we can define:  \begin{enumerate}  \item $\mModel{M}$ satisfies $\sFmla{\True}{!A}[\sigma]$ iff    $\mSat{M}{!A}[f(\sigma)]$.  \item $\mModel{M}$ satisfies $\sFmla{\False}{!A}[\sigma]$ iff    $\mSat/{M}{!A}[f(\sigma)]$.  \end{enumerate}\end{defn}Note that since $R$ is reflexive and transitive and $\sigma.{*}$denotes, $\sigma$, $\sigma.n_1$, $\sigma.n_1.n_2$, \dots, we also havethat $Rf(\sigma)f(\sigma.{*})$. \begin{defn}  Let $\Gamma$ be a set of prefixed !!{formula}s, and let $P(\Gamma)$  be the set of prefixes that occur in it. If $f$ is an interpretation  of~$P(\Gamma)$ in $\mModel{M}$, we say that $\mModel{M}$ satisfies  $\Gamma$ with respect to~$f$, $\mSat{M}{\Gamma}[f]$, if $\mModel{M}$  satisfies every prefixed !!{formula} in~$\Gamma$ with respect  to~$f$. $\Gamma$ is \emph{satisfiable} iff there is a  model~$\mModel{M}$ and interpretation~$f$ of $P(\Gamma)$ such that  $\mSat{M}{\Gamma}[f]$.\end{defn}\begin{prop}  If $\Gamma$ contains both $\sFmla{\True}{!A}[\sigma]$ and  $\sFmla{\False}{!A}[\sigma.{*}]$ for some !!{formula}~$!A$ and  prefix~$\sigma$, or it contains $\sFmla{\True}{\lfalse}[\sigma]$, then $\Gamma$ is unsatisfiable.\end{prop}\begin{proof}  Since always $\mSat/{M}{\lfalse}[f(\sigma)]$, a $\Gamma$ that  contains $\sFmla{\True}{\lfalse}$ is unsatisfiable.  There also cannot be a model~$\mModel{M}$ and interpretation~$f$ of  $P(\Gamma)$ such that both If $\mSat{M}{!A}[f(\sigma)]$, then by  \olref[sem][rel]{prop:true-monotonic}, since  $Rf(\sigma)(\sigma.{*})$, $\mSat{M}{!A}[f(\sigma)]$. So we cannot  have both $\mSat{M}{!A}[f(\sigma)]$ and  $\mSat/{M}{!A}[f(\sigma.{*})]$.\end{proof}\begin{thm}[Soundness]  \ollabel{thm:tableau-soundness}  If $\Gamma$ has a closed !!{tableau}, $\Gamma$ is unsatisfiable.\end{thm}\begin{proof}We call a branch of !!a{tableau} satisfiable iff the set of!!{signed formula}s on it is satisfiable, and let's call !!a{tableau}satisfiable if it contains at least one satisfiable branch.We show the following: Extending a satisfiable !!{tableau} by one ofthe rules of inference always results in a satisfiable !!{tableau}.This will prove the theorem: any closed !!{tableau} results byapplying rules of inference to the !!{tableau} consisting only ofassumptions from~$\Gamma$. So if $\Gamma$ were satisfiable, any!!{tableau} for it would be satisfiable. A closed !!{tableau},however, is clearly not satisfiable, since all its branches are closedand closed branches are unsatisfiable.Suppose we have a satisfiable !!{tableau}, i.e., !!a{tableau} with atleast one satisfiable branch. Applying a rule of inference either adds!!{signed formula}s to a branch, or splits a branch in two. If the!!{tableau} has a satisfiable branch which is not extended by the ruleapplication in question, it remains a satisfiable branch in theextended !!{tableau}, so the extended tableau is satisfiable. So weonly have to consider the case where a rule is applied to asatisfiable branch.Let $\Gamma$ be the set of !!{signed formula}s on that branch, and let$\sFmla{S}{!A}[\sigma] \in \Gamma$ be the !!{signed formula} to whichthe rule is applied. If the rule does not result in a split branch, wehave to show that the extended branch, i.e., $\Gamma$ together withthe conclusions of the rule, is still satisfiable. If the rule resultsin split branch, we have to show that at least one of the tworesulting branches is satisfiable.\begin{enumerate}\item The branch is expanded by applying $\TRule{\True}{\lnot}$ to  $\sFmla{\True}{\lnot !B}[\sigma] \in \Gamma$. Then the extended  branch contains the !!{signed formula}s $\Gamma \cup  \{\sFmla{\False}{!B}[\sigma.{*}]\}$. Suppose $\mSat{M}{\Gamma}[f]$.  In particular, $\mSat{M}{\lnot !B}[f(\sigma)]$. Thus,  $\mSat/{M}{!B}[w]$ for any $w$ such that $Rf(\sigma)w$, and that  includes $f(\sigma.{*})$. So, $\mModel{M}$ satisfies  $\sFmla{\False}{!B}[\sigma.{*}]$ with respect to~$f$.\item The branch is expanded by applying $\TRule{\False}{\lnot}$ to  $\sFmla{\False}{\lnot !B}[\sigma] \in \Gamma$: Exercise.\item The branch is expanded by applying $\TRule{\True}{\land}$ to  $\sFmla{\True}{!B \land !C}[\sigma] \in \Gamma$, which results in  two new !!{signed formula}s on the branch:  $\sFmla{\True}{!B}[\sigma]$ and $\sFmla{\True}{!C}[\sigma]$. Suppose  $\mSat{M}{\Gamma}[f]$, in particular $\mSat{M}{!B \land    !C}[f(\sigma)]$. Then $\mSat{M}{!B}[f(\sigma)]$ and  $\mSat{M}{!C}[f(\sigma)]$. This means that $\mModel{M}$ satisfies  both $\sFmla{\True}{!B}[\sigma]$ and $\sFmla{\True}{!C}[\sigma]$  with respect to~$f$.\item The branch is expanded by applying $\TRule{\False}{\lor}$ to  $\sFmla{\False}{!B \lor !C} \in \Gamma$: Exercise.\item The branch is expanded by applying $\TRule{\False}{\lif}$ to  $\sFmla{\False}{!B \lif !C}[\sigma] \in \Gamma$: This results in two  new !!{signed formula}s on the branch: $\sFmla{\True}{!B}[\sigma.n]$ and  $\sFmla{\False}{!C}[\sigma.n]$, where $\sigma.n$ is a  new prefix on the branch, i.e., $\sigma.n \notin P(\Gamma)$.     Since $\Gamma$ is satisfiable, there is a $\mModel{M}$ and  interpretation~$f$ of $P(\Gamma)$ such that $\mSat{M}{\Gamma}[f]$, in  particular $\mSat/{M}{!B \lif !C}[f(\sigma)]$. We have to show that  $\Gamma \cup \{\sFmla{\False}{!B \lif !C}[\sigma.n]\}$ is  satisfiable. To do this, we define an interpretation of $P(\Gamma)  \cup \{\sigma.n\}$ as follows:    Since $\mSat/{M}{!B \lif !C}[f(\sigma)]$, there is a $w \in W$ such  that $Rf(\sigma)w$ such that $\mSat{M}{!B}[w]$ and  $\mSat/{M}{!C}[w]$. Let $f'$ be like $f$, except that $f'(\sigma.n)  = w$. Since $f'(\sigma) = f(\sigma)$ and $Rf(\sigma)w$, we have  $Rf'(\sigma)f'(\sigma.n)$, so $f'$ is an interpretation of  $P(\Gamma) \cup \{\sigma.n\}$. Obviously  $\mSat{M}{!B}[f'(\sigma.n)]$ and $\mSat/{M}{!C}[f'(\sigma.n)]$.  Since $f(\sigma') = f'(\sigma')$ for all prefixes $\sigma' \in  P(\Gamma)$, $\mSat{M}{\Gamma}[f']$.  So, $\mModel{M}, f'$ satisfies  $\Gamma \cup \{\sFmla{\False}{!B \lif !C}[\sigma.n]\}$\end{enumerate}Now let's consider the possible inferences with two premises.\begin{enumerate}\item The branch is expanded by applying $\TRule{\False}{\land}$ to  $\sFmla{\False}{!B \land !C}[\sigma] \in \Gamma$, which results in  two branches, a left one continuing through  $\sFmla{\False}{!B}[\sigma]$ and a right one through  $\sFmla{\False}{!C}[\sigma]$. Suppose $\mSat{M}{\Gamma}[f]$, in  particular $\mSat/{M}{!B \land !C}[f(\sigma)]$.  Then  $\mSat/{M}{!B}[f(\sigma)]$ or $\mSat/{M}{!C}[f(\sigma)]$. In the  former case, $\mModel{M}, f$ satisfies $\sFmla{\False}{!B}[\sigma]$,  i.e., the left branch is satisfiable. In the latter, $\mModel{M}, f$  satisfies $\sFmla{\False}{!C}[\sigma]$, i.e., the right branch is  satisfiable.\item The branch is expanded by applying $\TRule{\True}{\lor}$ to    $\sFmla{\True}{!B \lor !C}[\sigma] \in \Gamma$: Exercise.\item The branch is expanded by applying $\TRule{\True}{\lif}$ to    $\sFmla{\True}{!B \lif !C}[\sigma] \in \Gamma$: Exercise.\end{enumerate}\end{proof}\begin{prob}Complete the proof of \olref[int][tab][sou]{thm:tableau-soundness}.\end{prob}\begin{cor}\ollabel{cor:entailment-soundness}If $\Gamma \Proves !A$ then $\Gamma \Entails !A$.\end{cor}\begin{proof}  If $\Gamma \Proves !A$ then for some $!B_1$, \dots, $!B_n \in  \Gamma$, $\Delta = \{\sFmla{\False}{!A}[1], \sFmla{\True}{!B_1}[1],  \dots, \sFmla{\True}{!B_n}[1]\}$ has a closed !!{tableau}. We want  to show that $\Gamma \Entails !A$. Suppose not, so for some  $\mModel{M}$ and $w$, $\mSat{M}{!B_i}[w]$ for $i=1$, \dots,~$n$, but  $\mSat/{M}{!A}[w]$. Let $f(1) = w$; then $f$ is an interpretation  of~$P(\Delta)$ into~$\mModel{M}$, and $\mModel{M}$ satisfies~$\Delta$ with  respect to~$f$. But by \olref{thm:tableau-soundness}, $\Delta$ is  unsatisfiable since it has a closed !!{tableau}, a  contradiction. So we must have $\Gamma \Proves !A$ after all.\end{proof}\begin{cor}\ollabel{cor:weak-soundness}If $\Proves !A$ then $!A$ is true in all models.\end{cor}\end{document}