(sous-formule)Logique propositionnelle .

Définition (sous-formule). L'ensemble des sous-formules d'une formule A est le plus petit ensemble tel que

A est une sous-formule de A.
Si (~B) est une sous-formule de A alors B est une sous-formule de A.
Si (B & C) est une sous-formule de A alors B et C sont des sous-formules de A.
Si (B v C) est une sous-formule de A alors B et C sont des sous-formules de A.
Si (B -> C) est une sous-formule de A alors B et C sont des sous-formules de A.
L'endroit où une sous-formule apparaît est son occurrence.
Exemples de sous-formules
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 souvent omettre les parenthèses en donnant des priorités aux connecteurs, dans l'ordre suivant : <-> , -> , & , v , ~ . Ainsi, ~p & q correspond à (~p) & q , etc.

Annexe : rappel sur les démonstrations par induction

Annexe : remarque sur une définition plus constructive de FOR