« first day (22 days earlier)      last day (18 days later) » 

18:07
@spaceisdarkgreen So it will include some sort of coding of these concepts in PA, and then carrying this coding over inside ZFC by means of $\omega$?
@spaceisdarkgreen By this, I was trying to understand why the existence and uniqueness proofs were an obstacle here. After all, any existence-and-uniqueness proof is relativisable to M in ZFC+.
And we should get an existence-uniqueness proof of the relativised concept...
I am thinking about some things at the moment, so feel free not to respond just yet (but you may, if you'd like)
(I'll be back in less than a day)
On a related note, is there a book discussing this "transitive model axiom"?
I thought about Chang&Keisler's book (Model theory), but it seems not to have a table of contents... :)
18:45
@LinearChristmas the coding could go like that. Or could do something more ergonomic where we make better use of set theory’s expressive power. Doesn’t really matter unless we actually want to do it for some reason.
@LinearChristmas were an obstacle where? Don’t understand.
@LinearChristmas Most set theory books will talk about transitive models of ZFC, and talk about how it is strictly stronger than Con(ZFC) to assume they exist. Especially during the treatment of forcing… I’m pretty sure it’s laid out explicitly in Kunen.

« first day (22 days earlier)      last day (18 days later) »