I have two definitions that seem equivalent of existential and universal quantifications as left and right adjoints of subsitution [1]. But I seem to have a counterexample...
So first for the definition take a function $f: A \to B$ then this induces a function or even a functor $$ f^{-1}: \mathcal P(B) \to \mathcal P(A)$$ and two other functors from $\mathcal P(A)$ to $\mathcal P(B)$ defined by
$\exists_f(X) = \{y: \exists x(x \in X \wedge f(x) = y)\}$
$\forall_f(X) = \{y: \forall x(f(x) = y \implies x \in X)\}$.
where the fact that these are left and right adjoints is given by the equation
$\exists_f(X) \subseteq Y \iff X ⊆ f^{−1}(Y)$
$f^{−1}(Y) \subseteq X \iff Y ⊆ \forall_f(X)$
Now I thought I'd take a simple example consisting of two types one containing people P = {A, E, B} with names N = {Adam, Αδάμ, Eve} B being a little baby boy that has not yet been given a name. So we have
f = { Adam ↦ A, Αδάμ ↦ A, Eve ↦ E }
and hence
$f^{-1}$={{} ↦ {},
{A} ↦ {Adam, Αδάμ}, {E} ↦ {Eve}, {B} ↦ {},
{A, B} ↦ {Adam, Αδάμ}, {B, E} ↦ {Eve}, {A,E} ↦ {Adam, Αδάμ, Eve},
{A, E, B} ↦ {Adam, Αδάμ, Eve} }
$\exists_f$ = {{} ↦ {},
{Adam} ↦ {A}, {Αδάμ} ↦ {A}, {Eve} ↦ {E},
{Adam, Αδάμ} ↦ {A}, {Adam, Eve} ↦ {A, E}, {Αδάμ, Eve} ↦ {A, E},
{Adam, Αδάμ, Eve} ↦ {A, E}
}
$\forall_f$ = {{} ↦ {},
{Adam} ↦ {}, {Αδάμ} ↦ {}, {Eve} ↦ {E},
{Adam, Αδάμ} ↦ {A}, {Adam, Eve} ↦ {E}, {Αδάμ, Eve} ↦ {E},
{Adam, Αδάμ, Eve} ↦ {A, E}}
But then we have the following counterexample to the adjunction it seems. Take the property Male = {A, B}
$f^{-1}$(Male) = {Adam, Αδάμ} ⊆ {Adam, Αδάμ} $\iff$ Male ⊆ $\forall_f${Adam, Αδάμ} = {A}
but clearly {A, B} ⊈ {B}
So where have I gone wrong here?
[1] I am coming at this from reading the article "Categorical Logic and Model Theory" in "Categories for the Working Philosopher" edited by Elaine Landry. https://books.google.co.uk/books?id=RIM8DwAAQBAJ&lpg=PA113&ots=VLJLR-Mn50&lr&pg=PA118#v=onepage&q&f=false The other is defined here on Stack Exchange in the answer to the question Right-adjoint to the inverse image functor
You haven't calculated $\forall_f(\{\mathrm{Adam}, A\delta\alpha\mu\})$ correctly. $\forall x (f(x) = B \implies x \in X)$ is true for any $X$ because there are no $x$ such that $f(x) = B$, so $B \in \forall_f(X)$ for any $X$.