Re: Torkel Franzen on truth

On Nov 15, 9:10 am, stevendaryl3...@xxxxxxxxx (Daryl McCullough)
wrote:
Newberry says...



On Nov 15, 3:12 am, stevendaryl3...@xxxxxxxxx (Daryl McCullough)
wrote:
No, we *don't* have that the human mind surpasses any machine.
There is no reason to believe that's true.

But we do. We know that G is true.

That does not prove that the human mind surpasses any machine.
You can certainly program a machine to know, among its basic
facts, that G(PA) is true.

Proof:
The axioms of PA are manifestly true
PA is consistent
"PA is consistent" is equivalent to G
G QED

This proof cannot be formalized.

That's just not true. It can perfectly well be formalized.
It just can't be formalized in the language of PA.

Extend PA to a new theory PA-plus in the following
way:

Add a new predicate symbol T(x). For every statement S
in the language of PA, add the axiom

S <-> T(#S)

where #S means the Godel code of S. Then add the
axiom

Ax Prove(PA,x) -> T(x)

where Prove(PA,x) is the formalization of the proof
predicate.

In PA-plus, it is perfectly straight-forward to prove
G(PA) (the Godel statement for PA).

A couple of comments. Firstly, I do not know if the proof you are
showing is the same as the manifest truth proof. Secondly, if I
understand you correctly the only difference between (Ex)P(x, #("F")
--> F and Ax Prove(PA,x) -> T(x) is the "T." It is not that it cannot
be formalized in the language of PA, it is that it leads to a
contradiction. Did we put the axiom on a meta-level just to avoid the
contradiction?

BTW, I do not understand this:
S <-> T(#S), where #S means the Godel code of S.
The Goedel number of S is true ... ?

.

Relevant Pages

  • Re: Torkel Franzen on truth
    ... add the axiom ... where #S means the Godel code of S. Then add the ... where Proveis the formalization of the proof ... G(the Godel statement for PA). ...
    (sci.logic)
  • Re: Godels Theorem and Model Theory
    ... does not say "There are no hyperfinite numbers". ... We can make a Godel code for any formula by starting with ... So it's not that the axiom *says* that anything is finite, ... Is there any reason we could not make it a part of the language? ...
    (sci.logic)
  • Re: Postulates for quantum mechanics (was; Is State Vector Reduction
    ... it is possible to check the reality contents of a physical theory. ... you use the words "a generic system is defined" in axiom 1 and the closed/open is necessary to define the system. ... of mathematical objects in these axioms (no connection with "reality" without a minimalist interpretation. ... a formalization of MI that meets the demands of ...
    (sci.physics.research)
  • Re: R6RS Ratified
    ... 20 years of history of formally developed language ... Economically speaking, formal language standards ... sell a new commodity to corporate customers. ... Formalization ...
    (comp.lang.scheme)
  • Re: A question about FOL theories and models
    ... You could formalize some meta-theory about G. ... Constructing a counter-model is only one way of proving ... function in the language and a relation for every ... the axiom-set "the axioms of G plus the denial of the axiom you ...
    (sci.logic)
Quantcast