Negation (Primitive Recursion)

Definition

Negation ( Primitive Recursion)

With representing false and representing true, negation is represented by the primitive-recursive function

where the dotted minus denotes truncated subtraction. Thus

On Boolean inputs, and . On all natural numbers, it is the zero test: it returns exactly when .

Construction

The constant function supplies , and the projection function supplies . Composition passes both to truncated subtraction:

Example

Negating encoded truth values