A name is said to be "fresh" if it does not occur in any existing properties or definitions in the current context.

A freshness qualifier (keyword: fresh) can be added to premises in compound judgments to require that the corresponding premise name supplied when applying the judgment is fresh.