category: reference This entry is about a section of the text * [[Giuseppe Primiero]], [[information and knowledge - a constructive type-theoretical approach]], Springer, 2008{#Primiero} This chapter 3 is the technical heart of the book. It gives an epistemic interpretation of CTT ([[nLab: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](#UpdatingBelief). Basic notions in this [[nLab:type theory|type theoretical]] framework are that of *context* (which are just the [[nLab:context|contexts]] familiar to type theorists) and that of *environment* (which has been presented by [Martin-Löf 1991a](#MartinLoefContextsAndEnvironments) who attributes this notion to Peter Landin) which is the logical translation of the notion of computer memory. # Contents * Automatic table of contents {: toc} ## 3.1 CTT as the general framework: informal description ### 3.1.1 Formalization of knowledge and information ### 3.1.2 Contexts: formal explanation #### The calculus of contexts and environments There are two specific types $$context : type$$ $$environment : type$$ subject to the following rules: +-- {: .un_defn} ###### Context formation rules $$(\;) : context$$ saying that contexts can be used as types and that we write contexts in brackets. $$\frac{\Gamma : context, \alpha\gamma : type (\Gamma)}{(\Gamma,x:\alpha) : context}$$ 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. =-- +-- {: .un_defn} ###### Environment formation rules $$(\;):(\;): context$$ where the first bracket expects environments and the second- expects contexts. $$\frac{\gamma:\Gamma\;a:\alpha\gamma}{(\gamma,x=a):(\Gamma,x:\alpha)}$$ This rule can be derived from two *rules of computation of environments* whose genesis is conceptually crucial to this chapter: =-- +-- {: .un_defn} ###### Environment computation rule 1 =-- +-- {: .un_defn} ###### Environment computation rule 2 =-- 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: +-- {: .un_defn} ###### Updating of contexts =-- +-- {: .un_defn} ###### Calculus of contexts =-- +-- {: .un_defn} ###### Updating of environments =-- ## 3.2 Representation of knowledge and information ### 3.2.1 Presuppositions ### 3.2.2 Assumptions ### 3.2.3 Types and meaning declarations ### 3.2.4 Truths and the role of assumptions ### 3.2.5 Defining information ## 3.3 Contexts as constructive possible worlds ### 3.3.1 introducing orderings: Kripke models ## 3.4 The knowledge framework ### 3.4.1 Updating information, extending knowledge ### 3.4.2 The structure of knowledge ## References * Borghuis, Kammarredine, Nederpelt, Formalizing Belief Revision in Type Theory, [[Formalizing Belief Revision in Type Theory|BibTex]] {#UpdatingBelief} * 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 {#MartinLoefContextsAndEnvironments}