While history of these matters is topical, I thought I might describe
the origin of this facility and the practical rationale for
conservativity at that time.
My memory is not completely reliable, so there might be something here
which I have misremembered but I think the main features will be good.
All of the definitional facilities had their origin prior to Andy Pitts
being asked to provide proofs of consistency, and the original
definitional facilities were found not to be conservative.
I started to work with HOL in 1986 and in the course of my work (not too
sure of the timing but definitely before HOL88) realised that the then
definitional facilities could be manipulated to derive a contradiction.
This I did, using a simple constant definition, and Rob Arthan then
observed that type definition could also achieve the same effect.
The remedy was straightforward so I think these holes were quickly fixed,
Mike Gordon, at that time, did not regard the definitional facilities as
part of the "The Logic" and did not consider that we had shown his
formulation of higher order logic to be inconsistent, but he was
nevertheless keen to avoid any more problems of this kind and doubtless
this figured in the rationale for getting some theoretical underpinning.
Not long thereafter we (at ICL) took a contract for the design, formal
verification, and manufacture of a secure hardware device, and the
origins of "new_specification" flowed from the approach we took to this
work.
This was 1988 I believe, but before HOL88 was available.
The specifications to be verified were to be available both in Z and in
HOL with the HOL versions being definitive.
In order to be able to say that HOL was a sound prover and that to the
best of our knowledge it was not possible to prove a falsehood in HOL,
we produced a minor variant of the HOL ITP, in which "new_axiom" and
"mk_thm" were disabled (once essential uses were in place) and a new
"delete_definition" was included.
"delete_definition" was our precursor to "new_specification" and
provided a first informal argument for the conservativity of
"new_specification".
The reason we wanted it was because Z allows constants to be "defined"
by "axiomatic specifications", which look awfully like arbitrary new
axioms, and we wanted a similar style of specification constrained to be
conservative.
The simple way to do this is using choice.
Thus a Z specification, which might be like this:
| c:T
|----------
| P c
introducing a new constant c having property P, is transcribed into
something in HOL which
looks similar but behind the scenes is translated into the definition:
c = @x:P x
This does ensure that the introduction of the new constant is
conservative, but goes a little bit too far.
The bit too far is of course, that all constants introduced in the same
way (with the same predicate P) are provably equal, which is not the
intention.
"delete_definition" allowed us to eliminate this overshoot, by
introducing a new definitional facility which was a precursor to
"new_specification" (I can't remember what we actually called it).
This allowed a new constant (or group of constants) to be introduced
using any property P of those constants.
The constant would be introduced using new_definition and choice.
We then proved the theorem:
?x:P |- P c
saved that and then deleted the definition made using choice (all behind
the scenes of course).
"delete_definition" deleted the axiom introduced by a definition, but
preserved the fact that the relevant constants had been defined, and
could not therefore be defined again.
Introducing "delete_definition" by a very elementary pragmatic argument,
clearly could not compromise the consitency of the system, since its
only effect was to remove theorems.
So we put it to Mike Gordon (who was a consultant on our project) that
this would be a good thing to add into HOL.
"delete_definition" proved controversial, but the effect it was intended
to realise was not quite so controversial, and after a bit of further
dialogue (mainly from our end with Rob) "new_specification" was born.
I think it probably first appeared in HOL88, but by then we had locked
down our little HOL fork for the hardware verification and so we
continued for that project to use a HOL which achieved the same effect
using :"delete_definition".
Presumably this added to Mike's concerns about consistency of HOL which
were addressed a few years later by Andy Pitts.
By then we were embedding Z in ProofPower-HOL.
Several decades later Rob decided on a little further liberalisation, I
can't remember why now (if I ever knew).
Whether the "it could be done with choice and delete_definition"
argument still works I don't know.
Roger Jones
------------------------------------------------------------------------------
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
