Définitions

Une formule φ est la 'conséquence logique' d'un ensemble de formules Γ si toute valuation donnant la valeur VRAI à toutes les formules de  Γ
entraînent la valeur VRAI pour φ.
Autrement dit il est impossible pour toutes les formules de   Γ d'être vraies
sans que φ soit elle-même vraie.
Notation :
Γ |= φ
exemple : Γ  = { P∧Q , Q⇒(¬R)}
φ = ¬R
Bien qu'il existe de nombreux moyens plus simples de s'en apercevoir on peut par exemple dresser une table de vérité avec 8 lignes.
Cela revient à dire que si
Γ = {φ12, ...,φn}
φ1∧φ2∧...∧φn⇒φ est une tautologie.
Un 'raisonnement' (argumentation) consiste en une liste de propositions appelée 'prémisses' suivie d'une proposition appelée 'conclusion'.
Le raisonnement est dit 'valide' si  C est une conséquence logique de Γ ={P1,...,Pn}
Pour établir la validité d'un raisonnement on peut :

Le fait qu'un raisonnement soit valide n'entraîne nullement que sa conclusion soit vraie.

La conclusion n'est vraie que si le raisonnement est valide et que toutes les prémisses sont vraies.

Nous allons voir ci-après une liste de raisonnements élémentaires simples ( Modus Ponens, Modus Tollens, Raisonnement par l'absurde) d'usage courant.

Café Python

Voici un programme qui effectue une vérification de preuve.