  The purpose of this work is to complete the algebraic foundations of
second-order languages from the viewpoint of categorical algebra as developed
by Lawvere. To this end, this paper introduces the notion of second-order
algebraic theory and develops its basic theory. A crucial role in the
definition is played by the second-order theory of equality $\M$, representing
the most elementary operators and equations present in every second-order
language. The category $\M$ can be described abstractly via the universal
property of being the free cartesian category on an exponentiable object.
Thereby, in the tradition of categorical algebra, a second-order algebraic
theory consists of a cartesian category $\Mlaw$ and a strict cartesian
identity-on-objects functor $\M \to \Mlaw$ that preserves the universal
exponentiable object of $\Mlaw$. Lawvere's functorial semantics for algebraic
theories can then be generalised to the second-order setting. To verify the
correctness of our theory, two categorical equivalences are established: at the
syntactic level, that of second-order equational presentations and second-order
algebraic theories; at the semantic level, that of second-order algebras and
second-order functorial models.
