Logical Contexts - rbjones/HoLoTruth GitHub Wiki

In talking about languages the distinction between meta-language and object-language is important. A meta-language is one in which one talks about some other language, the language about which one speaks is the object language. It may vary from one conversation to the next which language is the meta-language and which the object language, I might use language A to talk about language B at first, and then use language B to talk about language A. The use of abstract HOL as a universal representation means that in any such discussion, both the meta- and the object language will be different (or the same) concrete presentation of sentences for which the underlying representation is abstract HOL, which is therefore both the object- and the meta-language at once. Because of its pluralism in concrete languages and the high levels of automation which it is intended to support, meta-language or meta-notations, and meta-theoretic reasoning will be pervasive.

In order to maximise the re-usability of knowledge, as much of the work as possible will be done in abstract HOL, confining concrete presentations to the dialogue with human beings, and permitting therefore that the same knowledge can be presented in different concrete forms for different purposes or for different people or groups of people.

These considerations lead to a restructuring of the kinds of information which has traditionally been found in the theory hierarchy of a HOL interactive theorem prover (ITP). The most fundamental core of the architecture here proposed is therefore the notion of a logical context, the effect of which is to determine a signature or vocabulary and a collection of constraints on the values which may be taken by the names in the signature.

Each signature has associated with it two sets of names. The first set of names is the names of type constructors. The second set is that of term constants. The signature contains, for each type constructor name a set of non-negative whole number arities at which the constructor has been constrained, and for each term constant, a disjoint set of "types" at which the constant has been constrained.

A context consists of a signature and a sequence of constraints. Each constraint consists of a set of type constructor/arity pairs and a set of term constant/(polymorphic)type pairs and a sentence (boolean term of abstract HOL) which mentions those type constructors with the given arities, and those constants at the given types.