In the first half of the talk I will present the framework of nominal
algebra, an algebraic framework designed to axiomatise systems with
binding (such as lambda-calculus and first-order-logic) in the same
way as 'ordinary' algebra axiomatises groups, rings, and fields.

I will discuss applications to axiomatise substitution,
lambda-calculus, and first-order logic.

In the second half of the talk I will investigate a version of
first-order logic based on nominal ideas (and with a semantics as a
nominal algebra theory) which has strictly greater expressive power
than first-order logic; I will discuss its relation to first- and
second-order logic and state conservativity results with respect to
first-order logic, and a cut-elimination result.