Como el desarrollo histórico y las aplicaciones de la lógica de primer orden están muy ligados a la matemática, en lo que sigue se hará una introducción que contemple e ilustre esta relación, tomando ejemplos tanto de la matemática como del lenguaje natural.
Solo se ocupa de estudiar el modo en que hablamos y razonamos con expresiones lingüísticas.
En la lógica de primer orden, los predicados son tratados como funciones.
Por ejemplo, la oración «Caín mató a Abel» se puede formalizar así: O abreviando: Este procedimiento se puede extender para tratar con predicados que expresan relaciones entre muchas entidades.
Por ejemplo, la oración «Ana está sentada entre Bruno y Carlos» puede formalizarse: Una constante individual es una expresión lingüística que refiere a una entidad.
Por ejemplo «Marte», «Júpiter», «Caín» y «Abel» son constantes de individuo.
Además de las constantes individuales que hacen referencia a entidades determinadas, la lógica de primer orden cuenta con otras expresiones, las variables, cuya referencia no está determinada.
Las variables generalmente se representan con letras minúsculas cerca del final del alfabeto latino, principalmente la x, y y z. Del mismo modo, en la matemática, la x en la función f(x) = 2x no representa ningún número en particular, sino que es algo así como un espacio vacío donde se pueden insertar distintos números.
Por supuesto, al igual que con las constantes individuales, las variables sirven también para formalizar relaciones.
Sin embargo, también es posible dar un valor de verdad a la expresión si se le antepone un cuantificador.
[7] Esta maquinaria se puede adaptar fácilmente para formalizar oraciones con cuantificadores del lenguaje natural.
Combinando las conectivas con los predicados, constantes, variables y cuantificadores, es posible formalizar oraciones como las siguientes: Considérese el siguiente argumento clásico: La tarea de la lógica de primer orden consiste en determinar por qué los argumentos como este resultan válidos.
Para eso, el primer paso es traducirlos a un lenguaje más preciso, que pueda ser analizado mediante métodos formales.
Según lo visto más arriba, la formalización de este argumento es la siguiente: A continuación se define un lenguaje formal, Q, y luego se definen axiomas y reglas de inferencia sobre ese lenguaje que dan como resultado el sistema lógico SQ.
Para facilitar la lectura, se suelen omitir las comillas y utilizar distintas letras cerca del comienzo del alfabeto latino, con o sin subíndices, para distinguir nombres distintos: a, b, c, d, e, a1, a3, c9, etc. Una variable (o variable individual) es una x seguida de una o más comillas.
Para facilitar la lectura, se suelen omitir las comillas y utilizar distintas letras cerca del final del alfabeto latino, con o sin subíndices, para distinguir variables distintas: x, y, z, x1, x3, z9, etc. Un functor es una f seguida de uno o más asteriscos, y luego de una o más comillas.
Para facilitar la lectura, se suelen omitir los asteriscos y las comillas y utilizar distintas letras del alfabeto latino cerca de la f, con o sin subíndices, para distinguir functores distintos: f, g, h, f1, f3, h9, etc. Un predicado es una P seguida de uno o más asteriscos, y luego de una o más comillas.
Para facilitar la lectura, se suelen omitir los asteriscos y las comillas y utilizar distintas letras en mayúscula a lo largo del alfabeto latino para distinguir predicados distintos: P, A, B, C, S, T, etc.
En ese caso, y pasa a estar ligada por un cuantificador universal, porque la nueva fórmula es:
Pero esta fórmula ya no dice de un término que es máximo, sino algo muy distinto.
Dicho de una manera más general, si t es un término y
es una fórmula que posiblemente contiene a x como una variable libre, entonces
Sean A, B y C fórmulas bien formadas de Q.
Sean A y B fórmulas bien formadas de Q con como máximo una variable libre, x.
Sea t un término cerrado y A(x/t) el resultado de reemplazar toda aparición de x en A por t. Luego, los siguientes son axiomas lógicos: Intuitivamente, el cuarto axioma dice que lo que vale para todos vale para cualquiera.
Por ejemplo, un caso particular del axioma podría ser: «Si todos son mortales, entonces Abel es mortal»; o también: «Si todos son mortales, entonces el padre de Mateo es mortal» El quinto axioma es análogo al axioma K de la lógica modal, y un caso particular del mismo podría ser: «Si todos los humanos son mortales, entonces, si todos son humanos, todos son mortales.» Una interpretación es un par
Este estudio proporciona una visión de la utilidad del cálculo como herramienta deductiva.
Este resultado fue alcanzado de manera independiente por Alonzo Church en 1936 y por Alan Turing en 1937, dando así una respuesta negativa al Entscheidungsproblem planteado por David Hilbert en 1928.
Por otra parte, la lógica de primer orden monádica (con o sin identidad) es decidible, como lo demostró Leopold Löwenheim en 1915.
El teorema fue demostrado por primera vez por Kurt Gödel como una consecuencia del teorema de completitud, pero con el tiempo se han encontrado varias demostraciones adicionales.