Predicates

A predicate is a symbol which may reference objects in a sentence. A predicate may depend on zero or more arguments (objects), and may or may not have a sentence definition. Predicates are a convenient tool for formally defining a concept and for hiding complicated sentences under a label.

A sentence definition is a sentence used to define a predicate. If a predicate depends on n arguments, the sentence definition has n unbound variables. A predicate applied to n objects is a sentence logically equivalent to substituting in order those n objects for the unbound variables in the sentence definition.

A predicate identifier must begin with either a letter or an underscore, and may subsequently contain letters, digits, and underscores.

Predicates are quantified only by axiom schema and proof schema.

Creation

Bound predicates are created in the scope of a proof schema. Bound predicates have no sentence definition.

Predicates can also be created in any scope using the define command.

Examples

Suppose in is a relation representing set membership and subset is a predicate defined by the following sentence:

\[\forall X \forall Y (\text{subset}(X, Y) \leftrightarrow \forall Z (Z \in X \rightarrow Z \in Y)))\]

In CORE’s syntax, this sentence would be written as:

*X*Y(subset(X, Y) <-> *Z(Z in X -> Z in Y))

Then the sentence

*X(subset(X, X))

would mean:

*X*Z(Z in X -> Z in X)