Incomparable consistency strengths

[JOSEPH SHIPMAN]

Still very different from axioms like V=L, which capture constructions having an intrinsic meaning independent of *any* arbitrary choices. 

Sent from my iPhone

> On May 3, 2021, at 1:12 PM, Richard Heck <richard_heck at brown.edu> wrote:
> 
> On 4/30/21 11:47 AM, JOSEPH SHIPMAN wrote:
>>>>> 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.
>>> 
>> 
>> “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.
> 
> If we take any fixed set of choices---say, those in Boolos, Burgess, and
> Jeffrey---then this would be quite straightforward. Diagonalization is
> not just 'implicitly constructive'. It's as constructive as anything
> gets, if one wants to do it that way.
> 
> Gödel's own definitions each uses abbreviations from earlier ones, and
> some specific Gödel numbers are abbreviated, e.g., the codes of some
> axioms. (These are not explicitly calculated, though one could easily do
> that.) But everything is fully explicit (as it needed to be at the
> time). It would be trivial to write down a Rosser sentence as explicitly
> as Gödel writes down the first Gödel sentence. In fact, that's what
> Rosser does. He just substitutes his new provability predicate,
> explicitly defined, for Gödel's.
> 
> Some years ago, a student of mine used LaTeX macros to produce an
> explicit formalization of the provability predicate from Boolos's "Logic
> of Provability". It's about four and a half pages, completely
> unabbreviated. It would be easy to do the same for Boolos's
> concatenation operator, from which diagonalization is then easily
> definable (as Boolos does it). I'm teaching this stuff this summer.
> Maybe I'll do that. You could do something similar in Python or whatever.
> 
> Riki
> 
> 
> -- 
> 
> ----------------------------
> Richard Kimberly (Riki) Heck
> Professor of Philosophy
> Brown University
> 
> Pronouns: they/them/their
> 
> Email:           rikiheck at brown.edu
> Website:         http://rkheck.frege.org/
> Blog:            http://rikiheck.blogspot.com/
> Amazon:          http://amazon.com/author/richardgheckjr
> Google Scholar:  https://scholar.google.com/citations?user=QUKBG6EAAAAJ
> ORCID:           http://orcid.org/0000-0002-2961-2663
> Research Gate:   https://www.researchgate.net/profile/Richard_Heck
>