Proof analysis in intermediate logics (Q661286)

The authors continue the investigation of cut-free systems for superintuitionistic logics inspired by translating a formula \(F\) into a formula saying ``\(F\) is true in all Kripke models'' (of a given logic). The approach works smoothly when the condition on the accessibility relation in Kripke models is expressed by a geometric formula \(\forall\bar{Z}P\rightarrow \exists\bar{x}M\) where \(P\) is a conjunction of atomic formulas and \(M\) is a disjunction of conjunctions of atomic formulas.