\documentclass{article}

\usepackage{a4}
\usepackage{fullpage}
\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}}
\newcommand{\notforce}{\mathop{\textsf{\large I}\!\!\not\vdash}}
\newcommand{\UM}{{\cal U_M}}
\newcommand{\IM}{{\cal I_M}}

%% ==============================================================
%%                   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{Corrigé de l'examen final de logique}

\date{2003}

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

\section*{Exercice 1}

Posons $`x = `v \vee (`j \vee `q)$.

\begin{footnotesize}
\begin{displaymath}
  \prooftree
  \prooftree
  `x"|-" `x
  \quad %
  \prooftree
    \prooftree
  `x, `v "|-" `v
  \justifies  `x, `v "|-" `j \vee `v
  \endprooftree
   \justifies  `x, `v "|-"  `q \vee (`j \vee `v)
  \using (I \vee)
  \endprooftree
  \quad %
  %------
  \prooftree
  `x, `j \vee `q "|-" `j \vee `q%
  \quad % 
  \prooftree
  \prooftree
  `x, `j \vee `q, `j "|-" `j 
  \justifies  `x, `j \vee `q, `j "|-" `j \vee `v
  \using (I \vee)
  \endprooftree
  \justifies  `x, `j \vee `q, `j "|-" `q \vee (`j \vee `v)
  \using (I \vee)
  \endprooftree
  \quad % 
  \prooftree
  `x, `j \vee `q, `q "|-" `q 
  \justifies `x, `j \vee `q, `q "|-" `q \vee (`j \vee `v)
  \using (I \vee)
  \endprooftree
  \justifies  `x, `j \vee `q "|-" `q \vee (`j \vee `v)
  \using (E \vee)
  \endprooftree
  %------
  \justifies `x"|-" `q \vee (`j \vee `v)
  \using (E \vee)
  \endprooftree
  \justifies "|-"`x"=>" `q \vee (`j \vee `v)
 \using (MP)
  \endprooftree
\end{displaymath}
\end{footnotesize}

\section*{Exercice 3}
\begin{enumerate}
\item Il y a deux preuves
  \begin{displaymath}
    \prooftree
    `[] (`v "=>" `j) \qquad
    \prooftree    %-
    `[] `v \qquad 
    \prooftree   %--
    \justifies `[] `v "=>" `[] (`v "=>" `j) "=>" `[] `j
    \using (Distribution)
    \endprooftree %--
    \justifies `[] (`v "=>" `j) "=>" `[] `j
    \using (MP)
    \endprooftree %-
    \justifies `[] `j
    \using (MP)
    \endprooftree
  \end{displaymath}

  \begin{displaymath}
    \prooftree 
    \prooftree    %-
     \prooftree    %--
     `[] `v 
     \justifies `v 
     \using (Generalisation)
    \endprooftree %--
        \qquad 
     \prooftree    %--
     `[] (`v "=>" `j)
     \justifies `v  "=>" `j
     \using (Generalisation)
    \endprooftree %--
    \justifies `j
    \using (MP)
    \endprooftree %-
     \justifies `[] `j
     \using (Generalisation)
    \endprooftree
  \end{displaymath}

\item On a tout d'abord
  \begin{small}
  \begin{displaymath}
    \prooftree
    `[] (`v \wedge `j) "=>" `[] `j
    \qquad 
    \prooftree
    `[] (`v \wedge `j) "=>" `[] `v \qquad
    \prooftree
    \justifies
    (`[] (`v \wedge `j) "=>" `[] `v)  "=>" (`[] (`v \wedge `j) "=>" `[] `j) "=>"
    `[] (`v \wedge `j) "=>" `[] `v \wedge `[] `j
    \using (Classique)
    \endprooftree
    \justifies (`[] (`v \wedge `j) "=>" `[] `j) "=>" `[] (`v \wedge `j) "=>" `[] `v \wedge `[] `j
    \endprooftree
    \justifies `[] (`v \wedge `j) "=>" `[] `v \wedge `[] `j
    \using (MP)
    \endprooftree
  \end{displaymath}
\end{small}
On peut justifier $`[] (`v \wedge `j) "=>" `[] `v$ par l'arbre de preuve
\begin{scriptsize}
\begin{displaymath}
  \prooftree 
  \prooftree %-
  (`v \wedge `j) "=>" `v
  \justifies `[]((`v \wedge `j) "=>" `v)  
  \endprooftree %-
  \qquad %
  \prooftree %-
  `[] (`v \wedge `j) "=>" `[]((`v \wedge `j) "=>" `v) "=>" `[] `v
  \qquad
  (`[] (`v \wedge `j) "=>" `[]((`v \wedge `j) "=>" `v) "=>" `[] `v) "=>"
  `[]((`v \wedge `j) "=>" `v) "=>" `[] (`v \wedge `j) "=>" `[] `v
  \justifies `[]((`v \wedge `j) "=>" `v) "=>" `[] (`v \wedge `j) "=>" `[] `v
  \endprooftree %-
   \justifies `[] (`v \wedge `j) "=>" `[] `v
  \endprooftree
\end{displaymath}
\end{scriptsize}
où les feuilles sont, quant à elles, justifiées par $(Classique)$, $(Distribution)$ et $(Classique)$.  De son côté,
$`[](`v \wedge `j) "=>" `[]`j$ a quasiment le même arbre de preuve.

\item La règle de forçage $\force$ est définie par les quatre
  définitions classiques.


\begin{enumerate}
\item Si $`v$ est une $variable$ $p$:
 $\M,u \force `v$\qquad ssi\qquad $u \in\IM(p)$,

\item Si $`v$ est une $conjonction$ $\psi \wedge \theta$
 $\M,u \force `v$\qquad ssi\qquad $\M,u \force
   \psi$\quad et\quad $\M,u \force \theta$,

\item Si $`v$ est une $disjonction$ $\psi \vee \theta$
 $\M,u \force `v$\qquad ssi\qquad $\M,u \force
   \psi$\quad ou\quad $\M,u \force \theta$,

\item Si  $\bot$ est l'$absurde$, alors $\M,u \notforce \bot$,
\end{enumerate}

auxquelles on ajoute les deux définitions qui changent:
\begin{enumerate}
\item Si $`v$ est une $implication$ $\psi \Rightarrow \theta$ $\M,u
  \force `v$ ssi $\M,u \force \psi$ implique $\M,u \force \theta$
  (comme suggéré oralement),
  
\item Si $`v$ est l'application d'une modalité $`[]`j$: $\M,u \force
  `v$ ssi~\footnote{On aurait pu prendre $`[]`j$: $\M,u \force `v$ ssi
    $`j$: $\M,u \force `v$, mais ça n'aurait pas été vraiment dans
    l'esprit de l'exercice.} pour tout $v\ge_M u, \M,v \force `j$.
\end{enumerate}
On remarque qu'avec les définitions ci-dessus, la relation
$\force_\M$ n'est pas monotone, car l'ensemble $\{u \in \UM ~|~ u
\force_\M `j "=>" `q\}$ n'est pas «forcément» dirigé.  Par exemple si
$\UM = \{u_0,u_1,u_2\}$ avec $u_0 \le_\M u_1 \le_M u_2$ et si $\IM(p)
= \{u_1,u_2\}$ et $\IM(q) = \{u_2\}$ on a $u_0\force_\M p "=>"q$, puis
$u_1\notforce p "=>"q$ et $u_2\force_\M p "=>"q$, autrement dit $\{u \in
\UM ~|~ u \force_\M p "=>" q\} = \{u_0,u_2\}$.  C'est toute la différence
entre l'interprétation de la logique classique et l'interprétation de
la logique intuitionniste.

On définit $\M "|=" `v$ si pour tout $u\in \UM$ on a $u\force_\M `v$
et on définit $"|=" `v$ si pour tout modèle $\M$ on a $\M "|=" `v$.
Finalement cela signifie que $"|=" `v$ si pour tout modèle $\M$ et
pour tout $u\in \UM$ on a $u\force_\M `v$. Il faut vérifier pour
chaque règle si les affirmations de la partie supérieure où on
remplace $"|-"$ par $"|="$ sont satisfaites, l'affirmation de la
partie inférieure où on remplace $"|-"$ par $"|="$ est satisfaite.

\begin{itemize}
\item Pour la règle $(Classique)$\footnote{Ce raisonnement n'aurait
    pas fonctionné avec l'interprétation «habituelle» de $"=>"$.}, si
  $`v$ est un théorème classique alors pour tout modèle $\M$ et pour
  tout $u\in \UM$ on a $u\force_\M `v$ et donc par définition même
  $u\force_\M `v$.
   
\item Pour la règle $(MP)$, si $"|=" `v$ et si $"|="`v"=>"`j$ cela
  signifie que pour tout modèle $\M$ et pour tout $u\in \UM$ on a
  $u\force `v$ et $u\force`v"=>"`j$ donc $u\force `j$, ce qui implique
  par définition que $"|=" `j$.
  
\item Pour la règle $(Generalisation)$, si $"|=" `v$ cela signifie que
  pour tout modèle $\M$ et pour tout $u\in \UM$ on a $u\force `v$,
  donc pour tout $u\in \UM$ et pour tout $u \le v$ on $v\force `v$,
  donc $u\force`[]`v$ et donc $"|="`[]`v$.
\item Pour la règle $(Distribution)$, il faut vérifier que quand on a
  $v\force `v$ pour tout $v\ge u$, quand on a $v'\force `v "=>"`j$ pour
  $v'\ge u$, on a alors $v''\force `j$ pour tout $v''\ge u$, ce qui
  semble aller de soi.
\item Pour la règle $(T)$, il faut vérifier que quand on a $v\force
  `v$ pour tout $v\ge u$, on a $u\force `v$, ce qui est une
  conséquence de la réflexivité de $\ge$.
\end{itemize}

\item L'opérateur $"->"$ correspond à l'implication intuitionniste,
  car on voit que dans les modèles de Kripke, il satisfait: 
  \begin{itemize}
  \item Si $`v$ est $`j"->"`q$ autrement dit $`[](`j"=>"`q)$: $\M,u
    \force `v$ ssi pour tout $v\ge_M u, \M,v \force `j"=>"`q$
    c'est-à-dire si $\M,v \force `j$ alors $\M,v \force `q$.
  \end{itemize}
\end{enumerate}
\end{document}
