Re: Godel cant tell us what makes a mathematical statement true

herbzet wrote:

Nam Nguyen wrote:

Unfortunately, that's how we've done reasoning after Hilbert's
Program. I'm not defending Hilbert's one-size-catch-all formal
system, only his syntactical provability. What we've done since
Godel is to replace that formal system with one-encoding-size-catch-all
arithmetic (interpretation) truth system.

I'm not sure what you're talking about with this last sentence.

Could you expand a bit on what you mean by "What we've done
since Godel is to replace that formal system with one-encoding-
size-catch-all arithmetic (interpretation) truth system"?

Let's just say the formal system in question, for undecidability, is
ZF and the suspected undecidable formula in ZF is G(ZF). Suppose now
we adhere to Hilbert's syntactical-ism where we don't have the concept
of arithmetical truth and where formulas are devoid of meanings; and
proving theorems is exactly nothing more than just a manipulation of
strings of symbols, based on some syntactical rules of inference.
Then G(ZF)'s undecidability means ZF proves neither G(ZF) nor ~G(ZF).
But how would we demonstrate a system T not prove a particular F in
general? After all, a formal system is designed to prove formulas,
not to un-prove them!

The long and short of it is, we've learned through Godel's work,
there's some "faint" hope if we somehow encode G(ZF) and ~G(ZF), using
an "external system", say, named Ar (for Arithmetic), and using some of
Ar's properties, we'd perhaps have some satisfactory (mental) mapping
between these properties and the suspected unprovability of both G(ZF)
and ~G(ZF).

But what's exactly the nature of Ar, as an "external system"? Well, if
we stay with Hilbert's syntactical-ism then it must be just another formal
system. But in this case, we'd come the a full circle: how could we in Ar
demonstrate encoded(G(ZF)) and ~encoded(G(ZF)) aren't provable? The long
and short of it is, if we could, Ar would be that "one-size-catch-all"
formal system, because *all* the similarly constructed encoded(G(T))'s
and ~encoded(G(T))'s [with all the Ts satisfying some conditions of
course] would be proven in Ar; (and I think PM would be the natural choice
for this external encoding Ar, at the time).

In a nutshell, Godel couldn't have used PM to encode G(ZF), ~G(ZF),
or what had he: because of the circularity. What he did, probably
through some flash of intuition, is to use some key strategies, instead:

(1) Having alternative definition of "undecidability" using the concept
of model, which is based on intuition and not on Hilbert's
syntactical-ism: G(T) would be undecidable if it's true in a model
of T, but false in another one. (This in itself isn't new: we did
that with the the 5th postulate).

(2) Mapping the model truths and falsehoods in T to those in a
"fictitious formal" system Ar.

(3) Mentally (or rather in a meta level), ignore/remove the complete/full
formality of Ar, and retain only its models: at least one of its models
we'd deem as "the standard model of arithmetic".

In a nutshell, that's my summary of how we end-up replacing a would-be-
"one-size-catch-all" formal by aother "one-encoding-size-catch-all"
"the-standard-model-of-arithmetic": which is really just the natural numbers,
collectively!

--
"To discover the proper approach to mathematical logic,
we must therefore examine the methods of the mathematician."
(Shoenfield, "Mathematical Logic")


.

Relevant Pages

  • Re: Godel cant tell us what makes a mathematical statement true
    ... size-catch-all arithmetic truth system"? ... we stay with Hilbert's syntactical-ism then it must be just another formal ... through some flash of intuition, is to use some key strategies, instead: ... formality of Ar, and retain only its models: at least one of its models ...
    (sci.logic)
  • Re: Godel cant tell us what makes a mathematical statement true
    ... system, only his syntactical provability. ... size-catch-all arithmetic truth system"? ... we stay with Hilbert's syntactical-ism then it must be just another formal ... formality of Ar, and retain only its models: at least one of its models ...
    (sci.logic)
  • Re: Godel cant tell us what makes a mathematical statement true
    ... size-catch-all arithmetic truth system"? ... Then G's undecidability means ZF proves neither Gnor ~G. ... we stay with Hilbert's syntactical-ism then it must be just another formal ... formality of Ar, and retain only its models: at least one of its models ...
    (sci.logic)
  • Re: Formal statement of godels 1.incompleteness theorem
    ... Any rate let me share with you some thoughts on the the formality ... Truth and Semantics in FOL ... based on Rule of Inference we can't simply have: ...
    (sci.logic)
Quantcast