Go backward to A.1 Preliminaries
Go up to A Defining New Notions
Go forward to A.3 Explicit Function Definitions
p(x0, ..., xn-1) : <=> Fis 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.
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)).
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.
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
which is to be read as p(x0, ..., xn-1) : <=> F.pred p(x_0, ..., x_n-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) /\ Fwhich we usually express in the form defined below (provided that we operate in the domain of sets).
is a constrained predicate definition which introduces an n-ary predicate p such that
p subset S p(x0, ..., xn-1) : <=> F
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.
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.
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.