Re: Goedel - interesting problem?

From: Daryl McCullough (daryl_at_atc-nycorp.com)
Date: 06/07/04 

Date: 7 Jun 2004 07:33:18 -0700

|-|erc says...
>
>"Daryl McCullough" <daryl@atc-nycorp.com> wrote

>> That's just incorrect. Peano arithmetic cannot prove the statement
>>
>> "G has a proof" -> G
>>
>
>"plus a system for modus ponens" being predicate calculus.

Fine. The combination of Peano arithmetic plus the predicate
calculus cannot prove

       "G has a proof" -> G

>Isn't part of 'proof's defn an implication of the formula it proved.

I think maybe you are being misled by the informality here.
There is no formula in Peano arithmetic that literally says
"G has a proof". PA does not literally talk about proofs at
all, it only talks about numbers.

What really is going on is that there is a formula Pr(x) in PA, and
there is a coding of formulas as numbers such that

    G has a proof in PA <-> PA proves Pr(#G)

where #G is the code for G.

The interpretation of Pr(#G) as "G has a proof" is something
that takes place *outside* of PA. PA is unaware of this connection,
and PA is unaware that the number #G has anything to do with
formula G. So PA has no way of proving the implication

     Pr(#G) -> G 

--
Daryl McCullough
Ithaca, NY

Relevant Pages

  • Re: Existence, Self-identity and Uniqueness.
    ... you cannot substitute equals for equals any more. ... to additional preconditions. ... predicate calculus with identity. ...
    (sci.logic)
  • Re: Onto a potential relational manipulation language
    ... propositional calculus we have boolean algebra. ... I'd suggest that RL is predicate ... quantification since it has a form of projection in its lattice union. ...
    (comp.databases.theory)
  • Re: Onto a potential relational manipulation language
    ... propositional calculus we have boolean algebra. ... I'd suggest that RL is predicate ... RL must at least have quantification since it has a form of projection in its lattice union. ...
    (comp.databases.theory)
  • Re: completeness of predicate calculus
    ... dissertation had been on the completeness of predicate calculus (which ... she called limpid calculus). ... What exactly does it mean for predicate ... - that's a different sort of completeness. ...
    (sci.logic)