On finite linear intermediate predicate logics (Q1119624)

The paper deals with first-order predicate intermediate logics. For each \(n\geq 1\) let \(LP_ n^+\) be the logic of all Kripke frames (with varying domains) of height n. S. Yokota found a finite axiomatization for \(LP^+_ n\) (unpublished): \(LP^+_ n=HPC+\tilde P_ n\); here HPC is Heyting predicate calculus, and \(\tilde P_ 1=\forall x(p_ 1(x)\vee \neg p_ 1(x))\), \(\tilde P_ n=\forall x(p_ n(x)\vee (p_ n(x)\supset \tilde P_{n-1}))\). The author considers logics \(S^+_ n=LP^+_ n+(p\supset q)\vee (q\supset p)\) and constructs corresponding cut-free sequent calculi \(GS_ n\). \(GS_ n\) is proved to be strongly Kripke-complete: a sequent is provable in \(GS_ n\) iff it is valid in any linear Kripke frame of height n. It is worth noticing that completeness theorems for \(S^+_ n\) and \(LP^+_ n\) are non-trivial because these logics are not just quantified versions of corresponding propositional logics (quantified versions of propositional intermediate logics of finite slices are known to be Kripke-incomplete [the author, Rep. Math. Logic 15, 41-58 (1983; Zbl 0519.03016)].