%% Time-stamp: <modifié par Pierre Lescanne le  5 Sep 2002 à 11h55>
%% /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}
\usepackage{prooftree}

%% 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{}   
%--- couleurs ----
\definecolor{mauve}{rgb}{1,0,1}
\definecolor{cyanp}{rgb}{0,1,1}
\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{\ali}{\newline\hspace*{20pt}}
\newcommand{\Ra}{\ensuremath{\Rightarrow}}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}

\newcommand{\inferTwo}[3]{\bl{
 \begin{array}{c}
   #1 \hspace{2em} #2\\
   \hline \noalign{\vskip 1pt}#3
  \end{array}}}

\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]{%
{\color{cyanp}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}
    
%\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}
\vfill
\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 (philosophique, judiciaire)!}
 
\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}
\vfill
\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}
\vfill
\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 \bl{démonstrations} et \bl{calculs}.


\item \rouge{Formaliser} les objets informatiques,
  \begin{itemize}
  \item pour la sûreté (par exemple, la ligne 14 du métro parisien),
  \item et le sécurité.
  \end{itemize}
 
\end{itemize}
\vfill
\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)
  
  Des réductions sont possibles et utiles et la logique peut aider à
  en faire, %
  \ali mais il n'y pas de réduction ultime.

\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}
\vfill
\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 particulières d'objets mathématiques} : les
  propositions, les théorèmes, les jugements, les démonstrations, etc.
\end{itemize}
\vfill
\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.

\vfill
\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 du 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.
\vfill
\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}] \VERT{Veroff and McCune} :
Les algèbres de Boole peuvent être axiomatisées par l'axiome
\ali\bleu{
((x \sh z) \sh y) \sh ((x \sh (x \sh y)) \sh x) = y
}\\
\begin{footnotesize}
  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{footnotesize}
\end{description}
\vfill
\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}] \VERT{Veroff and McCune} :
Les algèbres de Boole peuvent être axiomatisées par l'axiome
\ali\bleu{
((x \sh z) \sh y) \sh ((x \sh (x \sh y)) \sh x) = y
}\\
\begin{footnotesize}
  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*}
}

{\color{mauve}Est-ce un théorème profond?}
\end{footnotesize}
\end{description}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Modèles}%
  Informellement, un \rouge{modèle} est une structure mathématique dans
  laquelle toutes les \rouge{règles de déduction} et les \rouge{axiomes} sont
  «\rouge{satisfaits}».
  
  On dit qu'une formule est \rouge{valide} si elle est satisfaite dans
  tous les modèles. \vfill
\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}
\vfill
\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.
\vfill
\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}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les concepts méta-logiques}%
  \VERT{La correction} est la propriété d'un système de preuve de
  \rouge{ne prouver que} des théorèmes qui sont \rouge{des formules
    valides}.
  
  \VERT{La cohérence} est la propriété d'un système de preuve d'être
  \rouge{absent de contradiction}, on ne peut pas prouver une propriété et son
  contraire.  
  
  \VERT{La complétude} est la propriété d'un système de preuve de
  \rouge{prouver toutes les formules valides}.

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

En logique on trouve :
\begin{itemize}
\item un \rouge{langage} d'expressions bien formées : 
  \begin{itemize}
  \item[$\cdot$] les \VERT{propositions} (construites avec des
    \emph{connecteurs}),
    
  \item[$\cdot$]  les \VERT{jugements}, 
  \item[$\cdot$] etc.
\end{itemize}
On dit aussi que c'est la \rouge{syntaxe}.
\item des \rouge{règles} de déduction,
\item des \rouge{axiomes}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les ingrédients de la logique 2/7}
Les \rouge{règles de déduction} 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}

Les propositions à partir desquelles ont fait la déduction dans la
règle s'appelle les \rouge{prémisses}.  La proposition que l'on déduit
s'appelle la \rouge{conséquence}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les ingrédients de la logique 3/7}
Les \rouge{axiomes} affirment que \VERT{certaines propositions sont
  des théorèmes}: on définit le prédicat unaire «être un théorème»
dans la méta-théorie et on affirme que les axiomes sont des formules
qui satisfont ce prédicat.

N.B. Les axiomes sont en général vus comme des règles sans prémisses.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les ingrédients de la logique 4/7} %
  Le but des axiomes et des règles de déduction 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}).  
  
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les ingrédients de la logique 5/7} %
  Les \rouge{preuves} sont des \rouge{arbres} dont 
  \begin{itemize}
  \item les \rouge{noeuds} sont les règles de déduction, 
  \item les \rouge{feuilles} sont les axiomes
  \item et la \rouge{racine} est le théorème dont c'est la preuve.
\end{itemize}

\vfill

\[\prooftree 
\prooftree %
\prooftree \ldots \qquad \ldots \justifies \ldots \using \rouge{(foo_1)} %
\endprooftree %
\qquad %
\prooftree \ldots \justifies \ldots \using \rouge{(bar)}%
\endprooftree %
 \justifies %
\ldots  \using \rouge{(foo_2)} %
\endprooftree %
\qquad %
\ldots \justifies \bl{\Gamma\vdash\Delta}  \using \rouge{(foo_1)}%
\endprooftree
\]

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les ingrédients de la logique 6/7}
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é}.

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

On interprète le langage dans 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 \VERT{prouvabilité} et la \VERT{validité}.

\vfill
\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}.

\vfill
\end{slide}
%%------------------------------------------------------
%\begin{slide}
%  \begin{center}
%    {\Large \bf \color{red}{\textit{L'organisation du cours}}}
%\end{center}
%\vfill
%\end{slide}
%%------------------------------------------------------
%\begin{slide}
%\heading{Pierre Lescanne}
%\begin{itemize}
%\item La logique \rouge{intuitionniste} et la logique classique,

%\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}
%\vfill
%\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}
\vfill
\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}
\vfill
\end{slide}
\end{document}
% LocalWords:  méta-théorie méta-théorèmes méta-logiques unaire dyadiques proof
% LocalWords:  infixes prouvabilité theory red
