If tm is a term of type bool, a call new_axiom tm creates a
theorem
|- tm
FAILURE CONDITIONS
Fails if the given term does not have type bool.
EXAMPLE
# let ax = new_axiom `x = 1`;;
val ax : thm = |- x = 1
Note that as with all theorems, variables are implicitly universally
quantified, so this axiom asserts that all numbers are equal to 1. Of course,
we can then derive a contradiction:
CONV_RULE NUM_REDUCE_CONV (INST [`0`,`x:num`] ax);;
val it : thm = |- F
Normal use of HOL Light should avoid asserting axioms. They can lead to
inconsistency, albeit not in such an obvious way. Provided theories are
extended by definitions, consistency is preserved.
COMMENTS
For most purposes, it is unnecessary to declare new axioms: all of classical
mathematics can be derived by definitional extension alone. Proceeding by
definition is not only more elegant, but also guarantees the consistency of the
deductions made. However, there are certain entities which cannot be modelled
in simple type theory without further axioms, such as higher transfinite
ordinals.