\documentclass{article} \usepackage{fancybox} \usepackage[francais]{babel} \usepackage[latin1]{inputenc} \usepackage{color} \title{\it La logique propositionnelle de Hilbert} \author{} \date{} \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} }} \begin{document} \maketitle \section{La logique propositionnelle minimale} \subsection{La syntaxe} Il n'y a qu'un \rouge{connecteur} \bleu{\Ra} et des \rouge{variables propositionnelles} \bleu{p}, \bleu{q}, \ldots, \bleu{p_1}, \bleu{p_2}, \ldots 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\]} \subsection{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 \subsection{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. \subsection{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. \subsection{Une règle} \noindent En logique propositionnelle minimale, il n'y a qu'une règle : le \rouge{Modus Ponens}~: \[\inferTwoLabel{MP}{p\Ra q}{p}{q}\] \noindent 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}. \vskip 2 mm \noindent 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}. \vskip 2 mm \VERT{Mais c'est à peu près la même chose, à une curryfication prés!} \subsection{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}~!} \subsection{Exercice} Prouver le lemme \bleu{B: (p \Ra q) \Ra (r \Ra p) \Ra r \Ra q)}. \subsection{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}\] \subsection{Exercice} 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)}.\] \subsection{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}\] \subsection{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. \subsection{Exercices} \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} \subsection{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 ! \section{La logique propositionnelle intuitionniste} \subsection{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} \subsection{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} \subsection{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} \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}$ \subsection{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}. \subsection{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). \subsection{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} \subsection{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 ? \subsection{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} \vskip 3 mm C'est comme construire une maison sur un terrain situé \centerline{à Vaise \rouge{ou} à Vénissieux !} \subsection{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{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