The only general policy for changing certificate content that we currently expect to adopt was alluded to in
A simple content alteration policy, one might deem it the default, is extreme sensitivity to the content and number of objects referred to by the certificate. It is this: if the content of any object the certificate refers to is changed, then the certificate must be deleted (or its content must be altered to mark it vestigial); its fate will be the same should multiple references within the certificate get "identified", by
For example, if a proof "goes bad" because of some alterations to underlying content, say a change of definition or deletion of an inference rule upon which it depended, or through forced identification of two "primitive" notions, then the objects certifying it as a well-formed proof (according to whatever standards) will be deleted or marked as stale. If they are altered to these vestigial forms rather than deleted, they may be useful in further attempts to attach new certificates to the proof.
A more permanently useful vestigial certification would be a certificate of object creation. An object creation certificate might be implemented to indicate that an object it refers to was created at a certain time in a certain
One might also implement kinds of certificates that are insensitive to some alteration of content in referenced objects. For example, one might adopt a criterion for mere annotation of programs or formal data that does not affect correctness, and leave "annotation insensitive" certificates intact if objects they refer to are altered merely in their annotations.
Returning to external significance of certificates, it is also possible for us to be mistaken or in disagreement about the external significance we have attributed to a kind of certificate. This lies beyond the responsibility of the closed map management system. For a scenario exploring this situation see
The most important promise implementors can make with regard to certification is that the policy for creation and update of each kind of certificate is permanent, once implemented. If a new policy is needed or desired, a new kind of certificate must be implemented.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html