@LinearChristmas I think things have gotten pretty muddled here. I would suggest going back and thinking about the issue of ZFC proving varphi. But varphi depends on M so this is nonsense. What ZFC actually proves is "if M is a countable transitive model of a large fragment of ZF to define omega, the power set operation and omega_1, then varphi(M)"

If you go the ZFC+ route, then you're all set on these first issues, but then if you try to relativize this statement to M, you're left with the question of how to interpret the M (the constant symbol) in M. Or more generally, that M is a model of (arbitarily large fragments of) ZFC, but not a model of ZFC+...

@spaceisdarkgreen What does it mean exactly, syntactically speaking, to say that “one cannot relativise a concept”?

Can't I always try, no matter the formula? I might just not like the result

@spaceisdarkgreen Fair enough... The last sentence “Or more generally, that M is a model of (arbitarily large fragments of) ZFC, but not a model of ZFC+...” I would have earlier said that M can also be made into a model for large enough parts of ZFC+

Simply by the "twice relatisation invariance"

However, you are correct that the definition of relativisation I had, strictly speaking, did not include relativising M itself.

I wonder what would break if simply defining M^M = M... Yes, M $\notin $ M, but that's no hurdle for syntactic relativisation.

@LinearChristmas You can always relativize relations, since thats just a formula. But to define a constant or a function there is always an existence and uniqueness proof that goes along with the definition. Like for instance when you write P(omega)^M you're assuming that M satisfies enough axioms to carry out the definition of P(omega).

@LinearChristmas But, yes, techinically, syntactically you could try but not necessarily like the results. e.g. you could write out some long formula that means z = P(omega) then have a sentence "\exists z (z=P(omega))\land phi(z)" and then relativize it to a model where P(\omega) makes no sense. It just generally ceases to be independent of your choice of how you phrased z = P(omega), and ceases to have the behavior you probably want.

@spaceisdarkgreen How is the axiom "exists a transitive model of ZFC" phrased exactly?

@spaceisdarkgreen That's very lucid, yes, thank you.

But if there is an existence and uniqueness proof of a constant / function, then that can always be completed as relativised to M, in ZFC+

So you must be saying, essentially, that the problem is the following: Even if (a) the definition of the concept is absolute, and (2) the ex. and uniq. proof may be done in relativised form, a subpart of the proof is not absolute.

Is that correct?

@LinearChristmas Fairly complicated. Saying there's a transitive set is easy of course, but then you need to formalize sentences, satisfaction of sentences in a model, then define what ZFC is, which includes e.g. a definition of what it means to be an instance of the replacement scheme

@LinearChristmas I'm not sure what you're getting at concerning ZFC+

I'm trying to follow, but issue at the bottom still seems to be there's no reason to expect M to be a model of ZFC+, in any reasonable sense. You can't interpret M as M, and while you could define "relativization to M" of a sentence in ZFC+'s language that way syntactically, there's no reason to expect it to behave "normally" as you aren't really interpreting the sentence inside M.

Though I haven't thought through trying what you were initially doing in that way to know exactly where it would break.