%% Time-stamp: <version du Tue  9 Jan 2001 à 21h14 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}

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

% \def\printlandscape{\special{landscape}}    % pour sortir en landscape
%                                             % avec dvips

% \slidesmag{5}
% \articlemag{1}

% \rotateheaderstrue       % si tu combines slide et slide*

\title{\textit{La logique propositionnelle classique}}

\author{}

\date{}

%\pagestyle{}

% \slidestyle{empty}

% \slideframe{}   

\newcommand{\vDash}{\mathbf{\mathtt{\large |\!\!\!=}}}
\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]{\bl{
 \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}
\begin{document}

\maketitle
%------------------------------------------------------

\section{En déduction naturelle}
On ajoute la règle dite de \rouge{réduction par l'absurde.}
\[\inferLabel{RAA}{\Gamma, \neg p\vdash\bot}{\Gamma\vdash p}\]
\vskip 2 mm

\rouge{Attention}: il ne faut pas confondre cela avec
\[\infer{\Gamma, p\vdash\bot}{\Gamma\vdash \neg p}\]
qui est en fait:
\[\infer{\Gamma, p\vdash\bot}{\Gamma\vdash p\Ra \bot}\]

\section{Exercice}
Prouvez
\begin{enumerate}
\item \bleu{\neg\neg p \Ra p}
\item \bleu{p \vee \neg p}
\item \bleu{((p \Ra q) \Ra p) \Ra p}
\end{enumerate}


\section{Correction et complétude}
\rouge{Interprétation:}  une fonction de \bleu{proposition} vers
\bleu{\{0,1\}}, somme et produit modulo 2.
\begin{itemize}
\item \bleu{v(p \Ra q)} = \bleu{1 + v(p) + v(p).v(q)}
\item \bleu{v(p \vee q)} = \bleu{v(p) + v(q) + v(p).v(q)} 
\item \bleu{v(p \wedge q)} = \bleu{v(p).v(q)} 
\item \bleu{\bot} = 0
\end{itemize}

\bleu{\Gamma \vDash_{NK} p} signifie que si \bleu{v(q)=1} pour tout
\bleu{q\in\Gamma} alors \bleu{v(p)=1}

\vskip 3 mm

La logique propositionnelle est \rouge{correcte}, \\ \hspace*{20pt}c-à-d
\bleu{\Gamma\vdash_{NK} p} implique \bleu{\Gamma\vDash_{NK} p} 

\vskip 2 mm

La logique propositionnelle est \rouge{complète}, \\ \hspace*{20pt}c-à-d
\bleu{\Gamma\vDash_{NK} p} implique \bleu{\Gamma\vdash_{NK} p} 


\end{document}
% LocalWords:  green Prop Intro