Intuitionistic validity in \(T\)-normal Kripke structures (Q685055)

Given any classical first-order theory \(T\), the author considers the set \({\mathcal H} T\) of all first-order sentences that are valid in every \(T\)- normal Kripke structure. A Kripke structure may be considered as a partially ordered set of classical structures and it is called \(T\)-normal iff each of these classical structures is a classical model of \(T\). The author's main motivation for studying such structures is his wish to extend model-theoretic techniques from classical logic to intuitionistic logic. He gives a very nice and surprising characterization of \({\mathcal H} T\): it is the set of all sentences that may be proved by intuitionistic logic from formulas of the form \(\theta^ \phi \to \phi\) where \(\theta\) is a semipositive formula (that is, each subformula of the form \(\theta_ 1\to \theta_ 2\) has \(\theta_ 1\) atomic; observe that \(\neg\psi\) abbreviates \(\psi\to \perp)\), \(\neg\theta\) follows by classical logic from \(T\), and \(\theta^ \phi\) is obtained from \(\theta\) by replacing each atomic subformula \(\chi\) of \(\theta\) by \(\chi\vee \phi\). In fact, \(\theta^ \phi\) is H. Friedman's \(\phi\)-translation of \(\theta\) [see \textit{H. Friedman}, Lect. Notes Math. 669, 21-27 (1978; Zbl 0396.03045)]. As a special case the author considers Peano arithmetic PA. He shows that \({\mathcal H}\text{PA}\) proves (intuitionistically) \(\Sigma_ 1^ 0\)-induction, and, using a very nice argument, that \({\mathcal H}\text{PA}\) does not prove \(\Pi_ 1^ 0\)-induction: \({\mathcal H}\text{PA}\) is a proper subtheory of Heyting arithmetic HA. The author concludes his paper with some questions. I have one more to ask: is it possible to make sense of the notion of a \(T\)-normal Kripke structure from an intuitionistic point of view, that is, if one uses an intuitionistic metalanguage?