Problem 8
Show that HA \(\vdash \varphi \vee \psi \leftrightarrow \exists x(x=0 \rightarrow \varphi) \wedge(x \neq 0 \rightarrow \psi))\),
Problem 16
Each Kripke model with bottom node \(k_{0}\) can be turned into a model over a
tree as follows: \(K_{t r}\) consists of all finite increasing sequences
\(\left\langle k_{0}, k_{1}, \ldots, k_{n}\right\rangle, k_{i}
Problem 27
Let \(\mathbf{D}=\mathbf{R}[X] / X^{2}\) be the ring of dual numbers. D has a
unique maximal ideal, generated by \(X\). Consider a Kripke model with two nodes
\(k_{0}, k_{1} ; k_{0}
Problem 28
Show that \(\forall x(\varphi \vee \psi(x)) \rightarrow(\varphi \vee \forall x \psi(x))(x \notin F V(\varphi))\) holds in all Kripke models with constant domain function (i.e. \(\forall k l(D(k)=D(l))\).
Problem 31
Consider intuitionistic predicate logic without function symbols. Prove the following extension of the existence property: \(\vdash \exists y \varphi\left(x_{1}, \ldots, x_{n}, y\right) \Leftrightarrow\) \(\vdash \varphi\left(x_{1}, \ldots, x_{n}, t\right)\), where \(t\) is a constant or one of the variables \(x_{1}, \ldots, x_{n} .\) (Hint: replace \(x_{1}, \ldots, x_{n}\) by new constants \(a_{1}, \ldots, a_{n}\) ).
Problem 34
Consider a language with identity and function symbols, and interpret a \(n\)-ary symbol \(F\) by a function \(F_{k}: D(k)^{n} \rightarrow D(k)\) for each \(k\) in a given Kripke model \(\mathcal{K}\). We require monotonicity: \(k \leq l \Rightarrow F_{k} \subseteq F_{l}\) and preservation of equality, where \(a \sim_{k} b \Leftrightarrow k \Vdash \bar{a}=\bar{b}_{1}: \vec{a} \sim_{k} \vec{b} \Rightarrow F_{k}(\vec{a}) \sim_{k}\) \(F_{k}(\vec{b})\). (i) Show \(K \Vdash \forall \vec{x} \exists ! y(F(\vec{x})=y)\) (ii) Show \(\mathcal{K} \| I_{4}\). (iii) Let \(\mathcal{K} \|-\forall \vec{x} \exists ! y \varphi(\vec{x}, y)\), show that we can define for each \(k\) and \(F_{k}\) satisfying the above requirements such that \(\mathcal{K} \| \forall(\vec{x} \varphi(\vec{x}, F(\vec{x}))\). (iv) Show that one can conservatively add definable Skolem functions. Note that we have shown how to introduce functions in Kripke models, when they are given by "functional" relations. So, strictly speaking, Kripke models with just relations are good enough.
