Pipe Operator

New objects can be constructed from a verified sentence value beginning with a top-level existential quantifier using the pipe operator.

Syntax

[sentence expression]|[object identifier], [object identifier], ...|

A pipe operator sentence term begins with a parent expression evaluating to a verified sentence value. The sentence referenced by the sentence value must begin with a top level existential quantifier. In other words, the sentence must be of the form ^X(P(X)) for some sentence P with one unbound object. Following the parent expression is the character |, one or more object identifiers, and a final | character.

For each object identifier, a top level existential quantifier is peeled from the parent expression sentence. A new object in the current scope is created with the object identifier, overwriting any variables or objects sharing the same identifier (This raises an error if the object or variable cannot be overwritten). Then, this new object is substituted for the unbound variable in the sentence. After doing this for each object identifier, the pipe operator sentence term evaluates to the remaining sentence.

The pipe operator can only be applied to a parent expression evaluating to a verified sentence value with no unbound predicates. Consequently, a pipe operator sentence term always evaluates to a verified sentence value with no unbound predicates.

Examples

If in is a relation, S and T are objects, and axiom_pairing is a sentence variable storing the following verified sentence:

*X*Y^Z(X in Z & Y in Z)

Then the expression axiom_pairing(S, T)|P| creates an object P and evaluates to the following verified sentence:

S in P & T in P

Working in set theory where in means set membership, P is now a set which contains both S and T. This new sentence value can act as a definition for P.