This entry is about a section of the text
This chapter 3 is the technical heart of the book. It gives an epistemic interpretation of CTT (constructive type theory) in terms of knowledge and information. This interpretation is explicated by considering CTT as a framework for the representation of knowledge processes with the operation of retrieving and extending knowledge. This formalization abstracts common processes in computer science. The interpretation given here is due to Giuseppe Primiero and is partially based on ideas of Borghuis, Kamarredine and Nederpelt.
Basic notions in this type theoretical framework are that of context (coinciding with the notion of context familiar to type theorists) and that of environment (which has been presented by Peer Martin-Löf 1991a who attributes this notion to Peter Landin) which is the logical translation of the notion of computer memory.
In philosophical logic a typing judgement $a:\alpha$ is called predication of $a$ in $\alpha$.
In this case $(-):\alpha$ is called the category of objects predicated in $\alpha$.
We say the object $\alpha$ on the right of the colon is meaning referring.
In philosophical logic a typing judgement $a:\alpha$ is called analytic with respect to some specific inference $I$ if it occurs more than one times in $I$.
The equivalence of types and concepts means that every judgement establishes the predication of a concept. A type is an element in the category of predication $(-) : type$. A context in this theory is regarded as a carrier of meaning.
Here the notion of information enters implicitly: Specific elements of proofs are regarded as carriers of information.
Assumptions are assertion conditions for judgements. The notion of information is related to the operations performed on the content of contexts.
calculus of contexts and environments?
There are two specific types
subject to the following rules:
The rule
is saying that contexts can be used as types and that we write contexts in brackets.
where $\gamma:environment$, $\gamma:\Gamma$, and $\alpha: type$. This rule declares the formation of a type $\alpha$ under a environment $\gamma$. It is an extension of a context in some environment.
The rule
in the first bracket expects environments and in the second- expects contexts.
This rule can be derived from two rules of computation of environments whose genesis is conceptually crucial to this chapter:
To avoid the circularity arising in the formalization of contexts we need some inductive construction called updating. Contexts are hence built by successive updating of the elements in it:
The notions of information and knowledge will be defined by the following structural aspects of CTT:
Presuppositions, in the basic form these are type declarations.
Assumptions, these are contained in contexts for dependent types and objects.
Context extension
Categorical judgements
It is important to notice that Presuppositions and Assumptions are thought of as different notions.
A presupposition for a judgement $a:\alpha$ is a judgment which is needed for the judgement $a:\alpha$ to make sense.
For example $a:\alpha$ has as $\alpha:type$ as a presupposition. We write in this case $\lt\alpha:\type\gt$ to indicate that $\alpha:type$ is a presupposition (for some judgement).
Notice that we could call $\alpha:type$ a type declaration of the type $\alpha$ and $a:\alpha$ an instatiation of the type $\alpha$.
The notion of assumption enters the definition of a dependent type. An assumption is the aspect on which a dependent type depends.
The aspect of a dependent type which depends (on some assumption) we could call knowable object.
We say the object $\alpha$ on the right of the colon in $a:\alpha$ is meaning referring.
Meaning is what is referred to $a$ by $\alpha$.
By definition of CTT a judgement is true if it has a proof.
We refer to this fact by saying that $(x:\alpha)$ carries the information that $[x/a]:type$ is true.
Recall that by definition types are general concepts.
Every typing judgements in a context is (by definition) informational data.
For example type declarations, assumptions and derived judgements are informational data with respect to the specific contexts they occur in.
A prefix (=initial segment) $(x_1:a_1,\dots,x_n:a_n)$ of a context $(x_1:a_1,\dots,x_n:a_n,x_{n+1}:a_{n+1},\dots,x_{n+k}:a_{n+k}):=\Gamma$ we could call an informational state in $\Gamma$.
We could call the collection of all judgements in an informational state its (underlying) knowledge state.
A context $\Delta$ is a carrier of information. We could think of the class of all extensions (see below) $\{\Gamma\leftarrow \Delta|\Gamma:context\}$ of the class of all information contained in $\Delta$.
An interpretation of (also called updating of …by or extension of…by)
in (resp. by)
is defined by giving a sequence of definitions:
see also [Ranta1994] pp.145-147
An extension $\Gamma\leftarrow \Delta$ of a context $\Gamma$ by a context $\Delta$ as defined above can be derived by the following basic cases:
(a) Addition of a type declaration (Introduction of a new context): i.e. $\Gamma=(x_1:\alpha_1,\dots,x_n:\alpha_n)$ is extended to $\Delta=x_1:\alpha_1,\dots,x_n:\alpha_n,\lt \alpha_{n+1}:type\gt)$
(b) Addition of a new assumption: i.e. $\Gamma=(x_1:\alpha_1,\dots,x_n:\alpha_n)$ is extended to $\Delta=x_1:\alpha_1,\dots,x_n:\alpha_n, x_{n+1}:\alpha_{n+1})$
(c) variable substitution (addition of a definition): i.e. $\Gamma=(x_1:\alpha_1,\dots,x_n:\alpha_n)$ is “extended” (the resulting expression may be shorter) to $\Delta=(\Gamma,x_k=a:\alpha_k)$
Borghuis, Kammarredine, Nederpelt, Formalizing Belief Revision in Type Theory, BibTex
Peer Martin-Löf, Contexts and environments, unpublished notes by P. Mäenpaä and A. Rata of a series of lectures given at Stockholm University
Aarne Ranta: type-theoretical grammar, 1994, Oxford University Press