A término es un "nombre": las variables y las constantes son términos.
Y los términos se pueden fabricar utilizando símbolos de función.
Ejemplo: $n$ es una variable, $0$ es una constante y $+$ es un símbolo de función (binario).
Así, $n,0$ y $n+0$ son términos.
Fórmulas son declaraciones.
Las fórmulas atómicas son los componentes básicos de las declaraciones de fabricación.
Son fórmulas que no tienen subpartes que sean fórmulas.
Se fabrican con predicado símbolos, como por ejemplo $\text {Even}(x)$ , la igualdad y los términos.
Así, $\text {Even}(n), 0=0$ y $n+0=n$ son fórmulas atómicas.
Con las conectivas y los cuantificadores podemos escribir fórmulas más complejas, como $\forall n (n+0=n)$ y $0=0 \to \forall n (n+0=n)$ .
En cuanto al ejemplo, debido a que ""hay 1" es un cuantificador numérico y su tratamiento es un poco complicado, utilizaré "hay al menos una moto a la que le queda x cantidad de combustible".
Podemos analizarlo con los predicados $\text {Bike}(y)$ expresando "y es una bicicleta" y $\text {FuelLeft}(y,x)$ que expresa "a y le queda una cantidad x de combustible".
El enunciado completo se escribirá utilizando el cuantificador existencial para "hay al menos uno" ( $\exists$ ) y el conectivo "y" ( $\land$ ):
$\exists y \ (\text {Bike}(y) \land \text {FuelLeft}(y,x))$ .
En esta fórmula, $\text {Bike}(y)$ y $\text {FuelLeft}(y,x)$ son fórmulas atómicas, mientras que $(\text {Bike}(y) \land \text {FuelLeft}(y,x))$ es una fórmula no atómica.
