What does a Hilbert-type axiomatisation look like? The first thing one has to do is to fix a (formal) language. Usually one chooses first-order predicate logic with identity, i.e., a language containing names for variables (and, possibly, for constants), names for functions (if necessary), names for predicates including the identity predicate, logical connectives and quantifiers, and a set of grammatical rules to form sentences. The restriction to first-order logic means that only variables can be quantified over. Without going into details, it should be remarked that a more expressive language can be chosen, e.g., whereby quantification over predicates is allowed as well.