Once the theoretical tasks have been accomplished for translating knowledge between different formalisms, a general system for sharing mathematics requires a repository where mathematics can be archived in a common language. For this purpose, we intend to develop what might be called a ``Common Logical Library,'' by which we mean a library of objects with logically significant relations maintained between them. For example, a theorem about the natural numbers may depend on basic lemmas (possibly from different systems), and the logical library is required to maintain those inter-theory dependencies.
One might invent a lot of different notions of dependency of one object on another, but the design of a logical library aims at facilitating the use of such notions to support ``logical'' claims about collections of objects. For example, we might claim that a certain proof in the library is valid if the set of rules it depends on are valid. The logical library architecture must facilitate such arguments. This paradigm must be elaborated since there may be many ways in which a proof depends on rules and other kinds of objects.
Another aim of the logical library is that it should be able to effectively maintain and relate rule sets that may not even be compatible.
In a foundational system, the basic guarantee one needs to be able to make of a specific proof is that it can be made by composing a known, limited set of rules. A flexible accounting method is required since the rules in the library are not static--they may grow as more knowledge is introduced. Although one may well ask what rules are actually used to carry out a given proof, one often cares not exactly which rules were used, but whether all those rules fall within some familiar or distinguished set like ZF set theory, or one of the known heories. Also, when one calls upon a prover to prove some goal, it's not to attractive to see after the fact whether it restricted itself to the desired set of rules, it is better to restrict it when the proof is being made.
We use what we call ``Proof Sentinels'' to express the stipulations
limiting proofs to a given set of rules, axioms, and perhaps
other objects on which these may depend.
We shall embody these proof sentinels in expressions with these key features:=0in=0in
Carrying out a given proof may require many resources from the library, such as definitions, tactics, and lemmas, but the sentinel is supposed to indicate a reduction of validity to those things, such as rules, whose criteria of correctness lie outside the formal system. For example, one should be assured the proof is correct so long as the rules in the sentinel are.
The sentinal also provides the basis for accountability. One should normally be able to scrutinize the system's justifications for various semantic or logical claims. For example, it should be possible to replay proofs, and get hold of the primitive proofs whose existence is promised by refiners. Even if not every system ``claim'' can be accounted for, it is key that there be a distinction made between those that are accountable and those that aren't - one wants to know if no accountability may be expected in individual cases. For claims that are indicated as accountable, trust but verify. Independent checkers running in the background would be a paradigm of verifying accountability.