From: Aatu Koskensilta on
Frederick Williams <frederick.williams2(a)tesco.net> writes:

> Chris Menzel wrote:
>
>> [...] any such proof [of the consistency of PA], when formalized,
>> will be in a system stronger than PA itself [...]
>
> It seems to me that PA and a theory that proves its consistency can be
> incomparable. Isn't this the case with PRA + induction up to epsilon_0?

Yes, provided the induction is of the "quantifier-free" sort as the
technical jargon has it. This is a pet peeve I inherited from Torkel,
and point out in the Wikipedia article on Gentzen's consistency proof --
if some dimwit hasn't already replaced my text with inane twaddle, as is
sometimes the way of Wikipedia.

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

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

> Please clarify: by "simply two rather different proofs" do you mean
> "simply two rather different proofs of the same thing"?

The two claims

T proves that Q is consistent.

and

If T is consistent, so is Q.

are not the same. The first implies the second -- a consistent theory
(meeting the usual criteria) can't prove an inconsistent theory
consistent -- but not the other way around.

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

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: herbzet on


Aatu Koskensilta wrote:
> herbzet writes:
>
> > Please clarify: by "simply two rather different proofs" do you mean
> > "simply two rather different proofs of the same thing"?
>
> The two claims
>
> T proves that Q is consistent.
>
> and
>
> If T is consistent, so is Q.
>
> are not the same.

This is what I was getting at, and where I found your reply to
billh04 somewhat lacking.

I couldn't say at this point whether billh04's question has been
answered to his satisfaction

> The first implies the second -- a consistent theory
> (meeting the usual criteria) can't prove an inconsistent theory
> consistent -- but not the other way around.

--
hz
From: herbzet on


Aatu Koskensilta wrote:

> The two claims
>
> T proves that Q is consistent.
>
> and
>
> If T is consistent, so is Q.
>
> are not the same. The first implies the second -- a consistent theory
> (meeting the usual criteria) can't prove an inconsistent theory
> consistent

If a consistent theory can prove a consistent theory inconsistent, why
can't a consistent theory prove an inconsistent theory consistent?

--
hz
From: Aatu Koskensilta on
herbzet <herbzet(a)gmail.com> writes:

> Yeh -- what *exactly* is being assumed has not been grindingly
> specified at a low level. We're not there yet. Hopefully, we won't
> have to go there.

We have to! Here goes: a consistent Sigma-1 complete formal theory T
can't prove for an inconsistent formal theory Q the claim "Q is
consistent". This is because "Q is inconsistent" is a Sigma-1 statement,
and so if true provable in T.

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

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus