Proof Verification Can Be Hard!

TL;DR

This paper challenges the common belief that proof verification is always easy, highlighting that certain inference rules like the restricted ω-rule make proof verification computationally hard, especially in more powerful proof systems.

Contribution

It demonstrates that proof verification can be computationally hard when powerful inference rules are used, contrary to conventional wisdom in proof systems.

Findings

Proof verification becomes non-semi-decidable with the restricted ω-rule.

Traditional proof systems have easier verification, but more powerful rules increase complexity.

Hardness of proof verification is under-appreciated in many proof-related communities.

Abstract

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 {\omega}-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.