Appendix A Proof of Lemma 4
We sketch the respective proofs and derivations in \(\mathbb {ICK}\):
$$\begin{aligned} (\text {NEC}):\qquad \phi{} & {} {}&\text {premise}\end{aligned}$$
(A1)
$$\begin{aligned} \phi&\leftrightarrow \top{} & {} \text {(A1)}, ({\alpha }0), \text {(MP)}\end{aligned}$$
(A2)
$$\begin{aligned} (\psi&\square \hspace{-4.0pt}\rightarrow \phi )\leftrightarrow (\psi \square \hspace{-4.0pt}\rightarrow \top ){} & {} \text {(A2), (RC)}\square \end{aligned}$$
(A3)
$$\begin{aligned} \psi&\square \hspace{-4.0pt}\rightarrow \phi{} & {} \text {(A3)}, ({\alpha }5), ({\alpha }0), \text {(MP)} \end{aligned}$$
(A4)
$$\begin{aligned} (\text {RM}\square ):\qquad \phi&\rightarrow \psi{} & {} \text {premise}\end{aligned}$$
(A5)
$$\begin{aligned} (\phi&\wedge \psi )\leftrightarrow \phi{} & {} \text {(A5)}, ({\alpha }0), \text {(MP)}\end{aligned}$$
(A6)
$$\begin{aligned} (\chi&\square \hspace{-4.0pt}\rightarrow (\phi \wedge \psi ))\leftrightarrow (\chi \square \hspace{-4.0pt}\rightarrow \phi ){} & {} \text {(A6)}, \text {(RC}\square )\end{aligned}$$
(A7)
$$\begin{aligned} (\chi&\square \hspace{-4.0pt}\rightarrow \phi )\rightarrow (\chi \square \hspace{-4.0pt}\rightarrow \psi ){} & {} \text {(A7)}, ({\alpha }1), ({\alpha }0), \text {(MP)} \end{aligned}$$
(A8)
$$\begin{aligned} \text {(RM}\diamond ):\quad \phi&\rightarrow \psi{} & {} \text {premise}\end{aligned}$$
(A9)
$$\begin{aligned} (\phi&\vee \psi )\leftrightarrow \psi{} & {} \text {(A9)}, ({\alpha }0), \text {(MP)}\end{aligned}$$
(A10)
$$\begin{aligned} (\chi&\Diamond \hspace{-4.0pt}\rightarrow (\phi \vee \psi ))\leftrightarrow (\chi \Diamond \hspace{-4.0pt}\rightarrow \psi ){} & {} \text {(A10)}, \text {(RC}\diamond \end{aligned}$$
(A11)
$$\begin{aligned} (\chi&\Diamond \hspace{-4.0pt}\rightarrow \phi )\rightarrow (\chi \Diamond \hspace{-4.0pt}\rightarrow \psi ){} & {} \text {(A11)}, ({\alpha }3), ({\alpha }0), \text {(MP)} \end{aligned}$$
(A12)
$$\begin{aligned} (T1):\! (\psi&\! \wedge (\psi \rightarrow \chi ))\rightarrow \chi{} & {} ({\alpha }0), \text {(MP)}\end{aligned}$$
(A13)
$$\begin{aligned} \! (\phi&\! \square \hspace{-4.0pt}\rightarrow \! (\psi \wedge (\psi \rightarrow \chi )))\rightarrow (\phi \square \hspace{-4.0pt}\rightarrow \chi ){} & {} \text {(A13)}, \text {(RM}{\square )}\end{aligned}$$
(A14)
$$\begin{aligned} \! ((\phi&\! \square \hspace{-4.0pt}\rightarrow \! \psi )\! \wedge \! (\phi \! \square \hspace{-4.0pt}\rightarrow \! (\psi \! \rightarrow \! \chi )))\! \rightarrow \! (\phi \!\square \hspace{-4.0pt}\rightarrow \!\chi ){} & {} ({\alpha }1), \text {(A14)}, ({\alpha }0), \text {(MP)} \end{aligned}$$
(A15)
$$\begin{aligned} \text {(T2)}:\, ((\phi&\! \Diamond \hspace{-4.0pt}\rightarrow \psi )\! \wedge \! (\phi \! \square \hspace{-4.0pt}\rightarrow \! (\psi \! \rightarrow \! \chi )))\!\rightarrow \! (\phi \! \Diamond \hspace{-4.0pt}\rightarrow \! (\psi \! \wedge \! (\psi \rightarrow \chi )))\qquad \quad ({\alpha }2)\end{aligned}$$
(A16)
$$\begin{aligned} (\psi&\wedge (\psi \rightarrow \chi ))\rightarrow \chi \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad ({\alpha }0), \text {(MP)}\end{aligned}$$
(A17)
$$\begin{aligned} (\phi&\Diamond \hspace{-4.0pt}\rightarrow (\psi \wedge (\psi \rightarrow \chi )))\rightarrow (\phi \Diamond \hspace{-4.0pt}\rightarrow \chi )\qquad \qquad \qquad (A17), \text {(RM}\diamond )\end{aligned}$$
(A18)
$$\begin{aligned} ((\phi&\! \Diamond \hspace{-4.0pt}\rightarrow \! \psi )\! \wedge \! (\phi \! \square \hspace{-4.0pt}\rightarrow \! (\psi \! \rightarrow \! \chi )))\! \rightarrow \! (\phi \! \Diamond \hspace{-4.0pt}\rightarrow \! \chi )\,\,(A16), (A18), ({\alpha }0), \text {(MP)}\!\!\! \end{aligned}$$
(A19)
$$\begin{aligned} \text {(T3)}:\,\psi&\rightarrow ((\psi \rightarrow \chi )\rightarrow \chi )\qquad \qquad \qquad \qquad \qquad \qquad \qquad \quad ({\alpha }0), \text {(MP)}\end{aligned}$$
(A20)
$$\begin{aligned} (\phi&\square \hspace{-4.0pt}\rightarrow \psi )\rightarrow (\phi \square \hspace{-4.0pt}\rightarrow ((\psi \rightarrow \chi )\rightarrow \chi ))\qquad \qquad \qquad \text {(A20)}, \text {(RM}\square )\end{aligned}$$
(A21)
$$\begin{aligned} (\phi&\! \square \hspace{-4.0pt}\rightarrow \! \psi )\! \rightarrow \! ((\phi \! \Diamond \hspace{-4.0pt}\rightarrow \! (\psi \! \rightarrow \! \chi ))\! \rightarrow \! (\phi \! \Diamond \hspace{-4.0pt}\rightarrow \! \chi ))\,\,(\text {A21}), (\text {AT2}), ({\alpha }0), \text {(MP)} \end{aligned}$$
(A22)
$$\begin{aligned} (\text {T4}):\,(\phi&\square \hspace{-4.0pt}\rightarrow (\psi \rightarrow \bot ))\rightarrow ((\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\rightarrow (\phi \Diamond \hspace{-4.0pt}\rightarrow \bot ))\qquad \qquad \qquad \quad \text {(T2)}\end{aligned}$$
(A23)
$$\begin{aligned} ((\phi&\Diamond \hspace{-4.0pt}\rightarrow \psi )\rightarrow (\phi \Diamond \hspace{-4.0pt}\rightarrow \bot ))\rightarrow ((\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\rightarrow \bot )\quad ({\alpha }6), ({\alpha }0), \text {(MP)}\end{aligned}$$
(A24)
$$\begin{aligned} (\phi&\square \hspace{-4.0pt}\rightarrow \lnot \psi )\rightarrow \lnot (\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\qquad \qquad \qquad \quad \,\text {(A23)}, \text {(A24)}, ({\alpha }0), \text {(MP)}\end{aligned}$$
(A25)
$$\begin{aligned} ((\phi&\Diamond \hspace{-4.0pt}\rightarrow \psi )\rightarrow \bot )\rightarrow ((\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\rightarrow (\phi \square \hspace{-4.0pt}\rightarrow \bot ))\quad \qquad \quad ({\alpha }0), \text {(MP)}\end{aligned}$$
(A26)
$$\begin{aligned} \lnot&(\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\rightarrow (\phi \square \hspace{-4.0pt}\rightarrow \lnot \psi )\qquad \qquad \qquad \qquad \text {(A26)}, ({\alpha }4), ({\alpha }0), \text {(MP)} \end{aligned}$$
(A27)
Appendix B Proof of Lemma 12
(Part 1) Note that (\({\alpha }3\)) follows from (\({\alpha }1\)) in \(\textsf{CK}\) by applying (Ax1) plus duality principles; (\({\alpha }6\)) can be deduced from (\({\alpha }5\)) similarly. Moreover, (RM\(\square \)) and (T1) can be deduced in \(\textsf{CK}\) in the same way as in \(\textsf{IntCK}\). We sketch the proofs for the remaining axioms and inference rules:
$$\begin{aligned} ({\alpha }2):\,&(\phi \! \square \hspace{-4.0pt}\rightarrow \! \chi )\rightarrow (\phi \square \hspace{-4.0pt}\rightarrow (\lnot (\psi \wedge \chi )\rightarrow \lnot \psi ))\qquad \qquad ({\alpha }0), \text {(MP)}, \text {(RM}\square )\end{aligned}$$
(B28)
$$\begin{aligned}&(\phi \! \square \hspace{-4.0pt}\rightarrow \! \chi ) \! \rightarrow \! ((\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot (\psi \! \wedge \! \chi )) \! \rightarrow \! (\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot \psi ))\, \, \text {(B28)}, \text {(T1)}, ({\alpha }0), \text {(MP)}\!\!\!\end{aligned}$$
(B29)
$$\begin{aligned}&(\phi \! \square \hspace{-4.0pt}\rightarrow \! \chi ) \! \rightarrow \! (\lnot (\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot \psi ) \! \rightarrow \! \lnot (\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot (\psi \! \wedge \! \chi )))\quad \text {(B29)}, ({\alpha }0), \text {(MP)}\!\!\! \end{aligned}$$
(B30)
$$\begin{aligned}&(\phi \! \square \hspace{-4.0pt}\rightarrow \! \chi ) \! \rightarrow \! ((\phi \! \Diamond \hspace{-4.0pt}\rightarrow \! \psi ) \! \rightarrow \! (\phi \! \Diamond \hspace{-4.0pt}\rightarrow \! (\psi \! \wedge \! \chi )))\quad \text {(B30)}, \text {(Ax1)}, ({\alpha }0), \text {(MP)} \end{aligned}$$
(B31)
$$\begin{aligned} ({\alpha }4):\,&(\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\rightarrow (\phi \square \hspace{-4.0pt}\rightarrow \chi ){} & {} \text {premise}\end{aligned}$$
(B32)
$$\begin{aligned}&\lnot (\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot \psi ) \! \rightarrow \! (\phi \! \square \hspace{-4.0pt}\rightarrow \! \chi ){} & {} \text {(B32)}, \text {(Ax1)}, ({\alpha }0), (\text {MP}) \! \! \! \end{aligned}$$
(B33)
$$\begin{aligned}&(\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot \psi ) \! \rightarrow \! (\phi \square \hspace{-4.0pt}\rightarrow (\psi \rightarrow \chi )){} & {} ({\alpha }0), (\text {MP}), (\text {RM}\square )\end{aligned}$$
(B34)
$$\begin{aligned}&(\phi \! \square \hspace{-4.0pt}\rightarrow \! \chi ) \! \rightarrow \! (\phi \! \square \hspace{-4.0pt}\rightarrow \! (\psi \! \rightarrow \! \chi )){} & {} ({\alpha }0), (\text {MP}), (\text {RM}\square )\end{aligned}$$
(B35)
$$\begin{aligned}&\lnot (\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot \psi ) \! \rightarrow \! (\phi \! \square \hspace{-4.0pt}\rightarrow \! (\psi \! \rightarrow \! \chi )){} & {} (\text {B33}), (\text {B35}), ({\alpha }0), (\text {MP})\end{aligned}$$
(B36)
$$\begin{aligned}&{((\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot \psi ) \! \vee \! \lnot (\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot \psi )) \! \rightarrow \! (\phi \! \square \hspace{-4.0pt}\rightarrow \! (\psi \! \rightarrow \! \chi ))}{} & {} (\text {B34}), (\text {B36}), ({\alpha }0), (\text {MP})\end{aligned}$$
(B37)
$$\begin{aligned}&(\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot \psi ) \! \vee \! \lnot (\phi \! \square \hspace{-4.0pt}\rightarrow \! \lnot \psi ){} & {} \text {(Ax1)}\end{aligned}$$
(B38)
$$\begin{aligned}&\phi \! \square \hspace{-4.0pt}\rightarrow \! (\psi \! \rightarrow \! \chi ){} & {} (\text {B37}),(\text {B38}),(\text {MP}) \end{aligned}$$
(B39)
$$\begin{aligned} (\text {RA}\diamond ):\quad&\phi \leftrightarrow \psi \in \textsf{CK}{} & {} \text {premise}\end{aligned}$$
(B40)
$$\begin{aligned}&(\phi \square \hspace{-4.0pt}\rightarrow \lnot \chi )\leftrightarrow (\psi \square \hspace{-4.0pt}\rightarrow \lnot \chi ) \in \textsf{CK}{} & {} (\text {B40}),(\text {RA}\square )\end{aligned}$$
(B41)
$$\begin{aligned}&\lnot (\phi \square \hspace{-4.0pt}\rightarrow \lnot \chi )\leftrightarrow \lnot (\psi \square \hspace{-4.0pt}\rightarrow \lnot \chi ) \in \textsf{CK}{} & {} (\text {B41}),({\alpha }0),(\text {MP})\end{aligned}$$
(B42)
$$\begin{aligned}&(\phi \Diamond \hspace{-4.0pt}\rightarrow \chi )\leftrightarrow (\psi \Diamond \hspace{-4.0pt}\rightarrow \chi ) \in \textsf{CK}{} & {} (\text {B42}),\text {(Ax1)},({\alpha }0),(\text {MP}) \end{aligned}$$
(B43)
$$\begin{aligned} (\text {RC}\diamond ):\quad&\phi \leftrightarrow \psi \in \textsf{CK}{} & {} \text {premise}\end{aligned}$$
(B44)
$$\begin{aligned}&(\chi \square \hspace{-4.0pt}\rightarrow \lnot \phi )\leftrightarrow (\chi \square \hspace{-4.0pt}\rightarrow \lnot \psi )\in \textsf{CK}{} & {} (\text {B44}),({\alpha }0),(\text {MP}),(\text {RC}\square )\end{aligned}$$
(B45)
$$\begin{aligned}&(\chi \Diamond \hspace{-4.0pt}\rightarrow \phi )\leftrightarrow (\chi \Diamond \hspace{-4.0pt}\rightarrow \psi )\in \textsf{CK}{} & {} (\text {B45}),\text {(Ax1)},({\alpha }0),(\text {MP}) \end{aligned}$$
(B46)
Having now every element of \(\mathbb {ICK}\) deduced in \(\textsf{CK}\), we can deduce the remaining parts of Lemma 4 as it was done in Section 3.2.
As for Part 2, note that (Ax0) intuitionistically implies \(\lnot \lnot (\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\leftrightarrow (\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\), whence (Ax1) follows by (T4).
Appendix C Proofs of Some Technical Results from Section 5
All of the sketches in this Appendix are semi-formal but allow for an easy completion into full proofs in any complete Hilbert-style axiomatization of \(\textsf{FOIL}\). The following lemma lists most of the intuitionistic principles assumed in this appendix:
Lemma 1
Let \(\Gamma \cup \{\phi , \psi \} \subseteq \mathcal {L}_{fo}\), and let \(x \in Ind\). Then all of the following statements hold:
In case our formulas get too long, we will be replacing them with their labels, writing e.g. \((C123) \rightarrow (C124)\) instead of \(\phi \rightarrow \psi \) in case \(\phi \) did occur earlier as equation (C123) and \(\psi \) as equation (C124).
Proof of Lemma
15 (Part 1) Consider the following deduction D1 from premises:
$$\begin{aligned}&Sy' \wedge (\forall z)_O(Ezy^{\prime }\leftrightarrow ST_z(\psi )){} & {} \text {premise}\end{aligned}$$
(C47)
$$\begin{aligned}&\forall w(Rxy'w\rightarrow ST_w(\chi )){} & {} \text {premise}\end{aligned}$$
(C48)
$$\begin{aligned}&Sy \wedge (\forall z)_O(Ezy\leftrightarrow ST_z(\psi )){} & {} \text {premise}\end{aligned}$$
(C49)
$$\begin{aligned}&(\forall z)_O(Ezy\leftrightarrow Ezy'){} & {} text{by} (\text {C47}),(\text {C49})\end{aligned}$$
(C50)
$$\begin{aligned}&y \equiv y'{} & {} text{by} (\text {C50}),(\text {Th12})\end{aligned}$$
(C51)
$$\begin{aligned}&\forall w(Rxyw\rightarrow ST_w(\chi )){} & {} text{by} (\text {C48}),(\text {C51}) \end{aligned}$$
(C52)
We now reason as follows:
$$\begin{aligned}&Th, (\text {C47}), (\text {C48})\models _{fo} \forall y(Sy \wedge (\forall z)_O(Ezy\!\leftrightarrow \! ST_z(\psi ))\!\rightarrow \!\forall w(Rxyw\!\rightarrow \! ST_w(\chi ))){} & {} \!\!\!\!\!\!\!\!\!(\text {D1, (DT), (Gen)})\\&Th\models _{fo} \exists y'((\text {C47})\wedge (\text {C48}))\!\rightarrow \! \forall y(Sy \wedge (\forall z)_O(Ezy\leftrightarrow ST_z(\psi ))\!\rightarrow \!\forall w(Rxyw\rightarrow ST_w(\chi ))){} & {} \!\!\!\!(\text {(DT), (Bern)}) \end{aligned}$$
Now the definition of ST yields the result claimed for Part 1. Part 2 is proved by a parallel argument. \(\square \)
Proof of Lemma
16 We proceed by induction on the construction of \(\phi \in \mathcal {L}\).
Basis. If \(\phi = p \in Var\) (resp. \(\phi = \bot , \top \)), then the Lemma follows by (Th6) (resp. (Th7), (Th8)).
Induction step. The following cases are possible:
Case 1. \(\phi = \psi *\chi \), where \(*\in \{\wedge , \vee , \rightarrow \}\). We consider first-order deduction D2:
$$\begin{aligned}&\! Sx\wedge (\forall w)_O(Ewx\leftrightarrow ST_w(\psi )){} & {} \text {premise}\end{aligned}$$
(C53)
$$\begin{aligned}&\! Sy\wedge (\forall w)_O(Ewy\leftrightarrow ST_w(\chi )){} & {} \text {premise}\end{aligned}$$
(C54)
$$\begin{aligned}&\! Sz\wedge (\forall w)_O(Ewz\leftrightarrow (Ewx*Ewy)){} & {} \text {premise}\end{aligned}$$
(C55)
$$\begin{aligned}&\! (\forall w)_O((Ewx*Ewy)\! \leftrightarrow \! (ST_w(\psi )\! *\! ST_w(\chi )))\!\!{} & {} \text {by} (\text {C53}),(\text {C54})\end{aligned}$$
(C56)
$$\begin{aligned}&\! (\forall w)_O(Ewz\leftrightarrow (ST_w(\psi )*ST_w(\chi ))){} & {} \text {by} (\text {C55}),(\text {C56})\end{aligned}$$
(C57)
$$\begin{aligned}&\! \exists z(Sz\!\wedge \! (\forall w)_O(Ewz\!\leftrightarrow \! ST_w(\psi *\chi ))){} & {} \text {by} (\text {C55}),(\text {C57}), \text {def. of} \textit{ST} \end{aligned}$$
(C58)
We now reason as follows:
$$\begin{aligned}&Th, (\text {C53}), (\text {C54}) \models _{fo} \exists z(\text {C55})\rightarrow \exists z(Sz\wedge (\forall w)_O(Ewz\leftrightarrow ST_w(\psi *\chi ))){} & {} (\text {D2}, (\text {DT}), (\text {Bern}))\\&Th, (\text {C53}), (\text {C54}) \models _{fo} Sx\wedge Sy{} & {} \text {(trivially)}\\&Th, (\text {C53}), (\text {C54}) \models _{fo} (Sx\wedge Sy )\rightarrow \exists z(\text {C55}){} & {} (\text {Th9})\\&Th, (\text {C53}), (\text {C54}) \models _{fo}\exists z(Sz\wedge (\forall w)_O(Ewz\leftrightarrow ST_w(\psi *\chi ))){} & {} (\text {MP})\\&Th\models _{fo} \exists x(\text {C53}) \rightarrow (\exists z(\text {C54})\rightarrow \exists z(Sz\wedge (\forall w)_O(Ewz\leftrightarrow ST_w(\psi *\chi )))){} & {} (\text {DT}), (\text {Bern})\\&Th\models _{fo} \exists x(\text {C53}) \wedge \exists y(\text {C54)}{} & {} \text {(IH)}\\&Th\models _{fo}\exists z(Sz\wedge (\forall w)_O(Ewz\leftrightarrow ST_w(\psi *\chi ))){} & {} (\text {MP}) \end{aligned}$$
Case 2. \(\phi = \psi \square \hspace{-4.0pt}\rightarrow \chi \). We consider the following deductions from premises.
Deduction D3:
$$\begin{aligned}&Sy'\wedge (\forall w)_O(Ewy'\leftrightarrow ST_w(\psi )){} & {} \text {premise}\end{aligned}$$
(C59)
$$\begin{aligned}&\forall w(Rxy'w\rightarrow ST_w(\chi )){} & {} \text {premise}\end{aligned}$$
(C60)
$$\begin{aligned}&\exists y(((\text {C59})\wedge (\text {C60}))^y_{y'}){} & {} (\text {C59}), (\text {C60})\end{aligned}$$
(C61)
$$\begin{aligned}&ST_x(\psi \square \hspace{-4.0pt}\rightarrow \chi ){} & {} \text {by (C61), def. of} \textit{ST} \end{aligned}$$
(C62)
Deduction D4:
$$\begin{aligned}&(\text {C59}){} & {} \text {premise}\nonumber \\&Sy\wedge (\forall w)_O(Ewy\leftrightarrow ST_w(\psi )){} & {} \text {premise}\end{aligned}$$
(C63)
$$\begin{aligned}&\forall w(Rxyw\rightarrow ST_w(\chi )){} & {} \text {premise}\end{aligned}$$
(C64)
$$\begin{aligned}&(\forall w)_O(Ewy\leftrightarrow Ewy'){} & {} \text {by} (\text {C59}),(\text {C63})\end{aligned}$$
(C65)
$$\begin{aligned}&y \equiv y'{} & {} \text {by} (\text {C65}),(\text {Th12})\end{aligned}$$
(C66)
$$\begin{aligned}&\forall w(Rxy'w\rightarrow ST_w(\chi )){} & {} \text {by} (\text {C64}),(\text {C66}) \end{aligned}$$
(C67)
D3 and D4 lead to the following intermediate results:
$$\begin{aligned} {Th, (\text {C}59)\models _{fo}\forall w(Rxy'w\rightarrow ST_w(\chi ))\rightarrow ST_x(\psi \square \hspace{-4.0pt}\rightarrow \chi )}\!\!\!{} & {} \text {(D3, (DT))}\end{aligned}$$
(C68)
$$\begin{aligned} {Th, (\text {C}59)\! \models _{fo}\! \exists y((\text {C63})\wedge (\text {C64}))\!\rightarrow \!\forall w(Rxy'w\!\rightarrow \! ST_w(\chi ))}\!\!\!{} & {} \text {(D4, (DT), (Bern))}\end{aligned}$$
(C69)
$$\begin{aligned} {Th, (\text {C}59)\models _{fo}ST_x(\psi \square \hspace{-4.0pt}\rightarrow \chi )\rightarrow \forall w(Rxy'w\rightarrow ST_w(\chi ))}\!\!\!{} & {} ((\text {C69}), \text {def. of} \textit{ST})\end{aligned}$$
(C70)
$$\begin{aligned} {Th, (\text {C}59)\! \models _{fo}\! \forall x(ST_x(\psi \!\square \hspace{-4.0pt}\rightarrow \!\chi )\!\leftrightarrow \!\forall w(Rxy'w\!\rightarrow \! ST_w(\chi )))}\!\!\!{} & {} \text {(C68), (C70), (Gen)} \end{aligned}$$
(C71)
We now feed these results into the next deduction D5:
$$\begin{aligned}&(\text {C59}){} & {} \text {premise}\nonumber \\&Sz\wedge (\forall w)_O(Ewz\leftrightarrow ST_w(\chi )){} & {} \text {premise}\end{aligned}$$
(C72)
$$\begin{aligned}&Sy'\wedge Sz{} & {} \text {by} (\text {C59}), (\text {C72})\end{aligned}$$
(C73)
$$\begin{aligned}&\exists z'(\forall x)_O(Exz'\leftrightarrow \forall w(Rxy'w\rightarrow Ewz)){} & {} \text {by} (\text {C73}), (\text {Th10})\end{aligned}$$
(C74)
$$\begin{aligned}&\exists z'(\forall x)_O(Exz'\leftrightarrow \forall w(Rxy'w\rightarrow ST_w(\chi ))){} & {} \text {by} (\text {C72}), (\text {C74})\end{aligned}$$
(C75)
$$\begin{aligned}&\exists z'(\forall x)_O(Exz'\leftrightarrow ST_x(\psi \square \hspace{-4.0pt}\rightarrow \chi )){} & {} \text {by} (\text {C75}), (\text {C71}) \end{aligned}$$
(C76)
We now finish our reasoning as follows:
$$\begin{aligned} Th\models _{fo}\exists y'(\text {C59}) \rightarrow (\exists z(\text {C72}) \rightarrow \exists z'(\forall x)_O(Exz'\leftrightarrow ST_x(\psi \square \hspace{-4.0pt}\rightarrow \chi ))){} & {} (\text {D5, (DT), (Bern)})\\ Th\models _{fo} \exists y'(\text {C59}) \wedge \exists z(\text {C72}){} & {} \text {(IH)}\\ Th\models _{fo}\exists z'(\forall x)_O(Exz'\leftrightarrow ST_x(\psi \square \hspace{-4.0pt}\rightarrow \chi ))){} & {} (\text {MP}) \end{aligned}$$
Case 3. \(\phi = \psi \Diamond \hspace{-4.0pt}\rightarrow \chi \). Parallel to Case 2.
Proof of Proposition
5 We show that the standard translation of every axiom of \(\mathbb {ICK}\) first-order follows from Th and that the rules of \(\mathbb {ICK}\) preserve this property. First, note that every instance of (\({\alpha }0\)) is translated into an instance of (\({\alpha }0\)) and hence a \(\textsf{FOIL}\)-valid formula; the same is true for every instance of (\({\alpha }6\)). By Lemma 16, we also know that every instance of (\({\alpha }5\)) first-order-follows from Th. Next, the applications of (MP) translate into applications of this same rule (MP), and the applications of every rule in the set {(RA\(\square \)), (RC\(\square \)), (RA\(\diamond \)), (RC\(\diamond \))} translate to applications of some \(\textsf{FOIL}\)-deducible rule. It remains to consider the instances of axiomatic schemas (\({\alpha }1\))-(\({\alpha }4\)), which is a tedious but straightforward exercise in first-order intuitionistic reasoning. We display the reasoning for (\({\alpha }4\)) as an example.
Let \(\phi ,\psi ,\chi \in \mathcal {L}\). Consider the following first-order deduction D6 from premises:
$$\begin{aligned}&ST_x(\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\rightarrow ST_x(\phi \square \hspace{-4.0pt}\rightarrow \chi ){} & {} \text {premise}\end{aligned}$$
(C77)
$$\begin{aligned}&Sy\wedge (\forall z)_O(Ezy\leftrightarrow ST_z(\phi )){} & {} \text {premise}\end{aligned}$$
(C78)
$$\begin{aligned}&Rxyw\wedge ST_w(\psi ){} & {} \text {premise}\end{aligned}$$
(C79)
$$\begin{aligned}&\exists w(Rxyw\wedge ST_w(\psi )){} & {} \text {by} (\text {C79})\end{aligned}$$
(C80)
$$\begin{aligned}&\exists y((\text {C78})\wedge ){} & {} \text {by} (\text {C78}), (\text {C80})\end{aligned}$$
(C81)
$$\begin{aligned}&ST_x(\phi \Diamond \hspace{-4.0pt}\rightarrow \psi ){} & {} \text {by} (\text {C81}), \text {def. of} \textit{ST}\end{aligned}$$
(C82)
$$\begin{aligned}&ST_x(\phi \square \hspace{-4.0pt}\rightarrow \chi ){} & {} \text {by} (\text {C77}), (\text {C82})\end{aligned}$$
(C83)
$$\begin{aligned}&\forall y(Sy \wedge (\forall z)_O(Ezy\leftrightarrow ST_z(\phi )))\rightarrow \nonumber \\&\qquad \qquad \qquad \qquad \rightarrow \forall w(Rxyw\rightarrow ST_w(\chi ))){} & {} \text {by} (\text {C83}), \text {Lemma 15}\end{aligned}$$
(C84)
$$\begin{aligned}&\forall w(Rxyw\rightarrow ST_w(\chi )){} & {} \text {by} (\text {C78}), (\text {C84})\end{aligned}$$
(C85)
$$\begin{aligned}&ST_w(\chi ){} & {} \text {by} (\text {C79}), (\text {C85}) \end{aligned}$$
(C86)
We now reason as follows:
$$\begin{aligned}&Th, (\text {C77}), (\text {C78})\models _{fo} \forall w(Rxyw \rightarrow (ST_w(\psi ) \rightarrow ST_w(\chi ))){} & {} (\text {D6}, (\text {DT}), (\text {Gen}))\\&Th, (\text {C77}), (\text {C78})\models _{fo} \forall w(R(x,y,w) \rightarrow ST_w(\psi \rightarrow \chi )){} & {} \text {(def. of { ST})}\\&Th, (\text {C77}), (\text {C78})\models _{fo} \exists y((\text {C78})\wedge \forall w(Rxyw \rightarrow ST_w(\psi \rightarrow \chi )))\\&Th, (\text {C77}), (\text {C78})\models _{fo} ST_x(\phi \square \hspace{-4.0pt}\rightarrow (\psi \rightarrow \chi )){} & {} \text {(def. of { ST})}\\&Th, (\text {C77})\models _{fo} \exists y(\text {C78})\rightarrow ST_x(\phi \square \hspace{-4.0pt}\rightarrow (\psi \rightarrow \chi )){} & {} (\text {DT}), (\text {Bern})\\&Th\models _{fo} \exists y(\text {C78}){} & {} (\text {Lemma 16})\\&Th, (\text {C77})\models _{fo}ST_x(\phi \square \hspace{-4.0pt}\rightarrow (\psi \rightarrow \chi )){} & {} (\text {MP})\\&Th\models _{fo}(\text {C77})\rightarrow ST_x(\phi \square \hspace{-4.0pt}\rightarrow (\psi \rightarrow \chi )){} & {} (\text {DT})\\&Th\models _{fo}ST_x(((\phi \Diamond \hspace{-4.0pt}\rightarrow \psi )\rightarrow (\phi \square \hspace{-4.0pt}\rightarrow \chi ))\rightarrow (\phi \square \hspace{-4.0pt}\rightarrow (\psi \rightarrow \chi ))){} & {} (\text {def. of}\,\, ST) \end{aligned}$$