Definitions

Definitions can have the form

The name must be a new constant name, one that has never appeared before in any axioms or definitions, and the term is an expression with the one restriction that every substitution leaves it unaltered. Saying this another way, the term has no free variables.

For example, let’s look at the definitions of zero and additive identity in the fundamental facts about real numbers.

Although that is the presentation style on the website, internally, additive identity is defined in a different form that is equivalent, but less familiar from textbooks:

This “internal” form has the variables x and y in it, but both are bound in functional terms like {x. ... } and {y. ... }, so substitutions leave them alone.

The two forms of definitions can be converted to each other by unbinding or rebinding the equation.

Any definition of this kind can be treated as a true statement (like an axiom), and using it in a proof can never result in a contradiction – unless a contradiction was already provable without the new definition.