Re: help with Godel's

herbzet wrote:
Barb Knox wrote:

In article <MPG.2054d528fefaa10e989d5e@xxxxxxxxxxxx>,
David Marcus <DavidMarcus@xxxxxxxxxxxxxx> wrote:

herbzet wrote:
[SNIP]

And, while we're on the subject, what are we to make of
a sentence like ~Con(PA), which, intuitively, says that
PA has no models, but, if PA does have models, is true in
some of them???

Our intuitive understanding of the sentence doesn't match its meaning in
such a model.

Hi Barb, thanks for your concise reply.

Yes, very helpful.

Do you mind if I put
the screws to it a little to see if I completely understand?

In particular, Con is defined in terms of Provable, Con(PA) being
equivalent to ~Provable(PA,"1=0"). Provable(axioms,theorem) is the case
if there is a sequence of proof-steps, each of which is either an
instance of one of the given axioms or an application of modus ponens to
2 previous steps in the sequence.

OK.

Now, in the standard model of PA, every number is finite,
therefore every proof has a finite sequence of steps.

Is it a part of the definition of the proof-predicate "Provable(X,Y)"
that the proof of Y from X has n steps?

I would guess "yes", so that in the standard model a proof would
indeed be finite in length, since every n is finite in that model.

Right.

And I suppose in a non-standard model, n might be infinite, so
the proof-predicate would allow proofs of infinite length.

Although ... I find it odd that the syntactic object,
a "proof", would be different in different _models_ of
a theory, because it is the _syntactic_ object that
_determines_ the models.

The syntactic objects are the same. The theorems are the same. We do
math using the standard model of PA. The problem is that a non-standard
model thinks something is the Godel number of a proof that isn't really.

In this standard model, Con(PA) is true.

How does this follow from what you said?

Because PA has a model (the standard model), hence is consistent. And,
that's what Con(PA) says.

So far, so good. But
in each of the non-standard models, there are numbers which are
infinite, and ~Con(PA) refers to a proof (of "0=1") that has an infinite
number of steps. But we (in standard-model-land) wouldn't consider that
to be a legitimate proof.

Yeah, we wouldn't. This proof-predicate obviously doesn't capture
the notion of "proof".

Such is the depth of my confusion.

It captures it the best it can within the context of PA. PA only has the
first order versions of Peano's axioms, so you don't have the full
induction axiom.

--
David Marcus
.

Loading