Re: FOL, ZFC, NGB and Prolog

Keith Ramsay wrote:
> galathaea wrote:
> |tom wrote:
> |(I thought Goedel equated provability and truth).
> |
> |to which aatu koskensita responded:
> |Quite the opposite, really, provided we're speaking about formal
> |provability.
> |
> |that is not quite true
>
> I don't see how.
>
> Goedel was about as far away from identifying formal provability
> and truth as it's possible to get. He considered the human mind
> to have a power to recognize mathematical truth that transcended
> anything mechanical, and was consequently optimistic about our
> ability eventually to know mathematical truths even if they're not
> formally provable from any axioms we have today. Goedel is often
> cited as a prototypical example of a hard-core mathematical
> Platonist. The interested reader can have a look at his essay on
> the meaning of the continuum hypothesis.
>
> He wrote elsewhere about an axis he termed "left" versus "right"
> (not related as far as I can see to political left and right).
> "Left" in his terms represented all the reductionist tendancies,
> including such things as mathematical formalism and materialism.
> "Right" meant the opposite tendancy toward belief in transcendence.
> He saw the "left" as having made big advances, but he had strong
> sympathies with the "right". Trying to identify truth with formal
> proof is just the kind of "leftward" ambition (e.g. of Hilbert)
> that he enjoyed thwarting.
>
> |goedel, like many mathematicians of the time, struggled with the
> |definition of truth
>
> I would assume he was familiar with the problems with that. It
> doesn't indicate that he came anywhere near identifying it with
> proof.
>
> |and at times he did study the "truth as proof" school
>
> I don't know what "school" you have in mind, unless perhaps you
> mean the Vienna circle. He parted ways with them on somewhat
> similar issues, with their tending to identify the meaning of a
> statement with its verification conditions, and his not doing so.
>
> |but his conceptions of its meaning was not a necessary component to
> his
> |major arguments in metamathematics
>
> He made a point of proving his metamathematical results in a
> cleanly mathematical way, apparently in part to prevent their
> being criticized for any concepts they might mention that weren't
> purely mathematical. But his position was not that such concepts
> (e.g. the truth of statements of arithmetic) were ill-defined, as
> his other writings make clear.
>
> |however, the constructivists of the time equated truth and provability
>
> Not all constructivists do identify truth and provability, and those
> who do are identifying truth with informal provability. Brouwer, for
> example, was the constructivist of the time best known to us. I don't
> know whether he ever identified truth with informal provability, but
> he was about as negative about the formalization of mathematics as
> anybody ever has been.
>
> |and this later was incorporated into the foundations of computation
>
> I think this is misleading.
>
> |which express the incompleteness theorems much more directly
>
> The incompleteness theorems as proven by Goedel are pretty
> thoroughly direct. The indirectness, such as it is, is
> largely due to his showing along the way how formalism can
> be encoded in arithmetic. Sticking to computational terms
> is in a sense more direct, but doesn't have anything to do
> with identifying truth and provability.
>
> |the key concept is inaccesibility
> |(or the dual notion of platonic truth)
> |
> |to tom:
> |if you are truly interested in the connections between computation and
> |proof theory
> |start with the curry-howard isomorphism
> |it is the centerpiece on which the connection is made formal
>
> I agree with this advice.
>
> Keith Ramsay

Sir, thank You very much indeed for all Your kind comments. You have
been most helpful to me, I dare say I would not have made _any progress
whatsoever without the information You kindly provided. *IF* this is
not too much to ask, and *IF* you think I deserve it, please kindly
grant me _only the three letters. Oh, please.

Thank You.
Tom

.

Relevant Pages

  • Re: The Law of the Excluded Middle again (long)
    ... "Inside the scope of quantification, ... to equate (or confuse) truth with provability." ...
    (sci.math)
  • Re: FOL, ZFC, NGB and Prolog
    ... |(I thought Goedel equated provability and truth). ... Goedel was about as far away from identifying formal provability ... and truth as it's possible to get. ... including such things as mathematical formalism and materialism. ...
    (sci.logic)
  • Re: Godel cant tell us what makes a mathematical statement true
    ... are identifying truth with provability. ... oppose such a truth definition I've given. ... But we can formalize the mathematical defintion of 'truth' so that we ... we must therefore examine the methods of the mathematician." ...
    (sci.logic)
  • Re: A little knowledge is a dangerous thing - THE HALTING PROOF
    ... is NOT "Truth" in some huge mystic medieval sense, ... INDEED, the statement encoding "PA is consistent", ... finite number of things, verification is trivial. ... > Provability Thesis: A true arithmetic relation ...
    (sci.logic)
  • Re: Goedel - interesting problem?
    ... Note it says that the *formal system* in question has "theorems that can ... the important point is the contrast ... as a synonym simply for "truth of arithmetic". ... provability is explicit in the terminology. ...
    (sci.logic)
Quantcast