[FOM] formalism freeness

[Harvey Friedman]

TOBY MEADOWS:

>>> > Kennedy (2013) suggests a pluralistic approach involving generalised
>>> > constructibility and more widely the concept of "formalism freeness",
>>> > and its dual, the concept of the entanglement of a semantically given
>>> > object with its underlying formalism.

FRIEDMAN

>>> I am a little bit familiar with generalized constructibility, and I
>>> assume that "formalism freeness" means a deliberate non commitment to
>>> any fixed formalism? I would like an elaboration of what
>>> "entanglement" means here, e.g., by examples.

MEADOWS:

>> I might invite Professor Kennedy to talk about this.

JULIETTE KENNEDY:

> Thanks for the below invitation to discuss the ideas of my 2013 BSL paper,
> formalism freeness and entanglement in particular. (I have seen just a part
> of the thread so I am not sure who asked the question.)
>
> One of the things formalism freeness refers to is the stability of a
> semantically given structure under change of the underlying formalism.
>
> The concept comes from Gödel's 1946 Princeton Bicentennial Lecture, in which
> he notes that with the concept of computability, many different formalisms
> define the same class of functions. He then asks whether the "formalism
> independence" (as he called it) exhibited by the concept of computability,
> might be obtained in the cases of provability and definability.

FRIEDMAN

I see what you are referring to, and I would have called it "formalism
robustness", following the term "robust" which generally means
invariant under reasonable changes.
https://en.wikipedia.org/wiki/Robustness Maybe the term isn't precise
or doesn't fit exactly, but "free" also has problems. E.g., I though
that "formalism free" emphasized that "there is no formalism".

In a sense, FOL= itself is robust, in that you arrive at essentially
the same thing no matter how you set it up, as long as you set up
reasonably.

KENNEDY:

> ... With
> Magidor and Väänänen we were able to show that many different logics can be
> substituted for first order logic in the construction of L (and the same is
> true of substituting other logics for second order logic in the Myhill-Scott
> characterization of HOD). That is, L does not depend in an essential way on
> being defined in first order logic (and the respective is true of HOD).
>
> On the other hand by substituting other logics for first order logic in the
> construction of L, one sees some interesting new intermediate models. See:
>
> https://www.newton.ac.uk/files/preprints/ni16006_0.pdf

FRIEDMAN:

But you presumably need to assume or "know" that 0# exists in order to
get any intermediate models. This reminds me of an old question going
back to Solovay. In general informal terms, 0# seems very special.
This is the natural explicitly given exit out of L. I remember that
Solovay made a series of conjectures bearing on this, and most were
resolved in the direction of not characterizing 0#.

My question is: what is the state of the art positive results
concerning 0# being special? Jensen covering seems like a germ of such
a positive result, and say elementary embedding from L into L. But are
they really what we should be looking for?

Recall that we are in comparatively great shape with regard to the
Turing jump and the higher levels of the hyperarithmetic hierarchy.
For the Turing jump there is the robust theory of relative r.e.
completeness. For the latter there is the theory of 2-least upper
bounds. What about the hyperjump?

KENNEDY:

>... The dual notion, "entanglement" has to do with something logicians are very
> familiar with, namely that a small change in the signature induces a massive
> change. For example, one has a 0-1 law for (finite) relational structures,
> but the 0-1 law fails if one allows function symbols in the language.

FRIEDMAN

This is why I tend to like "formalism robustness" as a name.

Harvey Friedman