Abstract: Abstract A new first-order logic, functional logic, was proposed recently by Staples, Robinson and Hazel. The logic provides a formal means of describing and reasoning about dependence on an implicit parameter, a prime motivation being the unification of the Hoare logic used to reason about procedural programs with the powerful and well established techniques of classical logic. Viewed more abstractly, independently of possible applications, functional logic may be described as a logic with primitives, axioms and inference rules appropriate for reasoning about the properties of mathematical functions. In this paper, the completeness of functional logic is proved; that is, it is shown that any term of a theory in the logic which is true in all models is a theorem.