The Open Logic Text

en · official · sha256:de96217946bc974d6d29e328d69d0e127a37d433136352dd85fc3afbcf8baa41

% part: intuitionistic-logic % chapter: introduction % section: axiomatic-derivations \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{int}{int}{axd} \olsection{Axiomatic \usetoken{P}{derivation}} Axiomatic !!{derivation}s for intuitionistic propositional logic are the conceptually simplest, and historically first, !!{derivation} systems. They work just as in classical propositional logic. \begin{defn}[!!^{derivability}] If $\Gamma$ is a set of !!{formula}s of $\Lang L$ then a \emph{!!{derivation}} from $\Gamma$ is a finite sequence $!A_1$, \dots,~$!A_n$ of !!{formula}s where for each $i \le n$ one of the following holds: \begin{enumerate} \item $!A_i \in \Gamma$; or \item $!A_i$ is an axiom; or \item $!A_i$ follows from some $!A_j$ and $!A_k$ with $j < i$ and $k < i$ by modus ponens, i.e., $!A_k \ident !A_j \lif !A_i$. \end{enumerate} \end{defn} \begin{defn}[Axioms] The set of $\PAx$ of \emph{axioms} for the intuitionistic propositional logic are all !!{formula}s of the following forms: \begin{align} & (!A \land !B) \lif !A \ollabel{ax:land1}\\ & (!A \land !B) \lif !B \ollabel{ax:land2}\\ & !A \lif (!B \lif (!A \land !B)) \ollabel{ax:land3}\\ & !A \lif (!A \lor !B) \ollabel{ax:lor1}\\ & !A \lif (!B \lor !A) \ollabel{ax:lor2}\\ & (!A \lif !C) \lif ((!B \lif !C) \lif ((!A \lor !B) \lif !C)) \ollabel{ax:lor3}\\ & !A \lif (!B \lif !A) \ollabel{ax:lif1}\\ & (!A \lif (!B \lif !C)) \lif ((!A \lif !B) \lif (!A \lif !C)) \ollabel{ax:lif2}\\ & \lfalse \lif !A \ollabel{ax:lfalse1} \end{align} \end{defn} \begin{defn}[!!^{derivability}] !!^a{formula}~$!A$ is \emph{!!{derivable}} from $\Gamma$, written $\Gamma \Proves !A$, if there is !!a{derivation} from $\Gamma$ ending in $!A$. \end{defn} \begin{defn}[Theorems] !!^a{formula}~$!A$ is a \emph{theorem} if there is !!a{derivation} of~$!A$ from the empty set. We write $\Proves !A$ if $!A$ is a theorem and $\Proves/ !A$ if it is not. \end{defn} \begin{prop} If $\Gamma \Proves !A$ in the axiomatic !!{derivation} system for intuitionistic logic, $\Gamma \Proves !A$ also in classical logic. In particular, if $!A$ is an intuitionistic theorem, it is also a classical theorem. \end{prop} \begin{proof} Every intuitionistic axiom is also a classical axiom, so every !!{derivation} in intuitionistic logic is also !!a{derivation} in classical logic. \end{proof} \end{document}

Referencing norms: AXD_INT

en · official · sha256:86b1e7b4ef34a6bbb3053b9a57b675723fe3e4a9cf4ef328d0066af4be0e74e4

% part: intuitionistic-logic % chapter: introduction % section: bhk-interpretation \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{int}{int}{bhk} \olsection{The Brouwer--Heyting--Kolmogorov Interpretation} \begin{editorial} Proofs of validity of intuitionistic propositions using the BHK interpretation are confusing; they have to be explained better. \end{editorial} There is an informal constructive interpretation of the intuitionist connectives, usually known as the Brouwer--Heyting--Kolmogorov interpretation. It uses the notion of a ``construction,'' which you may think of as a constructive proof. (We don't use ``proof'' in the BHK interpretation so as not to get confused with the notion of !!a{derivation} in a formal !!{derivation} system.) Based on this intuitive notion, the BHK interpretation explains the meanings of the intuitionistic connectives. \begin{enumerate} \item We assume that we know what constitutes a construction of an atomic statement. \item A construction of $!A_1 \land !A_2$ is a pair $\tuple{M_1, M_2}$ where $M_1$ is a construction of~$!A_1$ and $M_2$ is a construction of~$!A_2$. \item A construction of $!A_1 \lor !A_2$ is a pair $\tuple{s, M}$ where $s$ is~$1$ and $M$ is a construction of~$!A_1$, or $s$ is~$2$ and $M$ is a construction of~$!A_2$. \item A construction of $!A \lif !B$ is a function that converts a construction of~$!A$ into a construction of~$!B$. \item There is no construction for~$\lfalse$ (absurdity). \item $\lnot !A$ is defined as synonym for $!A \lif \lfalse$. That is, a construction of $\lnot !A$ is a function converting a construction of~$!A$ into a construction of~$\lfalse$. \end{enumerate} \begin{ex} Take $\lnot \lfalse$ for example. A construction of it is a function which, given any construction of $\lfalse$ as input, provides a construction of~$\lfalse$ as output. Obviously, the identity function~$\Id{}$ is such a construction: given a construction~$M$ of~$\lfalse$, $\Id{}(M) = M$ yields a construction of~$\lfalse$. \end{ex} Generally speaking, $\lnot !A$ means ``A construction of $!A$ is impossible''. \begin{ex} Let us prove $!A \lif \lnot \lnot !A$ for any proposition~$!A$, which is $!A \lif ((!A \lif \lfalse) \lif \lfalse)$. The construction should be a function~$f$ that, given a construction~$M$ of $!A$, returns a construction~$f(M)$ of $(!A \lif \lfalse) \lif \lfalse$. Here is how~$f$ constructs the construction of $(!A \lif \lfalse) \lif \lfalse$: We have to define a function $g$ which, when given a construction~$h$ of $!A \lif \lfalse$ as input, outputs a construction of~$\lfalse$. We can define $g$ as follows: apply the input~$h$ to the construction~$M$ of $!A$ (that we received earlier). Since the output~$h(M)$ of $h$ is a construction of $\lfalse$, $f(M)(h) = h(M)$ is a construction of~$\lfalse$ if $M$ is a construction of~$!A$. \end{ex} \begin{ex} Let us give a construction for $\lnot(!A \land \lnot !A)$, i.e., $(!A \land (!A \lif \lfalse)) \lif \lfalse$. This is a function~$f$ which, given as input a construction~$M$ of $!A \land (!A \lif \lfalse)$, yields a construction of~$\lfalse$. A construction of a conjunction $!B_1 \land !B_2$ is a pair $\tuple{N_1, N_2}$ where $N_1$ is a construction of~$!B_1$ and $N_2$ is a construction of~$!B_2$. We can define functions $p_1$ and $p_2$ which recover from a construction of $!B_1 \land !B_2$ the constructions of $!B_1$ and $!B_2$, respectively: \begin{align*} p_1(\tuple{N_1, N_2}) &= N_1\\ p_2(\tuple{N_1, N_2}) &= N_2 \end{align*} Here is what $f$ does: First it applies $p_1$ to its input~$M$. That yields a construction of~$!A$. Then it applies $p_2$ to~$M$, yielding a construction of~$!A \lif \lfalse$. Such a construction, in turn, is a function~$p_2(M)$ which, if given as input a construction of~$!A$, yields a construction of~$\lfalse$. In other words, if we apply $p_2(M)$ to $p_1(M)$, we get a construction of~$\lfalse$. Thus, we can define $f(M) = p_2(M)(p_1(M))$. \end{ex} \begin{ex} Let us give a construction of $((!A \land !B) \lif !C) \lif (!A \lif (!B \lif !C))$, i.e., a function $f$ which turns a construction~$g$ of $(!A \land !B) \lif !C$ into a construction of $(!A \lif (!B \lif !C))$. The construction $g$ is itself a function (from constructions of $!A \land !B$ to constructions of~$C$). And the output $f(g)$ is a function~$h_g$ from constructions of $!A$ to functions from constructions of~$!B$ to constructions of~$!C$. Ok, this is confusing. We have to construct a certain function $h_g$, which will be the output of $f$ for input~$g$. The input of~$h_g$ is a construction~$M$ of~$!A$. The output of $h_g(M)$ should be a function~$k_M$ from constructions~$N$ of~$!B$ to constructions of~$!C$. Let $k_{g,M}(N) = g(\tuple{M, N})$. Remember that $\tuple{M, N}$ is a construction of~$!A \land !B$. So $k_{g,M}$ is a construction of $!B \lif !C$: it maps constructions~$N$ of~$!B$ to constructions of~$!C$. Now let $h_g(M) = k_{g,M}$. That's a function that maps constructions~$M$ of~$!A$ to constructions $k_{g,M}$ of $!B \lif !C$. Now let $f(g) = h_g$. That's a function that maps constructions $g$ of $(!A \land !B) \lif !C$ to constructions of $!A \lif (!B \lif !C)$. Whew!{} \end{ex} The statement $!A \lor \lnot !A$ is called the Law of Excluded Middle. We can prove it for some specific $!A$ (e.g., $\lfalse \lor \lnot \lfalse$), but not in general. This is because the intuitionistic disjunction requires a construction of one of the disjuncts, but there are statements which currently can neither be proved nor refuted (say, Goldbach's conjecture). However, you can't refute the law of excluded middle either: that is, $\lnot \lnot (!A \lor \lnot !A)$ holds. \begin{ex} To prove $\lnot \lnot (!A \lor \lnot !A)$, we need a function~$f$ that transforms a construction of $\lnot(!A \lor \lnot !A)$, i.e., of $(!A \lor (!A \lif \lfalse)) \lif \lfalse$, into a construction of~$\lfalse$. In other words, we need a function $f$ such that $f(g)$ is a construction of~$\lfalse$ if $g$ is a construction of $\lnot(!A \lor \lnot !A)$. Suppose $g$ is a construction of $\lnot(!A \lor \lnot !A)$, i.e., a function that transforms a construction of $!A \lor \lnot !A$ into a construction of~$\lfalse$. A construction of $!A \lor \lnot !A$ is a pair $\tuple{s, M}$ where either $s = 1$ and $M$ is a construction of $!A$, or $s = 2$ and $M$ is a construction of $\lnot !A$. Let $h_1$ be the function mapping a construction~$M_1$ of $!A$ to a construction of $!A \lor \lnot !A$: it maps $M_1$ to $\tuple{1, M_1}$. And let $h_2$ be the function mapping a construction~$M_2$ of $\lnot !A$ to a construction of $!A \lor \lnot !A$: it maps $M_2$ to $\tuple{2, M_2}$. Let $k$ be $\comp{h_1}{g}$: it is a function which, if given a construction of~$!A$, returns a construction of~$\lfalse$, i.e., it is a construction of~$!A \lif \lfalse$ or $\lnot !A$. Now let $l$ be $\comp{h_2}{g}$. It is a function which, given a construction of $\lnot !A$, provides a construction of~$\lfalse$. Since $k$ is a construction of $\lnot !A$, $l(k)$ is a construction of~$\lfalse$. Together, what we've done is describe how we can turn a construction~$g$ of $\lnot(!A \lor \lnot !A)$ into a construction of~$\lfalse$, i.e., the function $f$ mapping a construction~$g$ of $\lnot(!A \lor \lnot !A)$ to the construction $l(k)$ of~$\lfalse$ is a construction of $\lnot\lnot(!A \lor \lnot !A)$. \end{ex} As you can see, using the BHK interpretation to show the intuitionistic validity of !!{formula}s quickly becomes cumbersome and confusing. Luckily, there are better !!{derivation} systems for intuitionistic logic, and more precise semantic interpretations. \end{document}

Referencing norms: BHK, BhkCovered, bhk_covered, bhk_requirement

en · official · sha256:64437ddd0e0fded35f092fbbec39f9a5367081e3a501c51203980bfb13e61a9b

% part: intuitionistic-logic % chapter: introduction % section: constructive-reasoning \documentclass[../../../include/open-logic-chapter]{subfiles} \begin{document} \olfileid{int}{int}{cr} \section{Constructive Reasoning} In contrast to extensions of classical logic by modal operators or second-order quantifiers, intuitionistic logic is ``non-classical'' in that it restricts classical logic. Classical logic is \emph{non-constructive} in various ways. Intuitionistic logic is intended to capture a more ``constructive'' kind of reasoning characteristic of a kind of constructive mathematics. The following examples may serve to illustrate some of the underlying motivations. Suppose someone claimed that they had determined a natural number~$n$ with the property that if $n$ is even, the Riemann hypothesis is true, and if $n$ is odd, the Riemann hypothesis is false. Great news!{} Whether the Riemann hypothesis is true or not is one of the big open questions of mathematics, and they seem to have reduced the problem to one of calculation, that is, to the determination of whether a specific number is even or not. What is the magic value of~$n$? They describe it as follows: $n$ is the natural number that is equal to $2$ if the Riemann hypothesis is true, and $3$ otherwise. Angrily, you demand your money back. From a classical point of view, the description above does in fact determine a unique value of $n$; but what you really want is a value of $n$ that is given \emph{explicitly}. To take another, perhaps less contrived example, consider the following question. We know that it is possible to raise an irrational number to a rational power, and get a rational result. For example, $\sqrt{2}^2 = 2$. What is less clear is whether or not it is possible to raise an irrational number to an \emph{irrational} power, and get a rational result. The following theorem answers this in the affirmative: \begin{thm} There are irrational numbers $a$ and $b$ such that $a^b$ is rational. \end{thm} \begin{proof} Consider $\sqrt{2}^{\sqrt{2}}$. If this is rational, we are done: we can let $a = b = \sqrt{2}$. Otherwise, it is irrational. Then we have \[ (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{\sqrt{2} \cdot \sqrt{2}} = \sqrt{2}^2 = 2, \] which is rational. So, in this case, let $a$ be $\sqrt{2}^{\sqrt{2}}$, and let $b$ be~$\sqrt 2$. \end{proof} Does this constitute a valid proof? Most mathematicians feel that it does. But again, there is something a little bit unsatisfying here: we have proved the existence of a pair of real numbers with a certain property, without being able to say \emph{which} pair of numbers it is. It is possible to prove the same result, but in such a way that the pair $a$, $b$ \emph{is} given in the proof: take $a = \sqrt{3}$ and $b = \log_3 4$. Then \[ a^b = \sqrt{3}^{\log_3 4} = 3^{1/2 \cdot \log_3 4} = (3^{\log_3 4})^{1/2} = 4^{1/2}= 2, \] since $3^{\log_3 x} = x$. Intuitionistic logic is designed to capture a kind of reasoning where moves like the one in the first proof are disallowed. Proving the existence of an $x$ satisfying~$!A(x)$ means that you have to give a specific~$x$, and a proof that it satisfies $!A$, like in the second proof. Proving that $!A$ or $!B$ holds requires that you can prove one or the other. Formally speaking, intuitionistic logic is what you get if you restrict !!a{derivation} system for classical logic in a certain way. From the mathematical point of view, these are just formal deductive systems, but, as already noted, they are intended to capture a kind of mathematical reasoning. One can take this to be the kind of reasoning that is justified on a certain philosophical view of mathematics (such as Brouwer's intuitionism); one can take it to be a kind of mathematical reasoning which is more ``concrete'' and satisfying (along the lines of Bishop's constructivism); and one can argue about whether or not the formal description captures the informal motivation. But whatever philosophical positions we may hold, we can study intuitionistic logic as a formally presented logic; and for whatever reasons, many mathematical logicians find it interesting to do so. \end{document}

Referencing norms: IPL

en · official · sha256:f331f2bca166ba4be8c2f8f333a19a8f8c68c2959a75386712bda9a626a5b185

% part: intuitionistic-logic % chapter: introduction % section: syntax \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{int}{int}{syn} \olsection{Syntax of Intuitionistic Logic} The syntax of intuitionistic logic is the same as that for propositional logic. In classical propositional logic it is possible to define connectives by others, e.g., one can define $!A \lif !B$ by $\lnot !A \lor !B$, or $!A \lor !B$ by $\lnot(\lnot !A \land \lnot !B)$. Thus, presentations of classical logic often introduce some connectives as abbreviations for these definitions. This is not so in intuitionistic logic, with two exceptions: $\lnot !A$ can be---and often is---defined as an abbreviation for $!A \lif \lfalse$. Then, of course, $\lfalse$ must not itself be defined!{} Also, $!A \liff !B$ can be defined, as in classical logic, as $(!A \lif !B) \land (!B \lif !A)$. !!^{formula}s of propositional intuitionistic logic are built up from \emph{!!{propositional variable}s} and the propositional constant~$\lfalse$ using \emph{logical connectives}. We have: \begin{enumerate} \item !!^a{denumerable} set~$\PVar$ of !!{propositional variable}s $\Obj p_0$, $\Obj p_1$, \dots \item The propositional constant for !!{falsity}~$\lfalse$. \item The logical connectives: $\land$ (conjunction), $\lor$ (disjunction), $\lif$ (conditional) \item Punctuation marks: (, ), and the comma. \end{enumerate} \begin{defn}[Formula] \ollabel{defn:formulas} The set~$\Frm[L_0]$ of \emph{!!{formula}s} of propositional intuitionistic logic is defined inductively as follows: \begin{enumerate} \item $\lfalse$ is an atomic !!{formula}. \item Every !!{propositional variable}~$\Obj p_i$ is an atomic !!{formula}. \item If $!A$ and $!B$ are !!{formula}s, then $(!A \land !B)$ is !!a{formula}. \item If $!A$ and $!B$ are !!{formula}s, then $(!A \lor !B)$ is !!a{formula}. \item If $!A$ and $!B$ are !!{formula}s, then $(!A \lif !B)$ is !!a{formula}. \tagitem{limitClause}{Nothing else is !!a{formula}.}{} \end{enumerate} \end{defn} In addition to the primitive connectives introduced above, we also use the following \emph{defined} symbols: $\lnot$ (negation) and $\liff$ (!!{biconditional}). Formulas constructed using the defined operators are to be understood as follows: \begin{enumerate} \item $\lnot !A$ abbreviates $!A \lif \lfalse$. \item $!A \liff !B$ abbreviates $(!A \lif !B) \land (!B \lif !A)$. \end{enumerate} Although $\lnot$ is officially treated as an abbreviation, we will sometimes give explicit rules and clauses in definitions for~$\lnot$ as if it were primitive. This is mostly so we can state practice problems. \end{document}

Referencing norms: IFOL

en · official · sha256:cfd759f0f325373f88de276d78710ec8242471617d9c5b84334463d4a379eb00

% 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 propositional logic, we have to give a definition of what counts as a model relative to which we can evaluate !!{formula}s. On the basis of such a definition it is then also possible to define semantics notions such as 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}

Referencing norms: KRIPKE_MODEL, MONOTONICITY

en · official · sha256:019b0df8ea379bece2fbf8615a7b99cb5cf5c311ff30be33dc11d1238aa144e8

% 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}

en · official · sha256:925771a788740e61733f15bc8cfab7a6cabf2c96824607e90025935b02d42a6c

% 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}

en · official · sha256:a21f6ebbcd23aee5024cfdea8534d751c95b7026a6b5fbf47dcc3cc90df75b51

% 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 the relational 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}