Intuitionistic Logic

Semantics

content/intuitionistic-logic/semantics/semantics.tex

% part: intuitionistic-logic% chapter: semantics\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{int}{sem}{Semantics}\begin{editorial}  This chapter collects definitions for semantics for intuitionistic  logic. So far only Kripke and topological semantics are  covered. There are no examples yet, either of how models make  formulas true or of proofs that formulas are valid.\end{editorial}\olimport{introduction}\olimport{relational-models}\olimport{semantic-notions}\olimport{topological-semantics}\OLEndChapterHook\end{document}

content/intuitionistic-logic/semantics/introduction.tex

% part: intuitionistic-logic% chapter: semantics% section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sem}{int}\olsection{Introduction}No logic is satisfactorily described without a semantics, andintuitionistic logic is no exception. Whereas for classical logic, thesemantics based on !!{valuation}s is canonical, there are severalcompeting semantics for intuitionistic logic. None of them arecompletely satisfactory in the sense that they give anintuitionistically acceptable account of the meanings of theconnectives.The semantics based on !!{relational model}s, similar to the semanticsfor modal logics, is perhaps the most popular one.  In this semantics,!!{propositional variable}s are assigned to worlds, and these worldsare related by an accessibility relation. That relation is always apartial order, i.e., it is reflexive, antisymmetric, andtransitive.Intuitively, you might think of these worlds as states of knowledge or``evidentiary situations.''  A state~$w'$ is accessible from~$w$ iff,for all we know, $w'$ is a possible (future) state of knowledge, i.e.,one that is compatible with what's known at~$w$.  Once a propositionis known, it can't become un-known, i.e., whenever $!A$ is known at~$w$and~$Rww'$, $!A$ is known at~$w'$ as well. So ``knowledge'' ismonotonic with respect to the accessibility relation.If we define ``$!A$ is known'' as in epistemic logic as ``true in allepistemic alternatives,'' then $!A \land !B$ is known at~$w$ if in allepistemic alternatives, both $!A$ and~$!B$ are known. But sinceknowledge is monotonic and $R$ is reflexive, that means that $!A \land!B$ is known at $w$ iff $!A$ and $!B$ are known at~$w$.  For the samereason, $!A \lor !B$ is known at $w$ iff at least one of them isknown. So for $\land$ and $\lor$, the truth conditions of theconnectives coincide with those in classical logic.The truth conditions for the conditional, however, differ fromclassical logic. $!A \lif !B$ is known at~$w$ iff at no $w'$ with$Rww'$, $!A$ is known without $!B$ also being known. This is not thesame as the condition that $!A$ is unknown or $!B$~is knownat~$w$. For if we know neither $!A$ nor $!B$ at~$w$, there might be afuture epistemic state~$w'$ with $Rww'$ such that at $w'$, $!A$ isknown without also coming to know~$!B$.We know $\lnot !A$ only if there is no possible future epistemic statein which we know~$!A$. Here the idea is that if $!A$ were knowable,then in some possible future epistemic state~$!A$ becomes known. Sincewe can't know $\lfalse$, in that future epistemic state, we would know$!A$ but not know~$\lfalse$.On this interpretation the principle of excluded middle fails. Forthere are some $!A$ which we don't yet know, but which we might cometo know. For such !!a{formula}~$!A$, both $!A$ and~$\lnot !A$ are unknown, so$!A \lor \lnot !A$ is not known. But we do know, e.g., that $\lnot(!A\land \lnot !A)$. For no future state in which we know both $!A$ and$\lnot !A$ is possible, and we know this independently of whether ornot we know~$!A$ or $\lnot !A$.!!^{relational model}s are not the only available semantics forintuitionistic logic. The topological semantics is another: herepropositions are interpreted as open sets in a topological space, andthe connectives are interpreted as operations on these sets (e.g.,$\land$ corresponds to intersection).\end{document}

content/intuitionistic-logic/semantics/relational-models.tex

% part: intuitionistic-logic% chapter: semantics% section: relational-models\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sem}{rel}\olsection{\usetoken{P}{relational model}}In order to give a precise semantics for intuitionistic propositionallogic, we have to give a definition of what counts as a model relativeto which we can evaluate !!{formula}s. On the basis of such adefinition it is then also possible to define semantics notions suchas validity and entailment. One such semantics is given by!!{relational model}s.\begin{defn}  !!^a{relational model} for intuitionistic propositional logic is a  triple $\mModel{M} = \tuple{W, R, V}$, where  \begin{enumerate}  \item $W$ is a non-empty set,  \item $R$ is a partial order (i.e., a reflexive, antisymmetric, and transitive binary relation) on~$W$, and  \item $V$ is a function assigning to each !!{propositional    variable}~$p$ a subset of~$W$, such that  \item $V$ is monotone with respect to $R$, i.e., if $w    \in V(p)$ and $Rww'$, then $w' \in V(p)$.  \end{enumerate}\end{defn}\begin{defn}\ollabel{defn:true-at-w}  We define the notion of $!A$ \emph{being true at $w$ in    $\mModel{M}$}, $\mSat{M}{!A}[w]$, inductively as follows:  \begin{enumerate}  \item \indcase{!A}{p}{$\mSat{M}{\indfrm}[w]$ iff $w \in V(p)$.}  \item \indcase{!A}{\lfalse}{not $\mSat{M}{\indfrm}[w]$}.  \item \indcase{!A}{\lnot !B}{$\mSat{M}{\indfrm}[w]$ iff for no    $w'$ such that $Rww'$, $\mSat{M}{!B}[w']$}.  \item \indcase{!A}{!B \land !C}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w]$ and $\mSat{M}{!C}[w]$}.  \item \indcase{!A}{!B \lor !C}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w]$ or $\mSat{M}{!C}[w]$ (or both)}.  \item \indcase{!A}{!B \lif !C}{$\mSat{M}{\indfrm}[w]$ iff for every    $w'$ such that $Rww'$, not $\mSat{M}{!B}[w']$ or    $\mSat{M}{!C}[w']$} (or both).  \end{enumerate}  We write $\mSat/{M}{!A}[w]$ if not $\mSat{M}{!A}[w]$. If $\Gamma$ is  a set of !!{formula}s, $\mSat{M}{\Gamma}[w]$ means $\mSat{M}{!B}[w]$  for all $!B \in \Gamma$.\end{defn}\begin{prob}  Show that according to \olref[int][sem][rel]{defn:true-at-w},  $\mSat{M}{\lnot !A}[w]$ iff $\mSat{M}{!A \lif \lfalse}[w]$.\end{prob}\begin{prop}\ollabel{prop:true-monotonic}  Truth at worlds is monotonic with respect to~$R$, i.e., if  $\mSat{M}{!A}[w]$ and $Rww'$, then $\mSat{M}{!A}[w']$.\end{prop}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[int][sem][rel]{prop:true-monotonic}.\end{prob}\end{document}

content/intuitionistic-logic/semantics/semantic-notions.tex

% part: intuitionistic-logic% chapter: semantics% section: semantic-notions\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sem}{sem}\olsection{Semantic Notions}\begin{defn}  We say $!A$ is \emph{true in the model $\mModel{M} = \tuple{W,R,V}$,} $  \mSat{M}{!A}$, iff $\mSat{M}{!A}[w]$ for all $w \in W$.  $!A$ is \emph{valid}, $\Entails !A$, iff it is true in all models.  We say a set of !!{formula}s~$\Gamma$ \emph{entails}~$!A$, $\Gamma  \Entails !A$, iff for every model~$\mModel{M}$ and every~$w$ such  that $\mSat{M}{\Gamma}[w]$, $\mSat{M}{!A}[w]$.\end{defn}\begin{prop}\ollabel{prop:sat-entails}  \begin{enumerate}  \item\ollabel{prop:sat-entails1} If $\mSat{M}{\Gamma}[w]$ and    $\Gamma \Entails !A$, then $\mSat{M}{!A}[w]$.  \item\ollabel{prop:sat-entails2} If $\mSat{M}{\Gamma}$ and $\Gamma    \Entails !A$, then $\mSat{M}{!A}$.  \end{enumerate}\end{prop}\begin{proof}  \begin{enumerate}  \item Suppose $\mSat{M}{\Gamma}$. Since $\Gamma \Entails !A$, we    know that if $\mSat{M}{\Gamma}[w]$, then $\mSat{M}{!A}[w]$. Since    $\mSat{M}{\Gamma}[u]$ for all every $u \in W$,    $\mSat{M}{\Gamma}[w]$. Hence $\mSat{M}{!A}[w]$.  \item Follows immediately from \olref{prop:sat-entails1}.  \end{enumerate}\end{proof}\begin{defn}\ollabel{defn:restrict}  Suppose $\mModel{M}$ is a relational model and $w \in W$. The  \emph{restriction} $\mModel{M}_w=\tuple{W_w, R_w, V_w}$  of~$\mModel{M}$ to~$w$ is given by:  \begin{align*}    W_w & = \Setabs{u \in W}{Rwu},\\    R_w  & = R \cap (W_w)^2, \text{ and}\\    V_w(p) & = V(p) \cap W_w.  \end{align*}\end{defn}\begin{prop}\ollabel{prop:restrict}  $\mSat{M}{!A}[w]$ iff $\mSat{M_w}{!A}$.\end{prop}\begin{prob}  Prove \olref[int][sem][sem]{prop:restrict}. \end{prob}\begin{prop}  Suppose for every model~$\mModel{M}$ such that $\mSat{M}{\Gamma}$,  $\mSat{M}{!A}$. Then $\Gamma \Entails !A$.\end{prop}\begin{proof}  Suppose that $\mSat{M}{\Gamma}[w]$. By the \olref{prop:restrict}  applied to every~$!B \in \Gamma$, we have $\mSat{M_w}{\Gamma}$. By  the assumption, we have $\mSat{M_w}{!A}$. By \olref{prop:restrict}  again, we get $\mSat{M}{!A}[w]$.\end{proof}\end{document}

content/intuitionistic-logic/semantics/topological-semantics.tex

% part: intuitionistic-logic% chapter: semantics% section: topological-semantics\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{int}{sem}{top}\olsection{Topological Semantics}Another way to provide a semantics for intuitionistic logic is usingthe mathematical concept of a topology.\begin{defn}  Let $X$ be a set. A \emph{topology on~$X$} is a set $\Top{O}  \subseteq \Pow{X}$ that satisfies the properties below. The  !!{element}s of~$\Top{O}$ are called the \emph{open sets} of the  topology. The set $X$ together with $\Top{O}$ is called a  \emph{topological space}.  \begin{enumerate}  \item The empty set and the entire space are open: $\emptyset$, $X \in    \Top{O}$.  \item Open sets are closed under finite intersections: if $U$, $V \in    \Top{O}$ then $U \cap V \in \Top{O}$  \item Open sets are closed under arbitrary unions: if $U_i \in    \Top{O}$ for all $i \in I$, then $\bigcup \Setabs{U_i}{i \in      I} \in \Top{O}$.  \end{enumerate}\end{defn}We may write $X$ for a topology if the collection of open sets can beinferred from the context; note that, still, only after $X$ is endowedwith open sets can it be called a topology.\begin{defn}  A \emph{topological model} of intuitionistic propositional logic is  a triple $\mModel{X} = \tuple{X, \Top{O}, V}$ where $\Top{O}$ is a  topology on~$X$ and $V$ is a function assigning an open set in  $\Top{O}$ to each propositional variable.  Given a topological model~$\mModel{X}$, we can define $\Prop{X}{!A}$  inductively as follows:  \begin{enumerate}  \item $\Prop{X}{\lfalse} = \emptyset$  \item $\Prop{X}{p} = V(p)$  \item $\Prop{X}{!A \land !B} = \Prop{X}{!A} \cap \Prop{X}{!B}$  \item $\Prop{X}{!A \lor !B} = \Prop{X}{!A} \cup \Prop{X}{!B}$  \item $\Prop{X}{!A \lif !B} = \Interior{(X \setminus \Prop{X}{!A}) \cup    \Prop{X}{!B}}$  \end{enumerate}  Here, $\Interior{V}$ is the function that maps a set $V \subseteq X$  to its \emph{interior}, that is, the union of all open sets it  contains. In other words,  \[  \Interior{V} = \bigcup \Setabs{U}{U \subseteq V \text{ and } U \in \Top{O}}.  \]\end{defn}Note that the interior of any set is always open, since it is a unionof open sets. Thus, $\Prop{X}{!A}$ is always an open set.Although topological semantics is highly abstract, there are ways tothink about it that might motivate it. Suppose that the !!{element}s,or ``points,'' of $X$ are points at which statements can beevaluated. The set of all points where $!A$ is true is the propositionexpressed by~$!A$. Not every set of points is a potential proposition;only the !!{element}s of $\Top{O}$ are.  $!A \Entails !B$ iff $!B$ istrue at every point at which~$!A$ is true, i.e., $\Prop{X}{!A}\subseteq \Prop{X}{!B}$, for all~$X$. The absurd statement~$\lfalse$is never true, so $\Prop{X}{\lfalse} = \emptyset$.How must the propositions expressed by $!B \land !C$, $!B \lor !C$,and $!B \lif !C$ be related to those expressed by $!B$ and~$!C$ forthe intuitionistically valid laws to hold, i.e., so that $!A \Proves!B$ iff $\Prop{X}{!A} \subset \Prop{X}{!B}$? We require $\lfalse\Proves !A$ for any $!A$, which is satisfied because $\emptyset\subseteq U$ for all $U$.  Since $!B \land !C \Proves !B$, we requirethat $\Prop{X}{!B \land !C} \subseteq \Prop{X}{!B}$, and similarly$\Prop{X}{!B \land !C} \subseteq \Prop{X}{!C}$. The largest setsatisfying $W \subseteq U$ and $W \subseteq V$ is $U \cap V$.Conversely, $!B \Proves !B \lor !C$ and $!C \Proves !B \lor !C$, andso we require that $\Prop{X}{!B} \subseteq \Prop{X}{!B \lor !C}$ and$\Prop{X}{!C} \subseteq \Prop{X}{!B \lor !C}$. The smallest set~$W$such that $U \subseteq W$ and $V \subseteq W$ is $U \cup V$.The definition for $\lif$ is tricky: $!A \lif !B$ expresses theweakest proposition that, combined with $!A$, entails $!B$. That $!A\lif !B$ combined with $!A$ entails~$!B$ is clear from $(!A \lif !B)\land !A \Proves !B $. So $\Prop{X}{!A \lif !B}$ should be thegreatest open set such that $\Prop{X}{!A \lif !B} \cap \Prop{X}{!A}\subset \Prop{X}{!B}$, leading to our definition.\end{document}