\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{Primiero, information and knowledge, chapter 3, formal representation of the notion of information}

This entry is about a section of the text

\begin{itemize}%
\item [[Giuseppe Primiero]], [[information and knowledge - a constructive type-theoretical approach]], Springer, 2008

\end{itemize}
This chapter 3 is the technical heart of the book. It gives an epistemic interpretation of CTT ([[nLab:constructive type theory]]) in terms of \emph{knowledge} and \emph{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 \hyperlink{UpdatingBelief}{Borghuis, Kamarredine and Nederpelt}.

Basic notions in this [[nLab:type theory|type theoretical]] framework are that of \emph{context} (coinciding with the notion of [[nLab:context]] familiar to type theorists) and that of \emph{environment} (which has been presented by \hyperlink{MartinLoefContextsAndEnvironments}{Peer Martin-Löf 1991a} who attributes this notion to Peter Landin) which is the logical translation of the notion of computer memory.

\begin{udefn}
In philosophical logic a typing judgement $a:\alpha$ is called \emph{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 \emph{meaning referring}.

\end{udefn}
\begin{udefn}
In philosophical logic a typing judgement $a:\alpha$ is called \emph{analytic with respect to some specific inference $I$} if it occurs more than one times in $I$.

\end{udefn}
\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{31_ctt_as_the_general_framework_informal_description}{3.1 CTT as the general framework: informal description}\dotfill \pageref*{31_ctt_as_the_general_framework_informal_description} \linebreak
\noindent\hyperlink{311_formalization_of_knowledge_and_information}{3.1.1 Formalization of knowledge and information}\dotfill \pageref*{311_formalization_of_knowledge_and_information} \linebreak
\noindent\hyperlink{312_contexts_formal_explanation}{3.1.2 Contexts: formal explanation}\dotfill \pageref*{312_contexts_formal_explanation} \linebreak
\noindent\hyperlink{the_calculus_of_contexts_and_environments}{The calculus of contexts and environments}\dotfill \pageref*{the_calculus_of_contexts_and_environments} \linebreak
\noindent\hyperlink{32_representation_of_knowledge_and_information}{3.2 Representation of knowledge and information}\dotfill \pageref*{32_representation_of_knowledge_and_information} \linebreak
\noindent\hyperlink{321_presuppositions}{3.2.1 Presuppositions}\dotfill \pageref*{321_presuppositions} \linebreak
\noindent\hyperlink{322_assumptions}{3.2.2 Assumptions}\dotfill \pageref*{322_assumptions} \linebreak
\noindent\hyperlink{323_types_and_meaning_declarations}{3.2.3 Types and meaning declarations}\dotfill \pageref*{323_types_and_meaning_declarations} \linebreak
\noindent\hyperlink{324_truths_and_the_role_of_assumptions}{3.2.4 Truths and the role of assumptions}\dotfill \pageref*{324_truths_and_the_role_of_assumptions} \linebreak
\noindent\hyperlink{325_defining_information}{3.2.5 Defining information}\dotfill \pageref*{325_defining_information} \linebreak
\noindent\hyperlink{33_contexts_as_constructive_possible_worlds}{3.3 Contexts as constructive possible worlds}\dotfill \pageref*{33_contexts_as_constructive_possible_worlds} \linebreak
\noindent\hyperlink{331_introducing_orderings_kripke_models}{3.3.1 introducing orderings: Kripke models}\dotfill \pageref*{331_introducing_orderings_kripke_models} \linebreak
\noindent\hyperlink{34_the_knowledge_framework}{3.4 The knowledge framework}\dotfill \pageref*{34_the_knowledge_framework} \linebreak
\noindent\hyperlink{341_updating_information_extending_knowledge}{3.4.1 Updating information, extending knowledge}\dotfill \pageref*{341_updating_information_extending_knowledge} \linebreak
\noindent\hyperlink{342_the_structure_of_knowledge}{3.4.2 The structure of knowledge}\dotfill \pageref*{342_the_structure_of_knowledge} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{31_ctt_as_the_general_framework_informal_description}{}\subsection*{{3.1 CTT as the general framework: informal description}}\label{31_ctt_as_the_general_framework_informal_description}

\hypertarget{311_formalization_of_knowledge_and_information}{}\subsubsection*{{3.1.1 Formalization of knowledge and information}}\label{311_formalization_of_knowledge_and_information}

\begin{udefn}
The equivalence of types and \emph{concepts} means that every judgement establishes the predication of a concept. A type is an element in the \emph{category of predication} $(-) : type$. A context in this theory is regarded as a carrier of \emph{meaning}.

\end{udefn}
\begin{udefn}
Here the notion of \emph{information} enters implicitly: Specific elements of proofs are regarded as \emph{carriers of information}.

\end{udefn}
\begin{udefn}
Assumptions are assertion conditions for judgements. The notion of information is related to the operations performed on the content of contexts.

\end{udefn}
\hypertarget{312_contexts_formal_explanation}{}\subsubsection*{{3.1.2 Contexts: formal explanation}}\label{312_contexts_formal_explanation}

\hypertarget{the_calculus_of_contexts_and_environments}{}\paragraph*{{The calculus of contexts and environments}}\label{the_calculus_of_contexts_and_environments}

[[calculus of contexts and environments]]

There are two specific types

\begin{displaymath}
context : type
\end{displaymath}
\begin{displaymath}
environment : type
\end{displaymath}
subject to the following rules:

\begin{udefn}
The rule

\begin{displaymath}
(\;) : context
\end{displaymath}
is saying that contexts can be used as types and that we write contexts in brackets.

\begin{displaymath}
\frac{\itexarray{\Gamma : context\\ \alpha\gamma : type (\Gamma)}}{(\Gamma,x:\alpha) : context}
\end{displaymath}
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.

\end{udefn}
\begin{udefn}
The rule

\begin{displaymath}
(\;):(\;): context
\end{displaymath}
in the first bracket expects environments and in the second- expects contexts.

\begin{displaymath}
\frac{\gamma:\Gamma\;a:\alpha\gamma}{(\gamma,x=a):(\Gamma,x:\alpha)}
\end{displaymath}
This rule can be derived from two \emph{rules of computation of environments} whose genesis is conceptually crucial to this chapter:

\end{udefn}
\begin{udefn}
\end{udefn}
\begin{udefn}
\end{udefn}
To avoid the circularity arising in the formalization of contexts we need some inductive construction called \emph{updating}. Contexts are hence built by successive updating of the elements in it:

\begin{udefn}
\end{udefn}
\begin{udefn}
\end{udefn}
\begin{udefn}
\end{udefn}
\hypertarget{32_representation_of_knowledge_and_information}{}\subsection*{{3.2 Representation of knowledge and information}}\label{32_representation_of_knowledge_and_information}

The notions of \emph{information} and \emph{knowledge} will be defined by the following structural aspects of CTT:

\begin{enumerate}%
\item \emph{Presuppositions}, in the basic form these are type declarations.


\item \emph{Assumptions}, these are contained in contexts for dependent types and objects.


\item \emph{Context extension}


\item \emph{Categorical judgements}



\end{enumerate}
It is important to notice that \emph{Presuppositions} and \emph{Assumptions} are thought of as different notions.

\hypertarget{321_presuppositions}{}\subsubsection*{{3.2.1 Presuppositions}}\label{321_presuppositions}

\begin{udefn}
A \emph{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 \emph{type declaration} of the type $\alpha$ and $a:\alpha$ an \emph{instatiation of the type $\alpha$}.

\end{udefn}
\hypertarget{322_assumptions}{}\subsubsection*{{3.2.2 Assumptions}}\label{322_assumptions}

\begin{udefn}
The notion of \emph{assumption} enters the definition of a dependent type. An \emph{assumption} is the aspect on which a \emph{dependent type} depends.

The aspect of a dependent type which depends (on some assumption) we could call \emph{knowable object}.

\end{udefn}
\hypertarget{323_types_and_meaning_declarations}{}\subsubsection*{{3.2.3 Types and meaning declarations}}\label{323_types_and_meaning_declarations}

\begin{udefn}
We say the object $\alpha$ on the right of the colon in $a:\alpha$ is \emph{meaning referring}.

\emph{Meaning} is what is referred to $a$ by $\alpha$.

\end{udefn}
\hypertarget{324_truths_and_the_role_of_assumptions}{}\subsubsection*{{3.2.4 Truths and the role of assumptions}}\label{324_truths_and_the_role_of_assumptions}

\begin{udefn}
By definition of CTT a judgement is true if it has a proof.

We refer to this fact by saying that $(x:\alpha)$ \emph{carries the information} that $[x/a]:type$ is true.

\end{udefn}
\hypertarget{325_defining_information}{}\subsubsection*{{3.2.5 Defining information}}\label{325_defining_information}

Recall that by definition types are \emph{general concepts}.

\begin{udefn}
Every typing judgements in a context is (by definition) \emph{informational data}.

For example type declarations, assumptions and derived judgements are informational data with respect to the specific contexts they occur in.

\end{udefn}
\begin{udefn}
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 \emph{informational state in $\Gamma$}.

\end{udefn}
\begin{udefn}
We could call the collection of all judgements in an informational state its (underlying) \emph{knowledge state}.

\end{udefn}
\begin{udefn}
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$.

\end{udefn}
\hypertarget{33_contexts_as_constructive_possible_worlds}{}\subsection*{{3.3 Contexts as constructive possible worlds}}\label{33_contexts_as_constructive_possible_worlds}

\hypertarget{331_introducing_orderings_kripke_models}{}\subsubsection*{{3.3.1 introducing orderings: Kripke models}}\label{331_introducing_orderings_kripke_models}

\hypertarget{34_the_knowledge_framework}{}\subsection*{{3.4 The knowledge framework}}\label{34_the_knowledge_framework}

\hypertarget{341_updating_information_extending_knowledge}{}\subsubsection*{{3.4.1 Updating information, extending knowledge}}\label{341_updating_information_extending_knowledge}

\begin{udefn}
An interpretation of (also called \emph{updating of \ldots{}by} or \emph{extension of\ldots{}by})

\begin{displaymath}
\Gamma=x_1:\alpha_1,\dots,x_n:\alpha(x_1,\dots,x_n)
\end{displaymath}
in (resp. by)

\begin{displaymath}
\Delta=y_1:\beta_1,\dots,y_n:\beta(y_1,\dots,y_n)
\end{displaymath}
is defined by giving a sequence of definitions:

\begin{displaymath}
\itexarray{
x_1=f_1(y_1,\dots,y_m):\alpha_1
\\
\vdots
\\
x_n=f_n(y_1,\dots,y_m):\alpha_n(f_1(y_1,\dots,y_m),\dots, f_n(y_1,\dots,y_n))
}
\end{displaymath}
\end{udefn}
\begin{udefn}
see also Ranta1994 pp.145-147

An \emph{extension $\Gamma\leftarrow \Delta$ of a context $\Gamma$ by a context $\Delta$} as defined above can be derived by the following basic cases:

(a) \emph{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) \emph{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) \emph{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)$

\end{udefn}
\hypertarget{342_the_structure_of_knowledge}{}\subsubsection*{{3.4.2 The structure of knowledge}}\label{342_the_structure_of_knowledge}

\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item Borghuis, Kammarredine, Nederpelt, Formalizing Belief Revision in Type Theory, [[Formalizing Belief Revision in Type Theory|BibTex]]


\item 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


\item Aarne Ranta: type-theoretical grammar, 1994, Oxford University Press



\end{itemize}
[[substitution]]



\end{document}