Abstract
The main issue of this chapter concerns how the epistemic benefits of an ideal system may come to be distributed over it. In particular, we are interested in whether they are evenly or unevenly distributed over it; where to say that the epistemic benefits of T are evenly distributed over it is to say that there is no isolable subsystem of T containing all or nearly all of its humanly useful ideal proofs. When the epistemic benefits of a system can be compressed into one of its parts, we say that the system is “localizable”.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
Notes
For a discussion concerning theoretical or in-principle limitations, see Gandy [1982] and Dummett [1975].
Since in giving this argument, we rely heavily upon the Thesis of Strict Instrumentalism, it seems only proper that we entitle the ensuing problem for the SA the “Problem of Strict Instrumentalism”.
Actually, as we shall see later on in the discussion of the Convergence Problem, there is no inherent need to make the estimated upper bound on finitary reasoning and the estimated lower bound on the ideal method be the same theory. One need only require that the former be a subsystem of the latter, and then prove G2 in the following (strengthened) form: not- ~F, Con(F2) (where F, is the estimated upper bound on finitary reasoning, and F2 the estimated lower bound on the ideal method).
By a “logically proper subset” of T’s axioms, we mean a subset of T’s axioms that does not imply, on T’s logic, all of T’s axioms.
Part of the reason why the instrumentalist has an affinity for conditional localization is because of his capacity for unconditional localization. This capacity, in turn, is based upon the TSI; i.e., the belief that only a finite portion of the proofs of an ordinary ideal system are efficient enough to be put to any gainful epistemic use. Because he believes this, the thought (which is fundamental to conditional localization) that he might have to make do with a finite part of an ideal system’s resources is not an unduly troubling one to the instrumentalist.
There may, however, be a negative connection. That is, there may be systems (e.g., system V of Theorem 1.5 of Jerslow 119761) that are too weak to sustain G2.
Actually, our argument shall deal with the unconditional localizations of only a subclass of the usual systems; namely, the so-called reflexive systems (e.g., PA and ZF). We shall define the notion of reflexivity shortly.
In calling a formal system an upper bound on finitary thought, the advocate of the Standard Strategy is not committed to saying that the proofs or reasonings of finitary thought are expressed by derivations in the system, but only that the results (i.e., the conclusions or “theorems”) of such reasoning are expressed by theorems of the system. This is a result of the fact that in order to refute the Hilbertian’s program for a given ideal system S, he need only show that its consistency is not finitarily provable; and in order to do this, he need only supplement a proof of G2 for S with an argument to the effect that its consistency is finitarily provable only if Con(S) is a theorem of S.
Strictly speaking, of course, it is not just the size of the useful product that counts, but the degree of its usefulness (i.e., the degree of its efficiency and reliability) as well. However, since such considerations are not particularly germane to the present argument, they will not be emphasized.
This just reiterates the by now familiar claim that the Replacement Strategy cannot be based upon an unsystematic (i.e., case-by-case) approach to the soundness problem, since such an approach entails use of the very 0-methods that M-replacement is intended to avoid.
For a “direct” proof of this see Ryll-Nardzewski [1952]. And for a proof based upon the reflexivity of PA and an appeal to G2, see Mostowski [1952], or Montague [1957]. By calling PA non-finitely axiomatizable, we mean that the theorem-set of PA is not the logical closure of any finite set of its axioms.
Put less roughly, T (a system based on an infinite number of axioms) is reflexive if and only if for every system TF based on a finite number of T’s axioms, Con(TF) (i.e., the “usual” formula of T taken to express TF’s consistency) is provable in T.
After all, G2 is proven for Q in Bezboruah and Shepherdson [1976], and it doesn’t seem implausible to suppose that PAH will include Q. At any rate, we won’t contest such an assumption.
Of course some of the real theorems eliminated by (i) are eliminated nonprovisionally. This is true, for example, of those real theorems which are themselves so long and/or complex that any proof containing them must, by the very fact of that containment, be unfeasible. We are, however, not very interested in such cases, since what we really want to know is whether all feasible finitary reasoning is codifiable in PAH; and the elimination of theorems which are themselves unfeasible still leaves this possibility open.
So, we are interested in condition (i) because of its capacity to potentially eliminate feasibly complicated real theorems. But why? The answer, once again, is that the Hilbertian is interested only in gainful applications of the Metamathematical Replacement Strategy. And since any such application must be based upon a manageable proof of real-soundness, it follows that unfeasibly complicated real theorems can play no part in carrying out the Hilbertian’s program. Thus, the question of crucial interest to him is not whether PAH subsumes all of finitary thought, but whether it subsumes all of feasible finitary thought.
Could condition (i) lead to the elimination of anything but real theorems that are themselves unfeasible? The answer is `yes’. For it is at least possible that there are axioms of PA which appear only in unfeasible proofs of feasible theorems (i.e., theorems which are not by themselves so complicated as to be unfeasible). Still, we do not believe that the eliminations authorized by condition (i) cast nearly so much suspicion on PAH’s ability to serve as a bound on feasible finitary proof as those authorized by condition (ii). Therefore, most of our case against PAH is to be seen as resting upon condition (ii). h In other words, even if R is a real formula having only problematic real proofs, it does not necessarily follow that the Hilbertian will back some ideal proof of R. For if the ideal proofs of R are themselves long and complex enough, there may be no gain in replacing the problematic 0-proofs of R with an M-proof.
It should be noted that the real theorems of PA potentially eliminated by condition (ii) need not be unfeasible. In fact they might be highly feasible and provable by highly feasible ideal proofs. This is so because a real theorem’s being provable by means of a highly feasible ideal proof does not prohibit it’s also being provable by means of a highly feasible real proof. Thus, condition (ii) targets a different class of eliminations than condition (i).
We do not believe that there is any point to considering the case where PRA is taken as a lower bound on ideal reasoning. For inasmuch as PRA is taken to be a formalization of finitary reasoning, the Hilbertian is neither obliged to nor interested in proving its soundness.
Note that such a result cannot be derived from G2 for PAH since there are no grounds for believing that PRA is a subsystem of PAH.
Of course, the unconditional localization associated with Hilbertian residues, and the conditional localization associated with Rosser formalization have quite different bearings on the traditional assessment of Hilbert’s Program. The former suggests that the usual formalizations of ideal mathematics are too strong, and that if we weaken them appropriately, we either lose G2 for the weakened system, or the Convergence Problem becomes unsolvable (i.e., the weakened system doesn’t subsume finitary reasoning, so that even if G2 does hold for it, no anti-Hilbertian conclusion ensues). The latter, on the other hand, attacks the very idea of there being a connection between the mathematical strength of a formal system, and G2’s holding of it. And since belief in such a connection is so deeply embedded in the Standard Strategy, it follows that the challenge raised by Rosser formalization penetrates to the very heart of the Gödelian’s tactics.
It is worth noting that the Hilbertian could claim a large degree of success for his program even if he couldn’t carry it out for the full range of useful ideal methods. Thus, if he could satisfactorily establish the reliability only of that part of ideal mathematics that is responsible for most of its efficiency, he could claim a large measure of success for his program. Hilbertian instrumentalism therefore appears to have considerable built-in resiliency; so long as there is some class of 0-proofs whose replacement by M-proofs yields a significant epistemic gain, the Replacement Strategy (i.e., Hilbert’s Program) will admit of significant application.
That is, we have not shown that the real-soundness of our localizations of the usual systems (e.g., PAH and PAR) can be proven finitarily.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1986 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Detlefsen, M. (1986). The Convergence Problem and the Problem of Strict Instrumentalism. In: Hilbert’s Program. Synthese Library, vol 182. Springer, Dordrecht. https://doi.org/10.1007/978-94-015-7731-1_5
Download citation
DOI: https://doi.org/10.1007/978-94-015-7731-1_5
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-8420-0
Online ISBN: 978-94-015-7731-1
eBook Packages: Springer Book Archive