Formule atomique
En logique mathématique, une formule atomique ou atome est une formule qui ne contient pas de sous-formules propres. La structure d'une formule atomique dépend de la logique considérée, p. ex. en logique des propositions, les formules atomiques sont les variables propositionnelles.
Les atomes sont les formules les plus simples dans un système logique et servent à construire les formules les plus générales. Ainsi, les formules bien formées dans un système logique sont définies récursivement, en donnant les règles pour créer des formules bien formées à partir d'autres formules bien formées, les formules atomiques servant de point de départ à la construction récursive.
À partir des formules atomiques, on crée, dans les logiques où il existe une négation, des formules très simples qui sont appelées des littéraux ; ce sont soit des formules atomiques, soit des négations de formules atomiques. Ainsi, si les formules s'écrivent a et la négation s'écrit ¬, les littéraux sont soit a, soit ¬a.