Definition:Definitional Abbreviation

From ProofWiki
Jump to navigation Jump to search


When discussing a formal language, some particular WFFs may occur very often.

If such WFFs are very unwieldy to write and obscure what the author tries to express, it is convenient to introduce a shorthand for them.

Such a shorthand is called a definitional abbreviation.

It does not in any way alter the meaning or formal structure of a sentence, but is purely a method to keep expressions readable to human eyes.


A very common example of a definitional abbreviation in predicate logic is to write:

$\exists! x: \phi \left({x}\right)$

in place of the formally correct alternatives:

$\exists x: \left({ \phi \left({x}\right) \land \forall y: \left({\phi \left({y}\right) \implies x = y}\right)}\right)$
$\exists x: \forall y: \left({ \phi \left({y}\right) \iff x = y}\right)$

to express that 'there exists a unique $x$ such that $\phi \left({x}\right)$ holds', where $\phi$ is some unary predicate symbol.

The benefit of this construct readily becomes apparent when $\phi$ is already a very long formula in itself.