Lógica de primer orden

La lógica de predicados de orden 1 es la más común ya que cubre las necesidades de la mayoría de usuarios. Es como LP0, pero incluye el uso de variables, cuantificadores ($\forall$ y $\exists$), y nuevas reglas de deducción natural para estos dos. Pero, claro, las variables tienen un dominio posible, una asignación, puede haber constantes, las fórmulas se pueden unificar, skolemizar, y maltratar de muchas otras maneras que antes no teníamos.

Por todo esto, la LP1 es suficiente para formalizar la teoría de conjuntos, y por tanto casi toda la matemática, excepto algunos temas de topología.

El problema es que, a diferencia de LP0, la lógica de primer orden no es decidible. No hay ningún procedimiento de decisión que nos permita decir, para una fórmula $P$, si $P$ es válida o no. Este resultado lo encontraron de forma independiente Church y Turing.

Y para la validez, el problema de la decisión es semidecidible. Tal como dice el teorema de la completitud de Gödel del 1929, cualquier fórmula que sea lógicamente válida es demostrable. Así demostró la completitud de LP1, haciendo un gran favor a todos (Hilbert había demostrado la completitud de LP0, pero con LP1 no pudo).