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

## A.2 Explicit Predicate Definitions

Definition 137 (Explicit Predicate Definition) Let p be a predicate constant of arity n that is not yet in use, x0, ..., xn-1 be n distinct variables, and F be a formula in which p does not occur and with no other free variables than x0, ..., xn-1. Then the phrase
p(x0, ..., xn-1) : <=> F
is an  explicit predicate definition (explizite Prädikatsdefinition) which introduces an n-ary predicate constant p together with an axiom
forall x0, ..., xn-1: p(x0, ..., xn-1) <=> F.
We call p(x0, ..., xn-1) the  definiendum ("the one to be defined") and F the  definiens ("the defining one").

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 x0, ..., xn-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

p(x) : <=> ~p(x)
which lead to a contradiction. The restriction that all free variables of the definiens must occur in the definiendum is to avoid "definitions" as
p(x) : <=> x <= y.
where p(1) may hold or not, depending on the current assignment of y.

A predicate definition in natural language is usually expressed as

x is (called) a P, if ...,
introducing the unary predicate P(x), or
x and y are P, if ...
introducing the binary predicate P(x, y), or
x is a P of y, if ...
which also introduces P(x, y).

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

Example
• The statement
p is prime, if its only divisors are 1 and p.
introduces the unary predicate
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.
introduces the binary predicate
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.
is 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 general term a*y appears where only a variable is allowed.

Logic Evaluator  A predicate is explicitly defined by a statement

```pred p(x_0, ..., x_n-1) <=> F;
```
which is to be read as p(x0, ..., xn-1) : <=> F.

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

Let x be such that P. Then x is a Q if F.
or, shorter,
A P is a Q if F.
This is to be interpreted as the definition of a predicate by a conjunction:
Q(x) : <=> P(x) /\  F
which we usually express in the form defined below (provided that we operate in the domain of sets).

Definition 138 (Constrained Predicate Definition) Let p be a predicate constant of arity n that is not yet in use and S be a term in which p does not occur, x0, ..., xn-1 be n distinct variables, and F be a formula in which p does not occur and with no other free variables than x0, ..., xn-1. Then
 p subset S p(x0, ..., xn-1) : <=> F
is a  constrained predicate definition which introduces an n-ary predicate p such that
forall x0, ..., xn-1: p(x0, ..., xn-1) <=> (<x0, ..., xn-1> in S /\  F).

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

Example
• The definition
 | subset N x N x | y : <=> exists p in N: x*p = y
is to be understood as
x | y : <=> x in N /\  y in N /\  exists p in N: x*p.
• The definition
Let 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.
as well as the definition
A partial function is a binary relation where every element of the domain is in relation to at most one element of the range.
are to be read as the definition of a unary predicate
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