%% Time-stamp: <modifié par Pierre Lescanne le 18 Dec 2002 à 12h08>
%% /MIM-1/LOGIQUE/00-01/COURS+TRANSP/Predicat/predicats.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}
\usepackage[all]{xy}
\usepackage{qsymbols}
\input{mes_couleurs}


%% 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{Le Calcul des Prédicats}}}

\author{}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

% --- retour a la ligne --- 
\newcommand{\ali}{\newline\hspace*{20pt}}

% --- quelqus symboles
\newcommand{\et}{\mathop{\&}}
\newcommand{\cb}{\bar{c}}
\renewqsymbol{`|}{\mathop{\rouge{|}}}
\newcommand{\eqp}{\stackrel{.}{=}}
\newcommand{\Ag}{\mathfrak{A}}
\renewcommand{\phi}{\varphi}
%% <...> are angle brackets.
\mathcode`\<=\string"4268 \mathcode`\>=\string"5269 %

\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

\newenvironment{eqnarraybleu}%
  {\begin{color}{blue}\begin{eqnarray*}}
  {\end{eqnarray*}\end{color}}

\newcommand{\interp}[2]{\llbracket#1\rrbracket_{\mathfrak{#2}}}
\newcommand{\expA}[1]{#1^{\mathfrak{A}}}

\newcommand{\heading}[1]{%
{\color{mauve}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

\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}
  \begin{center}
    {\Large \bf \color{red}{\textit{Les structures}}}

\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Structures} 
Une \rouge{structure} est un triplet \bleu{\Ag = <A,\mathbf{P},\mathbf{F}, \{c_i\in I\}>} où
\begin{itemize}
\item \bleu{A} est un ensemble non vide (le \rouge{support} ou l'\rouge{univers} de la
  structure),
\item \bleu{\mathbf{P}} est un n-uple \bleu{P_1, ..., P_n} de prédicats,
\item \bleu{\mathbf{F}} est un m-uple \bleu{F_1, ..., F_m} de fonctions
  totales,
\item les \bleu{c_i} sont des éléments de \bleu{A} (les
  \rouge{constantes}).
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exemples} 
  \begin{itemize}
  \item \bleu{<\mathbb{R}, +, `., ^{-1}, 0, 1>} est le corps des
    réels,
  \item \bleu{<\mathbb{N},``< >} est l'ensemble ordonné des naturels.
  \end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le type de similarité} 
Le \rouge{type de similarité} d'une structure \bleu{\Ag =
  <A,P_1, ... P_n,F_1,..., F_n, \{c_i\in I\}>} est la suite \bleu{<r_1,
  ..., r_n; a_1, ..., a_m, `k>} où
\begin{itemize}
\item \bleu{R_i ``(= A^{r_i}},
\item \bleu{F_j : A^{a_j} "->" A},
\item \bleu{`k = |\{c_i \in I\}|} (le cardinal de \bleu{I}).
\end{itemize}

\vspace*{20pt}

Chaque structure contient la relation binaire d'\rouge{identité} qui est
notée~\bleu{=}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exemples} 
  \begin{itemize}
  \item \bleu{<\mathbb{R}, +, `., ^{-1}, 0, 1>} a pour type de
    similarité \bleu{<-; 2, 2, 1; 2>},
  \item \bleu{<\mathbb{N},``< >} a pour type de similarité \bleu{<2;
      -; 0>}.
  \end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{red}{\textit{La syntaxe}}}

\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La syntaxe 1/2} %
  Supposons que l'on a un langage de type de similarité \bleu{<r_1, ...,
    r_n; a_1, ..., a_m, `k>}.

Les entités syntaxiques sont
\begin{enumerate}
\item les \rouge{symboles de prédicats} \bleu{P_1, \ldots, P_n, Q, R, \eqp},
\item les \rouge{symboles de fonctions} \bleu{f_1, \ldots, f_m},
\item les \rouge{symboles de constantes} \bleu{\cb_i} pour \bleu{i\in I},
\item les \rouge{variables} \bleu{x_0, x_1, x_2, \ldots}
\item les \rouge{connecteurs} \bleu{\vee, \wedge, "=>", "<=>", \bot, `A, `E}
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La syntaxe 2/2} 
Les \rouge{termes} sont
\begin{eqnarraybleu}
  t, t' & \rouge{::=} & \cb_i `| x_j `| f(t, ..., t)
\end{eqnarraybleu}
Les \rouge{formules} sont
\begin{eqnarraybleu}
  `f, `j &\rouge{::=} & \bot  `| P(t,\ldots, t) `| t \eqp t' \\
  && `| `f \vee `j `| `f \wedge `j `| `f "=>" `j `| `f "<=>" `j
  `| `! `f `| (`A x_i) `f `| (`E x_i) `f
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La syntaxe 2/2} 
Les \rouge{termes} sont
\begin{eqnarraybleu}
  t, t' & \rouge{::=} & \cb_i `| x_j `| f(t, ..., t)
\end{eqnarraybleu}
Les \rouge{formules} sont
\begin{eqnarraybleu}
  `f, `j &\rouge{::=} & \bot  `| P(t,\ldots, t) `| t \eqp t' \qquad\qquad
  \textrm{\VERT{Les atomes}}\\
  && `| `f \vee `j `| `f \wedge `j `| `f "=>" `j `| `f "<=>" `j
  `| `! `f `| (`A x_i) `f `| (`E x_i) `f
\end{eqnarraybleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La syntaxe 3/2} Les notions de \rouge{variables libres}, de
  \rouge{variables liées}, de \rouge{formules closes} sont les mêmes
  qu'en lambda-calcul, sauf qu'ici les lieurs sont~\bleu{`A} et
  \bleu{`E}

Les formules closes sont appelées des \rouge{sentences}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Parenthèses et priorités} 
Les conventions sur les parenthèses sont les suivantes.
\begin{itemize}
\item On omet les parenthèses les plus externes.
\item On enlève les parenthèses dans les négations.
\item \bleu{\vee} et \bleu{\wedge} ont priorité sur \bleu{"=>"} et
  \bleu{"<=>"}.
\item \bleu{\neg} a priorité sur tout autre opérateur.
\item On enlève les parenthèses autour des quantifications \bleu{`A x} et
  \bleu{`E x} chaque fois que c'est possible.
\item Les quantificateurs ont priorité sur tous les connecteurs
  logiques.

\item On fusionne les listes de quantificateurs identiques \bleu{`E
    x_1 x_2 `A x_3 x_4 x_5 `f} au lieu de \bleu{`E
    x_1 `E x_2 `A x_3 `A x_4 `A x_5 `f}.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le cas du signe \bleu{=}} 

On peut vouloir utiliser le symbole  \bleu{=} à la fois dans la
théorie est la métathéorie.  Pour faire la différence on emploie
souvent  
\begin{itemize}
\item \bleu{`=} pour l'égalité syntaxique des expressions dans la
métathéorie,
\item \bleu{=} comme symbole d'égalité dans la structure.
\item  et \bleu{\eqp} comme symbole d'égalité du langage
  de la métathéorie,
\end{itemize}

\vspace*{20pt}

Nous accepterons l'utilisation de \bleu{=} à la place de \bleu{\eqp}
quand il n'y aura pas de confusion possible.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Substitutions de termes dans les termes} 
\begin{itemize}
\item \bleu{x[x:=t] = t}
\item \bleu{y[x:=t] = y}
\item \bleu{\cb[x:=t] = \cb}
\item \bleu{f(t_1,...,t_p)[x:=t] = f(t_1[x:=t], ...,t_p[x:=t]})
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Substitutions de termes dans les formules} 
On applique la convention de Barendregt
\begin{itemize}
\item \bleu{\bot[x:=t] \quad \rouge{=} \quad \bot}
\item \bleu{P[x:=t] \quad \rouge{=} \quad P}
\item \bleu{(t_1 \eqp t_2) [x:=t] \quad \rouge{=} \quad (t_1[x:=t] \eqp t_2[x:=t] }
\item \bleu{P(t_1,...,t_p)[x:=t] \quad \rouge{=} \quad P(t_1[x:=t], ...,t_p[x:=t]})
\item \bleu{(`f `[] `g)[x:=t] \quad \rouge{=} \quad `f[x:=t] ~`[]~ `g[x:=t] }
\item \bleu{(`!`f)[x:=t] \quad \rouge{=} \quad `!(`f[x:=t])}
\item \bleu{(`A y `f)[x:=t] \quad \rouge{=} \quad `A y (`f[x:=t])}
\item \bleu{(`E y `f)[x:=t] \quad \rouge{=} \quad `E y (`f[x:=t])}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Convention} %
  Parfois pour mettre en évidence que \bleu{x} peut apparaître dans
  \bleu{`f} on écrit \bleu{`f(x)}.
  
  Alors au lieu de \bleu{`f(x)[x:=t]} on écrit alors \bleu{`f(t)}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le langage étendu} %
  Le \rouge{langage étendu} \bleu{L(\Ag)} de
  \bleu{\Ag} est obtenu en ajoutant au langage \bleu{L} du
  type de similarité de \bleu{\Ag} des symboles de constantes
  pour tous les éléments de \bleu{A} (le support de
  \bleu{\Ag}).

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Substitutions de formules dans les formules} 
Pas difficile !
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{red}{\textit{La sémantique}}}

\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un exemple} %
Considérons la structure \bleu{\mathfrak{Z} = <\mathbb{Z}, ``<, +, -,
  0>}.

Le langage a son alphabet 
\begin{itemize}
\item des \rouge{symboles de prédicats} \bleu{\eqp, L},
\item des \rouge{symboles de fonctions} \bleu{P, M},
\item des \rouge{symboles de constantes} \bleu{\overline{0}}.
\end{itemize}

\bleu{L(\mathfrak{Z})} contient de plus un symbole de constante
\bleu{\overline{m}} \ali pour chaque \bleu{m\in\mathbb{Z}}. 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des termes dans \bleu{\mathfrak{Z}}}
L'interprétation \bleu{t^{\mathfrak{Z}}} de chaque terme \bleu{t} de
\bleu{L(\mathfrak{Z})} est un élément de \bleu{\mathbb{Z}}.

\begin{displaymathbleu}
      \begin{array}[c]{l@{\qquad\qquad}l}
\hline
t &  t^{\mathfrak{Z}}\\
\hline
\overline{m}  & m\\
P(t_1,t_2) & t_1^{\mathfrak{Z}} + t_2^{\mathfrak{Z}}\\
M(t) & - t^{\mathfrak{Z}}
    \end{array}
\end{displaymathbleu}
Grosso modo, on interprète 
\begin{itemize}
\item \bleu{m} par «son nombre», 
\item \bleu{P} par \emph{plus} 
\item et \bleu{M} par \emph{moins}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des sentences dans \bleu{\mathfrak{Z}}}

\begin{footnotesize}
\bl{
\begin{math}
\begin{array}{c@{\vspace*{-5pt}}c}
\begin{array}{lcl}
  \interp{\bot}{Z} & = & 0\\
  \interp{t\eqp s}{Z} &=& \left\{
    \begin{array}{l}
      1 \textrm{~si~} t^{\mathfrak{Z}} = s^{\mathfrak{Z}}\\
      0 \textrm{~sinon}
    \end{array}
       \right.\\
 \interp{L(t,s)}{Z} & = & \left\{
    \begin{array}{l}
      1 \textrm{~si~} t^{\mathfrak{Z}} ``< s^{\mathfrak{Z}}\\
      0 \textrm{~sinon}
    \end{array}
       \right.
     \end{array}
&
\begin{array}{lcl}
 \interp{`f \wedge `j}{Z} & = & min(\interp{`f}{Z}, \interp{`j}{Z})\\
 \interp{`f \vee `j}{Z} & = & max(\interp{`f}{Z}, \interp{`j}{Z})\\
 \interp{`f `[] `j}{Z} & = & \textit{(comme d'habitude)}\\
 \interp{`A x `f}{Z} & = & min\{\interp{`f[x:=\overline{n}]}{Z} ~|~ n\in \mathbb{Z}\}\\
 \interp{`E x `f}{Z} & = & max\{\interp{`f[x:=\overline{n}]}{Z} ~|~ n\in \mathbb{Z}\}\\
 \end{array}
\end{array}
\end{math}}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des sentences dans \bleu{\mathfrak{Z}}}
On voit que \bleu{\interp{`A x `f}{A}} prend la valeur 1 si toutes les
instances de \bleu{\interp{`f}{A}} prennent la valeur 1.

C'est une généralisation de \bleu{\wedge}.

De même  \bleu{\interp{`E x `f}{A}} est une généralisation de
\bleu{\vee}.

Quand il n'y aura pas de confusion on écrira \bleu{\interp{`f}{}} au
lieu de \bleu{\interp{`f}{A}}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des termes}
Considérons  \bleu{\Ag =
  <A,P_1, ... P_n,F_1,..., F_m, \{c_i\in I\}>} de type de similarité \bleu{<r_1,
  ..., r_n; a_1, ..., a_m, |I|>}

On définit la fonction \bleu{(`.)^{\Ag}: \textsf{termes}_{\Ag} "->" A}
  \begin{eqnarraybleu}
    \expA{\cb_i} & = & c_i \\
    \expA{\overline{a}} & = & a \\
    \expA{(\overline{F_i}(t_1,...t_p))} & = &
    F_i(\expA{t_1},...,\expA{t_p}).
  \end{eqnarraybleu}
  où \bleu{\overline{F_i}} est le symbole correspondant à la fonction
  \bleu{F_i} et où \bleu{p = a_i}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des sentences}
\begin{eqnarraybleu}
  \interp{\bot}{A} & = & 0\\
  \interp{\overline{R}}{A} & = & R \\
  \interp{\overline{R_i}(t_1,...t_p)}{A} & = & 
    \left\{
      \begin{array}{l}
        1 \textrm{~si~} <\expA{t_1}, ..., \expA{t_p}>\in R_i \qquad
        \textrm{où~} p = r_i\\
        0 \textrm{~sinon}
      \end{array}
    \right.\\
\interp{t_1\eqp t_2}{A} & = & 
    \left\{
      \begin{array}{l}
        1 \textrm{~si~} \expA{t_1}=\expA{t_2}\\
        0 \textrm{~sinon}
      \end{array}
    \right.
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des sentences}
\begin{eqnarraybleu}
  \interp{`f \wedge `j}{A} & = & min(\interp{`f}{A}, \interp{`j}{A})\\
  \interp{`f \vee `j}{A} & = & max(\interp{`f}{A}, \interp{`j}{A})\\
  \interp{`f "=>" `j}{A} & = & max(1 - \interp{`f}{A}, \interp{`j}{A})\\
  \interp{`f "<=>" `j}{A} & = &  \left\{
      \begin{array}{l}
        1 \textrm{~si~} \interp{`f}{A}=\interp{`j}{A}\\
        0 \textrm{~sinon}
      \end{array}
    \right.\\
  \interp{`!`f}{A} & = & 1 - \interp{`f}{A}
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des sentences}
\begin{eqnarraybleu}
  \interp{`A x `f}{A} & = & min\{\interp{`f[x:=\overline{a}]}{A} ~|~ a\in A\}\\
  \interp{`E x `f}{A} & = & max\{\interp{`f[x:=\overline{a}]}{A} ~|~ a\in A\}
\end{eqnarraybleu}
\vfill
A partir de maintenant, nous supposerons que toutes les structures ont
les mêmes types de similarité.

On écrira \bleu{\Ag "|="_K `f} pour \bleu{\interp{`f}{A} = 1}.

Cela se lira \rouge{la structure \bleu{\Ag} valide la sentence
  \bleu{\phi}} \ali ou bien \rouge{la sentence \bleu{\phi} est valide
  dans la structure \bleu{\Ag}} \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des formules}
Si \bleu{FV(`f) = \{z_1,...z_k}, la \rouge{clôture universelle} de
  \bleu{`f} est 
  \begin{displaymathbleu}
    Cl(`f) = `A z_1...z_k `f.
  \end{displaymathbleu}

\bleu{\Ag "|="_K `f} ssi \bleu{\Ag "|="_K Cl(`f)}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des formules}
\bleu{"|="_K `f} ssi \bleu{\Ag "|="_K `f} pour tout
\bleu{\Ag} de type adéquat.

\bleu{\Ag "|="_K `G} ssi \bleu{\Ag "|="_K `j} pour
tout \bleu{`j\in`G},

\bleu{`G"|="_K `f} ssi \bleu{\Ag "|="_K `G} implique
\bleu{\Ag "|="_K `f}, si \bleu{`G \cup \{`f\}} est
constitué de sentences.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des formules}
\verdir{Lemme :} 

  \bleu{\Ag "|="_K `f \wedge `j} \textrm{~si et seulement si~}  \bleu{\Ag "|="_K `f}
  \textit{~et~}  \bleu{\Ag "|="_K `j}

  \bleu{\Ag "|="_K `f \vee `j} \textrm{~si et seulement si~}  \bleu{\Ag "|="_K `f}
  \textit{~ou~}  \bleu{\Ag "|="_K `j}

  \bleu{\Ag "|="_K \neg `f} \textrm{~si et seulement si~}  \bleu{\Ag "|/=" `f}

  \bleu{\Ag "|="_K `f "=>" `j} \textrm{~si et seulement si~}  \bleu{\Ag "|="_K `f}
  \textit{~implique~}  \bleu{\Ag "|="_K `j}

  \bleu{\Ag "|="_K `f "<=>" `j} \textrm{~si et seulement si~}  \bleu{\Ag "|="_K `f}
  \textit{~est équivalent à~}  \bleu{ "|="_K `j}

 \bleu{\Ag "|="_K `A x `f } \textrm{~si et seulement si~}
 \bleu{\Ag "|="_K `f[x:=\overline{a}]} \textit{pour tout} \bleu{a\in A}.

 \bleu{\Ag "|="_K `E x `f} \textrm{~si et seulement si~}
 \bleu{\Ag "|="_K `f[x:=\overline{a}]} \textit{pour un} \bleu{a\in A}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des formules}
\verdir{Preuve du lemme :}  on le fait dans deux cas seulement.

\bleu{\Ag "|="_K `f \vee `j} équivaut à
\bleu{max(\interp{`f}{A},\interp{`j}{A}) = 1} ce qui équivaut à ce que
  \bleu{\interp{`f}{A} = 1} ou \bleu{\interp{`j}{A} = 1} ce qui
  équivaut donc à  \bleu{\Ag "|="_K `f} ou  \bleu{\Ag "|="_K `j}.


\bleu{\Ag "|="_K `A x `f} équivaut à
\bleu{min\{\interp{`f[x:=\overline{a}]}{A} ~|~ a\in A\} = 1} ce qui
équivaut à ce que pour tout \bleu{a\in A} on ait
\bleu{\interp{`f[x:=\overline{a}]}{A} = 1} ce qui revient donc à ce que
pour tout \bleu{a\in A} on ait \bleu{\Ag "|="_K `f[x:=\overline{a}]}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{red}{\textit{Quelques propriétés}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quantificateurs et négations}
\bleu{"|="_K `!`A x `f "<=>" `E x `!`f}

\bleu{"|="_K `!`E x `f "<=>" `A x `!`f}

\bleu{"|="_K `A x `f "<=>" `!`E x `!`f}

\bleu{"|="_K `E x `f "<=>" `! `A x `!`f}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Permutation et oubli de quantificateurs}
\bleu{"|="_K `A x  `A y `f "<=>" `A y `A x `f}

\bleu{"|="_K `E x  `E y `f "<=>" `E y `E x `f}

\bleu{"|="_K `A x `f "<=>" `f} si \bleu{x\notin FV(`f)}

\bleu{"|="_K `E x  `f "<=>" `f} si \bleu{x\notin FV(`f)}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Formules prénexes} %
  Une formule \bleu{`f} est en \rouge{forme prénexe}, on dit aussi
  que \bleu{`f} est \emph{prénexe}, si \bleu{`f} consiste d'un suite
  (éventuellement vide) de quantificateurs suivie d'une formule sans
  quantificateurs.

\verdir{Exemple :} \bleu{(`A x) P(x) "=>" (`E y) P(y)} n'est pas en
forme prénexe,

tandis que \bleu{(`E y\ x) (P(x) "=>" P(y))} est en forme prénexe.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Formules en forme prénexe}
\verdir{Theorem : } Pour chaque \bleu{`f} il existe une formule prénexe
\bleu{`j} telle que \bleu{"|="_K `f "<=>" `j}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{red}{\textit{La déduction naturelle}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les règles}
On ajoute à la logique propositionelle les règles

\bleu{
  \begin{array}{c@{\hspace*{50pt}}c}
\prooftree
`G "|-"_K `f(x)
\justifies `G "|-"_K `A x `f(x)
\using \rouge{`A I}
\endprooftree
&
\prooftree
`G "|-"_K `A x `f(x)
\justifies `G "|-"_K `f(t)
\using \rouge{`A E}
\endprooftree
  \end{array}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction}
\verdir{Théorème :} \bleu{`G "|-"_K `f} implique  \bleu{`G "|="_K `f}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Complétude}
\verdir{Théorème :} \bleu{`G "|="_K `f} implique  \bleu{`G "|-"_K `f}.

\vspace*{5pt}

Autrement dit, la logique classique est complète pour les modèles à
base de structures tel que nous venons de les présenter.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Complétude}%
\verdir{Théorème :} \bleu{`G "|="_K `f} implique \bleu{`G "|-"_K
  `f}.

\vspace*{5pt}

Autrement dit, la logique classique est complète pour les modèles à
base de structures tel que nous venons de les présenter.

\vspace*{20pt}

{\Huge \verdir{Je fais l'impasse !}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{red}{\textit{L'approche à la Hilbert}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les axiomes et les règles} On a deux axiomes

\begin{displaymathbleu}
  \prooftree \justifies "|-" `A x ~`f(x) "=>" f(t) \using \rouge{`A_1}
  \endprooftree
\end{displaymathbleu}

\begin{displaymathbleu}
  \prooftree \justifies  "|-" (`A x ~(`f "=>" `j(x))) "=>" `f "=>" `A x ~`j(x)
  \using \rouge{`A_2} \quad x\notin FV(`f) \endprooftree
\end{displaymathbleu}

et une règle

\begin{displaymathbleu}
 \prooftree
 "|-" `f(x)
\justifies  "|-" `A x ~`f(x)
\using \rouge{`A I}
\endprooftree
\end{displaymathbleu}
  \vfill
\end{slide}
%------------------------------------------------------
\end{document}
% LocalWords:  triplet n-uple m-uple métathéorie
