category: reference This entry is about a section of the text * [[Giuseppe Primiero]], [[information and knowledge - a constructive type-theoretical approach]], Springer, 2008{#Primiero} # 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$. =-- +-- {: .un_defn} ###### Environment formation rules $$(\;):(\;): context$$ $$\frac{\gamma:\Gamma\;a:\alpha\gamma}{(\gamma,x=a):(\Gamma,x:\alpha)}$$ =-- ## 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