Axiom systems for first order logic with finitely many variables
James Steven Johnson · Journal of Symbolic Logic · 1973
Abstract J. D. Monk has shown that for first order languages with finitely many variables there is no finite set of schema which axiomatizes the universally valid formulas. There are such finite sets of schema which axiomatize the formulas valid in all structures of some fixed finite size.