# Definition:Definitional Abbreviation

## Definition

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.

## Example

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.