Predicate Definitions
Predicate definitions can be used to obtain verified sentences. If a predicate or relation has a sentence definition, then by definition the predicate or relation applied to objects makes a true sentence when the corresponding sentence definition with those objects substituted is true.
Syntax
#[identifier]
A predicate definition expression term begins with a #
character followed by an identifier. The identifier may be either a predicate identifier or a relation identifier.
Behavior
There must be a predicate or relation which is accessible from the current scope and shares the same identifier, otherwise an error is raised. If the predicate or relation does not have a sentence definition, then an error is raised.
If a predicate P
depending on n objects shares the same identifier, denote the sentence definition as A(X1, X2, ..., Xn)
for unbound objects X1
, X2
,…, Xn
. The output of the expression is a verified sentence of the following form:
*X1*X2*[...]*Xn(A(X1, X2,..., Xn) <-> P(X1, X2,..., Xn))
If a relation R
shares the same identifier, denote the sentence definition as A(X1, X2)
for unbound objects X1
and X2
. The output of the expression is a verified sentence of the following form:
*X1*X2(A(X1, X2) <-> X1 R X2)
Examples
Suppose in
is a relation and =
is a relation such that for unbound objects A
and B
, A = B
if and only if:
*X(X in A <-> X in B)
In other words, the above sentence is the sentence definition for =
where A
and B
are the first and second unbound objects.
Suppose now that X
, A
, and B
are objects, eq
is a variable storing the following verified sentence:
A = B
And member
is a variable storing the following verified sentence:
X in A
Then the following expression:
#=(A, B)(eq)(X)(member)
Evaluates to the verified sentence:
X in B
If successor
is a predicate depending on two objects such that for unbound objects C
and D
, successor(C, D)
if and only if:
*Y(Y in C <-> Y in D | Y = D)
Then the following expression:
#successor
Evaluates to the following verified sentence:
*C*D(*Y(Y in C <-> Y in D | Y = D) <-> successor(C, D))