Spahn Primiero, information and knowledge, chapter 3, formal representation of the notion of information (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

category: reference

This entry is about a section of the text

Contents

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:typecontext : type
environment:typeenvironment : type

subject to the following rules:

Context formation rules
():context(\;) : context
Γ:context,αγ:type(Γ)(Γ,x:α):context\frac{\Gamma : context, \alpha\gamma : type (\Gamma)}{(\Gamma,x:\alpha) : context}

saying that contexts can be used as types and that we write contexts in brackets.

Γ:context,αγ:type(Γ)(Γ,x:α):context\frac{\Gamma : context, \alpha\gamma : type (\Gamma)}{(\Gamma,x:\alpha) : context}

where γ:environment\gamma:environment, γ:Γ\gamma:\Gamma, andα:type\alpha: type. This rule declares the formation of a type α\alpha under a environment γ\gamma.

Environment formation rules
():():context(\;):(\;): context
γ:Γa:αγ(γ,x=a):(Γ,x:α)\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

Revision on August 4, 2012 at 19:16:15 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.