Re: help with Godel's



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. 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.

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.

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

How does this follow from what you said?

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.

--
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum viditur.
| BBB aa a r bbb |
-----------------------------

I wish I knew Latin.

--
hz
.

Relevant Pages

  • Re: help with Godels
    ... previous steps in the sequence. ... Is it a part of the definition of the proof-predicate "Provable" ... the axioms of PA, even if we allow n to be infinite? ...
    (sci.logic)
  • Re: Garry Denkes Gold & Brass Plates @ Westbury White Horse Eye
    ... "Barb Knox" wrote in ... I said the string is infinite length, you but in claiming its finite because P=0. ... >>You can see why I introduce basic examples to pin your meaning. ... You are better off partitioning Mickey Mouse maths ...
    (sci.math)
  • Re: Garry Denkes Gold & Brass Plates @ Westbury White Horse Eye
    ... "Barb Knox" wrote in ... I said the string is infinite length, you but in claiming its finite because P=0. ... >>You can see why I introduce basic examples to pin your meaning. ... You are better off partitioning Mickey Mouse maths ...
    (sci.logic)
  • Re: infinitely many nns = infinite nns?
    ... Barb Knox wrote: ... The set FN itself is clearly infinite, by any of the usual definitions of infinite set. ... You can prove and/or define, all day, that there are only finite numbers -- proofs and/or definitions that IMPLICITLY assume potential infinity -- and you can prove and/or define, all day, that there are infinitely many numbers -- proofs and/or definitions that IMPLICITLY assume actual infinity -- and that's wonderful, I absolutely will buy and totally believe in both and. ...
    (sci.logic)
Loading