Équivalence des formules bien formées
Formules équivalentes :
Deux formules sont équivalentes quand elles ont même valeur dans toutes interprétation (notation : A ≡ B).
Fondamental : Règle de substitution uniforme
Soit la formule φ contenant les atomes p1, p2, . . ., pn. Soit la formule φ∗ obtenue en substituant aux atomes p1, p2, . . ., pn les formules 1, 2, . . ., n. Alors si ╞ φ, on a ╞ φ∗.
Propriété des formules équivalentes
Soient A, B et C trois formules bien formées.
╞ [(A ∧ B) ≡ (B ∧ A)] commutativité
╞ [(A ∨ B) ≡ (B ∨ A)] . . .
╞ [(A ≡ B) ≡ (B ≡ A)] . . .
╞ [((A ∧ B) ∧ C) ≡ ((A ∧ (B ∧ C))] associativité
╞ [((A ∨ B) ∨ C) ≡ (A ∨ (B ∨ C))] . . .
╞ [((A ≡ B) ≡ C) ≡ (A ≡ (B ≡ C))] . . .
╞ [((A ∧ B) ∨ C) ≡ ((A ∨ C) ∧ (B ∨ C))] distributivité
╞ [((A ∨ B) ∧ C) ≡ ((A ∧ C) ∨ (B ∧ C))] . . .
╞ [(A ∧ (A ∨ B)) ≡ A] absorption
╞ [(A ∨ (A ∧ B)) ≡ A] . . .
╞ [(A ∧ A) ≡ A] idempotence
╞ [(A ∨ A) ≡ A] . . .
╞ [¬(A ∧ B) ≡ (¬A ∨ ¬B)] lois de Morgan
╞ [¬(A ∨ B) ≡ (¬A ∧ ¬B)] . . .
╞ [(A → B) ≡ (¬A ∨ B)] implication
╞ [(A → B) ≡ ¬(A ∧ ¬B)] . . .
╞ [(A ≡ B) ≡ ((A → B) ∧ (B → A))] équivalence
╞ [(A ≡ B) ≡ ((A ∧ B) ∨ (¬A ∧ ¬B))] . . .
╞ [(A → B) ≡ (¬B → ¬A)] contraposition
╞ [(A → (B → C)) ≡ ((A → B) → (A → C))] auto-distributivité
╞ [(A → (B → C)) ≡ (B → (A → C))] import-export
╞ [((A → B) ∧ (B → C)) ≡ (A → C)] transitivité