Incomparable consistency strengths

[JOSEPH SHIPMAN]

“By diagonalization” is not explicit.

Can the sentence be written down? It doesn’t need to be 100% formalized but it still needs to be explicitly given which is not the same as a proof that there is such a thing.

Illustrative example: The set theoretic axiom known informally as “V=L” is very difficult to write down in full explicitly, but it can still be written down clearly enough in a page or so of standard-journal-level-of-formality mathematical exposition, by giving some explicit operations from sets to sets and a transfinite construction indexed by the ordinals and stating that all sets appear at some stage of this construction. 

That’s acceptable but an “existence proof” citing “diagonalization” is not even if it is “implicitly constructive”, because it conceals a whole meta-later of formalization and coding and depends on many arbitrary choices.

Criterion: your definitions should be explicit enough that two graduate students you set to produce actual formalized sentences A and B suitable to my query will produce sentences that, while not identical, are logically equivalent. V=L is the kind of thing I expect would result in logically equivalent “renderings” from different graduate students. The Rosser sentences you hint at will require a lot more detail from you before I’d have that confidence.

— JS

Sent from my iPhone

> On Apr 30, 2021, at 10:50 AM, Mirko Engler <mir.engler at gmail.com> wrote:
> 
> 
> 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/080d2c7d/attachment-0001.html>