From aed690c583c4cac1ee8d20793edd551087653dd2 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Tue, 19 Dec 2023 10:36:11 +0100 Subject: Change my mind about name of third part. --- transp-inf110-03-super.tex | 681 --------------------------------------------- 1 file changed, 681 deletions(-) delete mode 100644 transp-inf110-03-super.tex (limited to 'transp-inf110-03-super.tex') diff --git a/transp-inf110-03-super.tex b/transp-inf110-03-super.tex deleted file mode 100644 index 79b9570..0000000 --- a/transp-inf110-03-super.tex +++ /dev/null @@ -1,681 +0,0 @@ -%% This is a LaTeX document. Hey, Emacs, -*- latex -*- , get it? -\documentclass[mathserif,a4paper,aspectratio=169]{beamer} -%\documentclass[a4paper]{article} -%\usepackage[envcountsect,noxcolor]{beamerarticle} -\usepackage[shorthands=off,french]{babel} -\usepackage[utf8]{inputenc} -\usepackage[T1]{fontenc} -\usepackage{lmodern} -\DeclareUnicodeCharacter{00A0}{~} -\DeclareUnicodeCharacter{2026}{...} -% Beamer theme: -\usetheme{Goettingen} -%\usecolortheme{albatross} -%\usecolortheme{lily} -%\setbeamercovered{transparent} -% A tribute to the worthy AMS: -\usepackage{amsmath} -\usepackage{amsfonts} -\usepackage{amssymb} -\usepackage{amsthm} -% -\usepackage{mathrsfs} -\usepackage{mathpartir} -\usepackage{flagderiv} -% -\usepackage{graphicx} -\usepackage{tikz} -\usetikzlibrary{arrows,automata,calc} -% -\newcommand{\itempoint}{\strut\hbox{\color{beamerstructure}\donotcoloroutermaths$\blacktriangleright$}\nobreak\hskip.5em plus.5em\relax} -\renewcommand{\thefootnote}{\textdagger} -\newcommand{\dbllangle}{\mathopen{\langle\!\langle}} -\newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}} -%\newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}} -%\newcommand{\dottedland}{\mathbin{\dot\land}} -%\newcommand{\dottedlor}{\mathbin{\dot\lor}} -%\newcommand{\dottedtop}{\mathord{\dot\top}} -%\newcommand{\dottedbot}{\mathord{\dot\bot}} -%\newcommand{\dottedneg}{\mathop{\dot\neg}} -\mathchardef\emdash="07C\relax -\newcommand{\mpdotsabove}[1]{\inferrule*{\vdots}{#1}} -%\setlength{\derivskip}{4pt} -% -% -% -\title{Logique(s) et typage(s) d'ordre(s) supérieur(s)} -\subtitle{INF110 (Logique et Fondements de l'Informatique)} -\author[David Madore]{David A. Madore\\ -{\footnotesize Télécom Paris}\\ -\texttt{david.madore@enst.fr}} -\date{2023–2024} -\mode{% -\beamertemplatenavigationsymbolsempty -\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize\hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}} -} -\setbeamercolor{myhighlight}{fg=black,bg=white!90!green} -\colorlet{mydarkgreen}{green!50!black} -\begin{document} -\mode
{\maketitle} -% -\setlength\abovedisplayskip{2pt plus 2pt minus 2pt} -\setlength\belowdisplayskip{2pt plus 2pt minus 2pt} -% -\begin{frame} -\titlepage -{\footnotesize\center{\url{http://perso.enst.fr/madore/inf110/transp-inf110.pdf}}\par} -{\tiny -\immediate\write18{sh ./vc > vcline.tex} -\begin{center} -Git: \input{vcline.tex} -\end{center} -\immediate\write18{echo ' (stale)' >> vcline.tex} -\par} -\end{frame} -% -\section*{Plan} -\begin{frame} -\frametitle{Plan} -\tableofcontents -\end{frame} -% -\section{Les quantificateurs : discussion informelle} -\begin{frame} -\frametitle{Limitations du calcul propositionnel} - -\itempoint On a parlé pour l'instant de \textbf{calcul - propositionnel}, qui ne connaît que les affirmations logiques et les -connecteurs propositionnels $\Rightarrow,\land,\lor,\top,\bot$. - -\medskip - -\itempoint Mais il y a deux notations logiques essentielles en -mathématiques au-delà de ces connecteurs : les -\textbf{quantificateurs} $\forall,\exists$, qui : -\begin{itemize} -\item prennent une formule $P(x)$ dépendant d'une variable $x$ libre, -\item lient cette variable pour former une nouvelle formule $\forall - x. P(x)$ ou $\exists x. P(x)$. -\end{itemize} - -\medskip - -\itempoint Intuitivement, il faut penser à $\forall$ et $\exists$ -comme des « $\land$ et $\lor$ en famille », c'est-à-dire que : -\begin{itemize} -\item $\forall x.P(x)$, parfois noté $\bigwedge_x P(x)$ est à $P\land - Q$ ce que $\prod_i p_i$ est à $p\times q$, -\item $\exists x.P(x)$, parfois noté $\bigvee_x P(x)$ est à $P\lor Q$ - ce que $\sum_i p_i$ est à $p + q$. -\end{itemize} - -\medskip - -\itempoint Il existe de \alert{nombreux systèmes logiques} différant -notamment en \alert{ce qu'on a le droit de quantifier} (qui sont les -$x$ ici ?). - -\smallskip - -\textcolor{brown}{Commençons par une discussion informelle de - $\forall$ et $\exists$.} - -\end{frame} -% -\begin{frame} -\frametitle{L'interprétation BHK des quantificateurs} - -On a déjà vu l'interprétation informelle des connecteurs, on introduit -maintenant les quantificateurs : - -\begin{itemize} -\item {\color{darkgray} un témoignage de $P\land Q$, est un témoignage - de $P$ et un de $Q$,} -\item {\color{darkgray} un témoignage de $P\lor Q$, est un témoignage - de $P$ ou un de $Q$, et la donnée duquel des deux on a choisi,} -\item {\color{darkgray} un témoignage de $P\Rightarrow Q$ est un moyen - de transformer un témoignage de $P$ en un témoignage de $Q$,} -\item {\color{darkgray} un témoignage de $\top$ est trivial,} \quad - \itempoint {\color{darkgray} un témoignage de $\bot$ n'existe pas,} -\item un témoignage de $\forall x.P(x)$ est un moyen - de transformer un $x$ quelconque en un témoignage de $P(x)$, -\item un témoignage de $\exists x.P(x)$ est la donnée d'un certain - $x_0$ et d'un témoignage de $P(x_0)$. -\end{itemize} - -\end{frame} -% -\begin{frame} -\frametitle{Curry-Howard pour le $\forall$} - -\itempoint On a vu que Curry-Howard fait correspondre -\alert{conjonction logique} $P\land Q$ {\footnotesize (« un témoignage - de $P$ et un de $Q$ »)} avec \alert{type produit} $\sigma\times\tau$ - {\footnotesize (« une valeur de $\sigma$ et une de $\tau$ »)}. - -\medskip - -\itempoint De façon analogue, la \alert{quantification universelle} -$\forall x. P(x)$ {\footnotesize (« une façon de transformer $x$ en un - témoignage de $P(x)$ »)}, qui est une sorte de \emph{conjonction en -famille} $\bigwedge_x P(x)$, correspondra au \alert{type produit en - famille} $\prod_x \sigma(x)$ {\footnotesize (« fonction renvoyant - une valeur de $\sigma(x)$ pour chaque $x$ »)}. - -\medskip - -\itempoint Ceci présuppose l'existence de \alert{familles de types} $x -\mapsto \sigma(x)$ (= types dépendant de quelque chose) dont on puisse -prendre le produit. - -\medskip - -\itempoint Une preuve de $\forall x.P(x)$ correspondra à un terme de -forme $\lambda(x:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond -à $P(x)$. - -\medskip - -\itempoint Remarquer que $\forall x.P$, si $P$ ne dépend pas de $x$, -« ressemble » à $I \Rightarrow P$ de la même manière que $\prod_{i\in - I} X = X^I$. {\footnotesize (Les détails dépendent de la nature de - la quantification.)} - -\end{frame} -% -\begin{frame} -\frametitle{Curry-Howard pour le $\exists$} - -\itempoint On a vu que Curry-Howard fait correspondre -\alert{conjonction logique} $P\lor Q$ {\footnotesize (« un témoignage - de $P$ ou un de $Q$, avec la donnée duquel on a choisi »)} avec -\alert{type somme} $\sigma+\tau$ {\footnotesize (« une valeur de - $\sigma$ ou une de $\tau$, avec un sélecteur entre les deux »)}. - -\medskip - -\itempoint De façon analogue, la \alert{quantification existentielle} -$\exists x. P(x)$ {\footnotesize (« la donnée d'un $x_0$ et d'un - témoignage de $P(x_0)$ »)}, qui est une sorte de \emph{disjonction -en famille} $\bigvee_x P(x)$, correspondra au \alert{type somme en - famille} $\sum_x \sigma(x)$ {\footnotesize (« donnée d'un $x_0$ et - d'une valeur de type $\sigma(x_0)$ »)}. - -\medskip - -\itempoint Une preuve de $\exists x.P(x)$ correspondra à un terme de -forme $\langle x_0, \cdots\rangle$, où le type de $(\cdots)$ -correspond à $P(x_0)$. {\footnotesize (De nouveau, il faut des - « familles de types ».)} - -\medskip - -\itempoint Remarquer que $\exists x.P$, si $P$ ne dépend pas de $x$, -« ressemble » à $I \times P$ de la même manière que $\sum_{i\in I} X = -I\times X$. {\footnotesize (Les détails dépendent de la nature de la - quantification.)} - -\medskip - -\itempoint Mais Curry-Howard atteint ses limites : il n'est pas dit -que d'une preuve de $\exists x.P(x)$ on \alert{puisse extraire} le -$x_0$ correspondant dans autre chose qu'une preuve. {\footnotesize - (Les détails dépendent du système logique précis considéré {\tiny et - si Martin-Löf est dans la salle}.)} - -\end{frame} -% -\begin{frame} -\frametitle{Le problème du $\exists$ et des types sommes} - -Doit-on croire à ceci (pour $U$ et $V$ deux types) ? -\[ -(\forall(x:U).\,\exists(y:V).\,P(x,y)) -\Rightarrow -(\exists(f:U\Rightarrow V).\,\forall(x:U).\,P(x,f(x))) -\] - -\medskip - -{\footnotesize (Cet énoncé porte le nom d'\alert{axiome du choix} : - c'est un analogue pour la théorie des types de l'axiome du choix (de - Zermelo) en théorie des ensembles.)\par} - -\medskip - -\itempoint Si on voit $\forall$ et $\exists$ comme des types produit -et \alert{somme} en famille respectivement, \alert{oui} : -$\forall(x:U).\,\exists(y:V).\,P(x,y)$ représente une fonction qui -prend un $x$ de type $U$ et renvoie un $y$ de type $V$ ainsi qu'un -$P(x,y)$ correspondant : on peut collecter tous ces $y$ en une -fonction $f : U \Rightarrow V$. - -\medskip - -\itempoint Si on voit $\exists$ comme un quantificateur -\alert{logique}, alors \alert{non} : le $y$ renvoyé par $\exists$ ne -peut servir qu'à l'intérieur d'une preuve, pas être collecté en une -fonction. - -\medskip - -\itempoint C'est ici la différence principale entre des systèmes comme -Coq (où l'énoncé ci-dessus ne sera pas prouvable pour $P : U\times V -\to \mathit{Prop}$) et les systèmes à la Martin-Löf comme Agda (où -Curry-Howard est suivi « jusqu'au bout » : il n'y a pas de $\exists$ -uniquement logique). - -\end{frame} -% -\begin{frame} -\frametitle{Imprédicativité} - -\itempoint On appelle \textbf{imprédicativité} la possibilité de -définir une proposition ou un type en quantifiant sur toutes les -propositions ou types \alert{y compris celui qu'on définit} : c'est -une forme de circularité. - -\medskip - -\itempoint P.ex., $\forall (Z:*).\, (Z \Rightarrow A)$ représente le -type des fonctions capables de renvoyer un type $A$ à partir d'un type -$Z$ quelconque, y compris celui qu'on définit. - -\smallskip - -Cette imprédicativité est utile pour définir des constructions sur les -types. - -\medskip - -{\footnotesize - -Exemples (informellement, et en notant « $*$ » le « type des types » -imprédicatif) : -\begin{itemize} -\item $A \; \cong \; \forall (Z:*).\, (Z \Rightarrow A)$ : donné une - valeur $x$ de type $A$ on peut en fabriquer une de type - $Z\Rightarrow A$ comme $\lambda(z:Z).\, x$ pour tout type $Z$, mais - réciproquement, donné une valeur de type $\forall (Z:*).\, (Z - \Rightarrow A)$ on peut l'appliquer à $Z = \top$ pour obtenir une - valeur de type $A$. -\item $A \; \cong \; \forall (Z:*).\, ((A \Rightarrow Z) \Rightarrow - Z)$ : dans un sens on fabrique $\lambda(k:A \Rightarrow Z).\, kx$ - comme pour le CPS, dans l'autre sens, appliquer à $Z = A$ et - l'identité. -\item $\bot \; \cong \; \forall (Z:*).\, Z$ -\quad\itempoint $A\land B \; \cong \; \forall (Z:*).\, ((A \Rightarrow B - \Rightarrow Z) \Rightarrow Z)$ -\item $A\lor B \; \cong \; \forall (Z:*).\, ((A \Rightarrow Z) - \Rightarrow (B\Rightarrow Z) \Rightarrow Z)$ -\end{itemize} - -\par} - -\medskip - -\itempoint Cela \alert{peut} donner des incohérences logiques -(paradoxe de Girard). - -\end{frame} -% -\section{Logique du premier ordre} -\begin{frame} -\frametitle{Logique du premier ordre : principe} - -\itempoint La \textbf{logique du premier ordre} ou \textbf{calcul des - prédicats} est la plus simple qui ajoute les quantificateurs. Les -« choses » sur lesquelles on a le droit de quantifier s'appellent des -\textbf{individus}. - -\medskip - -\itempoint Côté typage, elle n'est pas très heureuse : les -« individus » apparaissent comme un type unique, \textit{ad hoc}, -qu'on ne peut presque pas manipuler (la logique ne permet pas de faire -des couples, fonctions, etc., des individus). - -\medskip - -\itempoint Néanmoins, elle a une \alert{grande importance - mathématique} car le dogme « orthodoxe » est que : -\begin{center} -Les mathématiques se font dans la « théorie des ensembles\\de -Zermelo-Fraenkel en logique du premier ordre » ($\mathsf{ZFC}$). -\end{center} - -Le manque d'expressivité de la logique (pas de couples, fonctions, -etc.) est \alert{compensé par la théorie elle-même} (constructions -ensemblistes des couples, fonctions, etc.). - -\medskip - -{\footnotesize\itempoint La \alert{sémantique} (Tarskienne) de la - logique du premier ordre a aussi des propriétés agréables (théorème - de complétude de Gödel).\par} - -\end{frame} -% -\begin{frame} -\frametitle{Logique du premier ordre : sortes de variables et syntaxe} - -\itempoint En (pure) logique du premier ordre, on a diverses sortes de -variables : -\begin{itemize} -\item les \textbf{variables d'individus} ($x$, $y$, $z$...) en nombre - illimité, -\item les \textbf{variables de prédicats} $n$-aires, ou de - \textbf{relations} $n$-aires [entre individus] ($A^{(n)}$, - $B^{(n)}$, $C^{(n)}$...), pour chaque entier naturel $n$. -\end{itemize} - -\medskip - -\itempoint L'indication d'arité des variables de prédicats est -généralement omise (elle peut se lire sur la formule). - -\medskip - -\itempoint Une \textbf{formule} (logique) est (inductivement) : -\begin{itemize} -\item l'application $A^{(n)}(x_1,\ldots,x_n)$ d'une variable - propositionnelle à $n$ variables d'individus, -\item l'application d'un connecteur : $(P\Rightarrow Q)$, $(P\land - Q)$, $(P\lor Q)$ où $P,Q$ sont deux formules, ou encore $\top$, - $\bot$, -\item une quantification : $\forall x.P$ ou $\exists x.P$, qui - \alert{lie} la variable d'individu $x$ dans $P$. -\end{itemize} - -\medskip - -\itempoint\alert{On ne peut quantifier que sur les individus - (« premier ordre »).} - -\end{frame} -% -\begin{frame} -\frametitle{Exemples de formules du premier ordre} - -\itempoint Les \textbf{formules propositionnelles} sont encore des -formules du premier ordre, en interprétant chaque variable -propositionnelle comme une variable de prédicat $0$-aire -(« nullaire ») : $A\land B \Rightarrow B\land A$ par exemple. - -\bigskip - -Autres exemples (qui seront par ailleurs tous démontrables) : -\begin{itemize} -\item $(\forall x.A(x)) \land (\exists x.\top) \Rightarrow (\exists - x.A(x))$ (ici, $A$ est un prédicat unaire) -\item $(\forall x.\neg A(x)) \Leftrightarrow (\neg\exists x.A(x))$ (idem) -\item $(\exists x.\neg A(x)) \Rightarrow (\neg\forall x.A(x))$ (idem) -\item $(\exists x.A) \Leftrightarrow (\exists x.\top) \land A$ (ici, - $A$ est un prédicat \alert{nullaire}) -\item $(\forall x.A) \Leftrightarrow ((\exists x.\top) \Rightarrow A)$ - (idem) -\item $(\exists x.\forall y.B(x,y))\Rightarrow (\forall y.\exists - x.B(x,y))$ (ici, $B$ est un prédicat binaire) -\end{itemize} - -\bigskip - -\textbf{N.B.} On a suivi la convention que $\forall,\exists$ ont une -priorité plus faible que les connecteurs -$\Rightarrow,\lor,\land,\neg$. Tout le monde n'est pas d'accord avec -cette convention ! - -\smallskip - -\textbf{N.B.2 :} Il serait peut-être préférable de noter $Bxy$ que -$B(x,y)$. - -\end{frame} -% -\begin{frame} -\frametitle{Logique du premier ordre : aperçu des règles} - -\begin{tabular}{c|c|c} -&Intro&Élim\\\hline -$\Rightarrow$ -&\scalebox{0.65}{$\inferrule{\Gamma,{\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash P\Rightarrow Q}$} -&\scalebox{0.65}{$\inferrule{\Gamma\vdash P\Rightarrow Q\\\Gamma\vdash P}{\Gamma\vdash Q}$} -\\\hline -$\land$ -&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\\\Gamma\vdash Q_2}{\Gamma\vdash Q_1\land Q_2}$} -&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_1}$} -\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_2}$} -\\\hline -$\lor$ -&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1}{\Gamma\vdash Q_1\lor Q_2}$} -\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_2}{\Gamma\vdash Q_1\lor Q_2}$} -&\scalebox{0.65}{$\inferrule{\Gamma\vdash P_1\lor P_2\\\Gamma,{\color{mydarkgreen}P_1}\vdash Q\\\Gamma,{\color{mydarkgreen}P_2}\vdash Q}{\Gamma\vdash Q}$} -\\\hline -$\top$ -&\scalebox{0.65}{$\inferrule{\strut}{\Gamma\vdash \top}$} -&\scalebox{0.65}{(néant)} -\\\hline -$\bot$ -&\scalebox{0.65}{(néant)} -&\scalebox{0.65}{$\inferrule{\Gamma\vdash \bot}{\Gamma\vdash Q}$ -(ou pour la logique classique : $\inferrule{\Gamma,\neg Q\vdash \bot}{\Gamma\vdash Q}$)} -\\\hline -$\forall$ -&$\inferrule{\Gamma, {\color{mydarkgreen}x}\vdash Q}{\Gamma\vdash \forall x. Q}$ ($x$ \alert{frais}) -&$\inferrule{\Gamma\vdash \forall x. Q}{\Gamma\vdash Q[x\backslash t]}$ -(v.l. de $t$ sont ds $\Gamma$) -\\\hline -$\exists$ -&$\inferrule{\Gamma\vdash Q[x\backslash t]}{\Gamma\vdash \exists x. Q}$ -(v.l. de $t$ sont ds $\Gamma$) -&$\inferrule{\Gamma\vdash \exists x. P\\\Gamma, {\color{mydarkgreen}x}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$ -($x$ \alert{frais}) -\\ -\end{tabular} - -\smallskip - -\itempoint « $x$ frais » = « $x$ n'apparaît nulle part ailleurs », -cf. transp. suivants. - -\smallskip - -\itempoint $\Gamma$ peut contenir des formules et des variables -d'individus « introduites libres ». - -\smallskip - -\itempoint « v.l. de $t$ sont ds $\Gamma$ » = les variables libres de -$t$ doivent être dans $\Gamma$, -cf. transp. \ref{caveat-inhabited-domain}. - -\end{frame} -% -\begin{frame} -\frametitle{Règles d'introduction et d'élimination de $\forall$} - -\itempoint \underline{Introduction du $\forall$ :} pour montrer -$\forall x. Q$, on s'arrange (quitte à renommer la variable liée) pour -que $x$ soit « frais », c'est-à-dire qu'il n'apparaisse (libre) dans -\alert{aucune hypothèse} en cours ($\Gamma$) : si on montre $Q$ sur ce -$x$ « arbitraire », on peut conclure $\forall x. Q$. - -\smallskip - -{\footnotesize (Rédaction : « soit $x$ arbitraire (…) on a $Q(x)$ ; - donc $\forall x. Q(x)$ ».)\par} - -\bigskip - -\itempoint \underline{Élimination du $\forall$ :} pour utiliser -$\forall x. Q$, on peut l'appliquer à un $t$ quelconque (en général un -\alert{terme}, mais ici nos seuls termes d'individus sont des -variables), dont les variables libres \alert{doivent} apparaître dans -$\Gamma$. - -\smallskip - -{\footnotesize (Rédaction : « on a $\forall x. Q(x)$ ; en particulier, - on a $Q(t)$ ».)\par} - -\end{frame} -% -\begin{frame} -\frametitle{Règles d'introduction et d'élimination de $\exists$} - -\itempoint \underline{Introduction du $\exists$ :} pour montrer -$\exists x. Q$, on peut le montrer sur un $t$ quelconque (en général -un terme), dont les variables libres \alert{doivent} apparaître dans -$\Gamma$. - -\smallskip - -{\footnotesize (Rédaction : « on a $Q(t)$ ; en particulier, on a - $\exists x. Q(x)$ ».)\par} - -\bigskip - -\itempoint \underline{Élimination du $\exists$ :} pour utiliser -$\exists x. P$ pour montrer une conclusion $Q$, on s'arrange (quitte à -renommer la variable liée) pour que $x$ soit « frais », c'est-à-dire -qu'il n'apparaisse (libre) dans \alert{aucune hypothèse} en cours -($\Gamma$) \alert{ni dans la conclusion} $Q$ : si on montre $Q$ à -partir de $P$ sur ce $x$ « arbitraire », on peut conclure $Q$ à partir -de $\exists x. P$. - -\smallskip - -{\footnotesize (Rédaction : « on a $\exists x. P(x)$ : soit $x$ - arbitraire tel que $P(x)$ (…) on a $Q$ ; donc $Q$ ».)\par} - -\medskip - -Cette règle est désagréable comme celle d'élimination du $\lor$ (il -faut démontrer la même conclusion $Q$ indépendamment du cas). Elle -est moins désagréable en calcul des séquents : -\[ -\inferrule{\Gamma, x, P\vdash Q}{\Gamma, \exists x. P\vdash Q} -\text{\quad($x$ \alert{frais})} -\] - -\end{frame} -% -\begin{frame} -\frametitle{Exemple de preuve en logique du premier ordre} - -{\footnotesize - -\[ -\inferrule*[left={$\Rightarrow$Int}]{ -\inferrule*[Left={$\forall$Int}]{ -\inferrule*[Left={$\exists$Élim}]{ -\inferrule*[Left={Ax}]{ }{\exists x.\forall y.B(x,y) \vdash \exists x.\forall y.B(x,y)} -\\ -\inferrule*[Right={$\exists$Int}]{ -\inferrule*[Right={$\forall$Élim}]{ -\inferrule*[Right=Ax]{ }{x,\;\forall y.B(x,y),\;y' \vdash \forall y.B(x,y)} -}{x,\;\forall y.B(x,y),\;y' \vdash B(x,y')} -}{x,\;\forall y.B(x,y),\;y' \vdash \exists x'.B(x',y')} -}{\exists x.\forall y.B(x,y),\;y' \vdash \exists x'.B(x',y')} -}{\exists x.\forall y.B(x,y) \vdash \forall y'.\exists x'.B(x',y')} -}{\vdash (\exists x.\forall y.B(x,y))\Rightarrow (\forall y'.\exists x'.B(x',y'))} -\] - -} - -Présentation avec les seules conclusions : - -{\footnotesize - -\[ -\inferrule*[left={$\Rightarrow$Int(\textcolor{mydarkgreen}{$u$})}]{ -\inferrule*[Left={$\forall$Int(\textcolor{mydarkgreen}{$y'$})}]{ -\inferrule*[Left={$\exists$Élim(\textcolor{mydarkgreen}{$x$},\textcolor{mydarkgreen}{$v$})}]{ -\inferrule*[Left={\textcolor{mydarkgreen}{$u$}}]{ }{\exists x.\forall y.B(x,y)} -\\ -\inferrule*[Right={$\exists$Int}]{ -\inferrule*[Right={$\forall$Élim}]{ -\inferrule*[Right={\textcolor{mydarkgreen}{$v$}}]{ }{\forall y.B(x,y)} -}{B(x,y')} -}{\exists x'.B(x',y')} -}{\exists x'.B(x',y')} -}{\forall y'.\exists x'.B(x',y')} -}{(\exists x.\forall y.B(x,y))\Rightarrow (\forall y'.\exists x'.B(x',y'))} -\] - -} - -\end{frame} -% -\begin{frame} -\frametitle{Exemple de preuve : présentation drapeau} - -{\footnotesize -\begin{flagderiv}[example-1st-order-proof] -\assume{mainhyp}{\exists x.\forall y.B(x,y)}{} -\assume{vary}{y'}{} -\assume{exhyp}{x,\;\forall y.B(x,y)}{} -\step{bare}{B(x,y')}{$\forall$Élim sur \ref{exhyp} et $y$} -\step{exbare}{\exists x'.B(x',y')}{$\exists$Int sur $x$ et \ref{bare}} -\conclude{extrude}{\exists x'.B(x',y')}{$\exists$Elim sur \ref{mainhyp} de \ref{exhyp} dans \ref{exbare}} -\conclude{mainconc}{\forall y'.\exists x'.B(x',y')}{$\forall$Intro de \ref{vary} dans \ref{extrude}} -\conclude{}{(\exists x.\forall y.B(x,y))\Rightarrow(\forall y'.\exists x'.B(x',y'))}{$\Rightarrow$Intro de \ref{mainhyp} dans \ref{mainconc}} -\end{flagderiv} -\par} - -\smallskip - -{\footnotesize « Supposons $\exists x.\forall y.B(x,y)$. Considérons - un $y'$ arbitraire. Considérons un $x$ tel que $\forall y.B(x,y)$. - En particulier, on a $B(x,y')$. En particulier, $\exists - x'.B(x',y')$. Or on pouvait trouver un tel $x$ car $\exists - x.\forall y.B(x,y)$, donc on a bien la conclusion $\exists - x'.B(x',y')$. Le choix de $y'$ étant arbitraire, $\forall - y'. \exists x'. B(x',y')$. Finalement, on a prouvé $(\exists - x.\forall y.B(x,y))\Rightarrow(\forall y'.\exists - x'.B(x',y'))$. »\par\strut\par} - -\end{frame} -% -\begin{frame} -\label{caveat-inhabited-domain} -\frametitle{Pourquoi des variables d'individus avec les hypothèses ?} - -\itempoint L'introduction d'une variable d'individu libre porte en -elle l'hypothèse que \alert{l'univers des individus est habité} -($\exists x. \top$). Ce fait \alert{n'est pas prouvable} sans cette -hypothèse. On a $z \vdash \exists x.\top$ (ici $z$ variable qcque) -mais \alert{on n'a pas} $\vdash \exists x.\top$. - -\medskip - -\itempoint Exiger que les variables d'individus libres dans le terme -$t$ soient déjà dans $\Gamma$ permet d'écarter la démonstration -\alert{incorrecte} suivante : -\[ -\inferrule*[left={$\exists$Int}]{ -\inferrule*[Left={$\top$Int}]{ }{\vdash\top} -}{\vdash\exists x.\top} -\] - -\medskip - -\itempoint En revanche, celle-ci \alert{est correcte} (en utilisant le -terme $z$ pour $t$ dans $\exists$Int) : -\[ -\inferrule*[left={$\forall$Int}]{ -\inferrule*[Left={$\exists$Int}]{ -\inferrule*[Left={$\top$Int}]{ }{z\vdash\top} -}{z\vdash\exists x.\top} -}{\vdash\forall z.\exists x.\top} -\] - -\medskip - -\textbf{N.B.} Ces problèmes n'ont rien à voir avec la logique -intuitionniste, ils sont identiques en logique classique. On -\alert{n'a pas} non plus $\forall x.A(x) \Rightarrow \exists x.A(x)$. - -\end{frame} -% -\end{document} -- cgit v1.2.3