Proof Verification Can Be Hard!
Naveen Sundar Govindarajulu, Selmer Bringsjord · arXiv (Cornell University) · 2017
The generally accepted wisdom in computational circles is that pure proof verification is a solved problem and that the computationally hard elements and fertile areas of study lie in proof discovery. This wisdom presumably does hold for conventional proof systems such as first-order logic with a standard proof calculus such as natural deduction or resolution. But this folk belief breaks down when we consider more user-friendly/powerful inference rules. One such rule is the restricted ω-rule, which is not even semi-decidable when added to a standard proof calculus of a nice theory. While presumably not a novel result, we feel that the hardness of proof verification is under-appreciated in most communities that deal with proofs. A proof-sketch follows.