%% Time-stamp: <version du Wed 13 Dec 2000 à 18h03 par Pierre Lescanne>
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
%\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{stmaryrd,amssymb}
\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
\usepackage[all]{xy}

%\renewenvironment{slide}[1]{#1} 
%\def\printlandscape{}  % pour sortir en portrait
%\slidesmag{1} 
%\usepackage{fullpage}

%% Time-stamping  
%% compute the time in hours and minutes; 
 \newcount\timehh\newcount\timemm \timehh=\time 
 \divide\timehh by 60 \timemm=\time
 \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255
 \newcommand{\timestamp}
 { {\protect\small\sl\today\ -- 
 \ifnum\timehh<10 0\fi\number\timehh\,h\,
   \ifnum\timemm<10 0\fi\number\timemm}}
                                          % avec dvips

\def\printlandscape{\special{landscape}}    % pour sortir en landscape
                                            % avec dvips

\slidesmag{5}
\articlemag{1}

\rotateheaderstrue       % si tu combines slide et slide*

\title{\rouge{\textit{Les modèles de Kripke}}\\
      \rouge{\textit{de la logique propositionnelle}}}

\author{}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

\newcommand{\rouge}[1]{{\color{red}#1}}
\newcommand{\VERT}[1]{{\color{green}#1}}
\newcommand{\bleu}[1]{\textcolor{blue}{$#1$}}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}

\renewcommand{\S}{\textbf{S}}
\newcommand{\N}{\texttt{\small |}\!\textsf{N}}
\newcommand{\R}{\texttt{\small |}\!\textsf{R}}
\newcommand{\vDash}{\mathop{|\!\!\!=}}
\newcommand{\pr}{\mathop{\underline{\textsf{prefix}}}}
\newcommand{\mlt}{\prec\!\!\prec}
\renewcommand{\phi}{\varphi}
\newcommand{\force}{\mathop{\textsf{\large I}\!\!\vdash}}
\newcommand{\notforce}{\mathop{\textsf{\large I}\!\!\not\vdash}}

\newcommand{\M}{{\cal M}}
\newcommand{\RM}{{\cal R_M}}
\newcommand{\UM}{{\cal U_M}}
\newcommand{\IM}{{\cal I_M}}
\newcommand{\Ra}{\ensuremath{\Rightarrow}}
\newcommand{\ra}{\ensuremath{\rightarrow}}
\newcommand{\RaE}{\VERT{\Ra E}}
\newcommand{\RaI}{\VERT{\Ra I}}
\newcommand{\et}{\mathop{\&}}
 \newcommand{\infer}[2]{
 \begin{array}{c}
   #1\\
   \hline \noalign{\vskip 1pt}#2
  \end{array}}
\newcommand{\inferThreeLabel}[5]{\bl{
\begin{array}{cc}
 {\VERT{#1}} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\hspace{2em} #4\\
   \hline \noalign{\vskip 1pt}#5
  \end{array}
\end{array}}}

\newcommand{\inferTwoLabel}[4]{\bl{
\begin{array}{cc}
 {\VERT{#1}} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}
\end{array}}}

\newcommand{\leafLabel}[2]{\bl{
 {\VERT{#1}} \quad
  \begin{array}{c}
  #2
  \end{array} }}

\newcommand{\inferLabel}[3]{\bl{
    \begin{array}{cc}
    {\VERT{#1}} \quad
    \begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \end{array}
  \end{array}
  }}

    
\newcommand{\heading}[1]{%      % ca c'est des commandes a moi
  \begin{center}                % mais ca peut t'interesser
    \large\bf
    \color{cyan}{\shadowbox{#1}}%
  \end{center}
  \markright{#1}
  \vspace{1ex minus 1ex}}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{green}{\bf\Ovalbox{#1}}
  \end{center}}

\begin{document}

%------------------------------------------------------
\begin{slide}
    \maketitle
    \addtocounter{slide}{-1}
    \slidepagestyle{empty}

\vfill 

\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Notations}
À partir de maintenant, je note 
\begin{enumerate}
\item les propositions \bleu{\phi, \psi,\chi, \theta} etc.
  
\item les variables propositionnelles \bleu{p, q, r, s, t},
 
\item les environnements \bleu{\Gamma, \Theta, \Sigma}
\end{enumerate}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les modèles de Kripke (cas général)}
Un \rouge{modèle de Kripke} est un triplet \bleu{\M=(\UM,\IM,\RM)} où
\begin{itemize}
\item \bleu{\UM} est un ensemble  dont les éléments sont appelés 
  \begin{itemize}
  \item des \VERT{mondes},
  \item des \VERT{mondes possibles},
  \item des \VERT{étapes (de raisonnement)},
  \item des \VERT{états}.
\end{itemize}
\item \bleu{\IM : Variables \rightarrow {\cal P}(\UM)}.  Intuitivement
  \bleu{\IM(p)} est l'ensembles des mondes où la variable \bleu{p} est
  satisfaite.
\end{itemize}
Les mondes sont notés \bleu{u, v, w}.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les modèles de Kripke (cas général)}
\begin{itemize}
\item \bleu{\RM = (R_1,..R_n)} est un ensemble de relations dites
  \rouge{relations d'accessibilité}.\\Si \bleu{u\,R_i\,v} alors le
  monde \bleu{v} est accessible à partir de \bleu{u} pour
  \bleu{i}\footnote{On verra plus tard ce que ça signifie.}. 
\end{itemize}
Les propriétés (transitivité, réflexivité, symétrie ou antisymétrie)
des relations \bleu{R_i} jouent un rôle.\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les modèles de Kripke (cas propositionnelle)}
\begin{enumerate}
\item \rouge{Il n'y a qu'une relation} notée \bleu{\le_\M}, qui est un ordre,
  c-à-d réflexive, antisymétrique et transitive.
\item \bleu{\IM} est \rouge{dirigé}, c-à-d que pour toute variable
  propositionnelle \bleu{p},
  \centerline{si~~\bleu{u\in\IM(p)}
~et~ \bleu{u\le_\M v} ~~~~alors~~~~ \bleu{v\in\IM(p)}.}
\end{enumerate}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Forcage}
On définit sur \bleu{\UM} une relation dite de \rouge{forcage} qui
s'écrit\footnote{parfois aussi notée \bleu{\M,u\vDash u}}:
\begin{itemize}
\item ~~~~~~~~~ \bleu{\M,u \force \phi} 
\item 
ou ~~~~
 \bleu{u \force_\M \phi} 
\item 
ou ~~~~
 \bleu{u \force \phi} ~~~~s'il n'y a pas d'ambiguïtés sur \bleu{\M}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Forcage}
\begin{footnotesize}
\begin{enumerate}
\item Si \bleu{\phi} est une \rouge{variable} \bleu{p}:
\begin{center}
 \bleu{\M,u \force \phi} ~~~~~~~~~~ssi~~~~~~~~~~ \bleu{u \in\IM(p)}
\end{center}
\item Si \bleu{\phi} est une \rouge{conjonction} \bleu{\psi \wedge \theta}
\begin{center}
 \bleu{\M,u \force \phi} ~~~~~~~~~~ssi~~~~~~~~~~ \bleu{\M,u \force
   \psi}~~~~et~~~~ \bleu{\M,u \force \theta}
\end{center}
\item Si \bleu{\phi} est une \rouge{disjonction} \bleu{\psi \vee \theta}
\begin{center}
 \bleu{\M,u \force \phi} ~~~~~~~~~~ssi~~~~~~~~~~ \bleu{\M,u \force
   \psi}~~~~ou~~~~ \bleu{\M,u \force \theta}
\end{center}
\item Si \bleu{\phi} est une \rouge{implication} \bleu{\psi \Rightarrow \theta}
\begin{center}
  \bleu{\M,u \force \phi}
  
  ssi
  
  pour tout \bleu{v\ge_M u}~~si~~\bleu{\M,v \force \psi}~~alors~~
  \bleu{\M,v \force \theta}
\end{center}
\item Si  \bleu{\bot} est l'\rouge{absurde}, alors \bleu{\M,u \notforce \bot}.
\end{enumerate}
\end{footnotesize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Monotonicité du forcage}
\rouge{Proposition} \fbox{\bleu{\force_\M} \VERT{est monotone}.}
\begin{center}
 Si~~\bleu{\M,u \force \phi} ~~et~~ \bleu{u\le_\M
   v}~~~~~~~~~~alors~~~~~~~~~~ \bleu{\M,v \force \phi} 
\end{center}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Monotonicité du forcage}
\rouge{Proposition} \fbox{\bleu{\force_\M} \VERT{est monotone}.}
\begin{center}
 Si~~\bleu{\M,u \force \phi} ~~et~~ \bleu{u\le_\M
   v}~~~~~~~~~~alors~~~~~~~~~~ \bleu{\M,v \force \phi} 
\end{center}

\vspace*{20pt}

\VERT{En exercice !}


\vspace*{20pt}

Donc pour tout \bleu{\phi}, l'ensemble
\bleu{\{u\in\UM~|~u\force\phi\}} est dirigé.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice}
Soit le modèle de Kripke \bleu{\cal A}:

\begin{center}
\bl{
\xymatrix{u_1 \ar@{-}[dr]&& u_2 \ar@{-}[dl]\\& u_0}
}
\end{center}
où \bleu{u_0\force p} et \bleu{u_1\force q}. 
\begin{enumerate}
\item Donnez les valeurs de \bleu{\cal I_A} pour \bleu{p} et \bleu{q}.
\item Annotez les mondes qui forcent \bleu{p\vee q}, \bleu{p\wedge q},
  \bleu{p\Rightarrow q}
\end{enumerate}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques définitions}
\begin{enumerate}
\item \bleu{\M\vDash \phi} ~~~~~~~~(\bleu{\M} \rouge{modélise} \bleu{\phi},
  \bleu{\phi}\rouge{est valide dans} \bleu{\M}) si pour tout
  \bleu{u\in\M}, on a \bleu{\M,u\force \phi}.
\item \bleu{\vDash \phi}, ~~~~~~~(\bleu{\phi} \rouge{est valide}), si pour
  tout modèle de Kripke \bleu{\M}, on a \bleu{\M\vDash\phi}.
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Théorème de correction} \fbox{Si \bleu{\vdash\phi} alors
  \bleu{\vDash\phi}.}
\begin{itemize}

\vspace*{6pt}

\item On fait la preuve dans le cas de la logique minimale.
\item On va prouver un lemme, pour lequel on a besoin d'une définition.
\end{itemize}

\vspace*{12pt}

\rouge{Définition:} \bleu{\Gamma\vDash\phi} où
\bleu{\Gamma\equiv\{\phi_1,...,\phi_n\}} 

signifie que pour tout
modèle \bleu{\M} et tout \bleu{u\in\UM},
  
\begin{center}
  \bleu{u\force_\M\phi_1},..., \bleu{u\force_\M\phi_n} implique
  \bleu{u\force_\M\phi}.
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Lemme} \fbox{Si \bleu{\Gamma\vdash\phi} alors
  \bleu{\Gamma\vDash\phi}.}

La démonstration se fait par \rouge{induction sur la structure de l'arbre de
preuve} de \bleu{\Gamma\vdash\phi}.

On fixe le modèle \bleu{\M} dans la preuve. 

On suppose que pour tout 
\bleu{u}, on a \bleu{u\force_\M\phi_1},..., \bleu{u\force_\M\phi_n}.

On  cherche à montrer que \bleu{u\force_\M\phi}.

\begin{itemize}
\item \rouge{L'arbre est réduit à une feuille.} Alors
  \bleu{\phi\in\Gamma} et comme \bleu{u\force_\M\phi_1},...,
  \bleu{u\force_\M\phi_n}, on a \bleu{u\force_\M\phi}
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Lemme} \fbox{Si \bleu{\Gamma\vdash\phi} alors
  \bleu{\Gamma\vDash\phi}.}
\begin{itemize}
\item \rouge{Le n{\oe}ud de la racine est la règle \RaI{}} et donc le jugement
  est \bleu{\Gamma\vdash\psi\Ra\theta}.  
  
  Par induction il existe un arbre de preuve pour \bleu{\Gamma,
    \psi\vdash\theta}.
  
  L'hypothèse d'induction nous dit que pour n'importe quel monde
  \bleu{w} tel que \bl{\[w\force\phi_1,...,w\force\phi_n,
    w\force\psi\]} on a \bl{\[w\force\theta.\]}

Considérons maintenant un monde \bleu{u} tel que
\bl{\[u\force\phi_1,...,u\force\phi_n.\]}

Si \bleu{v} est monde tel que \bleu{u\le_\M v} et \bleu{v\force\psi}.

Par monotonicité,  \bl{\[v\force\phi_1,...,v\force\phi_n.\]}
On peut donc appliquer l'hypothèse de récurrence à \bleu{v} et l'on a 
\bleu{v\force\theta}.  

Par la définition de \bleu{\force} sur
\bleu{\phi\equiv\psi\Ra\theta} cela donne \bleu{u\force\phi}.


\end{itemize}
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Lemme} \fbox{Si \bleu{\Gamma\vdash\phi} alors
  \bleu{\Gamma\vDash\phi}.}
\begin{itemize}
\item \rouge{Le n{\oe}ud de la racine est la règle \RaE{}} 

On a donc deux arbres de preuve pour \bleu{\Gamma\vdash\psi} et \bleu{\Gamma\vdash\psi\Ra\phi}.

Soit \bleu{u} tel que
\bl{\[u\force\phi_1,...,u\force\phi_n.\]}
alors par hypothèse d'induction d'une part \bleu{u\force\psi} d'autre
part \bleu{u\force\psi\Ra\phi}.

Par définition de \bleu{u\force\psi\Ra\phi}, on a \bleu{u\force\phi}.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Lemme} \fbox{Si \bleu{\Gamma\vdash\phi} alors
  \bleu{\Gamma\vDash\phi}.}
\begin{itemize}
\item \rouge{Le n{\oe}ud de la racine est la règle \VERT{$\bot$}.} 

Si \bleu{u\force\psi} (pour tout \bleu{\psi\in\Gamma}) alors
\bleu{u\force \bot}, mais on sait que ça n'est pas possible, donc
chaque fois qu'on a \bleu{u\force\psi} (pour tout
\bleu{\psi\in\Gamma}), on aussi \bleu{u\force \phi}, donc
\bleu{\Gamma\vDash \phi}.

\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Lemme} \fbox{Si \bleu{\Gamma\vdash\phi} alors
  \bleu{\Gamma\vDash\phi}.}
\begin{itemize}
\item \rouge{Le n{\oe}ud de la racine est la règle \VERT{$\vee I_g$}}
  avec \bleu{\Gamma \vdash \theta\vee\chi}.
  
  L'hypothèse d'induction dit que pour tout \bleu{u\in\UM} 
  \begin{itemize}
  \item si pour tout \bleu{\psi\in\Gamma} on a \bleu{u\force \psi}
    alors \bleu{u\force \theta},
  \end{itemize}
donc aussi \bleu{u\force \theta\vee\chi}.

\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Lemme} \fbox{Si \bleu{\Gamma\vdash\phi} alors
  \bleu{\Gamma\vDash\phi}.}
\begin{itemize}

\item \rouge{Le n{\oe}ud de la racine est la règle \VERT{$\vee E_g$}}
  avec comme prémisse 
  
  \bleu{\Gamma\vdash \phi \vee \psi}, ~~~~~~~~~ \bleu{\Gamma, \phi
    \vdash \theta} ~~~~ et ~~~~\bleu{\Gamma, \psi\vdash \theta}

et comme conclusion
   \bleu{\Gamma \vdash \theta}.
   
   Considérons les \bleu{u} qui satisfont \bleu{u\force \chi} pour
   \bleu{\chi\in\Gamma}.
   
   L'hypothèse d'induction nous dit que pour ces \bleu{u}, on doit
   avoir \bleu{u\force \phi \vee \psi}.
   
   Si de plus \bleu{u\force \phi} alors \bleu{u\force \theta}.
   
   Et si de plus \bleu{u\force \psi} alors \bleu{u\force \theta}
   aussi.

Mais comme on sait que  \bleu{u\force \phi} ou \bleu{u\force \psi}
alors dans tous les cas \bleu{u\force \theta}. 
\end{itemize}
\vfill
\end{slide}

\end{document}
% LocalWords:  green forcage ssi ud
