I've been mechanizing some set theory (IZF).
I want to experiment with encoding a fragment of first order constructive logic in terms of sets and define separation in terms of simpler primitives.
I think you want something like
$$ \{ x \in e \mid P \} = \{ \{ x \mid y \in [P] \} \mid x \in e \}$$
$$ \begin{align*} [\bot] = & \emptyset \\ [\top] = & \{ \emptyset \}\\ [P \vee Q] = & [P]\cup [Q] \\ [P \wedge Q] = & \{ [P] \mid x \in [Q] \}\\ [P \rightarrow Q] = &[\{(x, [\top]) \mid x \in [P]\} = \{ (x, [Q]) \mid x \in [P] \}] & \\ [\exists x\in e. P] = & \{ [P] \mid x \in e \} \\ [\forall x\in e. P] = & [\{(x, [\top]) \mid x \in e\} = \{ (x, [P]) \mid x \in e \}]\\ [e_1 = e_2] = & [ e_1 \in \{ e_2 \} ]\\ [ e_1 \in e_2] = & ? \end{align*}$$
Some of the details feel very unclear to me and I'm not sure how wanting constructive logic changes things.
I think you can pretty much always do Goedel sentences but that's kind of a sledgehammer and wouldn't be nice at all in a theorem prover.
I'm sure there must be a standard sort of way to do this coding in the literature?