From: Aatu Koskensilta on
Sergei Tropanets <trop.sergei(a)gmail.com> writes:

> By Con(T) I understand (and I suppose Charlie also does so) SYNTACTIC
> consistency and I use the following general result:
>
> if it is not the case that T |-- not Q then Con(T+Q).
>
> So of course by 2nd incompleteness
>
> <<This implies Con(PA + Con(PA)) and Con(PA + not Con(PA)).>>

Nope. By the second incompleteness theorem we know that if PA is
consistent then "PA is consistent" is not provable in PA. It does not
follow that "PA is inconsistent" is not provable in PA.

> Where I need Sigma-1 soundness of PA there?

You need Sigma-1 soundness -- or the rather more impenetrable condition
of omega-consistency -- to conclude "PA is inconsistent" is not provable
in PA.

> It was. In fact, Godel set forward this argument at his first
> presentation of 1st incompleteness theorem at philosophy conference.

The argument makes no apparent sense since "PA is inconsistent" is not a
finitistically meaningful statement in Hilbert's sense.

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechen kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on
Sergei Tropanets <trop.sergei(a)gmail.com> writes:

> On Jul 31, 11:09�am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
>> Nam Nguyen <namducngu...(a)shaw.ca> writes:
>
>> So when Andrew Wiles proved Fermat's last theorem he did so by finding a
>> "syntactical proof through rules of inference"?
>
> Are you sure he did prove it?

Sure.

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechen kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on
MoeBlee <jazzmobe(a)hotmail.com> writes:

> On Jul 31, 12:31�pm, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
>
>> I expect a prompt and groveling apology. Should an apology not prove
>> forthcoming, I will be forced to pout in impotent anger, and possibly
>> stomp my feet.
>
> You're such a pushover.

What if I further threaten to killfile you or claim to retire entirely
from Usenet? That'll show you!

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechen kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: MoeBlee on
On Jul 31, 1:47 pm, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:

> What if I further threaten to killfile you or claim to retire entirely
> from Usenet? That'll show you!

As once related to me by Giuseppe Peano in personal communication,
"Chill, dude."

MoeBlee


From: Sergei Tropanets on
On Jul 31, 11:29 pm, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> Sergei Tropanets <trop.ser...(a)gmail.com> writes:

> > By Con(T) I understand (and I suppose Charlie also does so) SYNTACTIC
> > consistency and I use the following general result:
>
> > if it is not the case that T |-- not Q then Con(T+Q).
>
> > So of course by 2nd incompleteness
>
> > <<This implies Con(PA + Con(PA)) and Con(PA + not Con(PA)).>>
>
> Nope. By the second incompleteness theorem we know that if PA is
> consistent then "PA is consistent" is not provable in PA. It does not
> follow that "PA is inconsistent" is not provable in PA.

Agreed. Thank you!


> > Where I need Sigma-1 soundness of PA there?
>
> You need Sigma-1 soundness -- or the rather more impenetrable condition
> of omega-consistency -- to conclude "PA is inconsistent" is not provable
> in PA.

Are Sigma-1 and omega-consistency equivalent? Sigma-1 => omega-con?
Vice versa?



> > It was. In fact, Godel set forward this argument at his first
> > presentation of 1st incompleteness theorem at philosophy conference.
>
> The argument makes no apparent sense since "PA is inconsistent" is not a
> finitistically meaningful statement in Hilbert's sense.
>

I can't agree with that. For example if somebody finds a concrete
formal proof of Q/\notQ from axioms of PA it would mean inconsistency
even for formalist (because it is efficiently checkable). The fact
that any formal proof in PA cannot end with Q/\notQ is meaningful
finitistically (as well as Goldbach's conjecture) because it is a
simple combinatorial conjecture (you can express it in PRA) which
Hilbert intended to prove by finitistic means.

Sergei Tropanets