There are 2 reasons for adding new axioms and axiom schemata (oracles):

(1) To save the work for proving something provable or constructible
(e.g.: one could assume the axioms for the real numbers instead of
constructing the reals; although in this case, the library includes a
construction of the reals)

(2) Because the axiom is not provable from within the logic, i.e.: you
want to make the theory stronger.

In case (1), maybe the axiom you needs are already proved or available
as a theory. You will have to search for it. Check the theory tree

In case (2), you can add a new axiom (refer to Thomas message) or state
your theorems as an implication, where the antecedent suffices to encode
your new axioms or axiom schemata.

Attachment: signature.asc
Description: OpenPGP digital signature

Check out the vibrant tech community on one of the world's most
engaging tech sites,!
hol-info mailing list

Reply via email to