Théorie de la preuve (démonstration)
Les tables de vérité (approche sémantique) permettent de décider si un énoncé est une tautologie, une contradiction ou ni l'une ni l'autre. Mais, une bonne partie de la logique que nous verrons par la suite, une telle méthode, ne peut pas lui être appliquée. En conséquence une autre approche, dite déductive, basée sur la formalisation de la théorie est proposée.
Pour spécifier notre système du calcul propositionnel formel nous avons besoin d'avoir :
Un alphabet (l'ensemble des symboles utilisés)
Un ensemble de suites finies de ces symboles qui sont appelées formules bien formées. Ce sont les phrases du langage formel.
Un ensemble fini de formules appelées axiomes
Un ensemble fini de règles : les règles de déduction.
Logique propositionnelle
