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* (coinciding with the notion of [[nLab:context]] familiar to type theorists) and that of *environment* (which has been presented by [Peer Martin-Löf 1991a](#MartinLoefContextsAndEnvironments) who attributes this notion to Peter Landin) which is the logical translation of the notion of computer memory. +-- {: .un_defn} ###### Terminological remark (predication) 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*. =-- +-- {: .un_defn} ###### Terminological remark (analyticity) In philosophical logic a typing judgement $a:\alpha$ is called *analytic with respect to some inference* if it occurs more than one times in the inference. =-- # Contents * Automatic table of contents {: toc} ## 3.1 CTT as the general framework: informal description ### 3.1.1 Formalization of knowledge and information +-- {: .un_defn} ###### Types are general concepts 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*. =-- +-- {: .un_defn} ###### Proofs are justifications for judgements Here the notion of *information* enters implicitly: Specific elements of proofs are regarded as *carriers of information*. =-- +-- {: .un_defn} ###### Contexts contain collections of assumptions for judgements Assumptions are assertion condition conditions for judgements. The notion of information is related to the operations performed on the content of contexts. =-- ### 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 The rule $$(\;) : context$$ is saying that contexts can be used as types and that we write contexts in brackets. $$\frac{\array{\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 The rule $$(\;):(\;): context$$ in the first bracket expects environments and in 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 The notions of *information* and *knowledge* will be defined by the following structural aspects of CTT: 1. *Presuppositions*, in the basic form these are type declarations. 1. *Assumptions*, these are contained in contexts for dependent types and objects. 1. *Context extension* 1. *Categorical judgements* It is important to notice that *Presuppositions* and *Assumptions* are thought of as different notions. ### 3.2.1 Presuppositions +-- {: .un_defn} ###### Presupposition 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$*. =-- ### 3.2.2 Assumptions +-- {: .un_defn} ###### Assumption 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*. =-- ### 3.2.3 Types and meaning declarations +-- {: .un_defn} ###### Meaning 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$. =-- ### 3.2.4 Truths and the role of assumptions +-- {: .un_defn} ###### Truth 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. =-- ### 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}