蕴涵命题演算公理化识别问题的不可判定性
逻辑
2015-09-25 v1 计算机科学中的逻辑
摘要
本文研究了作为直觉主义蕴涵命题演算有限公理化扩展的命题演算，并包含假言推理和代入规则。我们证明了针对这些演算的以下问题的不可判定性：给定的有限命题公式集是否构成固定命题演算的充分公理系统。此外，我们证明了该问题以下限制情形的同样结论：给定固定命题演算的有限定理集是否可推导出该演算的所有定理。这些结果的证明基于对 Post 引入的标签系统不可判定停机问题的归约。
引用
@article{arxiv.1407.7010,
title = {Undecidability of the problem of recognizing axiomatizations for implicative propositional calculi},
author = {Grigoriy V. Bokov},
journal= {arXiv preprint arXiv:1407.7010},
year = {2015}
}
备注
13 pages