« first day (23 days earlier)      last day (17 days later) » 

Linear Christmas
Linear Christmas
18:33
@spaceisdarkgreen Hmm... I did not find the entails symbol $\vDash$ in the registry of his newer set theory book. In the older one (Set theory and independence proofs), there is, of course, a lot of talk about transitive models but I could not find discussions on “transitive model axiom” or such.
Linear Christmas
Linear Christmas
18:50
The possibility of expressing, in the language of ZFC, statements such as "is a model of ZFC" or even expressing "is a model of some specified finite part of ZFC"... sound off alarms in my head a little bit.
For if we take a large enough finite part of ZFC, capable in particular of proving the reflection principle for itself, and expressing "is a model (of some set of sentences)", then this finite part of ZFC would prove its own consistency.
I do see some ways out of this conundrum:
a) maybe the proof of the reflection principle is not "closed wrt any finite part of ZFC", always requiring something not from a chosen finite list to prove itself;
b) a similar non-closedness thing but having to do with expressing "is a model of" or some related theorem in the background;
c) the word "model" really-really does not have the connotations I thought it did.
Linear Christmas
Linear Christmas
19:26
@spaceisdarkgreen The "obstacle" part was replying to your comment "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)."
Any existence and uniqueness proof attached to a definition will work for M in ZFC+, just in relativised form, because whatever axioms are used for the proof are there in ZFC+ in relatived form.
That's all I meant to say, I guess.

« first day (23 days earlier)      last day (17 days later) »