Modal theorems valid in a set theory model

Question

This is the question i would like to discuss, properly stated.

Given a model $M$ for a collection of set theory axioms (ZFC, for example), list all basic modal formulas $\phi$ such that $M\Vdash \phi$ and $\nVdash \phi$ (that is, $\phi$ is valid on the basic modal frame $M$, and $\phi$ is not a formula valid in the class of all basic modal frames).

I've been studying modal logic for a while now, albeit slowly. Recently, i've encountered the concept of frame definability, which is about relating modal formulas to the class of frames they are valid on. Now, i've never had any formal training on Set Theory, but thanks to the internet, i believe a large part of it consists of stating a collection of logical sentences such that any structure with signature $(W,\in)$ that models said collection behaves much like we'd expect sets to behave.

As it turns out, the structure signature $(W,\in)$ is precisely that of the basic modal frames, with the membership relation providing the interpretation for the $\Diamond$ modality. I can't help but wonder if there aren't any ways to define sets using modal logic, or if not, how "close" can we get to them.

Alas, i'm not sure if these questions are appropriate on a StackExchange site (too vague). So for now i'd like to know something simpler. We know that there are many modal formulas valid on the class of all frames; that's the smallest normal modal logic. My question is then, what does the set of modal formulas valid on a model of, say, ZFC, or NF, look like? Just how much bigger than the smallest normal modal logic is that set?

As a follow-up, maybe i could ask (if it isn't asking too much) if there are modal formulas that can distinguish between different models of the same set theory, that is, by being valid on one model but not in another.

EDIT: This question's previous wording was simpler; all i asked was whether there were a non-trivially (that is, not a member of the smallest normal modal logic) valid modal formula or not. As it turns out, there's a pretty easy one, $\Diamond \top$, since every set must be a member of another set (and in fact the infinite set consisting of $\{ \Diamond \top, \Diamond \Diamond \top, \Diamond \Diamond \Diamond \top, ... \}$ is valid).

I'm changing it to a harder statement (asking to define the entire logic generated by the set model), but perhaps even more interesting would be asking if there are non-trivially valid modal formulas for a "converse set theory" $M=(W,\in_c)$ model, in which $x\in_c y $ iff $y \in x$ (and, of course, your choice of axioms would need to be altered, in order to invert the operands in the $\in$ predicate). Dunno what to ask...

Answer 1

$(p\wedge\lozenge p\wedge\square q)\to \lozenge(p\wedge\lozenge q)$. I guess it holds in the models of ZFC. The intuitive meaning is 'if one set is in another set, then they can be both in a third set'

Answer 2

I think that when you talk about models of set theory (considered as modal frames), the answer would need to start with: If ZFC is consistent, then ... This may be not relevant if you are talking about modal formulas that are valid in ALL such frames, but if you wish to distinguish models, then, I believe, consistency of ZFC is to be assumed.

Secondly, perhaps not so closely related to the original question (but taking into account that the question is vague :) You'll find a lot of interesting in the following publication:

Goivanna D'Agostino. Modal logic and non-well-founded Set Theory: translation, bisimulation and interpolation. PhD Thesis, 1999, Institute for Logic, Language and Computation, Amsterdam.

Therein, modal formulas are interpreted as you wanted — in sets with $\ni$ relation (inverse membership). With two differences: first, in the underlying set theory, in place of the Foundation axiom, he accepts Aczel's Anti-Foundation Axiom, AFA (see e.g. Wikipedia for their formulation); second, it is natural to consider (and he considers) infinitary modal formulas (infinite conjunctions are allowed instead of finite). In this setting, e.g., sets of modal formulas are themselves sets in the sense of this AFA set theory, and modal formulas are so, too. So, modal formulas are sets that may have elements (formulas) etc. A intriguing fact is that every set, modulo bisimulation, is determined by a (unique) infinitary modal formula. And so on and so forth.