Go backward to A.1 PreliminariesGo up to A Defining New NotionsGo forward to A.3 Explicit Function Definitions |

is anp(x_{0}, ...,x_{n-1}) : <=>F

We callforallx_{0}, ...,x_{n-1}:p(x_{0}, ...,x_{n-1}) <=>F.

A predicate `p` is uniquely characterized by an explicit definition,
i.e., there is exactly one `p` that satisfies the new axiom (because for
every `x`_{0}, ..., `x`_{n-1},
`F` has a single truth value).

The restriction that `p` does not occur in `F` is necessary, e.g.
to avoid bogus "definitions" such as

which lead to a contradiction. The restriction that all free variables of the definiens must occur in the definiendum is to avoid "definitions" asp(x) : <=> ~p(x)

wherep(x) : <=>x<=y.

A predicate definition in natural language is usually expressed as

introducing the unary predicatexis (called) aP, if ...,

introducing the binary predicatexandyareP, if ...

which also introducesxis aPofy, if ...

The new constant being defined is often typeset in *italics* or
__underlined__.

- The statement
`p`is*prime*, if its only divisors are 1 and`p`.`p`__is prime__: <=> (**forall**`p`:`p`is a divisor of`x`=> (`p`= 1 \/`p`=`x`)). - The statement
`x`is a*divisor*of`y`, if`x`*`z`=`y`, for some`z`.`x`__is a divisor of__`y`: <=>**exists**`z`:`x`*`z`=`y`. - The statement
`x`is a*divisor*of`a`*`y`, if`x`*`z`=`a`*`y`, for some`z`.*not*a definition, because on the left hand side of the formula`x`is a divisor of`a`*`y`<=>**exists**`z`:`x`*`z`=`a`*`y`.`a`*`y`appears where only a variable is allowed.

**Logic Evaluator** A predicate is explicitly defined by a
statement

which is to be read aspredp(x_0, ...,x_n-1) <=>F;

**Constrained Predicate Definitions**
Sometimes a predicate definition conjoins some "side-conditions"
by saying

Letor, shorter,xbe such thatP. Thenxis aQifF.

AThis is to be interpreted as the definition of a predicate by a conjunction:Pis aQifF.

which we usually express in the form defined below (provided that we operate in the domain of sets).Q(x) : <=>P(x) /\F

is a

psubsetSp(x_{0}, ...,x_{n-1}) : <=>F

forallx_{0}, ...,x_{n-1}:p(x_{0}, ...,x_{n-1}) <=> (<x_{0}, ...,x_{n-1}> inS/\F).

Since a constraint just adds a condition, the corresponding predicate is still uniquely defined.

- The definition

is to be understood as`|`subset**N**x**N**`x`|`y`: <=>**exists**`p`in**N**:`x`*`p`=`y``x`|`y`: <=>`x`in**N**/\`y`in**N**/\**exists**`p`in**N**:`x`*`p`. - The definition
Let

as well as the definition`f`be a binary relation.`f`is a*partial function*if every element of its domain is in relation to at most one element of its range.A

are to be read as the definition of a unary predicate*partial function*is a binary relation where every element of the domain is in relation to at most one element of the range.`f`is a partial function : <=>

`f`is a binary relation /\

**forall**`x`,`y`_0,`y`_1: (<`x`,`y`_0> in`f`/\ <`x`,`y`_1> in`f`) =>`y`_0 =`y`_1.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999