Undecidability of the Problem of Recognizing Axiomatizations of Superintuitionistic Propositional Calculi |
| |
Authors: | Evgeny Zolin |
| |
Institution: | 1. Department of Mathematical Logic and Theory of Algorithms, Faculty of Mathematics and Mechanics, Moscow State University, Moscow, Russia
|
| |
Abstract: | We give a new proof of the following result (originally due to Linial and Post): it is undecidable whether a given calculus, that is a finite set of propositional formulas together with the rules of modus ponens and substitution, axiomatizes the classical logic. Moreover, we prove the same for every superintuitionistic calculus. As a corollary, it is undecidable whether a given calculus is consistent, whether it is superintuitionistic, whether two given calculi have the same theorems, whether a given formula is derivable in a given calculus. The proof is by reduction from the undecidable halting problem for the so-called tag systems introduced by Post. We also give a historical survey of related results. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|