From: ikastan@uranus.uucp (Ilias Kastanas) Subject: Re: Sensible Godel Theorem Question Date: 1 Sep 2000 01:54:31 GMT Newsgroups: sci.math Summary: [missing] In article <39ACB84E.E1E98FA1@trump.net.au>, William Hart wrote: ... > >What about the statement you give. Suppose we have: > >G: G is provable. > >This has the property you specify. Is G provable in the formal system? > >I can't see that it is. (But then I can't see that it isn't). What do people >think? > > People didn't quite know what to think... until Loeb settled the matter. A sentence H such that T |- H <-> Prov_T('H') ("asserting its own provability") is called a Henkin fixed-point. Any H is provable in T... and true (a nice counterpart to: any Goedel fixed-point is unprovable in T, and true). T, and Prov_T, are assumed to satisfy certain natural hypotheses (that also yield Goedel's theorem). Other fixed-points have been investigated (Rogers, Jeroslow...); see Boolos's excellent "The Unprovability of Consistency". And the situation has been generalized; appropriate names, if you want to do a search, are: Bernardi, Smorynski, Sambin, De Jongh. Ilias