Incomparable consistency strengths

[Mirko Engler]

Okay. By Diagonalization, there exists an R, s.t.

PA |- R <-> exists x (Proof (x, neg( R)) and forall z < x (not Proof (z,
R)))

Let phi:= not R and
      psi:= not (exists x (Proof(x, R) and forall z < or = x not Proof (z,
neg(R)))).

These two can be seen to be the incomparable Rosser sentences. I think that
is a construction by D. Guaspari / R. Solovay, but I am not sure. Check
Smorynski.
Is that what you mean by "given explicitly"? I am not aware of any
"natural" example.

Best,

Mirko Engler

Am Fr., 30. Apr. 2021 um 14:34 Uhr schrieb JOSEPH SHIPMAN <
joeshipman at aol.com>:

> This works but it involves finding “two incomparable Rosser sentences”.
> That’s an existence proof, I asked if they could be given explicitly.
> Rosser sentences are even worse for that than Godel sentences.
>
> — JS
>
> Sent from my iPhone
>
> On Apr 30, 2021, at 8:19 AM, Mirko Engler <mir.engler at gmail.com> wrote:
>
> 
> Dear Joseph Shipman,
>
> I guess a standard way of constructing those theories A and B is the
> following:
>
> First you take something like two incomparable Rosser-sentences phi and
> psi, s.t. PA does not prove phi -> psi and PA does not prove psi -> phi.
> These sentences will be Pi1 and hold in the standard model. For any
> consistent r.e. extension T of PRA,  every Pi1-sentence is modulo Con(T)
> provably equivalent to a consistency-statement, i.e. there are
> Pi1-sentences a and b s.t.:
> PRA+Con(PRA) |- phi <-> Con(PRA+a)
> PRA+Con(PRA) |- psi <-> Con(PRA+b)
> As Con(PRA+a) and Con(PRA+b) hold in the standard model, a and b hold in
> standard model themselves (for being Pi1).
> Now take A:= PRA+a and B:=PRA+b, so A and B also hold in the standard
> model. As PA |- Con(PRA), both the assumption that
> PA|-Con(A) -> Con(B) and PA|-Con(B) -> Con(A) lead to the contradiction
> that PA|- phi -> psi and PA|- psi -> phi.
> Of course, ZF|-Con(A) and ZF|-Con(B).
>
> All of the details can be found in Smorynski: Self-Reference and Modal
> Logic. Ch 6, Corollary 3.3. and Ch 7, Corollary 2.6.
>
> Best regards,
>
> Mirko Engler
>
> Am Fr., 30. Apr. 2021 um 07:26 Uhr schrieb JOSEPH SHIPMAN <
> joeshipman at aol.com>:
>
>> Can anyone give explicitly (not merely prove they exist, but actually
>> give the axioms or schemes in a level of specificity and detail typical of
>> published math papers) two axiomatized theories A and B such that
>> 1) ZF proves Con(A)
>> 2) ZF proves Con(B)
>> 3) PA does not prove Con(A)->Con(B)
>> 4) PA does not prove Con(B)->Con(A)
>> ?
>>
>> — JS
>>
>> Sent from my iPhone
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210430/3da34f6d/attachment-0001.html>