In his 1946 Princeton Bicentennial Lecture Gödel suggested the problem of finding a notion of definability for set theory which is "formalism free" in a sense similar to the notion of computable function --- a notion which is very robust with respect to its various associated formalisms.
One way to interpret this suggestion is to consider standard notions of definability in set theory, which are usually built over first order logic, and change the underlying logic. We show that constructibility is not very sensitive to the underlying logic, and the same goes for hereditary ordinal definability (or HOD). There are also some interesting intermediate models. This is joint work with Menachem Magidor and Jouko Väänänen. Time permitting we will present our second template, dealing with entanglement, specifically the entanglement of a logic with a predicate of set theory. This is the concept of symbiosis introduced by Väänänen in his 1978 Manchester thesis.