Jankov-style Formulas and Refutation Systems
Jankov-style Formulas and Refutation Systems

Summary/Abstract: The paper studies the logics which algebraic semantics comprises of the Hilbert algebras endowed with additional operations - the regular algebras. With any finite subdirectly irreducible regular algebra one can associate a Jankov formula. In its turn, the Jankov formulas can be used as anti-axioms for a refutation system. It is proven that a logic has a complete refutation system based on Jankov formulas if and only if this logic enjoys finite model property. Also, such a refutation system is finite, that is, it contains a finite number of axioms and anti-axioms, if and and only if the logic is tabular.

• Details
• Contents