Version sans JavaScript, en lecture seule : les ateliers, les quiz et l’exécution du code n’y sont pas. Version complète · Catalogue · Se connecter
Feuille d'exercices 6
La déduction naturelle
Écrire des preuves à la Fitch, des plus directes à celles qui demandent le raisonnement par l'absurde, et relier preuve et vérité. Chapitre 6.
Les preuves s'écrivent comme au chapitre 6 : une ligne par formule, avec sa justification ; une hypothèse provisoire ouvre une boîte (│), la règle qui la décharge la ferme.
Corrigé
1.
| # | Formule | Justification |
|---|---|---|
| 1 | │ $p$ | supposé |
| 2 | $p \to p$ | $\to_i$ 1 à 1 |
2.
| # | Formule | Justification |
|---|---|---|
| 1 | $p \land q$ | hypothèse |
| 2 | $q$ | $\land_{e2}$ 1 |
| 3 | $p$ | $\land_{e1}$ 1 |
| 4 | $q \land p$ | $\land_i$ 2, 3 |
3.
| # | Formule | Justification |
|---|---|---|
| 1 | │ $p$ | supposé |
| 2 | │ │ $q$ | supposé |
| 3 | │ │ $p$ | réitération de 1 |
| 4 | │ $q \to p$ | $\to_i$ 2 à 3 |
| 5 | $p \to (q \to p)$ | $\to_i$ 1 à 4 |
On a le droit de recopier une ligne d'une boîte extérieure encore ouverte (réitération).
Corrigé
1.
| # | Formule | Justification |
|---|---|---|
| 1 | $p \to (q \to r)$ | hypothèse |
| 2 | │ $p \land q$ | supposé |
| 3 | │ $p$ | $\land_{e1}$ 2 |
| 4 | │ $q$ | $\land_{e2}$ 2 |
| 5 | │ $q \to r$ | $\to_e$ 1, 3 |
| 6 | │ $r$ | $\to_e$ 5, 4 |
| 7 | $p \land q \to r$ | $\to_i$ 2 à 6 |
2.
| # | Formule | Justification |
|---|---|---|
| 1 | $p \land q \to r$ | hypothèse |
| 2 | │ $p$ | supposé |
| 3 | │ │ $q$ | supposé |
| 4 | │ │ $p \land q$ | $\land_i$ 2, 3 |
| 5 | │ │ $r$ | $\to_e$ 1, 4 |
| 6 | │ $q \to r$ | $\to_i$ 3 à 5 |
| 7 | $p \to (q \to r)$ | $\to_i$ 2 à 6 |
Une fonction qui prend une paire $(a, b)$ équivaut à une fonction qui prend $a$ et rend une fonction qui attend $b$ : c'est la curryfication, courante en programmation fonctionnelle.
Corrigé
1.
| # | Formule | Justification |
|---|---|---|
| 1 | $p \to q$ | hypothèse |
| 2 | │ $\lnot q$ | supposé |
| 3 | │ │ $p$ | supposé |
| 4 | │ │ $q$ | $\to_e$ 1, 3 |
| 5 | │ │ $\bot$ | $\lnot_e$ 4, 2 |
| 6 | │ $\lnot p$ | $\lnot_i$ 3 à 5 |
| 7 | $\lnot q \to \lnot p$ | $\to_i$ 2 à 6 |
2.
| # | Formule | Justification |
|---|---|---|
| 1 | $p \lor q$ | hypothèse |
| 2 | │ $p$ | supposé (cas 1) |
| 3 | │ $q \lor p$ | $\lor_{i2}$ 2 |
| 4 | │ $q$ | supposé (cas 2) |
| 5 | │ $q \lor p$ | $\lor_{i1}$ 4 |
| 6 | $q \lor p$ | $\lor_e$ 1, 2 à 3, 4 à 5 |
3.
| # | Formule | Justification |
|---|---|---|
| 1 | $\lnot(p \lor q)$ | hypothèse |
| 2 | │ $p$ | supposé |
| 3 | │ $p \lor q$ | $\lor_{i1}$ 2 |
| 4 | │ $\bot$ | $\lnot_e$ 3, 1 |
| 5 | $\lnot p$ | $\lnot_i$ 2 à 4 |
| 6 | │ $q$ | supposé |
| 7 | │ $p \lor q$ | $\lor_{i2}$ 6 |
| 8 | │ $\bot$ | $\lnot_e$ 7, 1 |
| 9 | $\lnot q$ | $\lnot_i$ 6 à 8 |
| 10 | $\lnot p \land \lnot q$ | $\land_i$ 5, 9 |
Corrigé
1.
| # | Formule | Justification |
|---|---|---|
| 1 | $\lnot\lnot p$ | hypothèse |
| 2 | │ $\lnot p$ | supposé |
| 3 | │ $\bot$ | $\lnot_e$ 2, 1 |
| 4 | $p$ | RAA 2 à 3 |
2.
| # | Formule | Justification |
|---|---|---|
| 1 | │ $\lnot(p \lor \lnot p)$ | supposé |
| 2 | │ │ $p$ | supposé |
| 3 | │ │ $p \lor \lnot p$ | $\lor_{i1}$ 2 |
| 4 | │ │ $\bot$ | $\lnot_e$ 3, 1 |
| 5 | │ $\lnot p$ | $\lnot_i$ 2 à 4 |
| 6 | │ $p \lor \lnot p$ | $\lor_{i2}$ 5 |
| 7 | │ $\bot$ | $\lnot_e$ 6, 1 |
| 8 | $p \lor \lnot p$ | RAA 1 à 7 |
- Pour $p \vdash \lnot\lnot p$, la conclusion est une négation : on suppose $\lnot p$, on obtient $\bot$ avec $p$, et $\lnot_i$ conclut. Dans les deux autres preuves, la conclusion n'est pas une négation, et aucune hypothèse n'est contradictoire : aucune autre règle ne permet de conclure. La logique sans RAA s'appelle la logique intuitionniste. On y démontre (résultat admis) que ni $\lnot\lnot p \to p$ ni $p \lor \lnot p$ ne sont prouvables.
Corrigé
- Soit $v$ qui rend vraies les hypothèses et $A \lor B$. Alors $A$ ou $B$ est vraie dans $v$. Si c'est $A$, $v$ rend vraies les hypothèses et $A$, donc $C$ ; sinon $B$, de même. Dans les deux cas $v \vDash C$.
- Non. L'interprétation $p = 0, q = 1$ rend $p \to q$ vraie et $q \to p$ fausse : $p \to q \not\vDash q \to p$. Par la correction, $p \to q \not\vdash q \to p$.