[FOM] Certificates are Fully Practical

[Timothy Y. Chow]

Alan Weir wrote:

> But even for non-formalist logicians the limited extent of concrete, 
> feasible provability surely has implications. We declare first-order 
> logic complete with respect to a particular semantics, but this whole 
> claim is senseless unless we idealise beyond feasible, concretely 
> realisable proof. Given that we do so, why not declare PA 
> negation-complete, since it is so in omega-logic, and read Godel's 
> beautiful results, the first theorem in particular, as telling us not 
> that truth and proof come apart but that finitary proof is too weak? The 
> gap arises, putting it crudely, because we are infinitistic in model 
> theory but finitistic in proof theory. Is there a rationale for this, or 
> is it an accidental product of Godel's prestige and the fact that when 
> he discovered the incompleteness theorems he was much more strongly 
> influenced by finitism than later?

I'm not sure I fully understand your question, but let me rephrase it 
according to my understanding.

Hilbert said, "We must know, we will know."  Someone objects that there 
are theorems whose shortest proofs are so long that we will never know 
them.  The rejoinder is, yeah, well, O.K., but we can take some 
consolation in the fact that *in principle* every assertion has a finite 
proof or disproof.

Goedel says, sorry, that's not a fact.

Now if I understand you correctly, you're asking, why can't we take 
consolation in the fact that every assertion has an infinitary proof or 
disproof?

My reply would be that that's pretty small consolation, if any.  "Finite" 
is admittedly not a perfect stand-in for "feasible," but "infinite" is an 
even worse stand-in.

Here's an analogy.  A genie offers to make me rich beyond my wildest 
dreams.  "Hooray!" I say.  The genie then adds that actually, it's really 
only my posthumous estate that will be worth billions, and I won't see any 
of the money during my lifetime.  I am disappointed, but at least happy 
for my children.  Do you think I will be cheered up if the genie says, 
"Just kidding---you'll be extremely rich only after an infinite amount of 
time passes"?

Tim