Interpretations of intuitionist logic in non-normal modal logics (Q1283321)

By a result of Hacking, Tarski translation \(t\) interprets the intuitionistic propositional calculus \(\mathbf { IPC}\) in the non-normal modal logic \(\mathbf { S3}\) (i.e. \(\mathbf { IPC} \vdash A\) iff \(\mathbf { S3} \vdash t(A)\), for any formula \(A\)). This motivates a translation of Kripke semantics for \(\mathbf { S3}\) into the following non-normal Kripke semantics for \(\mathbf { IPC}\). A non-normal model structure is \(M = \langle W, N, \leq, V \rangle\), where \((W, \leq)\) is a poset (of possible worlds), \(N\) is a non-empty subset of \(W\) (the set of normal worlds), \(V\) is a monotonic valuation of atoms in normal worlds, i.e. \[ (V(A,a) = 1 \Rightarrow (a \in N) \& ((a \leq b \in N) \Rightarrow (V(A,b) = 1)) \tag{1} \] holds for atomic \(A\) and \(a,b \in W\). The truth definition for the implication is as follows: \[ V(A \rightarrow B , a) = 1 \text{ iff } (a \in N) \& \forall b \geq a [V(A,b) = 1 \Rightarrow V(B,b) = 1], \] and similarly for \(\neg A\). A formula \(A\) is valid in \(M\) if \(\forall a \in N\;(V(A,a) = 1)\). This semantics is extended to the intuitionistic first-order calculus \(\mathbf { IQC}\): the truth definition for \(\forall\) is modified in the natural way, and the following (rather strong and unexpected) property is assumed: \[ D_a \not= \emptyset \text{ iff } a \in N \tag{2} \] where \(D_a\) is the individual domain of the world \(a \in W\). The paper shows soundness of this semantics for \(\mathbf {IQC}\); the completeness follows immediately from the completeness of the standard Kripke semantics. Reviewer's remark. The proposed non-normal Kripke semantics is actually equivalent to the standard one (for \(\mathbf { IPC}\) and \(\mathbf { IQC}\)). Namely, the validity in a non-normal model structure \(M = \langle W, N, \leq, V \rangle\) is equivalent to the validity in the standard Kripke model \(M = \langle N, \leq, V \rangle\), in which \(\leq\) and \(V\) are restricted to the set of worlds \(N\) --- since \((1)\) trivially holds for non-atomic \(A\), and the condition \((2)\) makes the equivalence obvious for \(\mathbf { IQC}\) too.