|
|
Aatu Koskensilta wrote:
> In the thread "Provable in T" the incompleteness theorem and their exact
> requirements - Sigma-1-completeness in particular - have been the
> subject of much discussion.
Yes; let's clarify
1) Whether we need sigma-1-completeness (DO we really
need it? Might we need something similar instead?
Might it be more or less than what we truly need?)
2) Why we need it, what we're using it for, if we need it, and
most importantly,
3) Whether you can possibly ever "need" something that
IS IN UBIQUITOUS OVERSUPPLY ALL the time in the first place.
> The first incompleteness theorem is usually expressed something like the
> following
>
> For any extension T of Robinson arithmetic we can effectively find a
> sentence G_T, s.t. G_T is true and undecidable in T iff T is
> (1-)consistent.
>
> As everyone knows, Robinson arithmetic is Sigma-1-complete: every true
> Sigma-1 sentence is provable in Robinson arithmetic,
Robinson arithmetic is a first-order theory.
But a sigma-1 truth of true arithmetic is going to
be a statement (however long&complicated -- well, actually,
there is a limit on how complicated it can be -- it can't have
universal quantifiers, for example) about ONE FINITE natural
number. Because of this, there is a finitary fragment of
PROPOSITIONAL
(zeroth-order) logic in which this truth is going to be provable.
> proved essentially by showing by induction - not
> in Robinson arithmetic itself! -
INDEED. The point being that if you want to show something
true about every finite/usual/natural number, induction
IN NATURAL language (or in whatever meta-language you
may desire) is ENTIRELY appropriate. It again bears stressing
that you are showing something ABOUT FINITE things.
> that every true Delta_0 sentence is provable in Robinson arithmetic
Again, "In Robinson Arithmetic" is conceding almost TOO much.
Of course they are provable in first-order Robinson Arithmetic, but
"Delta_0" invites people to think of quantifiers and first-order
considerations, which is INappropriate. Bounded quantifiers,
when the bounds ARE FINITE NATURAL numbers, yield sentences
that are JUST like FINITE CONJUNCTIONS AND DISJUNCTIONS,
i.e., that are FUNDAMENTALLY PROPOSITIONAL in character.
In other words, if our quantifier-scheme is delta_0 then we really
do NOT have ANY quantifiers AT ALL. This is a fundamentally
simpler universe than first-order considerations in general would
lead one to think. This is relevant to a discussion of the
arithmetica-
truth-coverage kind of "completeness" because NO first-order axioms
are relevant to the truth of PROPOSITIONAL theorems.
All the propositional tautologies showed up IN ADVANCE.
One Could Never Escape "completely" covering all of THEM.
> and hence by existential generalization so is every Sigma-1 truth.
Yes, but again, it bears stressing that it is NOT like, having the
delta_0 sentence, we, thanks to the powerful EG inference rule,
promoted it to some greater 1st-order sentence. EG is about
THROWING AWAY information. It is about FORGETTING WHICH
finite number we ALREADY proved this truth about, IN ZEROTH order
logic. Getting to every sigma-1 truth is NOT getting more,
above and beyond, the propositional arena; it is FORGETTING.
It is REgressing.
> Now, in the proof of the first incompleteness theorem the sentence G_T
> is constructed specifically as a (true) fixed point of the unprovability
> predicate for T, which can be taken to be Pi-1. We need
> Sigma-1-completeness for two things: that enough facts about
> substitution of specific terms in formulas are provable -
HOW MIGHT ANYthing involving *terms* be unprovable??
Terms, LIKE NUMBERS IN THE STANDARD MODEL,
MUST be *FINITE*! BECAUSE terms are finite, there will be
0th-order proofs that they satisfy any finitary non-Universal
predicate they satisfy. Yes, this does add up to sigma-1-
completeness, but I repeat, this starts to seem like a very
EASILY, indeed UNavoidably, achievable condition.
> so that the diagonal lemma goes through -, and that if G_T is,
> in fact, provable in T then it is provable in T that G_T is provable in T.
My point is simply that in order for either of these horrors to occur
(the diagonal lemma failing to go through or something being provable
but not provably provable), it would be necessary for same 0th-order
finite fact about a finite number to come up unprovable. Rupert et al
would say something like "by presuming/requiring that T be sigma-1
complete, we bar this possibility". My counterpoint would be that it
is
NOT by virtue of our ASSUMPTION of sigma-1-completeness that T turns
out to be sigma-1-complete. Provability of existentials over a
universe
of ONLY FINITE things is arguably going to follow in an inescapable
chain FROM 1-consistency, which is what you ACTUALLY needed
to assume.
> To get the second theorem we need more than just Sigma-1-completeness,
> namely *provable Sigma-1-completeness* - this might or might not have
> been one of Greene's points - plus a few facts about provability itself.
> One of the original derivability conditions in the second incompleteness
> theorem given by Bernays was effectively a form of provable
> Sigma-1-completeness:
>
> T |- f(x) = 0 --> Prov_T("f(x) = 0"), for f primitive recursive
At this point I just have to plead large amounts of confusion.
This is a point where it starts to MATTER whether T was vs. wasn't
presumed formal/r.e. to begin with.
If f(x)=0 and f is prim.rec. then IT IS provable that f(x)=0,
IRrespective of other facts about T OR about Prov_, other than
(perhaps) that x be something named by a term as opposed
to being anonymous (is T a model, an arbitrary theory, or what?)
To me, this seems a strange kind of assumption; one makes an
assumption in order to bar cases where the assumption was false;
so the question arises, how could f(x)=0 WITHOUT Prov_T("f(x)=0")
being true? This would entail that Prov_T was WRONG, that it
wasn't the true/actual provability predicate.
> If we have provable Sigma-1-completeness (together with a few facts
> about provability, i.e. that provability of P --> Q implies that the
> provability of P implies the provability of Q)
But the latter is surely a lemma, not an assumption, if modus ponens
is an inference rule in this formalism?
> we can, in T, see that if G_T were provable it would be provable
> in T that G_T is provable,
And this, to me, seems, rather than a "truth" that we could "see",
to be simply an axiom. A proof of s BY DEFINITION *constitutes* a
proof
of Provable(s), at least it does intuitively/semantically. One is thus
OBLIGATED
to take CARE to DEFINE one's actual proof-predicate so as to GUARANTEE
that that inference will be trivial. Something AXIOMatic like
Provable(s)<=df=>Ep[Proves(p,s)] would accomplish that. Or at least,
it would demote the question to showing that the Truth of Proves(p,s)
entails the Provability of Proves(p,s). But that was supposed to
follow
from the fact that Proves(,) Must be primitive recursive.
> contradicting the T-provable fact that G_T is a fixed point of the
> non-provability predicate, i.e. G_T <--> ~Prov_T("G_T").
This surely bears further stressing:
G_T is not provable in T, ~G_T is not provable in T,
Prov("G_T") is not provable in T, and ~Prov("G_T") is not provable in
T.
Worse, all this non-provability is itself ALSO NOT provable in T.
YET
G_T<->~Prov("G_T") IS provable IN T?!?!
|
|