A while ago there was a post about using Loeb’s theorem as an
alternative to Goedel’s theorem in arguments about mechanism;
could someone mail it to me?
Thanks in advance,
damjan.bojadz…@ijs.si
http://nl.ijs.si/~damjan/me.html
31
Dec
Loeb repost?
In article <1995Dec13.145027….@cathy.ijs.si>,
Inst. J. Stefan, Ljubljana, Slovenia <damjan.bojadz…@ijs.si> wrote:
>A while ago there was a post about using Loeb’s theorem as an
>alternative to Goedel’s theorem in arguments about mechanism;
>could someone mail it to me?
It is more than an alternative; Loeb’s theorem _implies_ Goedel’s
theorem. If Prov() is a provability predicate for T, Loeb asserts
that if T can formally deduce Prov(‘Q’) => Q, then T can formally deduce Q.
Goedel’s theorem is the particular case of Q being 0 = 1.
Ilias
>>A while ago there was a post about using Loeb’s theorem as an
>>alternative to Goedel’s theorem in arguments about mechanism..
>It is more than an alternative; Loeb’s theorem _implies_ Goedel’s
>theorem. If Prov() is a provability predicate for T, Loeb asserts
>that if T can formally deduce Prov(‘Q’) => Q, then T can formally
>deduce Q. Goedel’s theorem is the particular case of Q being 0 = 1.
I was at first confused by this, but now it looks ok; maybe it
should be added that the Goedel theorem you refer to is the
second one, while i had in mind the first; i also remember
that Loeb’s theorem is equivalent to Goedel’s second.
damjan.bojadz…@ijs.si
____________ __ ____________
\_____ / /- \ \ _____/
\_____ \____/ \____/ _____/
\_____ _____/
\____________@___________/
/ \
___~_____~__
/ http:// \
| nl.ijs.si |
| /~damjan/ |
| me.html |
\____________/
In article <4b8226$…@gap.cco.caltech.edu> ikas…@alumni.caltech.edu (Ilias Kastanas) writes:
>Loeb’s theorem was proven in the 1950′s, but the above fact is much
>more recent.
But the original proof is nicer. It applies also to the intuitionistic
case.
In article <1995Dec18.163615….@cathy.ijs.si>,
Inst. J. Stefan, Ljubljana, Slovenia <damjan.bojadz…@ijs.si> wrote:
>>>A while ago there was a post about using Loeb’s theorem as an
>>>alternative to Goedel’s theorem in arguments about mechanism..
>>It is more than an alternative; Loeb’s theorem _implies_ Goedel’s
>>theorem. If Prov() is a provability predicate for T, Loeb asserts
>>that if T can formally deduce Prov(‘Q’) => Q, then T can formally
>>deduce Q. Goedel’s theorem is the particular case of Q being 0 = 1.
>I was at first confused by this, but now it looks ok; maybe it
>should be added that the Goedel theorem you refer to is the
>second one, while i had in mind the first; i also remember
>that Loeb’s theorem is equivalent to Goedel’s second.
You are right, and I should have mentioned it. The full Loeb
theorem does follow by an easy argument from the particular case (Goedel),
essentially because Consis(T) and G(T) (Goedel sentence for T) are
logically equivalent, provably in a weak fragment of arithmetic (e.g. PRA).
Loeb’s theorem was proven in the 1950′s, but the above fact is much
more recent.
Also, I’m sorry if I caused confusion. The two theorems are just one
theorem in my head, I don’t number them; but in public I should.
Ilias
Ilias Kastanas (ikas…@alumni.caltech.edu) wrote:
> You are right, and I should have mentioned it. The full Loeb
> theorem does follow by an easy argument from the particular case (Goedel),
> essentially because Consis(T) and G(T) (Goedel sentence for T) are
> logically equivalent, provably in a weak fragment of arithmetic (e.g. PRA).
> Loeb’s theorem was proven in the 1950′s, but the above fact is much
> more recent.
Can you provide details or a reference? Loeb’s theorem certainly
doesn’t require much more work that Goedel’s, but I don’t see
how it follows from it.
> Ilias
Michael Lauer
mla…@cvbnet.cv.com
In message <4bbubq$…@hettar.cv.com> – mlauer@mugwump (Michael Lauer) writes:
:>
:>Ilias Kastanas (ikas…@alumni.caltech.edu) wrote:
:>> You are right, and I should have mentioned it. The full Loeb
:>> theorem does follow by an easy argument from the particular case (Goedel),
:>> essentially because Consis(T) and G(T) (Goedel sentence for T) are
:>> logically equivalent, provably in a weak fragment of arithmetic (e.g. PRA).
:>
:>> Loeb’s theorem was proven in the 1950′s, but the above fact is much
:>> more recent.
:>
:>Can you provide details or a reference? Loeb’s theorem certainly
:>doesn’t require much more work that Goedel’s, but I don’t see
:>how it follows from it.
:>
:>> Ilias
:>
:>Michael Lauer
:>mla…@cvbnet.cv.com
I’m doing this from vague memory. The idea is due to Kripke. It’s probably
in Boolos.
We want to prove: |- Bew ([S]) –> S ===> |- S
Assume not |- S
Consider the system PA + -S (suitably characterized) and its CON sentence
(suitably characterized). I’ll use |= for the turnstile of the system PA+
-S.
Then by G2, not |= CON(PA+ -S)
But that means not |- -S –> CON (PA + -S)
But CON (PA + -S) is equiv. to -BEW ([S])
Contrapose et voila.
In article <4bbubq$…@hettar.cv.com>, Michael Lauer <mlauer@mugwump> wrote:
>Ilias Kastanas (ikas…@alumni.caltech.edu) wrote:
>> You are right, and I should have mentioned it. The full Loeb
>> theorem does follow by an easy argument from the particular case (Goedel),
>> essentially because Consis(T) and G(T) (Goedel sentence for T) are
>> logically equivalent, provably in a weak fragment of arithmetic (e.g. PRA).
>> Loeb’s theorem was proven in the 1950′s, but the above fact is much
>> more recent.
>Can you provide details or a reference? Loeb’s theorem certainly
>doesn’t require much more work that Goedel’s, but I don’t see
>how it follows from it.
I believe it is due to Kripke, but I cannot think of where you might
find it.
Roughly, an extension of PA, PA + Q, is consistent iff PA does not
prove ~Q; consistency is provably equivalent to ~Prov( ~Q); so if PA
proves Prov(A)->A, i.e. ~A->~Prov(A), then PA + ~A proves ~Prov(A), that
is, its own consistency. Hence PA + ~A is inconsistent, and therefore PA
proves A.
The area is full of delights and surprises. Even knowing about the
consistency of ~Consis(PA), it is hard to avoid a double take when first
seeing the consistency of "B is undecidable and it is provable that B is
decidable".
Ilias
In article <TORKEL.95Dec20130…@athena.sics.se>,
Torkel Franzen <tor…@sics.se> wrote:
>In article <4b8226$…@gap.cco.caltech.edu> ikas…@alumni.caltech.edu (Ilias Kastanas) writes:
> >Loeb’s theorem was proven in the 1950′s, but the above fact is much
> >more recent.
> But the original proof is nicer. It applies also to the intuitionistic
>case.
The original proof is very nice; it also illuminates the properties
of a provability predicate.
Ilias
From: mlauer@mugwump (Michael Lauer)
Date: 21 Dec 1995 15:26:50 GMT
Can you provide details or a reference? Loeb’s theorem certainly
doesn’t require much more work that Goedel’s, but I don’t see
how it follows from it.
You should be able to find it in Smorynski’s book "Self-Reference
and Modal Logic" or in his survey article in the Handbook of
Math. Logic.