trivial
The built-in function trivial
accepts one sentence expression value, and if the sentence is trivially true, returns the same sentence value except verified.
Syntax
trivial([sentence argument expression])
Behavior
The argument must be an expression evaluating to a sentence expression value with no unbound objects or predicates. If the argument sentence is not trivially true, then an error is raised. Otherwise, the output is a verified sentence value storing the same sentence as the argument.
Note
Anything that can be proven using the trivial
built-in command can be proven without it. trivial
is usually used to save the programmer the time of having to prove simple statements that are obviously true. Due to the limited scope of what is defined as trivially true, there are other sentences that are just as obvious but must be proven manually.
Examples
If in
is a relation, the following expression:
trivial(<: *X*Y(X in Y -> ~~X in Y)>)
Returns the following verified sentence value:
*X*Y(X in Y -> ~~X in Y)