Glossary FDLnotes
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Content vs Infrastructure.

The Cornell effort toward developing digital libraries of algorithmic mathematics is explicitly bifurcated. We aim at generation of constructive math by means we have long developed and employed. But, and this is the topic of these notes, we also aim to design a repository system, a "Formal Digital Library" (FDL) that supports content that is radically different from ours, and perhaps even incompatible. Our intention is that our contributions toward content and content creation are but some of many possibilities, and we strive to avoid bias towards our content and methods. Our established status as providers of mathematics in a minority (though widely known) genre has made us sensitive to the possibilities of exclusion. Our suspicion that our content would be excluded from libraries of mathematics designed by those whose experience and loyalties lie with more widely employed genres has caused us to appreciate the need for a more radical inclusiveness. It is not our desire to use the general system design as a means to unfairly promote our mathematical preferences. The FDL design is intended to be neutral, and our content must vie for consideration on its own merits.

This means that we are not obliged to create methods for content creation generally, but must flexibly anticipate likely methods, including extant ones, and publish adequate methods to access and contribute to FDL collections. Because of the variety of semantical intentions and epistemic assumptions, sometimes incompatible, underlying different developments, flexible and stringent accounting methods must be introduced if these mixtures of content are to coexist.

What we offer are to-some-extent common syntactic structures, storage, and accounting services, especially accounting for formal facts contributing to arguments for validity of proofs. See the glossary entries for Text, Certificate and Proof.

Further, we shall not require a particular logic (even a particular form of assertion), type theory, tactics, or the use of the ML programming language. However, it should be noted that our experience with these has led us to reject a number of presumptions about methods of proof and expression and left us with an expectation of rather liberal practices. In particular, we have become accustomed to using a language in which, as in informal mathematical practice, the sensibleness of expressions is not always obvious, and must sometimes be demonstrated, and in which some other simplifying assumptions about notational adequacy are avoided (such as assuming there is a single domain of all values). Our use of tactics to formalize the notion of effectively explaining how to make inferences, rather than restricting our expression of inference to schematic forms, has forced us to deal with issues pertaining to accounting for reliability of programs. Briefly, we have already committed ourselves to, and are experienced with, sophisticated methods of applied logic, and are therefore more likely than we would otherwise be to anticipate a great variety of formal methods.

A major purpose for development of our newest system is to analyze many concerns about how to simultaneously support independent developments. Many of these concerns were driven by centrifugal forces within our own project, whose members represent a variety of different opinions about how to formulate and develop formal mathematics, sometimes differing even as to what is legitimate. Our desire despite this to share what we can in various ways has driven us to a flexible design. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Glossary FDLnotes