Indeed.  There is no need to distinguish axioms and axiom schemata (as Thomas 
said, oracles are not the latter). This is because of the INST and INST_TYPE 
rules of inference.  In a system with schemata, instantiation (or matching) is 
the way you check whether or not you have an oracle, and you have a special 
category of schema variable. The variables in HOL’s axioms are normal 
variables, and can be instantiated both in axioms and derived theorems.


From: Thomas Tuerk <>
Date: Tuesday, 13 March 2018 at 08:51
To: "" <>
Subject: Re: [Hol-info] HOL Help for Axiom.


just too clarify. Axioms and oracles are different things in HOL 4. In the 
context of HOL 4, an "oracle" usually refers to external proof tool which is 
trusted by HOL. Its results are "imported" using HOL's "oracle mechanism" 
(mk_oracle_thm and related). Oracles are __not__ axiom schemata. Axioms are 
only used to make your logic stronger, i.e. (2). Of course, in a theorem prover 
you can abuse axioms to do (1). However, even if you do it, you would not call 
it introducing new axioms. However, usually theorem provers provide a different 
mechanism for (1). In HOL 4 the oracle mechanism is used for (1). Things like 
"boosLib.cheat" are implemented with it.


On 12.03.2018 18:41, Mario Xerxes Castelán Castro wrote:

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.


Check out the vibrant tech community on one of the world's most

engaging tech sites,!


hol-info mailing list<>

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

Reply via email to