%% Time-stamp: <version du Thu 26 Oct 2000 à 20h26 par Pierre Lescanne>
%\documentclass[%
 % slidesonly,%  Pour sortir les transparents seuls
 % semrot,%      Permettre des rotations eventuelles
 % semhelv,%    Helvetica
 % a4%           A4 paper
 % ]{seminar}
\documentclass{article}
\usepackage{fullpage}
\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
%\usepackage[all]{xy}

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


\title{\rouge{\textit{La logique propositionnelle}}\\
      \rouge{\textit{(deduction naturelle)}}}

\author{}

\date{}

\title{Logique Propositionnelle}
% \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{\ra}{\ensuremath{\rightarrow}}
\newcommand{\RaE}{\VERT{\Ra E}}
\newcommand{\RaI}{\VERT{\Ra I}}
\newcommand{\et}{\mathop{\&}}
 \newcommand{\infer}[2]{
 \begin{array}{c}
   #1\\
   \hline \noalign{\vskip 1pt}#2
  \end{array}}
\newcommand{\inferThreeLabel}[5]{\bl{
\begin{array}{cc}
 {\VERT{#1}} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\hspace{2em} #4\\
   \hline \noalign{\vskip 1pt}#5
  \end{array}
\end{array}}}

\newcommand{\inferTwoLabel}[4]{\bl{
\begin{array}{cc}
 {\VERT{#1}} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}
\end{array}}}

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

\newcommand{\inferLabel}[3]{\bl{
    \begin{array}{cc}
    {\VERT{#1}} \quad
    \begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \end{array}
  \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}
\maketitle

\section{Déduction naturelle}
En \rouge{déduction naturelle}, on raisonne avec des hypothèses.  

Au lieu du jugement \bleu{\vdash p}, on utilise le jugement
\bleu{\Gamma \vdash p} où 
\begin{itemize}
\item \bleu{\Gamma} est un \rouge{ensemble de propositions} qui sont
  les hypothèses ou \rouge{antécédent}.
\item On écrit \bleu{\Gamma, p \vdash q} au lieu de \bleu{\Gamma \cup
    \{p\} \vdash q}\\ \hspace*{30pt} et \bleu{\vdash p} quand
  l'ensemble des hypothèses est vide.
\item \bleu{\Gamma \vdash p} se lit 
  \begin{itemize}
  \item ``\rouge{de \bleu{\Gamma} on déduit \bleu{p}}'' 
  \item ou ``\bleu{\Gamma} \rouge{infère}
    \bleu{p}'' 
  \item ou ``\rouge{sous les hypothèses \bleu{\Gamma} on a \bleu{p}}''.
  \end{itemize}
\end{itemize}

%------------------------------------------------------
\section{Les théorèmes}

Les théorèmes sont les jugements de la forme \bleu{\vdash p} qui
peuvent être déduits des axiomes et des règles.

On les trouvent donc à la \rouge{racine} d'un arbre de preuve.

%------------------------------------------------------

%------------------------------------------------------

\section{Logique propositionnelle minimale}

\subsection{L'axiome de la logique propositionnelle minimale}
Il n'y a qu'un seul axiome, 

\[\bl{\Gamma, p \vdash p} \]


%------------------------------------------------------

\subsection{Les règles de la logique propositionnelle minimale}
Il y a deux règles : \rouge{introduction} et \rouge{élimination} :

$\inferLabel{\Ra I}{\Gamma, p \vdash q}{\Gamma\vdash p\Ra q}$

$\inferTwoLabel{\Ra E}{\Gamma\vdash p\Ra q}{\Gamma\vdash p}{\Gamma\vdash q}$


%------------------------------------------------------

\subsection{Preuve de K}

\begin{center}
  \bl{ $\inferLabel{\RaE} {\inferLabel{\RaE} {p, q \vdash p} {p\vdash
        q \Ra p}} {\vdash p \Ra q \Ra p}$ }
\end{center}


%------------------------------------------------------
%\begin{slide}
%\heading{COQ}
%Le système COQ est fondé sur un système proche de la déduction naturelle.

%On utilise directement le système de preuve sous-jacent à COQ. 

%On écrit \bleu{p \ra q} au lieu de \bleu{p \Ra q} et on travaille
%directement dans \bleu{Prop}.

%Par la commande \bl{Intro} sur une \bleu{Prop} de la forme \bleu{p\ra
%  q}, on invoque la commande \RaI.

%\end{slide}
%------------------------------------------------------

\subsection{Exercice}

\vspace{20pt}
\begin{enumerate}
\item Prouver \bleu{Hilbert\_S}.
\item   Prouver \bleu{B: (p \Ra q) \Ra (r \Ra p) \Ra r \Ra q}.
\end{enumerate}

%------------------------------------------------------

\section{La logique propositionnelle}


\subsection{Les règles}
Les règles sont deux types :
\begin{itemize}
\item \rouge{règles d'introduction} : un connecteur qui n'était pas
  présent apparaît dans la proposition conséquente sous la barre
  d'inférence.
\item \rouge{règles d'élimination} : la proposition conséquente sous la barre
  d'inférence est construite en enlevant le connecteur principal d'un 
  des connecteurs conséquents d'un jugement au dessus de la barre.
\end{itemize}

\subsection{La syntaxe}
Il y a trois nouveaux connecteurs \bleu{\perp}, \bleu{\&} et \bleu{\vee}.

\begin{itemize}
\item \bleu{\perp} est unaire et représente l'absurde,

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


\subsection{L'axiome pour \bleu{\perp}}
Il n'y a qu'une règle et c'est \rouge{une règle d'élimination:}
\begin{center}
  $\inferLabel{\perp E}{\Gamma \vdash \perp}{\Gamma\vdash p}$
\end{center}

\subsection{Les règles du \bleu{\et}}

Il y a \rouge{ une règle d'introduction} et \rouge{deux règles d'élimination.}

\begin{center}
  $\inferTwoLabel{\et I}{\Gamma\vdash p}{\Gamma\vdash q} {\Gamma\vdash
    p \et q}$
\end{center}
\begin{center}
$\inferLabel{\et E_g}{\Gamma \vdash p\et q}{\Gamma\vdash p}$
\hfill
$\inferLabel{\et E_d}{\Gamma \vdash p \et q}{\Gamma\vdash q}$
\end{center}
\subsection{Les règles du \bleu{\vee}}

Il y a \rouge{deux règles d'introduction} et \rouge{une règle d'élimination}.
\begin{center}
$\inferLabel{\vee I_g}{\Gamma \vdash p}{\Gamma\vdash p\vee q}$
\hfill
$\inferLabel{\vee I_d}{\Gamma \vdash q}{\Gamma\vdash p\vee q}$
\end{center}

\begin{center}
  $\inferThreeLabel{\vee E} {\Gamma\vdash p\vee q}{\Gamma, p\vdash
    r}{\Gamma, q\vdash r} {\Gamma\vdash r}$
\end{center}

\end{document}
% LocalWords:  green Prop Intro