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.