We shall temporarily make one oversimplifying assumption while we discuss the content and use of sentinels, namely, that all the inference steps in a proof dag must have certificates containing the same sentinel. Thus, a sentinel is used as the a standard of coherency between different inferences.
A sentinel is an expression, and we sometimes emphasize this by calling it a sentinel expression. The sentinel is intended to represent a class of basic logical resources and methods as opposed to derived ones. For example, one might build an inference engine which takes as a parameter a primitive rule set; then a sentinel expression appropriate to inference certificates invoking this engine would indicate the kind of inference engine invoked along with the primitive rule set. The presumed external meaning of these inference certificates is that the engine restricts its dependency upon primitive rules to those mentioned in the sentinel (plus, perhaps, some "built-in" rules that need not be mentioned explicitly in the sentinel expression).
The sentinel is not a general indication of resource restriction. Inferences citing lemmas, or definitions, or derived rules or, in the case of tactic provers, sources for tactic code, do not require extension of the sentinel. Resources can be developed and employed based upon a sentinel without altering the sentinel. Thus, while one may wish for some reason to restrict the resources actually used by a particular inference certification, and while one may want to make a record of resources actually used in a particular inference certification, neither of these should be effected by choice of sentinel. The purpose of the sentinel is to express a common basis for acceptable inference (which may differ on different occasions).
Another part of the sentinel expression is an indication of when an inference engine itself is acceptable. While one could build a sentinel that depends upon a particular running inference engine process, this would not normally be practical since one normally builds many inference engine processes, over the course of time according to each method for doing so. Therefore, it is more practical to build into the sentinel the method for building (or finding) individual inference engines of the appropriate kind. Indeed, the reason that an individual inference engine process is trusted in the first place is really that it was built according to certain methods, so there would be little point in stipulating a specific running process (rather than the method for creating one) as the engine for a proof sentinel.
The sentinel expression becomes the basic epistemic focus for users. The hard work on the part of a person or community of persons is coming to trust the basic inferences endorsed by a sentinel expression, and the FDL process should support this connection by retaining the user recognizable sentinel expressions in certificates for inferences. The intention is that persons become familiar with particular sentinels which they come to trust. Thus, it must be possible for a sentinel expression to be expressed briefly and be recognizable; and yet since in fact there will often be some complex structure to the meaning of the sentinel expression, this means that abbreviation of expressions is key.
Continued at