Undecidability of the Problem of Recognizing Axiomatizations of Superintuitionistic Propositional Calculiстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 26 августа 2016 г.
Аннотация:Получено более простое доказательство, по сравнению с известным с 1963 г доказательством А.В.Кузнецова, результата о неразрешимости проблемы распознавания полноты произвольной конечной системы аксиом для произвольного фиксированного расширения интуиционистского исчисления высказываний. Доказательство основано на сведении к данной проблеме так называемой проблемы остановки для однородных систем продукций Поста; неразрешимость последней проблемы была установлена Минским в 1961 г. Дается обзор известных результатов в области алгоритмической распознаваемости свойств пропозициональных исчислений. ==========================================================================
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.