Una fórmula que no contiene conectivos lógicos (como ∧, ∨, →, ¬) ni cuantificadores; en lógica de primer orden una fórmula atómica (átomo) es típicamente un símbolo de predicado aplicado a una tupla de términos (incluyendo átomos de igualdad), sirviendo como bloque indivisible para construir fórmulas complejas.

Principio

Las fórmulas atómicas representan aserciones elementales sobre términos; las oraciones complejas se forman combinando átomos con conectivos lógicos y cuantificadores, y muchos sistemas de prueba reducen el razonamiento a manipulaciones de átomos (p. ej., la resolución opera sobre cláusulas construidas a partir de átomos y sus negaciones).

Demostración

En la lógica de primer orden, expresiones como P(a,b) o x = y (una vez instanciadas las variables) son fórmulas atómicas; en contraste, P(a) ∧ Q(a) no es atómica porque combina dos átomos mediante un conectivo.

Aplicación incorrecta

Tratar una oración compuesta como R(x) ∨ S(y) o una expresión cuantificada ∀x P(x) como atómica en procedimientos que requieren átomos (por ejemplo, pasar una fórmula no atómica a un algoritmo que espera átomos cerrados) conduce a errores.

Consecuencia

Los átomos proporcionan los elementos base para formas normales sintácticas (forma normal conjuntiva/disyuntiva, cláusulas) y para razonamiento automatizado: identificar y manipular átomos es crucial para unificación, resolución, construcción de modelos y métodos de tableau.

Inversión

Una fórmula molecular es la inversión: cualquier fórmula construida aplicando conectivos o cuantificadores a átomos, cuyo significado depende de la composición y cuyo comportamiento lógico no se reduce a una sola aplicación de predicado.

Límite

En lógica proposicional las fórmulas atómicas son variables proposicionales; en lógica de primer orden los átomos incluyen aplicaciones de predicado y la igualdad; algunas lógicas extendidas añaden conectivos integrados o átomos de orden superior, lo cual cambia lo que se considera atómico.

Tensión semántica

Surge tensión entre 'fórmula atómica' y 'enunciado atómico' (la primera puede contener variables libres mientras que el segundo está cerrado), y entre átomos ground (sin variables) usados en model checking y átomos generales en cálculos de prueba.

Síntesis

Una fórmula atómica es la aserción irreducible en un lenguaje lógico: un predicado (o igualdad) aplicado a términos, formando la base a partir de la cual se construyen fórmulas complejas, formas normales y procedimientos de razonamiento automatizado.