I see adjointness between the two concepts of "being a definable *set*" and "being a set-builder *formula*":




---



> 
> A set $X$ is **definable** when there is a formula $\phi(x)$ such that $X = \lbrace x : \phi(x)\rbrace$.
> 
> 
> 




---



> 
> A formula $\phi(x)$ is a **set-builder** when there is a set $X$ such that $X = \lbrace x : \phi(x)\rbrace$.
> 
> 
> 




---


In which (category theoretical) contexts this adjointness is made explicit and valuable?



Another adjoint pair: Definable sets and set-builder formulas
Given any pair of sets $X, Y$ (let me not be too specific about what "sets" means because what follows is robust with respect to changes in the definition), any relation $R : X \times Y \to 2$ whatsoever induces a contravariant adjunction between the poset of subsets of $X$ and the poset of subsets of $Y$ given by


$$2^X \ni S \mapsto F(S) = \{ y \in Y : xRy \forall x \in S \} \in 2^Y$$


$$2^Y \ni T \mapsto G(T) = \{ x \in X : xRy \forall y \in T \} \in 2^X.$$


A contravariant adjunction between posets is also known as an [antitone Galois connection](http://en.wikipedia.org/wiki/Galois_connection#Antitone_Galois_connection). Any such thing determines two closure operators, one on $2^X$ and one on $2^Y$, and it is often interesting to determine the corresponding closed subsets. Examples:


1. Let $L/K$ be a Galois extension, let $X = L$, and let $Y = \text{Gal}(L/K)$. The relation is "the element $y \in Y$ fixes the element $x \in X$." The adjunction sends a subset of $L$ to the subgroup of the Galois group fixing it and sends a subset of the Galois group to its fixed field. The fundamental theorem of Galois theory tells us that the closed subsets are the subgroups of the Galois group on the one hand and the subextensions of the Galois extension on the other.
2. Let $X = k[x\_1, ..., x\_n]$ be a polynomial ring over an algebraically closed field and let $Y = \mathbb{A}^n$ be the corresponding affine $n$-space. The relation is "the polynomial $x \in X$ vanishes on the point $y \in Y$." The adjunction sends a set of polynomials to the variety it cuts out and sends a set of points to the ideal of functions vanishing on it. The Nullstellensatz tells us that the closed subsets are the radical ideals on the one hand and the Zariski-closed subsets on the other (the second statement is tautologous; this is the definition of being Zariski closed. But the first one has content).
3. Let $X$ be the set of models of a first-order theory $T$ and let $Y$ be the set of possible sentences that could be added to $T$. The relation is "the sentence $y \in Y$ is true in the model $x \in X$." The adjunction sends a set of models to the set of sentences true in every model and sends a set of sentences to the set of models of those sentences (together with $T$). The completeness theorem tells us that the closed subsets are the deductively closed sets of sentences on one hand and whatever their sets of models are on the other.


In your example one of the "sets" is the set of all sets, the other is the set of all formulas, and the relation is "the set $x \in X$ satisfies the formula $y \in Y$." It is a version of the slogan "syntax is adjoint to semantics," an observation first made, as far as I know, by Lawvere. 


