POSTS, SET-THEORY
(Comment added in 2023-01-01: I wrote this post three months ago, but it was not posted at that time as I did not update my homepage.)
After the CHEESE workshop (so the next day of the workshop) I had a short chance to talk with Richard Matthews, and he told me that he would start his new postdoc position under Krivine and study classical realizability. One question he raised about classical realizability was: is there any relation between classical realizability and (iterated) symmetric model?
I conjecture classical realizability shows quite different nature from conventional set-theoretic constructions for models of ZF:
According to Streicher, Krivine’s Classical realizability provides a realizability topos over an order-pca. I do not know realizability topoi and order-pcas in detail (I only know terminologies), but I heard that realizability topoi are quite different from Grothendieck topoi and forcing and symmetric models are associated with the latter, which is known by the paper Complete topoi representing models of set theory by Blass and Scedrov.
However, I may miss something: Krivine also proved that the classical realizability model embeds a transitive class that is an elementary extension of a ground model. (See Theorem 30 of his On the structure of classical realizability models of ZF.) It may suggest classical realizability model may behave better than the “ordinary” realizability model.
It is just a rough conjecture, so who knows, I might be wrong. Or there might be another possibility, like an analogue of the Jech-Sochor theorem, so we might simulate some “bounded” results over the classical realizability using (iterated) symmetric models. For now, only god knows the true result, and then who will grip the star in “the book?”