Re: Name the thesis: "Formal sentences capture informal ones"

From: Torkel Franzen (torkel_at_sm.luth.se)
Date: 01/31/05

  • Next message: Russell Easterly: "Re: A Class of X3SAT Solvable in PolyTime" 
    Date: 31 Jan 2005 08:20:17 +0100

    tchow@lsa.umich.edu writes:

    > As I understand it, this is precisely the kind of project that Sol Feferman
    > undertook in his early years.

      If you mean the work in "Arithmetization of metamathematics in a general
    setting", this dealt with more pressing problems. He showed among
    other things that the incompleteness theorem holds in a general
    formulation provided we require the axioms of a theory to be defined
    by what we now call a Sigma-formula. However, a Sigma-formula which
    extensionally defines the axioms of e.g. PA can still be intensionally
    incorrect.

    > I think what Kunen's remarks indicate is that there is no way out of
    > the infinite regress other than by starting with an informal-to-formal
    > transition somewhere and then baldly postulating that it is correct.

      Yes, what I called a "direct" translation.

  • Next message: Russell Easterly: "Re: A Class of X3SAT Solvable in PolyTime"