Lògica de primer ordre

La lògica de predicats d'ordre 1 és la més comuna ja que cobreix les necessitats de la majoria d'usuaris. És com LP0, però inclou l'ús de variables, quantificadors ($\forall$ i $\exists$), i noves regles de deducció natural per a aquests dos. Però, és clar, les variables tenen un domini possible, una assignació, pot haver-hi constants, les fórmules es poden unificar, skolemitzar, i maltractar de moltes altres maneres que abans no teníem.

Per tot això, la LP1 és suficient per formalitzar la teoria de conjunts, i per tant gairebé tota la matemàtica, excepte alguns temes de topologia.

El problema és que, a diferència de LP0, la lògica de primer ordre no és decidible. No hi ha cap procediment de decisió que ens permeti dir, per a una fórmula $P$, si $P$ és vàlida o no. Aquest resultat el van trobar de manera independent Church i Turing.

I per a la validesa, el problema de la decisió és semidecidible. Tal com diu el teorema de la completesa de Gödel del 1929, qualsevol fórmula que sigui lògicament vàlida és demostrable. Així va demostrar la completesa de LP1, fent un gran favor a tots (Hilbert havia demostrat la completesa de LP0, però amb LP1 no va poder).