• Home
• Source
• Print

TD9 – Théorie de la preuve

Déduction naturelle

Nous rappelons ici les règles de la déduction naturelle spécifiques aux quantificateurs. Retrouvez les règles relatives aux connecteurs booléens dans la dernière feuille de TD.

Dans les règles ci-dessous, $x$ et $y$ sont des variables, alors que $t$ est un terme quelconque. On demande, en plus, que $y$ ne soit pas libre dans $Γ$, ni dans $q$.

Généralisation	$\dfrac{\Gamma\vdash p[y/x]}{\Gamma\vdash\forall x. p}I_\forall$	Spécialisation	$\dfrac{\Gamma\vdash\forall x. p}{\Gamma\vdash p[t/x]}E_\forall$
Introduction de $∃$	$\dfrac{\Gamma\vdash p[t/x]}{\Gamma\vdash\exists x. p}I_\exists$	Élimination de $∃$	$\dfrac{\Gamma\vdash\exists x. p \qquad \Gamma, p[y/x]\vdash q} {\Gamma\vdash q}E_\exists$

On rappelle que la notation $p[y/x]$ indique le prédicat obtenu en remplaçant dans $p$ toutes les occurrences libres de $x$ par $y$ ($α$-renommage). De la même façon, si $t$ est un terme, on note $p[t/x]$ le prédicat obtenu en remplaçant toutes les occurrences libres de $x$ par le terme $t$.

1. Écrire les preuves formelles des affirmations suivantes.

   • $∀x.p∧q \vdash (∀x.p) ∧ (∀x.q)$,

   • $(∀x.p) ∧ (∀x.q) \vdash ∀x.p∧q$,

   • $∃x.p∧q \vdash (∃x.p) ∧ (∃x.q)$,

   • $∃x.p∧q \vdash (∃x.p) ∧ q$ si $x$ n’est pas libre dans $q$,

   • $∃x.∀y.p \vdash ∀y.∃x.p$,

   • $∃x.p→q \vdash (∀x.p) → (∃x.q)$,

   • $¬∃x.p \vdash ∀x.¬p$,

   • $¬∀x.p \vdash ∃x.¬p$,

2. On veut montrer que $φ = ∃x.∀y.P(x)→P(y)$ est un théorème. Pour aider la compréhension, on va procéder par étapes, en utilisant des arguments pas tout à fait formels.

   • On interprète nos simboles comme des entiers, et le symbole $P$ comme le prédicat « $x$ est pair ». Donner une preuve formelle pour $φ$.
   • On reste dans les entiers, mais cette fois-ci on interprète $P$ comme le prédicat « $x ≤ 0 ∨ x ≥ 0$ » (toujours vrai). Donner une preuve formelle pour $φ$.
   • Donner maintenant une preuve formelle complète pour $φ$ (indépendamment de l’interprétation choisie).

Systèmes à la Hilbert

Nous utilisons maintenant seulement deux règles d’inférences, l’hypothèse et le modus ponens (la règle hypothèse est légèrement modifiée afin de rendre les preuves plus courtes):

$$\frac{}{\Gamma, p \vdash p}H,\qquad\qquad \frac{\Gamma \vdash p\to q \qquad \Gamma\vdash p}{\Gamma \vdash q}M,$$

et la liste (infinie) d’axiomes

1. $p\to( q\to p)$,
2. $(\neg p\to\neg q)\to( q\to p)$,
3. $( p \to ( q\to r)) \to (( p\to q) \to ( p\to r))$,
4. $\neg\neg p \to p$,
5. $p\to p$,
6. $( q\to p)\to(\neg p\to\neg q)$.

Chaque axiome donne lieux à une règle permettant de l’introduire ; par exemple, le premier axiome donne la règle

$$\frac{}{\Gamma \vdash p\to(q\to p)}\mathrm{Ax}_1.$$

Les axiomes 1-3 sont dus à Łukasiewicz, les autres sont redondants (dans le sens qu’ils pourraient être dérivés des trois premiers), mais nous les ajoutons pour simplifier les preuves.

1. Prouver que $A\vdash B\to A$.

2. Prouver que $\neg B\vdash B\to A$.

3. Prouver le raisonnement par contrapposée: $A\to B, \neg B \vdash \neg A$.

4. On va montrer que d’une proposition fausse on peut déduire n’importe quoi. Nous choisissons $A\wedge\neg A$ comme proposition fausse.

   • Calculez sa table de vérité et vérifiez qu’elle est bien une antilogie.
   • Dans notre logique nous avons fait le choix d’utiliser seulement les symboles $\to$ et $\neg$. En utilisant les équivalences bien connues, transformez $A\wedge\neg A$ en une formule équivalente qui n’utilise que $\neg$ et $\to$. Vérifiez que les deux formules sont bien équivalentes à l’aide des tables de vérité.
   • Montrez que $\neg(A\to A)\vdash B$.