On the No-Counterexample Interpretation

Relative consistency and interpretations (03F25) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Review text

In this paper essentially the question is treated whether G. Kreisel's no-counterexample interpretation (nci) passes from the premisses of an inference by modus ponens (mp) to the conclusio. This property is investigated for different theories and different kinds of the formulas involved. There are different solutions depending on whether the mp-inferences of a proof are considered simultaneously (global) or individually (local). Starting position is \textit{G. Kreisel}'s paper in J. Symb. Log. 16, 241-267 (1951; Zbl 0044.00302), especially the conditions (\(\gamma\)) and (\(\delta\)) for nci (page 245). In J. Symb. Log. 17, 43-58 (1952; Zbl 0046.00701), \textit{G. Kreisel} shows that the nci of \textbf{PA} by the \(\alpha(<\varepsilon_0\))-recursive functionals satisfies the conditions \((\alpha)-(\delta)\) of the first cited paper. He uses \(\varepsilon\)-substitution. This global result, which also holds if the \(\alpha(<\varepsilon_0\))-recursive functionals are replaced by Gödel's \(T\), can also be gained, following the paper of \textit{H. Schwichtenberg} in Handbook of mathematical logic, ed. by J. Barwise, Amsterdam: North Holland, 867-895 (1977; Zbl 0443.03001), using cut elimination. In this case induction on the length of the proof leads to the question of transferring nci along an mp-inference. This is a local transformation, and from this fact the paper gets its substance. Very subtle examinations give rise to plenty of results of which the following may be mentioned: Let \(T_n\) be the subsystem of Gödel's \(T\) such that the recursor \(R_\varrho\) is used only for types \(\varrho\) with \(\deg(\varrho)\leq n\). For in \textbf{PA} provable sentences \(A\) and \(A\rightarrow B\), no fixed \(T_n\) suffices for mp-nci. The whole system \(T\) is needed. For arbitrary sentences \(A\) and \(A\rightarrow B\) of the language of \textbf{PA}, not necessarily provable in \textbf{PA}, even \(T\) does not suffice to solve the nci of mp. \(\widehat{\mathbf{PR}}^\omega+{\mathbf{BR}}_{0,1}\) is needed instead, \(\widehat{\mathbf{PR}}^\omega\) being the set of predicative primitive functionals of finite type and \(\mathbf{BR}_{0,1}\) the schema of bar recursion of type 0 with values of type 1. On the other hand \textbf{PA}\(^\omega\) and \(T\) are sufficient for the local nci of the mp-rule. Finally the author investigates the relationship between \textit{G. Kreisel}'s concept of nci from the first paper cited above and J. Symb. Log. 23, 155-182 (1959; Zbl 0088.01502), where the already mentioned condition (\(\delta\)) is replaced by another condition (\(\delta'\)). He states that both conditions are incomparable: Kreisel already mentions in the first paper cited above that (\(\delta\)) does not imply (\(\delta'\)) in a special trivial case. The author shows that the nci of \textbf{PA}\(_{n+1}\) in \(T_n\) satisfies (\(\delta'\)) but not (\(\delta\)), \textbf{PA}\(_{n+1}\) being the fragment of \textbf{PA} with \(\Sigma^0_{n+1}\)-induction only. The paper contains a wealth of results and remarks. A net of references connects them to the bibliography. This leads to a glimpse of intricacy. Some concepts are mentioned before their definition. The paper is not at all a survey article but presents plenty of valuable material for experts.

Recommendations

Cites work

Cited in

(20)

This page was built for publication: On the No-Counterexample Interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4948521)