Isn't computational reflection problematic for QED? There seems enough
difficulty agreeing on a root logic (terms, formulae, theorems, and
proofs) without dealing with a formal notion of computation, which as
far as I can tell, is necessary for computational reflection, or even
Randy Pollack's proposal. Would we have to agree, not only on a root
logic, but a root computation system, into which we could translate all
our reflected decision procedures? Wouldn't the notionally simple root
logic then have to become rather more complex, in order to adequately
relate computation and proof?
A strong point of the QED proposal was that it forced no choices about
the underlying implementation system; however, consideration of
computational reflection seems to drag that back in.
Konrad.