Exercices de déduction naturelle en logique du premier ordre

L'extension de la déduction naturelle propositionnelle au premier ordre nécessite une règle d'introduction et une règle d'élimination pour chaque quantificateur, plus deux règles pour l'égalité, cf. la page de FitchJS, onglet Reference, item Rules for Quantificational Logic. Voici quelques exemples simples.

Emploi des règles d'élimination et d'introduction des quantificateurs

        Problem: (Ax)Px ⊢ (Ay)Py
        1  |_  (Ax)Px    Premise
        2  | |_  c       Flag
        3  | |   Pc      1  AE
        4  |   (Ay)Py    2-3  AI

        Problem: (Ex)Px ⊢ (Ey)Py
        1  |_  (Ex)Px      Premise
        2  | |_  Pc        Assumption
        3  | |   (Ey)Py    2  EI
        4  |   (Ey)Py      1,2-3  EE

Emploi des règles d'élimination et d'introduction de l'égalité

        Problem:  ⊢ a=a
        1    a=a    =I

        Problem: a=b ⊢ b=a
        1  |_  a=b    Premise
        2  |   a=a    =I
        3  |   b=a    1,2  =E

        Problem: a=b, b=c ⊢ a=c
        1  |   a=b    Premise
        2  |_  b=c    Premise
        3  |   a=c    2,1  =E

        Problem: Pa, a=b ⊢ Pb
        1  |   Pa     Premise
        2  |_  a=b    Premise
        3  |   Pb     2,1  =E

Exo 1

Pour chaque séquent ci-dessous, justifiez informellement qu'il est valide puis proposez une déduction naturelle à l'aide de FitchJS et des indications et débuts de preuve ci dessous.

p(a), q(a) ⊢ ∃ x (p(x) ∧ q(x))
∀ x p(x) ∧ ∀ x q(x)⊢∀ x (p(x)∧q(x))
p(b)⊢∃ x (p(x) ∨ q(x))
⊢ ¬ ∃ x (p(x) ∧ ¬ p(x))
¬ ∃ x (p(x) ∧ ¬ q(x)) ⊢p(a) → q(a)
∃ x (p(x) ∧ q(x))⊢∃ x p(x) ∧ ∃ x q(x)
∃ x ∀ y r(x,y)⊢ ∀ y ∃ x r(x,y)
∀ x (p(x) ∨ ¬ q(x)), q(b)⊢p(b)
∀ x (p(x) ∧ q(x))⊢∀y p(y) ∧∀z q(z)
∃ x (p(x) ∨ q(x)), ∀ x ¬ q(x)⊢∃ x p(x)

Indications :
1. &I, EI. 2. Préparer le AI final par l'introduction d'une constante c distinguée, puis construire Pc & Qc. 3. vI, EI. 4. Supposer la conclusion sans négation, aboutir à # et conclure. 5. Supposer Pa puis ~Qa pour finalement conclure par >I. 6. Démarrer par Pc & Qc comme hypothèse, conclure par EE. 7. Préparer le AI final par l'introduction d'une constante distinguée d suivie de l'hypothèse (Ay)Rcy. 8. Eliminer le quantificateur universel en introduisant(Pb v Qb), conclure par élimination de ce v. 9. Construire (Ay)Py puis (Az)Qz et conclure. 10. Démarrer par l'hypothèse (Pc v Qc) et conclure (Ex)Px par vE de ce v suivie d'un EE appliqué à la première prémisse.

--------------------------------------
Problem: Pa, Qa |- (Ex)(Px & Qx)
1  |   Pa    Premise
2  |_  Qa    Premise
--------------------------------------
Problem: ((Ax)Px & (Ax)Qx) |- (Ax)(Px & Qx)
1  |_  ((Ax)Px & (Ax)Qx)    Premise
--------------------------------------
Problem: Pb |- (Ex)(Px v Qx)
1  |_  Pb    Premise
--------------------------------------
Problem:  |- ~(Ex)(Px & ~Px)
1  |_  (Ex)(Px & ~Px)    Assumption
--------------------------------------
Problem: ~(Ex)(Px & ~Qx) |- (Pa > Qa)
1  |_  ~(Ex)(Px & ~Qx)    Premise
--------------------------------------
Problem: (Ex)(Px & Qx) |- ((Ex)Px & (Ex)Qx)
1  |_  (Ex)(Px & Qx)    Premise
--------------------------------------
Problem: (Ex)(Ay)Rxy ⊢ (Ay)(Ex)Rxy
1  |_  (Ex)(Ay)Rxy    Premise
--------------------------------------
Problem: (Ax)(Px v ~Qx), Qb ⊢ Pb
1   |   (Ax)(Px v ~Qx)    Premise
--------------------------------------
Problem: (Ax)(Px v ~Qx), Qb |- Pb
1  |   (Ax)(Px v ~Qx)    Premise
2  |_  Qb                Premise
--------------------------------------
Problem: (Ax)(Px & Qx) ⊢ ((Ay)Py & (Az)Qz)
1   |_  (Ax)(Px & Qx)        Premise
--------------------------------------
Problem: (Ex)(Px v Qx), (Ax)~Qx ⊢ (Ex)Px
1   |   (Ex)(Px v Qx)    Premise
2   |_  (Ax)~Qx          Premise
--------------------------------------

Exo 2

Examinez les deux déductions du verso de ce PDF. Expliquez informellement le sens et la validité des séquents puis précisément le détail des preuves.

Exo 3

Pour chaque séquent ci-dessous, déterminez informellement s'il est valide ou pas. Si vous pensez qu'il est valide, proposez une déduction naturelle à l'aide de FitchJS. Si vous pensez qu'il n'est pas valide, proposez un contre-exemple, i.e., une interprétation qui valide les prémisses mais pas la conclusion.

∀ x p(x) ⊢ p(a) ∧ p(b)
∃ x q(x) ⊢ q(a) ∨ q(b)
q(a) ∨ q(b) ⊢ ∃x q(x)
¬ p(c) ⊢ ∀ y ¬ p(y)
∀ x p(x), ∀ x (p(x)→ q(x)) ⊢ q(a)
∀ x p(x), ∀ x (p(x)→ q(x)) ⊢ ∀ x q(x)
p(b), ∃ x p(x) → ∃ x q(x) ⊢ q(b)
¬ ∃ x ¬(q(x) ∨ p(x)), ¬ p(c) ⊢ q(c)
¬ ∃ y q(y), ∀ y (p(y) → q(y)) ⊢ ¬ ∃ y p(y)
∃ x p(x), ∀ x (¬ p(x) ∨ q(x)) ⊢ ∀ x q(x)
∃ x p(x), ∃ x q(x) ⊢ ∃ x (p(x) ∧ q(x))
∃ x p(x), ∀ x( p(x) → ¬ q(x)) ⊢ ¬ ∃ x q(x)
∃ x q(x), ∀ x(q(x) ↔ p(x))⊢∃ x (p(x) ∨ r(x))
∃ y (p(y) ∨ ¬ q(y)), q(a) ∨ q(b)⊢ ∃ y ¬ p(y)

Exo 4

Donnez les preuves FitchJS des vingt premières équivalences de ce PDF :

∀ x p ⊢ p
p ⊢ ∀ x p
∃ x p ⊢ p
p ⊢ ∃ x p
∀ x (p(x) ∧ q(x)) ⊢ ∀ x p(x) ∧ ∀ x q(x)
∀ x p(x) ∧ ∀ x q(x) ⊢ ∀ x (p(x) ∧ q(x))
∃ x (p(x) ∨ q(x)) ⊢ ∃ x p(x) ∨ ∃ x q(x)
∃ x p(x) ∨ ∃ x q(x) ⊢ ∃ x (p(x) ∨ q(x))
∃ x (p(x) → q(x)) ⊢ ∃ x (¬ p(x) ∨ q(x))
∃ x (¬ p(x) ∨ q(x)) ⊢ ∃ x (p(x) → q(x))
∀ x p(x) ⊢ ∀ y p(y)
∃ x p(x) ⊢ ∃ y p(y)
∀ x (p(x)∧q) ⊢ ∀ x p(x)∧q
∀ x p(x)∧q ⊢ ∀ x (p(x)∧q)
∃ x (p(x)∧q) ⊢ ∃ x p(x)∧q
∃ x p(x)∧q ⊢ ∃ x (p(x)∧q)
¬ ∀ x p(x) ⊢ ∃ x ¬ p(x) Indication : s'inspirer de ¬(p∧q) ⊢ ¬p∨¬ q
∃ x ¬ p(x) ⊢ ¬ ∀ x p(x) Indication : s'inspirer de ¬p∨¬q ⊢ ¬(p∧q)
¬ ∃ x p(x) ⊢ ∀ x ¬ p(x) Indication : s'inspirer de ¬(p∨q) ⊢ ¬p∧¬q
∀ x ¬ p(x) ⊢ ¬ ∃ x p(x) Indication : s'inspirer de ¬p∧¬q ⊢ ¬(p∨q)

Exo 5

Montrez informellement puis via FitchJS la validité des déductions suivantes.

Socrate est un humain. Or tout humain est mortel. Donc Socrate est mortel.
Tout être humain est un primate. Les dauphins ne sont pas des primates. Il y a des dauphins qui sont intelligents. Par conséquent, on peut ne pas être un être humain et être intelligent.
Les amis d'amis sont amis. L'amitié est réciproque. J'ai un ami. Donc je suis mon propre ami.

Exo 6

Montrez informellement puis via FitchJS la validité de la déduction suivante.
Un dragon est heureux si tous ses enfants peuvent voler. Les dragons verts peuvent voler. Un dragon est vert si au moins un de ses parents est vert. Donc les dragons verts sont heureux.
Question subsidiaire : quelles sont les options d'un dragon rose pour être heureux ?

Exo 7

Le principe du buveur. On considère un bar avec au moins une personne (par exemple le barman). Montrez informellement puis via FitchJS la validité de la propriété suivante : il y a une personne dans le bar telle que si cette personne boit, tout le monde boit. Autrement dit, on prend une photo de tout le bar. Sur cette photo, on peut toujours identifier une personne qui, si elle boit, tout le monde boit.
Indications : On introduit une relation unaire p(x) qu'on interprète par "x boit". Il faut montrer que la formule ∃x (p(x) → ∀y p(y)) est valide.
Informellement : On considère une interprétation I quelconque de domaine non-vide D. Ou bien il existe x tel que p est faux. Conclure dans ce cas. Ou bien p est toujours vrai. Conclure dans ce cas. Enfin, conclure en général.
Syntaxiquement : Démarrer sur la loi du tiers exclu sur la formule ∀y p(y) ou bien sur la formule ∃x ¬p(x).
Voir également Wikipedia.