There are a number of algebraic theories (in equational logic specifically, no predicate symbols besides equality) which are of finite type (so the language has only finitely many function symbols) but not finitely axiomatizable. Often one demonstrates this with an infinite sequence of structures for the language, but in some cases one can establish this linguistically.

A simple example involves work with hyperidentities (check out my arxiv preprint for details, 1408.something something). We posit the theory given by the hyperidentity F(F(x)) ideq F(F(F(x))), which is short hand for an equational theory that says every unary function term t in a language has its square equal its cube, or forall x t(t(x)) = t(t(t(x)).

If we choose a language with one binary function symbol, we get a finitely axiomatizable theory. I forget what happens with two unary function symbols. With three, you get a recursively axiomatizable theory which is not finitely axiomatizable. You show this by looking at the Thue Morse sequence and use square free fragments to build long terms and show long instances are not derivable from short instances of the axioms.

It gets real fun with more complicated hyperidentities and larger sets of function symbols. Check out the preprint for other families of examples.

Gerhard "Is The Question Computably Decidable?" Paseman, 2020.06.19.