> I wouldn't fire the analyst in your example, by the way, because the fault would be mine: I should have just specified what complexity bound would be acceptab

> I wouldn't fire the analyst in your example, by the way, because the fault would be mine: I should have just specified what complexity bound would be acceptable in a termination proof of the algorithm for it to be practical for my purposes. I thought someone might say something like this. My counter is that if the analyst just used a normal proof system (i.e. one that doesn't assume false (in the standard model) axioms) then we could use Goedel's Dialectica [1] to mine the proof for some (probably crappy) complexity bound. That said, this is getting close to the edge of my knowledge on this subject. [1] http://math.stanford.edu/~feferman/papers/dialectica.pdf http://math.stanford.edu/~feferman/papers/dialectica.pdf