Subproject IV: Ideal Elements and Ideals of Efficiency
Efficiency & the
Evaluation of Hilbert's Program 
Efficiency considerations appear to have important ramifications for the proper understanding and evaluation of Hilbert's Program. Generally speaking, Hilbert prized the use of ideal elements for the efficiency or convenience it represented. Somewhat more accurately, he believed that proofs making use of ideal elements/methods were sometimes, in fact often, easier to discover than proofs exclusively employing the contentual methods of finitary reasoning. This suggests that the uses of ideal elements/methods that Hilbert really wanted to preserve were those that represent some gain in efficiency as compared to their simplest or most efficient finitary counterparts.
For ease of expression, let's
introduce some terminology. Call an ideal proof 
I
of a real theorem ρ
gainful
if I
is easier to discover than any purely real proof of ρ.
Further, for a given system 
that formalizes a body
of ideal reasoning let gain
be the set of theorems that
results from removing from
all real theorems of
for which there is no gainful ideal proof in .1
I
believe there is an historically and philosophically
plausible interpretation of Hilbert according to which his fundamental
commitment was to defend not the ideal methods per se,
but the gainful
ideal methods.
This raises questions
concerning the traditional evaluation of Hilbert's Program. The
reasoning behind that evaluation characteristically relies on a premise
to the effect that what Hilbert classified as real
(or finitary)
reasoning is a subsystem of the ideal reasoning to the proof of whose
consistency Hilbert was properly committed. This premise, however, is
open to doubt, even for someone who may accept that all finitary
reasoning is formalizable in . For in those cases where gain
is a subset of the theorems of , it
may be that gain
is axiomatizable by a set of axioms
weaker than the axioms of . This being so, it cannot
reasonably be maintained, without further argument, that the
consistency of gain
is finitarily provable only if the
consistency of is.
This in itself, of course,
gives no positive reason to believe that Hilbert's Program can be
carried out, either in whole or in significant part. It does, however,
suggest that the ultimate evaluation of Hilbert's Program is more
subtle and complex than it has generally been taken to be. The
following questions are indicative of some of this complexity.
Problems IV.1-4
1. What are the conditions that a concept of efficiency of the sort Hilbert had in mind--what was referred to above as discovermental complexity--ought to satisfy? How might such efficiency be reckoned or measured?
2. Are there significant ideal
systems , and significant
families 
of real
theorems such that for every ρ
in , there is at
least
one real proof of ρ that
is as efficient (however efficiency is measured) as
any ideal proof of ρ
in ? Are there
of
this type where the consistency of -
is
finitarily provable?2
3. Are there significant ideal
systems and irredundant ideal
axioms 
of
such that is
not used in any gainful proof in
of any real theorem? Are
there systems of this type where
the consistency of - 
3
is
finitarily provable?
4. Are there significant ideal
systems and irredundant ideal
axioms of
such that every real
theorem in whose gainful proof
participates has equally gainful proofs not involving ?
Are there systems of this type where the consistency of -
is
finitarily
provable?
1.
Note that we characterize gain
as a set of theorems, not as a formal axiomatic
system. Note further that from the assumption that gain
is a proper subset of the theorems of ,
it does not
follow
that the axioms of that are retained in gain
is a proper subset of
the axioms of .
2.
Some of the difficulties
here, of course, concern what -
might or ought
to to be taken to mean. Similarly for the systems -
mentioned
below.
3.
Here and in 4.
stands for the set of all of
the type mentioned.