Extendible formulas in two variables in intuitionistic logic (Q454378)

The paper presents alternative characterizations of exactly provable, extendible and projective formulas in intuitionistic propositional calculus (IPC) using \(n\)-universal models and definable \(p\)-morphisms between them. The notions of exactly provable formulas (also known as exact formulas) of extendible formulas and of projective formulas were introduced respectively by the second author in [Stud. Logic Found. Math. 110, 51--64 (1982; Zbl 0547.03037)], by the second author and \textit{A. Visser} in [in: Logic: from foundations to applications. European logic colloquium, Keele, UK, 1993. Oxford: Clarendon Press. 187--213 (1996; Zbl 0857.03041)] and by \textit{S. Ghilardi} in [J. Symb. Log. 64, No. 2, 859--880 (1999; Zbl 0930.03009)]. For an overview on \(n\)-universal models of IPC see [\textit{A. Chagrov} and \textit{M. Zakharyaschev}, Modal logic. Oxford: Clarendon Press (1997; Zbl 0871.03007)]. From the new characterizations above, the authors give an alternative proof of the fact that every exact formula is extendible; every projective formula is exact and extendible; and they obtain an alternative proof of Ghilardi's theorem (for the restricted case of formulas in two variables) -- every extendible formula is projective. Moreover, a new syntactic description of all (infinitely many) extendible formulas of IPC in two variables is derived.