\documentclass{article}

\usepackage{francais}
\usepackage{t1enc}
\usepackage{a4}
\usepackage[all]{xy}

\renewcommand{\S}{\textbf{S}}
\newcommand{\N}{\texttt{\small |}\!\textsf{N}}
\newcommand{\vDash}{\mathop{|\!\!\!=}}
\newcommand{\force}{\mathop{\textsf{I}\!\!\vdash}}
\newcommand{\notforce}{\mathop{\textsf{I}\!\!\vdash\!\!\!\!\!/}}
\newcommand{\K}{\mathcal{K}}


\begin{document}

\title{Magistère d'Informatique et Modélisation}
%\author{Devoir de Logique}
%\date{\emph{À remettre le xx mars 199?}}


%\title{DEA d'Informatique de Lyon}
\author{Complétude du calcul propositionnel intuitionniste} 
\date{}

\maketitle 

Le but de ce qui suit est de montrer la complétude du calcul
propositionnel intuitionniste vis-à-vis des modèles de Kripke. Sans
beaucoup nuire à la généralité, on se restreindra à un calcul ne
contenant que les connecteurs $\vee$ et $\rightarrow$.  Auparavant on
montre que l'on peut indifféremment considérer les modèles finis ou
les modèles finis et/ou infinis.

\section*{Partie 1~: Modèles finis ou infinis}

Dans cette partie on montre que pour le calcul propositionnel
intuitionniste, la validité dans les modèles de Kripke infinis se
ramène à la validité dans les modèles de Kripke finis.

L'ensemble des propositions est noté \textsf{PROP} et l'ensemble des
variables propositionnelles est noté $Var$.  Un ensemble $\Gamma$ de
propositions est \emph{stable par sous terme} (ou sous-formule) si
quand $\Gamma$ contient $\varphi$ il contient toutes les propositions
qui sont des sous-termes de $\varphi$.  

Un modèle de Kripke du calcul propositionnel est un triplet \(\K = (U,
\le, {\mathcal{I}})\), où $U$ est un ensemble fini ou infini, $\le$
est un ordre sur $U$ et $\mathcal{I}: Var \xymatrix{\ar@{>}[r] &}
\mathcal{P}(U)$ est tel que pour chaque variable
propositionnelle~$p\in Var$, $\mathcal{I}(p)$ est un sous-ensemble
dirigé de $U$, c'est-à-dire tel que $u\in\mathcal{I}(p)$ et $u\le v$
impliquent $v\in\mathcal{I}(p)$.  On définit une relation $\force_\K$
(ou plus simplement $\force$) sur $U \times \textsf{PROP}$ par
induction sur la structure des propositions:
\begin{itemize}
\item si la proposition est une variable propositionnelle $p$, alors
  $u \force p$ signifie que $u \in \mathcal{I}(p)$,
\item si  la proposition est de la forme $\varphi \vee \psi$, alors $u\force
  \varphi\vee \psi$, signifie que $u\force \varphi$ ou $u\force \psi$,
\item si la proposition est de la forme $\varphi \rightarrow \psi$, alors
  $u\force \varphi \rightarrow \psi$ signifie que  pour tout $v \ge u$ si $v\force
  \varphi$ alors $v\force \psi$.
\end{itemize}
$\varphi$ est valide dans $\K$, ce qui s'écrit $\K\vDash \varphi$, ssi pour
tout $u\in U$, $u\force \varphi$ et $\varphi$~est valide, ce qui s'écrit
$\vDash \varphi$, ssi pour tout modèle $\K$, $\K \vDash \varphi$.

Soient $\K$ un modèle de Kripke et $\Gamma$ un ensemble fini de
propositions stable par sous-terme.  Nous associons à $\K$ un modèle de Kripke
fini $\K_\Gamma = (U_\Gamma, \le_\Gamma, \mathcal{I}_\Gamma)$ comme
suit. On définit, pour chaque $u\in U$, \([u] =
\{\varphi\in\Gamma~|~u\force \varphi\}\) et \(U_\Gamma = \{[u]~|~u\in U\}.\)
L'ordre $\le_\Gamma$ est l'ordre d'inclusion des sous-ensembles de
\textsf{PROP}. On écrit $\force_\Gamma$ au lieu de $\force_{\K_\Gamma}$.
Par définition $\mathcal{I}_\Gamma(p) = \{[u]~|~p\in[u]\}$.  On dit
que $\K_\Gamma$ est obtenu par \emph{filtration} à partir de $\K$.

\begin{enumerate}
\item Montrez que $\K_\Gamma$ satisfait les critères de définition
  d'un modèle de Kripke.
\item Montrez que si $\varphi\in\Gamma$ les trois conditions suivantes sont
  équivalentes:
  \begin{itemize}
  \item[(i)] $[u]\force_\Gamma\varphi$ 
  \item[(ii)] $u\force \varphi$ 
  \item[(iii)] $\varphi\in[u]$.
\end{itemize}
\item Montrez que $U_\Gamma$ est fini.
\item Montrez que $\vDash \varphi$ si et seulement si $\K\vDash \varphi$
  pour tous les modèles $\K$ finis.
\end{enumerate}


\section*{Partie 2~: Ensembles premiers}

Dans la suite, on considère les modèles de Kripke finis ou infinis.

Un ensemble de propositions $\Delta$ est \emph{premier} s'il satisfait 
les deux conditions~:
\begin{itemize}
\item[\emph{a.}] $\Delta$ est clos par $\vdash$,
\item[\emph{b.}] quand $\psi\vee \chi \in\Delta$ alors ou bien
  $\psi\in\Delta,$ ou bien $\chi\in\Delta.$
\end{itemize}

Soient $\Gamma$ un ensemble de propositions et $\varphi$ une proposition
telle $\Gamma\not\vdash\varphi$, on veut construire un ensemble $\Gamma'$
premier qui contienne $\Gamma$ et tel que $\Gamma'\not\vdash\varphi$.
Pour cela, on ordonne les propositions disjonctives en une suite
$(\psi_1\vee\chi_1, ..., \psi_n\vee\chi_n,...)$ et l'on construit la
suite $\Gamma_k$ ainsi. $\Gamma_0$ est $\Gamma$.  Supposons construit
$\Gamma_k$ et considérons la première proposition de la suite
ci-dessus qui n'a pas été considérée et qui est telle que $\Gamma_k
\vdash \psi_{n_k}\vee\chi_{n_k}$.

\begin{enumerate}
\item Expliquez pourquoi une telle proposition $\psi_{n_k}\vee\chi_{n_k}$
  existe toujours.
\item Montrez que l'on n'a pas à la fois $\Gamma_k, \psi_{n_k} \vdash
  \varphi$ et $\Gamma_k, \chi_{n_k} \vdash \varphi$.  Ainsi on définit 
\[\Gamma_{k+1} := \left\{\begin{array}{l}
                         \Gamma_k \cup \{\psi_{n_k}\} \textrm{ si } 
                         \Gamma_k, \psi_{n_k} \not\vdash \varphi\\
                         \Gamma_k \cup \{\chi_{n_k}\} \textrm{ dans les
                           autres cas.}
                                \end{array}
                              \right.\]


\item  Soit $\Gamma' = \bigcup_{k\ge 0} \Gamma_k$.  Montrez que
  $\Gamma' \not\vdash \varphi$. 

\item Montrez que $\Gamma'$ est premier.
\end{enumerate}


\section*{Partie 3~:Théorème de complétude}
Dans cette partie on veut montrer que si $\Gamma\not\vdash\varphi$
alors il existe un modèle de Kripke $\K = (U, \le, \mathcal{I})$ et un
monde $u$ minimum dans $U$ telle que $u\force\Gamma$ et
$u\notforce\varphi$. On construit tout d'abord un ensemble premier
$\Gamma'$ tel que $\Gamma'\supseteq\Gamma$ et
$\Gamma'\not\vdash\varphi$.  $U$~est l'ensemble des suites finies
d'entiers ordonnées par l'ordre préfixe ($\varepsilon$ est la suite
vide).  Donc un monde de $U$ est un suite finie d'entiers
$\alpha\equiv a_1...a_p$.
\begin{enumerate}
\item On construit le modèle $\K$ et des ensembles $\Gamma(\alpha)$
  associés à chaque suite d'entiers $\alpha$ (c'est-à-dire à chaque
  monde de $U$).
\begin{itemize}
\item \textsf{cas} $\varepsilon$, $\Gamma(\varepsilon) = \Gamma'$.
\item \textsf{cas} $\alpha i$. Soit une suite $((\sigma_0,\tau_0),
  (\sigma_1,\tau_1), ..., (\sigma_n,\tau_n), ...,)$ énumérant tous les
  $(\sigma_i,\tau_i)$ tels que $\Gamma(\alpha), \sigma_i \not\vdash
  \tau_i$.  On peut construire un ensemble premier $\Gamma(\alpha i)$
  tel que $\sigma_i\in \Gamma(\alpha i)$ et $\Gamma(\alpha
  i)\not\vdash \tau_i$.  Pourquoi~?  
\end{itemize}
Par définition, $\alpha\in\mathcal{I}(p)$ si et seulement si
$p\in\Gamma(\alpha)$.
  
\item Supposant que pour tout $\beta$, $\beta\force \psi_1$ si et
  seulement si $\Gamma(\beta) \vdash \psi_1$ et $\beta\force \psi_2$
  si et seulement si $\Gamma(\beta) \vdash \psi_2$, montrez que
  $\alpha \force \psi_1 \rightarrow \psi_2$ implique $\Gamma(\alpha)
  \vdash \psi_1 \rightarrow \psi_2$.
\item Montrez que $\alpha\force \psi$ si et seulement si
  $\Gamma(\alpha) \vdash \psi$. 
\item Montrez que $\varepsilon\force\psi$ (pour chaque
  $\psi\in\Gamma$) et que $\varepsilon\notforce\varphi$.
\item Montrez que si $\vDash \varphi$ alors $\vdash \varphi$.
\end{enumerate}


\end{document}

% LocalWords:  french enc d'Informatique triplet Var PROP ii
