Logique & Démonstration

Introduction à la logique propositionnelle

Une logique pour exprimer des propositions

Une proposition

C’est une phrase, une formule, une affirmation, qui peut être vraie ou fausse

  • ✅ “Il fait beau”
  • ✅ “Si je suis un génie ou si je travaille bien, alors je n’irai pas au rattrapage”
  • ✅“42+0=42”
  • ✅ “\(p\to (p\land (r\lor \lnot q))\)”
  • ✅“42-0=58”
  • ✅“Le serveur est ouvert aux inscriptions”
  • ❌ “Allons à la pêche !”
  • ❌ “42 + 12”
  • ❌ “salade, tomates, oignons”
  • ❌ “Le serveur”
  • ❌ “Le serveur est-il ouvert aux inscriptions ?”

Construire des propositions

Les briques de base : les propositions atomiques

  • Les propositions Atomiques : du grec α-τομοσ (a-tomos), “ce qui ne peut être divisé”
  • Il peut y en avoir un nombre arbitraire (mais les propositions sont toujours de phrases finies)

Les assemblages : les propositions composées

  • Sont construites avec des propositions déjà constituées (soit atomiques, soit composées)
  • Se font avec les connecteurs logiques (en gérénal : “et”, “ou”, “non”, “implique”)
  • C’est un procédé inductif

Quelques règles pour l’écriture des formules

Important

Attention au parenthésage

Astuce

Dessiner ses formules comme des arbres

Exprimer des états

Theorem  démarrage_partie :
  ((serveur_ouvert \/ sandbox_ouvert) /\ connexion_ok)
    -> partie_peut_démarrer.
Theorem ouverture_serveur :
  ((connexion_internet=true) /\ login_registered /\ passwd_ok 
  /\ espace_dispo > 0 /\ (~ ban))
      -> serveur_ouvert.  
def transferer_fichier(connecte, admin, abonnement_actif, banni):
    assert connecte and (admin or (abonnement_actif and not banni))
    # ... transfert du fichier

Prouver des formules propositionnelles

Pourquoi
  • Identifier les théorèmes de la logique
  • Voir à quelles conditions certains états sont réalisés
  • Certifier les programmes
Comment
  • Tables de vérité
  • Déduction naturelle
  • Rocq (déduction naturelle automatisée)

TL;DR : Les conditions de vérité des connecteurs logiques

Conjonction : \(\land\)

\(A \land B\) est vrai si \(A\) et \(B\) sont vraies, sinon c’est faux.

Disjonction : \(\lor\)

\(A \lor B\) est faux si \(A\) et \(B\) sont fausses, sinon c’est vrai.

Négation : \(\lnot\)

\(\lnot A\) est vraie si \(A\) est fausse, et inversement.

Implication : \(\to\)

\(A\to B\) est fausse si \(A\) est vraie et \(B\) est fausse. Sinon c’est vrai.

Implication \(\neq\) causalité

  • \(p\) : Typhee gagne la compétition.
  • \(q\) : Typhee perd son battle.

“Si Typhee a gagné la compétition, alors c’est qu’il n’a pas perdu son battle”

❌ \(\lnot q \to p\)

✅ \(p\to \lnot q\)

“Si ma famille habite dans le Loir-Et-Cher, alors \(\sqrt{2}\) est irrationnel”

On se teste !

Les tables de vérité

  • Un tableau que l’on peut remplir algorithmiquement
  • Une table à connaître pour chaque connecteur
  • Permet de déterminer automatiquement si les formules sont :
    • des tautologies (toujours vraies)
    • des antilogies (toujours fausses)
    • équivalentes (mêmes conditions de vérité)

Les constantes

(À apprendre par ❤️)

\(\top\)

est toujours vraie

\(\bot\)

est toujours fausse

  • \(\lnot \bot\)
  • \(\bot\to(\bot\lor p)\)
  • \(\lnot \top \lor (p\land\bot)\)

Dans la suite du cours :

  • Une nouvelle méthode pour prouver des théorèmes
  • Une nouvelle logique pour parler de propriétés et d’individus
  • La preuve par logiciel