Characteristic formulas of partial Heyting algebras (Q2392011)

The notion of a characteristic (or Jankov) formula (introduced by \textit{V. A. Yankov} [Sov. Math., Dokl. 4, 1203--1204 (1963); translation from Dokl. Akad. Nauk SSSR 151, 1293--1294 (1963; Zbl 0143.25201)] is one of the very useful notions in the study of Heyting algebras. If \(\mathcal{U}\) is a finite subdirectly irreducible algebra, we can associate a formula \(\mathcal{J(U)}\) with the following properties: (Hom) If a formula \(\mathcal{J(U)}\) is refutable in algebra \(\mathcal{B}\), then algebra \(\mathcal{U}\) is embeddable into a quotient algebra of algebra \(\mathcal{B}\); (Ded) If a formula A is refutable in algebra \(\mathcal{U}\), then \(A\vdash\mathcal{J(U)}\), where \(\vdash\) is the derivability in intuitionistic propositional calculus (IPC) with substitution. Thus, a characteristic formula is the weakest formula among the formulas refutable in \(\mathcal{U}\) relative to derivability. In this paper, the author extends the idea of a Jankov formula to finite partial algebras. He introduces the characteristic formulas of finite partial algebras, studies the properties of these formulas and proves that any intermediate logic can be axiomatized by such formulas. Also, the correlations between characteristic formulas of finite partial algebras with canonical formulas are presented. In the final part, the author outlines how to construct characteristic formulas for finite partial algebras in varieties of Hilbert algebras with additional operations having congruence extension property and equationally definable principal congruences or, more generally, in regular varieties (because all we need to construct a characteristic formula of finite partial algebra is an implication with regular properties).