\documentclass[onesided,12pt]{article}

\usepackage[french]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{libertine}

\usepackage{graphicx}
\usepackage{fancyhdr}

\usepackage[margin=3.9cm]{geometry}

\usepackage{xspace}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{proof}

\usepackage[normalem]{ulem}

\newcommand{\eqdef}{\stackrel{\mbox{def}}{=}}

\newcommand{\interp}[1]{\llbracket {#1} \rrbracket}
\newcommand{\next}{\raisebox{-0.4mm}{\scalebox{1.7}{$\circ$}}}
\renewcommand{\S}{\mathcal{S}}
\newcommand{\R}{\mathrel{\mathcal{R}}}

\newcommand{\ignore}[1]{}

\newcounter{cptq} 
\setcounter{cptq}{1}

\newcommand{\espace}{\vspace{0.5cm}}

\newcommand{\question}[1][]{%
  \par\vspace{0.5cm}\noindent\textbf{Question \arabic{cptq}}{#1}%
  \stepcounter{cptq} \\ \noindent}

\newcounter{cptc} 
\setcounter{cptc}{1}

\newenvironment{correction}{%
  \par\vspace{0.3cm}\noindent\textbf{Correction \arabic{cptc}}%
  \stepcounter{cptc} \\ \noindent}{}

\newenvironment{enonce}{}{}

\usepackage{url}
\usepackage{comment}
\excludecomment{correction}
%\excludecomment{enonce}

\begin{document}

\begin{center}
  {\Large Logique 2021 \\[1ex] Devoir à la Maison \#2} \\[2ex]
  David Baelde
\end{center}

\vspace{3ex}

\begin{center}
  \begin{minipage}{9cm}
    Ceci est la troisième version: voir les annotations V3 en marge
    pour les modifications.

    Le devoir est à rendre pour le 10 mai 2021 avant le cours,
    sous la forme d'un PDF composé en \LaTeX et à déposer
    sur la page ecampus du cours.
    Pour rappel, les devoirs maison sont notés et remplaceront au moins
    en partie les épreuves sur table cette année.
    Vous pouvez travailler le DM en groupe, mais j'attends des rendus
    rédigés individuellement.
  \end{minipage}
\end{center}

\vspace{2ex}

Le futur est-il écrit à l'avance, ou chaque instant a-t-il plusieurs
futurs possibles? Autrement dit, le temps est-il une ligne droite ou
une structure arborescente? Cette question métaphysique se décline
en informatique où les réponses sont plus simples: les deux types de
modèles du temps sont utiles, selon le type de systèmes et de
propriétés auxquels on s'intéresse. Dans ce devoir, nous étudions
deux logiques temporelles simples, une sur chaque type de modèle.

Nous travaillerons dans ce DM sur des structures de Kripke, selon une
définition plus générale que celle du cours de logique constructive:
\begin{itemize}
  \item
    une structure de Kripke est ici donnée par un ensemble de mondes
    muni d'une relation binaire $\R$ arbitraire;
  \item
    \marginpar{~$\rhd$V2}
    pour chaque monde on a
    une interprétation des constantes propositionnelles
    (pour chaque $w$ et $P$ on a $\hat{P}_w\in\{0,1\}$).
\end{itemize}
Dans le cours, $\R$ était une relation réflexive et transitive notée
$\leq$, et l'interprétation était monotone: ce n'est plus le cas ici.

\section{Temps linéaire}

\begin{enonce}
  On considère des formules construites sur la grammaire suivante:
  $$ A,A' ::= \top \mid \bot \mid
  P \mid \lnot P \mid A \vee A' \mid A \wedge A' \mid \next A $$
  Il s'agit des formules de la logique propositionnelle,
  enrichies de l'opérateur $\next$, en forme normale négative.
  Ici, $P$ désigne un atome, i.e.\ une constante propositionnelle.
  La négation ne porte que sur les atomes, ce qui n'est pas une
  restriction du fait des lois de de Morgan: on verra que celles-ci
  s'étendent à notre modalité par $\lnot \next A = \next \lnot A$.

  La sémantique de ces formules est donnée en restreignant notre attention
  aux structures de Kripke linéaires, i.e.\ celles où pour tout monde
  $w$ il existe un unique $w'$ tel que $w \R w'$. Cet unique successeur
  sera noté $w+1$.
  \'Etant donné une structure $\S$ et un monde $w$ de $\S$,
  on définit par induction sur $A$ l'interprétation de $\interp{A}^w_{\S}$:
  \begin{eqnarray*}
    \interp{\top}^w_\S &=& 1 \\
    \interp{\bot}^w_\S &=& 0 \\
    \interp{P}^w_\S &=& \hat{P}_w \\
    \interp{\lnot P}^w_\S &=& 1-\hat{P}_w \\
    \interp{A \wedge A'}^w_\S &=& 1 \quad \text{ ssi } \quad
    \interp{A}^w_\S=1 \text{ et }
    \interp{A'}^w_\S=1 \\
    \interp{A \vee A'}^w_\S &=& 1 \quad \text{ ssi } \quad
    \interp{A}^w_\S=1 \text{ ou }
    \interp{A'}^w_\S=1 \\
    \interp{\next A}^w_\S &=& \interp{A}^{w+1}_\S
  \end{eqnarray*}
  Quand il n'y a pas ambiguité, on pourra omettre $\S$ dans $\interp{A}^w_\S$.

  On dira qu'une formule $A$ est valide quand on a
  $\interp{A}^w_\S = 1$ pour toute structure $\S$
  et pour tout monde $w$ de $\S$.
  Quand $\interp{A}^w_\S=1$ on dira que $\S,w$ est un modèle
  de $A$, ce que l'on notera $\S,w \models A$.
  Dans le cas contraire on dit que $\S,w$ est un contre-modèle
  de $A$.
\end{enonce}

\question
Parmi les formules $A_x$ suivantes, lesquelles sont valides?
Justifier.
  $$
  A_1 \eqdef P \vee \lnot P
  \quad\quad
  A_2 \eqdef P \vee (\next \lnot P)
  \quad\quad
  A_3 \eqdef (\next P) \vee (\next \lnot P)
$$

\question
\marginpar{~$\rhd$V2}
Montrer que toute formule est logiquement équivalente\footnote{
  Deux formules sont logiquement équivalentes quand
  elles ont les mêmes modèles.
} à une formule
qui ne contient aucune sous-formule de la forme
$\next \top$,
$\next \bot$,
$\next(A\wedge A')$ ou
$\next(A\vee A')$.

\bigskip

\begin{enonce}
  On considère des séquents \emph{monolatères}\footnote{
    Intuitivement, on peut se ramener à ces séquents en passant
    de $\Gamma \vdash \Delta$ à $\vdash \lnot\Gamma, \Delta$ et
    en mettant toutes les formules en forme normale négative.
  }
  $\vdash\Gamma$ où $\Gamma$ est un ensemble de formules.
  Leur sémantique est donnée en interprétant les ensembles comme des 
  disjonctions: le séquent $\vdash\Gamma$ est valide si
  $\bigvee_{A\in\Gamma} A$ l'est.
  On considère les règles de la Figure~\ref{fig:tl}, qui portent
  sur de tels séquents, comme système de preuve pour notre logique.
  Dans la dernière règle, $\next\Gamma$ dénote
  l'ensemble des formules $\next A$ tel que $A\in\Gamma$.
  Ces règles permettent par exemple de construire les dérivations
  suivantes:
  $$
  \infer{\vdash P \vee \next \top}{
    \infer{\vdash P, \next \top}{
      \infer{\vdash \top}{}}}
  \quad\quad
  \infer{\vdash \bigl((\next P) \wedge (\next Q)\bigl) \vee
                \bigl(\next (\lnot P \vee \lnot Q)\bigr)}{
  \infer{\vdash (\next P) \wedge (\next Q),
                \next (\lnot P \vee \lnot Q)}{
  \infer{\vdash \next P,
                \next (\lnot P \vee \lnot Q)}{
  \infer{\vdash P,
                \lnot P \vee \lnot Q}{
  \infer{\vdash P,
                \lnot P,\lnot Q}{}}}
  &
  \infer{\vdash \next Q,
                \next (\lnot P \vee \lnot Q)}{\vdots}}}
  $$
  \begin{figure}
    $$
    \infer{\vdash \Gamma,\top}
    \quad\quad
    \infer{\vdash \Gamma, P,\lnot P}{}
    \quad\quad
    \infer{\vdash \Gamma, A\vee A'}{
      \vdash \Gamma,A,A'}
    \quad\quad
    \infer{\vdash \Gamma, A\wedge A'}{
      \vdash \Gamma,A & \vdash \Gamma,A'}
    \quad\quad
    \infer{\vdash \next\Gamma,\Delta}{\vdash \Gamma}
    $$
    \caption{Calcul des séquents pour la logique du temps linéaire.}
    \label{fig:tl}
  \end{figure}
\end{enonce}

\question
Montrer que toutes les règles de la Figure~\ref{fig:tl} sont
correctes: si les prémisses d'une instance de la règle sont valides,
la conclusion l'est aussi.
On veillera à bien s'appuyer sur la notion de validité formellement
définie plus haut.

\question
Montrer que les quatre premières règles sont inversibles:
si la conclusion est valide alors les prémisses aussi.

\question
Considérons une instance de la dernière règle telle que
$\Delta$ ne contient que des atomes, négations d'atomes ou $\bot$,
\marginpar{~$\rhd$V3}
et ne contient pas à la fois un atome et sa négation.
Montrer que si la conclusion est valide alors la prémisse
l'est aussi.

\question
En déduire que le calcul est complet: tout séquent valide est
dérivable.

\section{Temps arborescent}

On considère maintenant un nouveau langage pour les formules,
en remplaçant la modalité $\next$ par les modalités $\Box$ et $\Diamond$:
  $$ A,A' ::= \top \mid \bot \mid
  P \mid \lnot P \mid A \vee A' \mid A \wedge A' \mid \Box A \mid
  \Diamond A $$

La sémantique de cette logique est définie sur des structures
de Kripke quelconques --- on pourrait se restreindre aux arbres, mais
cela ne changerait rien\footnote{
  Ceci est un corollaire du résultat de complétude que vous allez démontrer.
}. On oublie donc la contrainte de linéarité: un monde peut avoir plusieurs
successeurs; il peut aussi n'en avoir aucun.
La définition formelle de la sémantique ne change que pour les modalités:
\begin{eqnarray*}
  \interp{\Box A}^w_\S &=& 1
  \quad \text{ ssi } \quad
  \interp{A}^{w'}_\S = 1
  \text{ pour tout } w' \text{ tel que } w \R w' \\
  \interp{\Diamond A}^w_\S &=& 1
  \quad \text{ ssi } \quad
  \interp{A}^{w'}_\S = 1
  \text{ pour un } w' \text{ tel que } w \R w'
\end{eqnarray*}

\question
Parmi les formules suivantes, lesquelles sont valides? Justifier.
$$
  A_1 \eqdef (\Diamond\lnot P) \vee (\Diamond P)
  \quad\quad
  A_2 \eqdef (\Box\lnot P) \vee (\Box P)
  \quad\quad
  A_3 \eqdef (\Box\bot) \vee (\Diamond\top)
$$

\bigskip

On considère pour la logique du temps arborescent un calcul des séquents
défini par les mêmes quatre premières règles que dans la section précédente,
mais en remplaçant la règle modale précédente par la suivante:
$$
  \infer{\vdash \Box A, \Diamond\Gamma, \Delta}{\vdash A,\Gamma}
$$
Dans cette règles, les ensembles de formules $\Gamma$ et $\Delta$
peuvent être vides --- mais il n'est pas question pour la formule $A$
d'être vide. \marginpar{~$\rhd$V2}
On peut ainsi dériver, par exemple:
$$ \infer{\vdash \Box P, \Box Q, \Diamond \lnot P, \Diamond R, S}{
  \infer{\vdash P, \lnot P, R}{}}
  \quad\quad
  \infer{\vdash\Box\top}{\infer{\vdash \top}{}} $$

\question
Montrer que cette nouvelle règle modale est correcte.

\bigskip

On en conclut que les séquents dérivables sont valides. On cherche
maintenant à montrer la complétude du calcul.
On admettra que les quatre premières règles de la Figure~\ref{fig:tl}
sont inversibles pour la sémantique arborescente.

\question
On considère un séquent 
$\vdash\Box A_1,\ldots,\Box A_n,\Diamond\Gamma,\Delta$
pour $n\geq 0$,
où $\Delta$ ne contient que des atomes, négations d'atomes
et éventuellement $\bot$,
\marginpar{~$\rhd$V3}
et ne contient pas à la fois un atome et sa négation.
Montrer que si tous les séquents
$\vdash A_i,\Gamma$
sont invalides, alors le séquent précédent est aussi invalide.

\question
En conclure que ce calcul des séquents est complet pour la logique
du temps arborescent.

\question
Proposer une nouvelle règle, ou une modification de la règle modale,
pour obtenir un calcul correct et complet quand l'on modifie la sémantique
en ne considérant que des structures sans extrémité (tout monde a au moins
un successeur).

\question
Même question quand on se restreint aux structures transitives,
i.e.\ les structures où,
pour tous $w_1,w_2,w_3$ tel que $w_1 \R w_2 \R w_3$ on a aussi
$w_1 \R w_3$.

\end{document}
