Decidability of quantified propositional intuitionistic logic and S4 on trees of height and arity \(\leq \omega\) (Q1826435)

The long title describes the contents of this article, but not the context. In J. Symb. Log. 62, 529--544 (1997; Zbl 0887.03002), \textit{P. Kremer} showed that the set of quantified propositional formulas, valid with respect to all the Kripke structures (i.e., quasi-order with the minimal element), is highly undecidable; indeed, it is recursively isomorphic to the valid second-order formulas. He left open the problem: what happens if structures are confined to tree orders. The author answers this by showing the decidability in this setting. Actually, he considers three classes of structures: all the trees as described in the title, the exactly \(n\)-branching full tree, and the finite trees. In each of these classes, the set of valid formulas is decidable. He reduces the problem to the 1969 vintage result of \textit{M. O. Rabin} on the decidability of the second-order tree language [Trans. Am. Math. Soc. 141, 1--35 (1969; Zbl 0221.02031)] by giving a translation of intuitionism formulas to tree formulas. Modal system S4 is similarly shown to be decidable. The author also considers the case when the structures are linear orders of various kinds [Gödel-Dummet logics], and cites a number of open problems.