  We extend Lawvere-Pitts prop-categories (aka. hyperdoctrines) to develop a
general framework for providing "algebraic" semantics for nonclassical
first-order logics. This framework includes a natural notion of substitution,
which allows first-order logics to be considered as structural closure
operators just as propositional logics are in abstract algebraic logic. We then
establish an extension of the homomorphism theorem from universal algebra for
generalized prop-categories and characterize two natural closure operators on
the prop-categorical semantics. The first closes a class of structures (which
are interpreted as morphisms of prop-categories) under the satisfaction of
their common first-order theory and the second closes a class of
prop-categories under their associated first-order consequence. It turns out
these closure operators have characterizations that closely mirror Birkhoff's
characterization of the closure of a class of algebras under the satisfaction
of their common equational theory and Blok and J\'onsson's characterization of
closure under equational consequence, respectively. These "algebraic"
characterizations of the first-order closure operators are unique to the
prop-categorical semantics and do not have analogs, for example, in the
Tarskian semantics for classical first-order logic. The prop-categories we
consider are much more general than traditional intuitionistic prop-categories
or triposes (i.e., topos representing indexed partially ordered sets).
Nonetheless, to our knowledge, our results are still new even when restricted
to these special classes of prop-categories.
