%% Time-stamp: <version du Thu 26 Oct 2000 à 08h10 par Pierre Lescanne>
%% /MIM-1/LOGIQUE/00-01/COURS+TRANSP/HILBERT/transp.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

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

\def\printlandscape{\special{landscape}}     % pour sortir en landscape
\slidesmag{5}


\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}

%% 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


\articlemag{1}

\rotateheaderstrue       % si tu combines slide et slide*

\title{\color{red}{\textit{Introduction à la Logique}}}

\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}}
\newcommand{\Ra}{\ensuremath{\Rightarrow}}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\inferTwoLabel}[4]{\bl{
 {#1} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}}}

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

\newcommand{\inferLabel}[3]{\bl{
    {#1} \quad 
    \begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \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{Quels sont les buts de la logique ?}
\begin{itemize}
\item Pour \rouge{tous}
  
\item Pour les 
  \rouge{mathématiciens}
  
\item Pour les 
  \rouge{informaticiens}
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quels sont les buts de la logique ?}
\VERT{Pour tous}

\begin{itemize}
  
\item \rouge{Comprendre} la nature intime du \bl{raisonnement mathématique}
  \footnote{et du raisonnement non mathématique !}
 
\item Faire du ``raisonnement'' une \rouge{théorie mathématique}
  comme les autres.

\item Donner un sens précis à ce que peut-être le \rouge{vrai}\\
\hspace*{30pt}  dès qu'il s'agit de raisonnement et d'argumentation.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quels sont les buts de la logique ?}
\VERT{Pour les mathématiciens}
\begin{itemize}
\item S'assurer (se convaincre ?) que les mathématiques sont \rouge{exemptes
  de contradictions} et de paradoxes.

\item \rouge{Apprendre} une branche des mathématiques.

\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quels sont les buts de la logique ?}
\VERT{Pour les informaticiens}

\begin{itemize}

\item \rouge{Mécaniser} les processus de raisonnement.

\item \rouge{Exhiber les liens} entre \emph{démonstrations} et \emph{calculs}.


\item \rouge{Formaliser} les objets informatiques.
 
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Ce que la logique n'est pas}
\VERT{Point de vue personnel}
\begin{itemize}
\item Le \rouge{fondement ultime} auquel se réduisent les
  mathématiques, (point de vue réductionniste)
\item La discipline qui va faire \rouge{remplacer les humains} (en
  général) et les mathématiciens (en particulier) par des machines
  (point de vue mécaniste).
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{La logique, une théorie mathématique}
 
 \VERT{La logique est une théorie mathématique}\footnote{comme les
   autres !},
\begin{itemize}
\item elle \rouge{utilise les mathématiques} comme le font les autres branches 
  des mathématiques,
\item elle \rouge{étudie des sortes particuliers d'objets mathématiques} : les
  propositions, les théorèmes, les jugements, les démonstrations, etc.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un peu d'histoire}

 
L'histoire montre que \VERT{tout ce qui est susceptible de se
  mathématiser se mathématise.}


Au début, seuls les \rouge{entiers} sont des êtres mathématiques.

Puis les Anciens acceptent les \rouge{rationnels} et les \rouge{relatifs}.  

A la Renaissance, les \rouge{complexes} (ou imaginaires) deviennent eux-aussi
des êtres mathématiques.

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un peu d'histoire} 
 
  Au dix-neuf siècle 
  \begin{itemize}
  \item les \rouge{réels} (Dedekind), 
  \item puis les \rouge{fonctions} (en
    ``extension'') 
  \item et les \rouge{ensembles} (Cantor) deviennent des
    êtres mathématiques.
\end{itemize}  
Au début vingtième siècle, les \rouge{fonctions} (en ``intention'')
(Church et Curry) et les \rouge{théorèmes} (Boole, Frege etc.)
deviennent des êtres mathématiques.
  
Aujourd'hui (1980), les \rouge{démonstrations} (Curry et Howard)
deviennent des êtres mathématiques.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Mécaniser la logique ?}

Deux positions  s'affrontent.

\begin{description}
\item[\rouge{Le mathématicien ne sera jamais battu par une machine}]~\\ 
\VERT{Alain Connes} (le triangle de la pensée)
\item[\rouge{Il existe un théorème qui ne peut être prouvé que par un
  ordinateur}]~\\[-2pt]\VERT{Veroff and McCune}

Les algèbres de Boole peuvent être axiomatisées par le seul axiome
\[\bl{
((x \sh z) \sh y) \sh ((x \sh (x \sh y)) \sh x) = y
}\]

\end{description}
\end{slide}
%------------------------------------------------------
\begin{slide}
où est \bleu{|} est le symbole de Sheffer qui peut être interprété
comme
\bl{
\begin{eqnarray*}
x \sh y &=& \bar{x} \et \bar{y}.
\end{eqnarray*}
}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les deux niveaux de la logique}

En logique, il y a deux niveaux qui interfèrent et qu'il ne
faut pas confondre.

\begin{itemize}
\item La \rouge{théorie}, (on dit aussi parfois la \rouge{théorie objet}, si
  l'on veut être plus précis).  
  
\item La \rouge{méta-théorie}, c'est une mathématique dans laquelle on
  va raisonner sur l'objet.   C'est aussi un système logique !
  
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les deux niveaux de la logique}
  
Le \rouge{théorie objet} est l'objet logique que l'on étudie et que l'on
souhaite donc formaliser.

\vspace*{12pt}

En général, on accepte dans la \rouge{méta-théorie} toute la puissance du
raisonnement traditionnel.  Si elle est mécanisée, cela peut-être par
un système formel plus ou moins puissant.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les deux niveaux de la logique} 
  
  Dans la méta-théorie, on prouve des \VERT{méta-théorèmes}, c-à-d des
  théorèmes à propos de la théorie objet.

Quelques méta-théorèmes courants sont:
\begin{itemize}
\item la \rouge{correction},
\item la \rouge{cohérence},
\item la \rouge{complétude}.
\end{itemize}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les ingrédients de la logique}
\bl{Les aspects preuves}

En logique on trouve :
\begin{itemize}
\item un \rouge{langage} d'expressions bien formées : les
  \VERT{propositions} (construites avec des \emph{connecteurs}),
  les \VERT{jugements}, etc. \\
On dit aussi que c'est la \emph{syntaxe}.
\item des \rouge{axiomes},
\item des \rouge{règles}.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les ingrédients de la logique}

Les \rouge{axiomes} affirment que \VERT{certaines propositions sont des
  théorèmes}: on définit un prédicat unaire dans la méta-théorie.

Les \rouge{règles} montrent comment \VERT{construire des théorèmes à
  partir d'autres théorèmes}.  On définit dans la méta-théorie, 
\begin{itemize}
\item des fonctions des propositions vers les propositions (règles
  monadiques) 
\item ou des fonctions des couples de propositions vers les propositions
  (règles dyadiques)
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les ingrédients de la logique}
Le but des axiomes et des règles est de former des expressions
particulières, les \rouge{théorèmes} en construisant des objets
mathématiques particuliers les \rouge{démonstrations} (ou
\rouge{preuves}).

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les ingrédients de la logique}

Il y a différentes sortes d'objets: \VERT{propositions}\footnote{qui
  ne sont pas théorèmes}, \VERT{théorèmes}, etc.

Dans une logique, l'appartenance d'un objet à telle ou telle sorte se
décrète par un \rouge{jugement}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Syntaxe concrète et syntaxe abstraite}

Un \bl{ordinateur} a besoin qu'on lui parle de la syntaxe à un bas
niveau, c'est la \rouge{syntaxe concrète}, c-à-d les \VERT{virgules},
les \VERT{parenthèses}, les \VERT{retours à la ligne}, etc.

Un \bl{humain} préfère une syntaxe lisible et flexible, il a besoin de
la \rouge{syntaxe abstraite}, c-à-d plutôt la structure arborescente,
donc il souhaite des \VERT{opérateurs infixes},
l'\VERT{associativité}.

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les ingrédients de la logique}
\bl{Les aspects modèles}

On interprète le langage dans un univers mathématique particulier: les 
\rouge{modèles}.   On parle aussi de \rouge{sémantique}.

Les propositions qui sont ``satisfaites'' (dans un sens à préciser) par le
modèle sont dites \rouge{valides}.

Correction, cohérence et complétude établissent des \rouge{liens} entre 
\begin{itemize}
\item les \VERT{théorèmes} (propositions prouvables)
\item  et les \VERT{tautologies} (propositions valides),
\end{itemize}
c'est-à-dire entre la prouvabilité et la validité.

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les deux branches de la logique}

La partie de la logique où l'on s'intéresse plutôt aux démonstrations
s'appelle la la \rouge{théorie de la démonstration} ou théorie de la preuve
(proof theory).

La partie de la logique où l'on s'intéresse plutôt à la validité
s'appelle la \rouge{théorie des modèles}.

\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{red}{\textit{L'organisation du cours}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Deux enseignants} 

\begin{itemize}
\item \emph{Odile Millet-Botta},

\item \emph{Pierre Lescanne}.
\end{itemize}
qui feront cours et TD.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Odile Millet-Botta}
\begin{itemize}
\item La \rouge{logique classique} et les \rouge{modèles} de la logique classique,

\item Le \rouge{calcul des prédicats}, (la logique avec quantificateurs),

\item Le \rouge{calcul des séquents}
\item \rouge{\textsc{Prolog}}
\item La \rouge{théorie des ensembles}.
\end{itemize}
 
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Pierre Lescanne}
\begin{itemize}
\item La logique \rouge{intuitionniste},

\item Le lien avec le calcul : le \rouge{lambda calcul},

\item Les \rouge{modèles} de la logique de la logique intuitionniste,

\item D'autres logiques : \rouge{logique modale}, \rouge{logique épistémique} (ou
  logique de la connaissance).
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Bibliographie}

Un \rouge{livre de base} :

\begin{quote}
  R.~Lalement.  \bl{ Logique, Réduction, Résolution}.  Études et
  recherches en informatique. Masson, Paris, 1990.
\end{quote}


Ma \rouge{référence} :

  \begin{quote}
  D.~van Dalen.  \bl{ Logic and Structure}.  Springer Verlag, 1994.
\end{quote}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Bibliographie (suite)}

Un livre assez complet sur la logique de l'informatique en
\rouge{français} :
  \begin{quote}
  P.~Gochet, P.~Gribomont. \bl{Logique. Volume 1 : méthodes pour
    l'informatique fondamentale}, HERMES, 1990
\end{quote}

Sur la logique \rouge{épistémique} :

 \begin{quote}
  R.~Fagin, Y.~Halpern, Y.~Moses, and M.~Y.  Vardi.  \bl{ Reasoning
  about Knowledge}.  The MIT Press, 1995.
\end{quote}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{red}{\textit{La logique propositionnelle}}}
          
    {\Large \bf \color{red}{\textit{(approche à la Hilbert)}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{green}{\textit{La logique propositionnelle minimale}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La syntaxe}

Il n'y a qu'un \rouge{connecteur} \bleu{\Ra} \\
\hspace*{30pt}et des \rouge{variables propositionnelles} \bleu{p},
\bleu{q}, ..., \bleu{p_1}, \bleu{p_2}, ...

Par exemple, les expressions sont \bleu{p}, \bleu{p\Ra q}, \bleu{(p\Ra q) \Ra p}.

On adopte la convention d'\rouge{associativité à droite} à savoir que
\bl{\[p_1 \Ra (p_2 \Ra ... \Ra(p_{n-1} \Ra p_n)...))\]}
s'écrit
\bl{\[p_1 \Ra p_2 \Ra ... \Ra p_{n-1} \Ra p_n\]}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La méta-théorie} 
  
  Je choisis comme une méta-théorie, un système logique très
  puissant~: le \rouge{Calcul des Constructions Inductifs}, mécanisé
  dans l'\VERT{assistant de preuve} \rouge{COQ}.
  
  A la fin du cours, on aura une meilleure idée de ce qu'est le Calcul
  des Constructions Inductifs

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un peu de ``méta syntaxe''} 
  
\bleu{(p,q :proposition)} signifie ``pour tout \bleu{p} et tout
\bleu{q} qui sont des \rouge{propositions}''

\bleu{Inductive} signifie que l'on définit un concept : 
\VERT{proposition}, \VERT{theorem} par induction.

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le jugement \emph{theorem}} 
  
  En COQ, le \rouge{jugement} \emph{theorem} appliqué à \bleu{p} se note
  \bleu{(theorem ~p)}.

Nous le noterons \bleu{\vdash p} qui signifie que ``\bleu{p} est un
théorème''.

On omet \bleu{\vdash} dans les règles.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Une règle} 
  
  En logique propositionnelle minimale, il n'y a qu'une règle :\\ 
  \hspace*{30pt}le \rouge{Modus Ponens}~:

\[\inferTwoLabel{MP}{p\Ra q}{p}{q}\]
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le Modus Ponens}
En COQ, MP est une fonction 
\[\bl{(theorem~p\Ra q) \rightarrow (theorem~p) \rightarrow
  (theorem~q)}\] qui prend un objet du type \bleu{theorem~p\Ra q} où
\bleu{p\Ra q} est une proposition
et un objet du type \bleu{theorem~p} où \bleu{p} est une proposition
et fournit un objet du type \bleu{theorem~q}.

Plus précisément, c'est une fonction qui prend quelque chose du type
\bleu{p\Ra q} et rend une fonction qui à quelque chose de type
\bleu{p} associe quelque chose de type \bleu{q}.  \vfill

\VERT{Mais c'est à peu près la même chose, à une curryfication prés!}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Deux axiomes}
Il y a deux axiomes appelés \bleu{K} et \bleu{S}:

\rouge{\hrulefill}\\
$\leafLabel{\VERT{K}:}{\vdash p \Ra q \Ra p}$\\
\rouge{\hrulefill}

et

\rouge{\hrulefill}\\
$\leafLabel{\VERT{S}:}{\vdash (p \Ra q \Ra r) \Ra (p \Ra q) \Ra p \Ra r}$\\
\rouge{\hrulefill}

\VERT{Ne me demandez pas pour l'instant pourquoi ils s'appellent
  \bleu{K} et \bleu{S}~!}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice}

\vspace{20pt}

Prouver  le lemme \bleu{B: (p \Ra q) \Ra (r \Ra p) \Ra r \Ra q)}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Une règle dérivée : la règle C}

Notre but est de prouver une nouvelle règle applicable qui va nous
simplifier la vie: 

\[\inferLabel{rule\_{C}}{p \Ra q \Ra r}{q \Ra p \Ra r}\]


\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice}

\vspace{20pt}

Prouver,  en utilisant le lemme \bleu{B}, le lemme (la règle dérivée)

\[\bl{L: (theorem~q \Ra r) \rightarrow (theorem~p \Ra q) \rightarrow (theorem~p \Ra r)}.\]

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La règle Cut}

La règle \rouge{Cut} ou \rouge{règle de coupure} permet d'utiliser des
théorèmes intermédiaires (des lemmes!) ici \bleu{q}.

\[\inferTwoLabel{rule\_{Cut}}{q \Ra r}{p \Ra q }{p\Ra r}\]

\vfill

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le modèle \{0, 1\}}

Une formule est \rouge{valide classiquement} si elle prend la valeur
\bleu{1} pour l'interprétation de \bleu{\Ra} suivante :
\bl{
\begin{center}
\begin{math}
\begin{array}{c || c | c}
\Ra & 0 & 1\\
\hline\hline
0 & 1 & 1\\
\hline
1 & 0 & 1 
\end{array}
\end{math}
\end{center}
}
et quelles que soient les valeurs prises par les variables
propositionnelles.

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice}

\begin{enumerate}
\item Montrer que les axiomes $Hilbert_K$ et $Hilbert_S$ sont valides
  classiquement.
  
\item Montrer que la règle MP ``préserve'' les propositions valides
  classiquement. 
  
  En déduire que tous les théorèmes sont valides classiquement.
\item Montrer que la \rouge{formule de Pierce} \bleu{((p\Ra q) \Ra p)
    \Ra p} est valide classiquement.
  \end{enumerate}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Incomplétude}
\VERT{La formule de Pierce n'est pas un théorème de la logique minimale.}

La logique minimale est \rouge{incomplète} pour le modèle \{0, 1\}.

Il faut 
\begin{itemize}
\item soit changer de logique,

\item soit changer de modèles.
\end{itemize}
On fera les deux !
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Incomplétude}
\VERT{La formule de Pierce n'est pas un théorème de la logique minimale.}

La logique minimale est \rouge{incomplète} pour le modèle \{0, 1\}.

Il faut 
\begin{itemize}
\item soit changer de logique, \VERT{logique classique}

\item soit changer de modèles, \VERT{modèles de Kripke}
\end{itemize}
On fera les deux !
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{green}{\textit{La logique propositionnelle
          intuitionniste}}}

   {\large \bf \color{green}{\textit{(approche à la Hilbert)}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La syntaxe}
Il y a deux nouveaux connecteurs \bleu{\&} et \bleu{\vee}.

\begin{itemize}
\item \bleu{\&} et \bleu{\vee} représentent la conjonction et la
  disjonction.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les axiomes pour \bleu{\&} et \bleu{\vee}}
Il y a six axiomes.
\begin{footnotesize}

\rouge{\hrulefill}

$\leafLabel{\VERT{Or0:}}
     {\vdash (p \Ra  r) \Ra  (q \Ra  r) \Ra  (p \vee q) \Ra  r}$

$\leafLabel{\VERT{Or1:}}{\vdash   p \Ra  (p \vee q)}$

$\leafLabel{\VERT{Or2:}}{\vdash    q \Ra  (p \vee q)}$\\
\rouge{\hrulefill}

$\leafLabel{\VERT{And0:}}{\vdash   p \Ra  q \Ra  (p \& q)}$

$\leafLabel{\VERT{And1:}}{\vdash   (p \& q) \Ra  p}$

$\leafLabel{\VERT{And2:}}{\vdash   (p \& q) \Ra  q}$\\
\rouge{\hrulefill}

\end{footnotesize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques conséquences}
\begin{itemize}
\item \bleu{p \vee q ~\Ra~ q \vee p}
\item \bleu{p \vee (q \vee r) ~\Ra~ (p \vee q) \vee r}
\item \bleu{p \vee p ~\Ra~ p}
\item \bleu{(p \Ra q) ~\Ra~ (p \vee r) ~\Ra~ (q \vee r)}
\item \bleu{p \et q ~\Ra~ q \et p}
\item \bleu{p \et (q \et r) ~\Ra~ (p \et q) \et r}
\item \bleu{p \et p ~\Ra~ p}
\item \bleu{(p \Ra q) ~\Ra~ p \et r ~\Ra~ q \et r}
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques conséquences (suite)}
\begin{itemize}
\item \bleu{(p \et q) \vee (p \et r) ~\Ra~ p \et (q \vee r)}
\item \bleu{p \et (q \vee r) ~\Ra~ (p \et q) \vee (p \et r))}
\item \bleu{(p \vee q) \et (p \vee r) ~\Ra~ p \vee (q \et r)}
\item \bleu{p \vee (q \et r) ~\Ra~ (p \vee q) \et (p \vee r)}
\end{itemize}
Et des règles:

$\inferTwoLabel{}{p}{q}{p\et q}$ $\inferTwoLabel{}{p\Ra q}{p\Ra r}{p\Ra
  q\et r}$ $\inferTwoLabel{}{p1 \Ra q1}{p2 \Ra q2}{p1 \et p2 ~\Ra~ q1 \et q2}$

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le connecteur False}
Le connecteur \bleu{False} est régi par l'axiome :

\rouge{\hrulefill}

$\leafLabel{\VERT{F:}}{\vdash   False \Ra  p}$

\rouge{\hrulefill}

La négation est \bleu{\neg p \mathop{\VERT{\equiv}} p \Ra False}.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Réduire les connecteurs ?}
En logique intuitionniste, \rouge{on ne peut pas réduire les connecteurs} les
uns par rapport aux autres.

Chaque connecteur a sa vie propre.

Il faut donc des axiomes spécifiques pour chaque connecteur (voir
exercice ... dans le livre de van Dalen).

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La logique intuitionniste et la logique classique}
En logique intuitionniste les formules suivantes ne sont pas des
théorèmes.
\begin{itemize}
\item \bleu{\neg \neg p \Ra p}
\item \bleu{p \vee \neg p}
\item \bleu{(\neg p \Ra \neg q) \Ra q \Ra p} 
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le tiers exclus}
Le \rouge{tiers exclus} est la proposition \bleu{p \vee \neg p}.

En informatique, considérons la proposition \bleu{Null} à savoir\\
\hspace*{30pt}\VERT{``La variable \bleu{x} est nulle''}\footnote{On
  devrait préciser \VERT{``La variable \bleu{x} vaut  \rouge{toujours} zéro''}}.

Sa négation est \VERT{``La variable \bleu{x} n'est pas
  nulle''}\footnote{\VERT{``La variable \bleu{x} ne vaut
    \rouge{jamais} zéro''}}.

A-t-on \bleu{Null \vee \neg Null} ?

A-t-on une seule manière d'interpréter la négation ?

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La logique intuitionniste et les preuves}
En logique intuitionniste les preuves sont des \rouge{citoyens de première
classe}.

Une proposition est un théorème si on peut en exhiber une preuve.

Ainsi 
\begin{itemize}
\item d'une preuve de \bleu{\neg{\neg{p}}} on ne peut pas extraire une
  preuve de \bleu{p}.
\item on ne peut pas construire une preuve de \bleu{p \vee \neg{p}},
  car cet objet est construit à partir d'une preuve de \bleu{p} ou
  d'une preuve de \bleu{\neg{p}} \footnote{qu'on ne possède pas quand
    on affirme \bleu{p \vee \neg{p}}}.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  C'est comme construire une maison sur un terrain situé 
  
  \centerline{à Vaise \rouge{ou} à Vénissieux !}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La logique intuitionniste et les preuves}

\VERT{Retournons à \bleu{MP}.}

En fait, dans
\[\bl{(theorem~p\Ra q) \rightarrow (theorem~p) \rightarrow
  (theorem~q)}\] 
\bleu{MP} prend une preuve de \bleu{p\Ra q} et
retourne une fonction qui prend une preuve de \bleu{p} et retourne une
preuve de \bleu{q}.

Donc \bleu {(theorem~p\Ra q)} représente le \rouge{type}~\footnote{plutôt que
l'ensemble} des preuves de \bleu{p\Ra q}.

\end{slide}
%------------------------------------------------------
\end{document}
% LocalWords:  theorem Cut Ponens Dedekind Cantor Boole Frege proof theory red
% LocalWords:  Millet-Botta TD green Pierce Lalement Dalen Logic Springer Fagin
% LocalWords:  Verlag Gochet Gribomont HERMES Halpern Moses Vardi Reasoning The
% LocalWords:  about Knowledge Press MP Church Howard réductionniste Connes pt
% LocalWords:  Veroff McCune Sheffer False Null Vaise Bron
