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.
Michael
From: Thomas Tuerk <tho...@tuerk-brechen.de>
Date: Tuesday, 13 March 2018 at 08:51
To: "hol-info@lists.sourceforge.net" <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] HOL Help for Axiom.
Hi,
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.
Best
Thomas
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, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
