New formally undecidable propositions: Non-trivial lower bounds on proof complexity and related theorems (Q804570)

The `non-trivial' lower bounds (in the title) are shown to share several formal properties of consistency; especially in Hilbert's (cute) form, which he advertised by the slogan: from a proof of \(\perp\) follows the rest (cf. the \(\perp\)-rule on p. 175). Thus the paper serves very well, in effect if not on purpose, to review the conflict between (i) Gödel's view, 60 years ago, of his second theorem as (\textit{merkwürdig}, which means in Austrian German) a curiosity, and (ii) the popular view of its far-reaching significance; cf. the opening sentence on p. 169 (though the relevance of the particular `support' cited there is above this reviewer's head). Gödel's case, in scattered remarks (in his Königsberg lecture, the footnote \(48^ a\) of his paper etc.), is simple enough. (a) Consistency is a poor criterion (for significance): mathematically non-trivial principles are consistent, but the converse is patently false. (b) Familiar principles are usually seen to be consistent by interpretations which patently do not rely solely on the principles themselves. Tacitly, (c) if there is genuine doubt about the consistency of (other) principles, it is \textit{peu sérieux} to restrict methods of proof for consistency. During the last 60 years new rules of proof have been considered, for which other formulations of consistency and of the second theorem are suitable. Thus (d) cut-free rules are quite prominent, both in logic texts and in the only area where it is at all practical to restrict in advance rules of proof (automatic theorem-proving, overlooked on p. 176, l. 10 and elsewhere). Such rules prove their own Hilbert consistency. Also (e) suitable modifications of the rules, of which the canonical representation is the provability predicate used - but not interpreted - in Rosser's `trick', prove their own consistency (in its ordinary sense, but not their \(\Sigma^ 0_ 1\)-completeness); besides recalling the effort spent in practice on cross checks of proofs, and not recorded at all in more usual systems (overlooked on p. 176, l. 11 and elsewhere). The results underline most vividly Gödel's view; beginning with (a), where `non-trivial', quaintly, means merely: above a particular bounding function associated with Hilbert's advertisement. Like consistency, the `new formally undecidable propositions' are also of \(\Pi^ 0_ 1\) form, and so of no computational significance, though possibly useful cross checks in exercises of would-be computer science; `would-be' when it \textit{assumes} (like p. 180), bottom) that general or logically familiar classes of formulae, which are defined in syntactic \((=\) formalist) terms, are computationally rewarding; instead of searching for special classes that are (and which the author set out to avoid, p. 180, l. -6). For the present (re)view the paper is not spoilt by its otherwise quite staggering aberrations such as the indiscriminate list of independence results on p. 174. They are all supposed to be related to Gödel's - twist on Cantor's diagonal - argument (cf. p. 170, l. 2). In fact, von Neumann's (set-theoretic representation of the ordinal) \(\omega +\omega\), in II, was known during Gödel's schooldays to be - in modern terms, even second-order - independent of Zermelo's Z. The cases in (III) and (IV) require much more specific arguments; such as Gentzen's in proof theory or Paris' in the model theory of arithmetic. Reviewer's note in connection with (e) above. D. de Jongh recently solved the open question in the literature cited on p. 176, l. 4 and elsewhere; specifically, in a letter (of 5.IX. 1991) to the reviewer. The upshot is that Rosser's original variants of familiar formal rules for first-order arithmetic do not prove their own consistency. This is shown by use of the fact that those rules satisfy Hilbert's slogan far beyond the requirements (on p. 175) for a \(\perp\)-calculus.