Définition (alphabet). L'alphabet de la logique propositionnelle est constitué de
Notation. Nous utilisons p, q, r, p1, p2 ,... pour des variables propositionnelles.
Définition (formule). L'ensemble FOR des formules (ou formules bien formées) de la logique propositionnelle est le plus petit ensemble de mots construits sur l'alphabet tel que
Notation. Nous utilisons A , B , C , A1 , A2,... pour des formules (strictement parlant, A,B,... sont des metavariables, car ils ne font pas partie de l'alphabet de la logique). S , S1 , S2 ,... dénotent des ensembles de formules.
Remarque.
Notre jeu de connecteurs primitifs consiste en
FALSE , ~ , ∧ , ∨ , -> .
D'autres connecteurs peuvent être définis en tant que abréviations :
TRUE abrévie (~FALSE)
et l'équivalence
(A <-> B) abrévie ((A -> B) ∧ (B -> A)) .
(Annexe : remarque
sur des jeux de connecteurs alternatifs)
Définition (sous-formule). L'ensemble des sous-formules d'une formule A est le plus petit ensemble tel que
Définition (substitution uniforme).
Une substitution
(ou substitution uniforme) associe
à une variable propositionnelle p une formule A .
Elle est notée [p\A].
L'application de [p\A] à une formule B ,
notée (B)[p\A],
est le résultat du remplacement simultané de toutes
les occurrences de p dans B par A.
(A)[p\B] est appelé une instance de A.
Exemples de substitutions
Notation. On omet toujours les parenthèses les plus à l'extérieur. En général, l'omission de parenthèses peut être source d'ambiguïtés : ainsi, ~p ∧ q peut correspondre à (~p) ∧ q et à ~(p ∧ q) . Cependant, on peut omettre la plupart des parenthèses en donnant des priorités aux connecteurs, dans l'ordre suivant : <-> , -> , ∧ , ∨ , ~ . La négation ~ est le connecteur le plus fort : il `attire plus les parenthèses' que ∨, etc. Ainsi, ~p ∨ q correspond à (~p) ∨ q , etc.
Annexe : remarque sur une définition plus constructive de FOR
Annexe : rappel sur les démonstrations par induction
Définition (interprétation). Une interprétation I (ou valuation) est une application de l'ensemble des variables propositionnelles ATM dans l'ensemble des valeurs de vérité {0,1}.
Définition (interprétation des formules). Une interpretation donnée I peut être étendue à l'ensemble des formules FOR par :
Définition (validité, satisfiabilité).
Soit A une formule.
A est valide (ou tautologique ; noté |= A) si
I(A) = 1 pour toute interpretation I.
Sinon A est invalide ou falsifiable.
A est satisfiable ssi
il existe une interpretation I t.q. I(A) = 1.
Sinon A est insatisfiable ou contradictoire.
Exemples
Définition (conséquence logique).
Une formule A
est conséquence logique de
A1, ... ,An
(noté A1, ... ,An |= A)
ssi tout modèle de A1, ... ,An
est un modèle de A.
Exemples ;
plus sur la conséquence logique
Définition (axiomatique à la Hilbert). Les schémas d'axiome de la logique propositionnelle sont
A -> (B -> A)
(A -> B) -> ((A -> (B -> C)) -> (A -> C))
A -> (B -> A ∧ B)
(A ∧ B) -> A
(A ∧ B) -> B
A -> A ∨ B
B -> A ∨ B
(A -> C) -> ((B -> C) -> (A ∨ B -> C))
(A -> B) -> ((A -> ~B) -> ~A)
~~A -> A
~FALSE
A et A -> B sont appelées prémisses, et
B est appelée conclusion de la règle.
(Rappel :
on omet les parenthèses selon les priorités
suivantes : <-> , -> , ∧ , ∨ , ~ .)
Chaque formule qui a la forme d'un schéma est appelée un axiome.
Ainsi, un axiome est une
instance
d'un schéma.
P.ex. (p ∧ q) -> (r -> (p ∧ q)) est un axiome,
obtenu à partir du premier schéma A -> (B -> A).
Annexe :
remarque
sur une axiomatisation qui n'a pas besoin de la notion de schéma
(nécessitant une règle de substitution uniforme)
Définition (preuve). Soit A une formule. Une preuve de A est une liste finie de formules (A1, ... ,An) t.q.
Définition (prouvabilité, consistance).
Soit A une formule.
A est prouvable
(noté |- A) si
il existe une preuve de A.
A est consistante si
~A n'est pas prouvable.
Sinon A est inconsistante.
Exemples
Définition (déduction). Une déduction d'une formule A à partir d'hypothèses B1,...,Bm (noté B1,...,Bm |- A) est une liste finie de formules (A1, ... ,An) t.q.
Donc une preuve est une déduction à partir d'un ensemble vide d'hypothèses.
Parfois
les axiomes sont appellées `axiomes logiques', et
les hypothèses `axiomes non-logiques'.
Annexe : remarque sur des ensembles d'hypothèses infinis
Lemme (la règle de modus ponens préserve la validité). Si |= A et |= A -> B alors |= B.
Lemme
(la substitution uniforme
préserve la validité).
Soient A et B des formules et p un atome.
Si |= A alors
|= A[p\B].
(cf. la remarque
sur une axiomatisation avec une règle de substitution uniforme
dans la section sur la
théorie de la preuve)
Théorème d'adéquation.
Si |- A alors |= A.
(la démonstration utilise les lemmes précédents, et le fait que les axiomes sont valides)
Théorème de complétude.
Si |= A alors |- A.
(la démonstration est difficile)
Théorème de déduction. A |- B ssi |- A -> B.
Donc le problème de déduction A |- B peut être réduit au problème de prouvabilité |- A -> B .
Théorème de la conséquence logique (version sémantique du théorème de déduction). A |= B ssi |= A -> B.
Donc le problème de conséquence logique A |= B
peut être réduit au problème
de validité |= A -> B .
Annexe :
théorèmes d'adéquation et de complétude forte
(non pas entre validité et prouvabilité,
mais entre conséquence logique et déduction)
Théorème (existence d'une procédure de décision). La logique propositionnelle est décidable : il existe une procédure effective qui pour toute formule A en entrée s'arrête et retourne `oui' si A est valide, et `non' sinon.
Un exemple de procédure de décision est la
méthode des tables de vérité.
Une méthode plus efficace est la
méthode de balayage.
L'axiomatique est une caractérisation finie des formules valides :
elle peut être `rendue opérationelle' comme
procédure énumerant l'ensemble des formules prouvables.
Mais ceci ne nous donne qu'une procédure de semi-décision :
si la formule en question est valide, cette procédure va la trouver un jour,
mais si elle ne l'est pas alors la procédure ne s'arrêtera jamais.
Remarque. Étant donné les théorèmes d'adéquation et de complétude, les propriétés qui suivent peuvent être formulées et en termes de prouvabilité (avec |-) et en termes de validité (avec |=).
Théorème (remplacement des équivalences).
Soit B une sous-formule de A, et
soit |- B <-> C .
Si A' est obtenue à partir de A
par le remplacement de cette occurrences de
B par C
alors |- A <-> A'.
Exemples d'application
Remarque. Le remplacement en question n'est pas une substitution uniforme (cette dernière ne s'applique qu'aux atomes, et non à des formules ; de plus, elle s'applique à toutes les occurrences, et non à une ou plusieurs).
Définition (littéral, clause, forme normale conjonctive).
Un littéral est une
formule atomique ou la négation d'une formule atomique.
Une clause est une disjonction de littéraux.
Une formule est en forme normale conjonctive
si elle est une conjonction de clauses.
Exemples
Notation. Nous utilisons L, L1 , L2 ... pour des littéraux, et C, C1 , C2 ... pour des clauses.
Notation.
On suppose que les
disjonctions et conjonctions sont parenthésées à gauche :
une clause L1 ∨ L2 ∨ ... ∨ Ln est
((...(L1 ∨ L2) ∨ ...) ∨ Ln), et
une conjonction de clauses C1 ∧ C2 ... ∧ Cm est
((...(C1 ∧ C2) ...) ∧ Cm).
Ceci est justifié par
l'associativité de
la conjonction et de la disjonction
(v. aussi les exemples).
Par convention,
une disjonction de 0 littéraux est FALSE (la clause vide), et
une conjonction de 0 clauses est TRUE.
Notation.
Nous confondons une conjonction de clauses avec un ensemble de clauses, et
une clause avec un ensemble de littéraux.
Ceci est justifié par
la commutativité et l'idempotence de
la conjonction et de la disjonction.
Ainsi, la formule en forme normale conjonctive
(p ∨ q) ∧ (~p ∨ r)
sera confondu avec l'ensemble
{ {p ∨ q} , {~p ∨ r} }.
La clause vide FALSE sera confondu avec l'ensemble vide
{}.
Théorème.
Pour toute entrée A, l'algorithme
de mise en forme normale conjonctive s'arrête.
Il retourne une formule en forme normale conjonctive
équivalente à l'entrée.
(la démonstration utilise le théorème de la substitution
des équivalents :
les remplacements effectués par l'algorithme
correspondent à des équivalences prouvables)
Théorème. Une formule en forme normale conjonctive est valide ssi toute clause contient deux littéraux contradictoires, c-à-d chaque clause est de la forme L1 ∨ ... ∨ p ∨ ... ∨ ~p ∨ ... ∨ Ln.
Remarque. La liste des équivalences utilisées n'est pas complète : on a supposé tacitement que la commutativité de ∧ et de ∨ est exploité.
Remarque. Les exemples montrent que le choix de l'atome à substituer est crucial (une heuristique possible est de choisir l'atome qui a le plus d'occurrences dans A).
Théorème.
Pour tout entrée A, l'algorithme
de balayage s'arrête.
Il retourne TRUE si A est valide,
et FALSE sinon.
Démonstration.
La terminaison est assurée par le fait que
chaque passage de la boucle élimine un atome.
Ensuite, comme
|= A ssi |= (A[p\TRUE] ∧ A[p\FALSE]),
la deuxième étape préserve la validité.
Finalement, les simplifications correspondent à des
équivalences valides.
Remarque. L'équivalence A <-> (A[p\TRUE] ∧ A[p\FALSE]) n'est pas valide (exemple : A = p).