Ahora vamos a decir unas palabras sobre inferencia en la lógica de predicados. Vamos a ilustrar la deducción natural, para después decir unas palabras sobre completez y validez. Las reglas de inferencia de la deducción natural son una generalización de las que vimos para la lógica proposicional. Tenemos, ahora, que dar reglas para la eliminación y la introducción de cuantificadores. Vamos a ver las del cuantificador universal. Podemos eliminar un cuantificador universal instanciando, es decir, si algo es cierto para todo valor posible de "x", entonces también es cierto para un valor en particular de "x". Esto es similar a la regla de eliminación de la conjunción. La introducción del cuantificador universal es un poco más delicada. Se encierra en un rectángulo una demostración auxiliar, que empieza por introducir un valor arbitrario "x0", que no debe ocurrir fuera del rectángulo. Si podemos terminar con una fórmula alfa, con ocurrencias de "x0", entonces, aunque "x0" sea un valor particular, como fue arbitrario, podemos reescribir alfa con el parámetro "x" en lugar del valor particular "x0". Esto es similar a la introducción de la conjunción que deduce alfa y beta a partir de alfa y de beta, aunque son sólo dos fórmulas. Usamos este torniquete para indicar inferencia. Gödel demostró en 1929, que la lógica de predicados es correcta y completa, que es un resultado positivo. En contraste, el problema de validez y, por lo tanto, el de satisfactibilidad también, son indecidibles, que es un resultado negativo. Es decir, no existe ni va a existir nunca un algoritmo que decida si una fórmula arbitraria de primer orden es satisfactible o no. Church y Turing demostraron este resultado, independientemente, en 1936 y 1937. Recordemos que el problema SAT que vimos en lógica proposicional es NP-completo, lo que significa que actualmente sólo tenemos algoritmos que toman un tiempo exponencial. Ahora que tenemos una lógica más expresiva, es natural que resulte un problema más difícil que en la lógica proposicional.