Quantifiers

Quantifiers bind new objects in sentences. CORE has two quantifiers: universal and existential. Objects bound by a quantifier mask existing objects with the same identifier in the following sentence term.

Syntax

*[object identifier] [sentence term]
^[object identifier] [sentence term]

The universal and existential quantifiers are denoted by * and ^ respectively. After a quantifier follows a sentence term which may refer to the variable bound by the quantifier.

Universal Quantifiers

Universal quantifiers are denoted by *. If P is a sentence with an unbound object, then the sentence *X(P(X)) is interpreted to mean that for all objects X, the sentence P(X) is true.

A sentence of the form *X(P(X)) can be proven using the given command. A proven sentence of the form *X(P(X)) can be used to deduce P(Y) for any object with identifier Y using object substitution.

Existential Quantifiers

Existential quantifiers are denoted by ^. If P is a sentence with an unbound object, then the sentence ^X(P(X)) is interpreted to mean that there exists an object Y such that the sentence P(Y) is true.

A sentence of the form ^X(P(X)) can be proven using the choose command. A proven sentence of the form ^X(P(X)) can be used to construct an object Y in the current scope such that P(Y) is true. See Pipe Operator for more information.

Examples

If = is a relation and subset is a predicate depending on two objects, then one can form the following sentence:

*X*Y subset(X, Y) & subset(Y, X) -> X = Y

If the objects X and Y do not exist in the current scope or any parent scope, then this sentence is semantically invalid. The reason is that subset(X, Y) is a sentence term, so the sentence is parsed as:

((*X*Y(subset(X, Y))) & subset(Y, X)) -> (X = Y)

In this example, the objects X and Y which are quantified are only accessible within the sentence term subset(X, Y). If X and Y are objects accessible in the current scope, however, then this is a valid sentence. To avoid ambiguity, it is best practice to add parentheses after a sequence of quantifiers, as in the following example:

*X*Y(subset(X, Y) & subset(Y, X) -> X = Y)