Incomparable consistency strengths

[Richard Heck]

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