axiom

The axiom command is used to assert the truth of a sentence and store the sentence in a sentence variable as a verified sentence value.

Syntax

axiom [axiom identifier]: [sentence];

The axiom command begins with the keyword axiom, followed by a variable identifier. A : character denotes the beginning of a ; terminated sentence.

Axiom Schema

axiom [axiom identifier][[predicate0]([num args]), [predicate1]([num args]), ...]: [sentence];

Optionally, after the axiom identifier a list of unbound predicates may follow. The list of unbound predicates begins with a [ character. This is followed by a comma-separated list of predicates. Each entry in the list begins with a predicate identifier. After the predicate identifier, the number of arguments of the predicate depends on is denoted with parentheses and

Behavior

The sentence specified in the axiom command, which may depend on the optional list of unbound predicates, is stored as a verified sentence value into the variable with the identifier [axiom identifier].

For each axiom, an axiom dependency is created in the current scope. Since the axiom command creates a dependency, the command can only be used in a global scope or a dependent scope.

Axioms with unbound predicates act as axiom schema through the use of expression brackets.

Examples

Suppose < is a relation. Then the following commands:

object ZERO;
axiom zero_minimal: *X(~X < ZERO);

Create an object named ZERO and an axiom which asserts that no object X is related to ZERO by <, or with the usual interpretation of <, no object is less than ZERO.

The following command:

axiom strong_induction[P(1)]: *N(*M(M < N -> P(M)) -> P(N)) -> *N(P(N));

Encodes second-order strong induction as an axiom schema. The axiom can be applied to any predicate depending on one argument.