Theory structure

So far we have introduced a typed mathematical language and a few examples of specific types and then rules--for ${{\mathbb{N} }}$, lists, Cartesian products, functions, subsets, and quotients. The possibilities for new types are endless, and we shall see more of them in sections 3 and . For example, we could introduce the type Set and explore classical and computational set theories. We can introduce partial objects via the bar types that [35] developed. As we have seen, we can use the Magic rule or not or various weaker forms of it.

Some choices of rules are inconsistent, e.g. bar types and Magic or the impredicative $\mathbf{\triangle}$ type of [86] and dependent products on the fixed point rule with all types. How are we to keep track of the consistent possibilities?

One method is to postulate fixed theories in the typed logic such as Heyting Arithmeticarithmetic!Heyting's (HA, HA^*) (HA) (c.f. [113]) or Peano ArithmeticPeano arithmetic (HA + Magic) or IZF (c.f. [9,46,67,87]) or Intuitionistic Type Theory (ITT) or Higher Order Logic (HOL). We rely on a community of scholars to establish the consistency of various collections of axioms. Books like [113] study relationships between dozens of these theories. The space of them is very large.

Another possibility is to explore the ``tree of knowledge'' formed by doing mathematics in various contexts determined by the definitions and axioms used for any result. We can think of definitions and axioms as establishing contexts. N.G. de Bruijn [40] has proposed a way to organize this knowledge, including derivation of inconsistency on certain paths.

Essentially de Bruijn defined typed mathematical languages, PAL, Aut-68, Aut-QE, Aut-$\Pi$, which were used for writing definitions and axioms.²⁰ He proposed a logical framework for organizing definitions, axioms and theorems into books. We will explore these typed languages in the next section. They are more primitive than our typed logic.

The apparatus of AutomathAutomath is completely formal; it is a mechanism whose meaning is to be found completely in its ability to organize information and classify it without regard for content. Extending this attitude to the mathematics being expressed leads to the formalist philosophy of mathematics espoused by [63]. This is de Bruijn's view in fact, and it surely contrasts with Principia which found its meaning in the logical truths written into a fixed foundational theory. It will contrast as well to the Martin-Löf view, Girard's [48] view, the views of Coquand and Huet in Coq and my own view (as expressed to a large extent in Nuprl) in which the logical framework is organized to express computational meaning. It is noteworthy that the three influential philosophical schools--Formalism, Logicism, and Intuitionism, can be characterized rather sharply in this setting (and coexist!).

 

Table: Sequence of lines

indicator	identifier	definition	category
0	nat	PN	type
0	n	--	nat
0	real	PN	type
n	x	--	real

 

An Automath bookAutomath book is a sequence of linesline. A line has four parts as indicated in Table 2. Each line introduces a unique identifier which is either a primitive notionprimitive notion, PN, PN, or a block openerblock opener or is defined. The category part provides the grammatical category; type is a built-in category, defined types like nat are another.

The lines form two structures, one the linear order and the other a rooted tree. The nodes of the tree are identifiers, x, and the edges are from x to the indicator of the line having x as its identifier part. The complete contextcomplete context of x is the list of indicators from x back to the root. So each line uses as its indicator the last block opener in its context. When the definition and category components are included with x, the result is what de Bruijn calls the tree of knowledgetree of knowledge.

NuprlNuprl has a similar structure to its knowledge base, called a library. A library consists of lines. Each one is uniquely named by an identifier. These can include the equivalent of block openers, called theory delimiterstheory delimiters (begin_thyname, end_thyname). The library is organized by a dependency graphdependency graph which indicates the logical order among theories (the lines between delimiters). Unlike in Automath, the theory structure is a directed acyclic graph (dag). Theories can also be linked to a file system or a database which provides additional ``nonlogical'' structuring.

The NuprlNuprl 5 system also provides a structured library with mechanisms to control access to theories. There are two modes of accessing information. One is by collecting axioms, definitions, and theorems into controlled access theoriescontrolled access theories. These theories can only use the specific rules and axioms assembled at its root. Each type such as N or $S \times T$ is organized into a small theory consisting of its rules.²¹ More complex theories are built by collecting axioms.²² We will be specifying certain important theories later. One of them is Nuprl 4, the fixed logic in the Nuprl 4.2 release. Another theory could be Nuprl 4_bar, the theory with partial objects ([35]) or NuIZF, the formulation of IZF in type theory.

Another way to use the library we might call free accessfree access. A user can prove theorems using any rules whatsoever, even inconsistent collections. Once a theorem is proved, the system can define its root_system, the collection of all rules and definitions used to state and prove it. The root_system determines the class of theories into which the result can be ``planted.''