[FOM] Certificates are Fully Practical
Timothy Y. Chow
tchow at alum.mit.edu
Mon Sep 23 21:31:09 EDT 2013
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
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
More information about the FOM