Introduction aux règles de déduction logique

📋 Plan du Cours

1. Démonstration et utilisation des connecteurs
2. Notation H ⊢ P et état de la preuve
3. Implication : modus ponens et récurrence
4. Conjonction : introduction et éliminations
5. Disjonction : introduction et raisonnement par cas
6. Équivalence : double implication
7. Négation : introduction, double négation et absurde
8. Quantificateur universel : démonstration et condition
9. Quantificateur existentiel : introduction et utilisation
10. Règles Lean : tactiques et correspondances
11. Implication en Lean : intro, apply et specialize
12. Conjonction en Lean : constructor et And.left

📖 1. Démonstration et utilisation des connecteurs

🔑 Notions clés & Définitions

• Déduction naturelle : Méthode de preuve qui organise les raisonnements en règles d’introduction et d’élimination des connecteurs logiques.
• Règles de démonstration : En déduction naturelle, règles qui permettent d’établir un nouveau fait dont le connecteur principal est introduit.
• Règles d’utilisation : En déduction naturelle, règles qui permettent d’exploiter une hypothèse ou un théorème dont le connecteur principal est déjà présent.
• Introduction et élimination : Terminologie alternative en déduction naturelle où « introduction » remplace « démonstration » et « élimination » remplace « utilisation ».
• Turnstile : Symbole logique ` utilisé pour séparer les hypothèses courantes de l’énoncé à démontrer dans une notation de preuve.