LOGIQUE PROPOSITIONNELLE'alphabet'

Définition (alphabet). L'alphabet de la logique propositionnelle est constitué de

un ensemble dénombrable ATM de variables propositionnelles (ou formules atomiques, ou encore atomes)
les connecteurs FALSE , ~ , & , v , ->
les séparateurs (ou parenthèses) ( et )
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

si A est une formule atomique alors A est une formule
FALSE est une formule
(~A) est une formule si A est une formule
(A & B) est une formule si A et B sont des formules
(A v B) est une formule si A et B sont des formules
(A -> B) est une formule si A et B sont des formules
Exemples de formules

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 , ~ , & , v , -> . 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)