previous up next
Go backward to A.1 Preliminaries
Go up to A Defining New Notions
Go forward to A.3 Explicit Function Definitions
RISC-Linz logo

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 

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 

Author: Wolfgang Schreiner
Last Modification: October 4, 1999

previous up next