zbMATH — the first resource for mathematics

Much shorter proofs: A bimodal investigation. (English) Zbl 0697.03033
R. Parikh [J. Symb. Logic 36, 494-508 (1971; Zbl 0243.02037)] proved the existence of provable \(\Sigma_ 1\)-formulas p such that the shortest proof of p is much longer than the shortest proof of provability of p. This was based on the fact that Parikh’s theorem has only provable fixed points. In previous work the authors characterized other pairs of modal formulas which can stand here instead of “p is provable” and “p is provably provable”. Now they extend their treatment to the situation where different occurrences of “provable” refer to different theories.
Reviewer: G.Mints

03F20 Complexity of proofs
03B45 Modal logic (including the logic of norms)
Full Text: DOI