Exercices de déduction naturelle en logique propositionnelle

Exo 1

Pour chaque séquent ci-dessous, s'il vous paraît sémantiquement correct, proposez une preuve en déduction naturelle à l'aide de FitchJS puis transcrivez la dans ce format (exemples). Sinon, proposez un contre-modèle.
  1. p ∧ r, r ∧ s ⊢ p ∧ s
  2. q, q → ¬ r ⊢ ¬r ∨ t
  3. p, q, (p ∧ q) ↔ r ⊢ r
  4. p, ¬ q ⊢ r
  5. r ∧ s, p, (p ∨ q) → ¬ r ⊢ ⊥

Exo 2

Pour chaque séquent ci-dessous, s'il vous paraît sémantiquement correct, proposez une preuve en déduction naturelle à l'aide de FitchJS puis transcrivez la dans ce format (exemples). Sinon, proposez un contre-modèle.
  1. p ∨ q ⊢ p ∧ q
  2. p ∧ q ⊢ p ∨ q
  3. p, ¬ q, (q ↔ p) ⊢ ¬ r
  4. t → r ⊢ (p ∧ t) → r
  5. p ↔ q, r ⊢ p ↔ (q ∧ r)
  6. p, ¬ r ⊢ ¬ (p → r)
  7. p ∨ q, p → r, ¬ q ⊢ r
  8. ¬ p → q, ¬ q ∧ ¬ r ⊢ p

Exo 3

Pour chaque séquent ci-dessous, s'il vous paraît sémantiquement correct, proposez une preuve en déduction naturelle à l'aide de FitchJS puis transcrivez la dans ce format (exemples). Sinon, proposez un contre-modèle.
  1. q, q→r, q↔s ⊢ (p ∨ r) ∧ s
  2. p, p → q, r ∧ s ⊢ (q ∧ r) ∨ (q ∧ s)
  3. ¬ s ⊢ ¬(s ∧ r)
  4. p ∧ ¬ s, r → s, r ⊢ ⊥
  5. q ↔ ¬ r, p ⊢ q → (¬ r ∧ p)
  6. q → r ⊢ (p ∧ q) → (p ∧ r)
  7. p ∨ q, r, q → (p ∧ r) ⊢ p ∧ r
  8. (q∨ r) → p, r, ¬p ⊢ q
  9. ¬ t, s → t ⊢ t ↔ s
  10. (q ∧ r) ∨ (t ∧ r), ¬ r ⊢ ¬ t

Exo 4

Pour chaque séquent ci-dessous, s'il vous paraît sémantiquement correct, proposez une preuve en déduction naturelle à l'aide de FitchJS puis transcrivez la dans ce format (exemples). Sinon, proposez un contre-modèle.
  1. p ∨ q ⊢ q ∨ p
  2. p → q, q→r, p ⊢ r
  3. p→ (q ∨ r), p, ¬ q, ⊢ r
  4. p→ (q ∨ r), ¬ q, ¬ r ⊢ ¬ p
  5. ¬ p, p↔ q ⊢ ¬ q
  6. (r ∨ q) → t, (t ∧ q) → r, q ⊢ t ↔ r
  7. ¬(r → p), (r ∨ q) → p ⊢ q
  8. p → (q ∧ r), ¬ (q ∧ r) ⊢ ¬ p
  9. p ∨ r, p → q, r ↔ s ⊢ q∨ s
  10. ¬(p → q)⊢ p ∧ ¬ q
  11. p ∧ ¬ q ⊢ ¬(p → q)
  12. (p ∨ ¬ p) → q ⊢ q
  13. p ∧ ¬ p ⊢ ⊥
  14. ¬ p → q ⊢ p ∨ q
  15. (p → q) → r, ¬ r ⊢ p ∧ ¬ q
  16. p ∧ (¬ q → r), p → ¬ r ⊢ q
  17. (p → q)∧(q → p) ⊢ p↔q
  18. p↔q ⊢ (p → q)∧(q → p)
  19. p ∧ ¬ q ⊢ ¬(p ↔q)
  20. p∧q ⊢ p ↔ q
  21. (p → q) → (r → s), ¬ s ∨ ¬ q, p→ q ⊢ ¬ r ∨ ¬ p
  22. p ∧ r, ¬ s → ¬ p, p ⊢ r ∧ s
  23. (p → s)∨(p → (q∧r)), p ⊢ r∨s

Exo 5

Pour chaque tautologie ci-dessous, proposez une preuve en déduction naturelle à l'aide de FitchJS puis reproduisez la manuellement sur papier en utilisant les conventions du format Fitch (exemples).
  1. p → (q → p)
  2. (p∧r)→(p∧r)
  3. ¬ (p ∧ ¬ p)
  4. p ↔ ¬ ¬ p
  5. (¬ p → p) → p

Exo 6

Pour chaque équivalence logique ci-dessous (notez qu'elles sont exprimées en méta-langage logique car ≡ n'est pas un opérateur officiel du langage), proposez une preuve en déduction naturelle pour chacun des deux séquents associés à l'aide de FitchJS puis reproduisez les manuellement sur papier en utilisant les conventions du format Fitch (exemples).
  1. (p → q) ≡ ¬ ( p∧ ¬ q)
  2. (p → q) ∧ (q → p) ≡ p ↔ q
  3. p ≡ ¬ ¬ p
  4. (p → q) ∧ (¬ p → q) ≡ q

Exo 7

Pour chaque déduction naturelle arborescente de ce PDF, déterminez les prémisses, les hypothèses (chargées lorsqu'elles sont entre []), l'endroit où ces hypothèses sont déchargées, les règles de déduction naturelle utilisées, le séquent ainsi prouvé puis transcrivez cette déduction en notation de Fitch à l'aide de FitchJS.

Exo 8

Vous trouverez ci-dessous quatre raisonnements informels en langage naturel concernant les lois de De Morgan. Traduisez-les en FitchJS. Par opposition aux déductions natuelles en notation de Fitch, notez la concision des arguments en langage naturel qui masque souvent des formes de raisonnement non explicites — l'élimination de la disjonction, par exemple — qui peuvent être autant de sources d’erreurs dans les justifications informelles.
  1. ¬(p∨q) ⊢ ¬p∧¬q
    Supposons p. Alors nous avons p∨q, ce qui contredit la prémisse. Donc nous déduisons ¬p. Nous avons de même ¬q d'où la conclusion.
    Indication : 10 lignes de FitchJS.
  2. ¬p ∧ ¬q ⊢ ¬(p∨q)
    D'après la prémisse, nous avons ¬p et ¬q. Montrons ¬(p∨q) par l'absurde, en supposant p∨q. Si p est vrai, il y a contradiction. Idem pour q. CQFD.
    Indication : 10 lignes de FitchJS.
  3. ¬p ∨ ¬q ⊢ ¬(p∧q)
    Supposons ¬ p. Montrons ¬(p∧q) par l'absurde en supposant p∧q. Alors p est vrai ce qui contredit ¬p, d'où ¬(p∧q). De même, en supposant ¬q, nous déduisons ¬(p∧q). Dans les deux cas de figure, nous obtenons la conclusion.
    Indication : 12 lignes de FitchJS.
  4. ¬(p∧q) ⊢ ¬p∨¬ q
    Supposons la négation de la conclusion. Montrons p par l'absurde. Comme ¬p, ¬p∨¬q, ce qui contredit notre supposition. De même nous avons q et a fortiori p∧q, ce qui contredit la prémisse. Donc la conclusion est valide.
    Indication : 16 lignes de FitchJS.

Exo 9

Considérez la loi du tiers exclu et sa preuve en déduction naturelle. Donnez une version FitchJS de cette preuve. Puis reformulez cette dernière en français, dans le style des raisonnements informels de l'exercice 8.

Valid XHTML 1.0 Transitional