\documentclass{article}

\usepackage{a4}
\usepackage[latin1]{inputenc}
\usepackage[francais]{babel}
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{amsfonts,amsmath,amsthm,amssymb,stmaryrd}
\usepackage{prooftree}

\newcommand{\R}{\mathbb{R}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\A}{\ensuremath{\bl{\cal A}}}
\newcommand{\M}{{\cal M}}
\newcommand{\C}{{\cal C}}
\newcommand{\force}{\mathop{\textsf{I}\!\!\vdash}}

%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}
\newcommand{\la}{\xymatrix{\ar@{<-}[r] &}}
\newcommand{\case}[4]{\textbf{case}~#1~\textbf{of}~#2~\textbf{in}~#3~\textbf{or}~#4}


\title{Magistère d'Informatique et Modélisation}
\author{Examen final de logique}

\date{2003}

\begin{document}
\maketitle 
\thispagestyle{empty}

\emph{Documents autorisés.}

Dans les questions ouvertes, limitez votre réponse à au plus cinq lignes.



\section*{Exercice 1}

Démontrer en déduction naturelle la proposition $`v \vee (`j \vee `q)
"=>" `q \vee (`j \vee `v)$.

\section*{Exercice 2}

On ajoute au lambda calcul, deux opérateurs unaires $\textbf{pr}_1$,
$\textbf{pr}_2$ et un opérateur quaternaire $\case{\_}{\_}{\_}{\_}$.
On a alors la syntaxe suivante :
\begin{eqnarray*}
  M, N, P &::=& x ~|~ `l x . M ~|~ M~N ~|~ \textbf{pr}_1~ M ~|~ \textbf{pr}_2~M ~|~ \case{M}{x}{N}{P}
\end{eqnarray*}
où $x$ est une variable quelconque qui peut aussi bien être $y$, $z$,
$x_0$,..., $x_{10}$, ... On munit ce calcul des règles de typage du
$`l$-calcul auxquelles on ajoute les trois règles suivantes.
\begin{displaymath}
  \prooftree
  `G "|-" M : `s 
  \justifies`G "|-" \textbf{pr}_1~M : `s \vee `t
  \endprooftree
  \qquad \qquad
  \prooftree
   `G "|-" M : `t
  \justifies`G "|-" \textbf{pr}_2~M : `s \vee `t
  \endprooftree
\end{displaymath}

\begin{displaymath}
  \prooftree
  `G "|-" M : `s\vee `t \qquad `G, x : `s "|-" P : `r 
  \qquad `G, x : `t "|-" Q : `r  
            \justifies `G "|-" \case{M}{x}{P}{Q} : `r
  \endprooftree
\end{displaymath}

\begin{enumerate}
\item A quelles règles de déduction en logique correspondent ces
  règles de typage ?
\item Un type $`t$ est \emph{habité} s'il existe un terme $M$ de ce
  calcul tel que $"|-" M:`t$.  Montrer que le
  type $(`v \vee `j) "->" (`j \vee `v)$  est habité.
\item Est-ce que le type $`v \vee (`v "->" `j)$ est habité ?  Justifier
  votre réponse.
\item Donner une preuve en déduction naturelle de $`v \vee (`v "->"
  `j)$ (ici $"->"$ note l'implication).  Est-ce que cette preuve est
  intuitionniste? 
\end{enumerate}

\section*{Exercice 3}

On considère une logique enrichie d'un opérateur ; on dit une
\emph{modalité}. Cette modalité est notée $`[]$.  $`[]`v$ se lit
«toujours $`v$» ou «carré $`v$».  On aurait pu la noter $K_0 `v$ et la
lire «l'agent $0$ sait $`v$».  La syntaxe de cette logique est
\begin{eqnarray*}
  `v, `j &::=& p ~|~ \bot ~|~ `v "=>" `j ~|~ `v \vee `j ~|~ `v \wedge
  `j ~|~  `[] `v 
\end{eqnarray*}
qui contient aussi les règles suivantes:
\begin{displaymath}
\prooftree
"|-"_K `v
  \justifies "|-"_M `v
  \using (Classique)
  \endprooftree
%
  \qquad
%
 \prooftree
  "|-"_M `v \qquad "|-"_M `v "=>" `j
  \justifies  "|-"_M `j
  \using (MP)
  \endprooftree
\qquad 
  \prooftree
  "|-"_M `v
  \justifies"|-"_M `[] `v
  \using (Generalisation)
\endprooftree
\end{displaymath}
(où $"|-"_K `v$ signifie que $`v$ est un théorème de la logique
propositionnelle classique) et les axiomes suivants
 \begin{displaymath} 
  \prooftree
  \justifies "|-"_M `[] `v  "=>" `[](`v "=>" `j) "=>"`[] `j
  \using (Distribution)
  \endprooftree
\qquad
  \prooftree
  \justifies "|-"_M `[] `v  "=>" `v
  \using (T)
  \endprooftree
\end{displaymath}
\begin{enumerate}
\item Montrer que la règle 
  \begin{displaymath}
    \prooftree
    "|-"_M `[]`v \quad "|-"_M `[](`v "=>" `j) 
    \justifies "|-"_M `[] `j
    \endprooftree
  \end{displaymath}
est dérivable dans ce système.
\item Démontrer $`[] (`v \wedge `j) "=>" `[] `v \wedge `[]`j$.
% modèles de Kripke
\item On considère les mêmes modèles de Kripke que la logique
  intuitionniste.  Donner l'interprétation de la relation de forçage
  $\force$, en particulier pour les propositions de la forme $`[]`v$
  pour que les règles ci-dessus soient correctes.
\item On considère dans cette logique l'opérateur $"->"$ défini par
  $`v "->" `j$ si et seulement si $`[] (`v "=>" `j)$.   Que vous
  inspire cet opérateur? 
\end{enumerate}


\end{document}
