Editing Universal quantification (section)

== As adjoint ==
In [[category theory]] and the theory of [[elementary topos|elementary topoi]], the universal quantifier can be understood as the [[right adjoint]] of a [[functor]] between [[power set]]s, the [[inverse image]] functor of a function between sets; likewise, the [[existential quantifier]] is the [[left adjoint]].<ref>[[Saunders Mac Lane]], Ieke Moerdijk, (1992) ''Sheaves in Geometry and Logic'' Springer-Verlag. {{isbn|0-387-97710-4}} ''See page 58''</ref>

For a set <math>X</math>, let <math>\mathcal{P}X</math> denote its [[powerset]].  For any function <math>f:X\to Y</math> between sets <math>X</math> and <math>Y</math>, there is an [[inverse image]] functor <math>f^*:\mathcal{P}Y\to \mathcal{P}X</math> between powersets, that takes subsets of the codomain of ''f'' back to subsets of its domain. The left adjoint of this functor is the existential quantifier <math>\exists_f</math> and the right adjoint is the universal quantifier <math>\forall_f</math>.

That is, <math>\exists_f\colon \mathcal{P}X\to \mathcal{P}Y</math> is a functor that, for each subset <math>S \subset X</math>, gives the subset <math>\exists_f S \subset Y</math> given by
:<math>\exists_f S =\{ y\in Y \;|\; \exists x\in X.\ f(x)=y \quad\land\quad x\in S \},</math>
those <math>y</math> in the image of <math>S</math> under <math>f</math>.  Similarly, the universal quantifier <math>\forall_f\colon \mathcal{P}X\to \mathcal{P}Y</math> is a functor that, for each subset <math>S \subset X</math>, gives the subset <math>\forall_f S \subset Y</math> given by
:<math>\forall_f S =\{ y\in Y \;|\; \forall x\in X.\ f(x)=y \quad\implies\quad x\in S \},</math>
those <math>y</math> whose preimage under <math>f</math> is contained in <math>S</math>.

The more familiar form of the quantifiers as used in [[first-order logic]] is obtained by taking the function ''f'' to be the unique function <math>!:X \to 1</math> so that <math>\mathcal{P}(1) = \{T,F\}</math> is the two-element set holding the values true and false, a subset ''S'' is that subset for which the [[predicate (mathematical logic)|predicate]] <math>S(x)</math> holds, and
:<math>\begin{array}{rl}\mathcal{P}(!)\colon \mathcal{P}(1) & \to \mathcal{P}(X)\\ T &\mapsto X \\ F &\mapsto \{\}\end{array}</math>
:<math>\exists_! S = \exists x. S(x),</math>
which is true if <math>S</math> is not empty, and
:<math>\forall_! S = \forall x. S(x),</math>
which is false if S is not X.

The universal and existential quantifiers given above generalize to the [[presheaf category]].