Jeux de connecteurs primitifs

Le langage de la logique propositionnelle (Lp) est donc maintenant construit sur: Nous avons défini les deux derniers ( implication et équivalence) au moyen des 3 premiers.
Le jeu de connecteurs ¬, ∧, ∨ peut donc être considéré comme 'primitif' en ce sens que toute formule peut être remplacée par une formule équivalente ne comportant que ces trois opérateurs.
Mais sachant que ¬(P∨Q) ≡ ((¬P)∧(¬Q)) et que ¬(P∧Q) ≡ ((¬P)∨(¬Q)), on peut, si on veut, prendre comme jeu de connecteurs primitif soit ¬, ∧, soit ¬,  ∨
C'est à dire que toute formule est équivalente à une formule ne comportant que les connecteurs ¬ et ∨ ou bien que les connecteurs ¬ et ∧ .
On peut même si on veut être vraiment minimaliste, reconstruire toutes les formules avec seulement:
Dans ce cas ¬P est défini comme P⇒Faux
et P∨Q est défini comme : (P⇒Faux)⇒Q
Ces remarques conduisent à l'existence pour toute formule de formes dites 'normales'. Ces formes servent pour les démonstrations automatiques.

Forme normale conjonctive

Définitions (littéral, clause, forme normale conjonctive):
Nous admettrons que toute formule admet une forme normale conjonctive.
La démonstration sort du cadre de cet exposé.
Le lecteur interessé pourra se rapporter à la littérature existante ainsi qu'à la description des algorithmes de résolution.

Forme normale disjonctive

Définitions (littéral, clause, forme normale disjonctive):
Nous admettrons que toute formule admet une forme normale disjonctive.
(Même remarque que précédemment)