La lógica de primer orden (LPO, First-order logic en inglés) o cálculo de predicados de primer orden' es un sistema de la lógica matemática que extiende la lógica proposicional y a su vez es extendida por la lógica de segundo orden.

Las sentencias atómicas de la lógica de primer orden tienen la forma P(t₁, ... ,t_n) (un predicado con uno o más términos) en vez de las letras proposicionales como en la lógica proposicional. Usualmente, esto se escribe sin los paréntesis o comas.

Lo nuevo que tiene la lógica de primer orden que no está presente en la lógica proposicional es la cuantificación: si φ es cualquier sentencia, se introducen las nuevas construcciones ∀x φ y ∃x φ, que se leen "para todo x, φ" y "existe x, tal que φ". En la explicación usamos φ como φ(x). φ(a) representa el resultado de reemplazar todas las apariciones libres de x en φ(x) con a. Luego, ∀x φ(x) significa que φ(a) es verdadero para cualquier valor de a y ∃x φ significa que existe un a tal que φ(a) es verdadero. Los valores de las variables se toman del universo dado. Un refinamiento de la lógica de primer orden permite que las variables tomen valores de diferentes conjuntos.

La lógica de primer orden tiene suficiente poder expresivo para la formalización de casi toda la matemática. Una teoría de primer orden consiste de un conjunto de axiomas (usualmente finitos o recursivamente numerables) y las declaraciones o statements deducibles de ellos. La teoría de conjuntos usual (Zermelo-Frankel) es un ejemplo de teoría de primer orden. Además, es generalmente aceptado que toda la matemática clásica puede ser formalizada en esta teoría. Hay otras teorías que comunmente se formalizan independientemente en lógica de primer orden como la aritmética de Peano.

Definiendo la lógica de primer orden

---

El cálculo de predicados consiste de

• reglas de formación (i.e. definiciones recursivas para formar fórmulas bien formadas)
• reglas de transformación (i.e. reglas de inferencia para derivar teoremas)
• un conjunto (posiblemente infinito numerable) de axiomas o axiomas esquema

Los axiomas considerados aquí son los axiomas lógicos los cuales son parte del cálculo de predicados. Más adelante se agregan axiomas no-lógicos en teorías de primer orden específicas: no se consideran verdades de la lógica pero sí verdades de una teoría particular.

Cuando el conjunto de axiomas es infinito, se requiere de un algoritmo que pueda decidir para una fórmula bien formada si es un axioma o no. Más aún, debería existir un algoritmo que pueda decidir si la aplicación de una regla de inferencia es correcta o no.

Es importante notar que el cálculo de predicados puede ser formalizado de varias formas diferentes. No existe nada canónico sobre los axiomas y reglas de inferencia aquí dadas, pero cualquier formalización produce los mismos teoremas de la lógica (y deducir los mismos teoremas de cualquier conjunto de axiomas no-lógicos).

Vocabulario

---

El "vocabulario" se compone de

1. Un conjunto de variables de predicado (or relaciones) cada una con cierta aridad ≥1, que se denotan habitualmente con letras máyusculas P, Q, R, ...
2. Un conjunto de constantes, habitualmente denotadas con letras minúsculas a, b, c, ...
3. Un conjunto de funciones, cada una con cierta aridad ≥ 1, la cuales se denotan habitualmente con letras minúsculas f, g, h, ...
4. Un conjunto infinito de variables, habitualmente denotadas por letras minúsculas x, y, z, ...
5. Operadores lógicos (o conectivos): : ¬ ("no" lógico), ∧ ("y" lógico), ∨ ("o" lógico), → (implicación), ↔ (si y sólo si).
6. Símbolos que denotan los cuantificadores: ∀ (cuantificación universal), ∃ (cuantificación existencial).
7. Paréntesis izquierdo y derecho.
8. A veces, pero no siempre, se incluye un símbolo de identidad o igualdad = .

Hay varias variaciones menores listadas a continuación:

• El conjunto de símbolos primitivos (operadores y cuantificadores) a veces varía. Algunos símbolos pueden ser omitidos como primitivos y tomados como abreviatura. por ejemplo (P ↔ Q) es una abreviatura para (P → Q) ∧ (Q → P). Por otro lado, es posible incluir otros operadores como primitivos, como la constante de verdad ⊤ ("top") para "verdadero" y la constante de falsedad ⊥ ("bottom") para "falso" (estos operadores tienen aridad 0), la barra de Sheffer (Sheffer stroke) (P | Q). El mínimo número de símbolos primitivos requeridos es uno, pero si nos restringimos a los operadores listados anteriormente necesitamos tres, por ejemplo ¬, ∧, and ∀ son suficientes.
• Algunos libros y papers más antiguos usan la notación φ ⊃ ψ para φ → ψ, ~φ para ¬φ, φ & ψ para φ ∧ ψ, y numerosas notaciones para los cuantificadores; por ejemplo, ∀x φ puede estar escrito como (x)φ.
• La igualdad a veces se considera parte de la lógica de primer orden. En ese caso, el símbolo de igualdad se incluye en el vocabulario y se comporta sintácticamente como un predicado binario. Este caso se llama a veces lógica de primer orden con igualdad.
• Las constantes en realidad son funciones de aridad 0, de esta manera puede ser posible omitir las constantes y permitir a las funciones tener cualquier aridad. Sin embargo, tradicionalmente se usa el término "función" sólo para funciones de aridad mayor o igual a 1.
• En la definición anterior las relaciones deber tener aridad mayor o igual que 1. Es posible permitir relaciones de aridad 0; estas podrían ser consideradas como variables proposicionales.
• Hay diferentes convenciones acerca de dónde poner los paréntesis; por ejemplo, una podría ser ∀x o (∀x). A veces se usan dos puntos (:) o punto (.) en vez de parentesis para desambiguar fórmulas. Una notación interesante pero poco usual es la notación polaca, donde se omiten todos los paréntesis, y se escribe ∧, ∨, delante de los argumentos en vez de entre ellos. La notación polaca es compacta pero poco común por ser difícil para ser leída por los humanos.
• Una observación técnica es que si existe un símbolo de función de aridad 2 representando el par ordenado (o símbolo de predicado de aridad 2 representando la relación) no se necesitan funciones y predicados de aridad mayor que 2.

Usualmente se considera que el conjunto de constantes, funciones y relaciones forman un lenguaje, mientras que las variables, los operadores lógicos y cuantificadores se los considera pertenecientes a la lógica. Por ejemplo, el lenguaje de la teoría de grupos consiste de una constante (el elemento identidad), una función de aridad 1 (la inversa), una función de aridad 2 (el producto), y una relación de aridad 2 (la igualdad), omitida por los autores que incluyen la igualdad en la lógica subyacente.

Reglas de formación

---

Las reglas de formación definen los términos, fórmulas y las variables libres en ellas de la siguiente manera.

Un conjunto de términos es definido recursivamente por las siguientes reglas:

1. Cualquier constante es un término (sin variables libres)
2. Cualquier variable es un término (cuya única variable libre es sí misma)
3. Cualquier expresión f(t₁,...,t_n) de n≥1 argumentos (donde cada argumento t_i es un término y f es un símbolo de función de aridad n) es un término. Sus variables libres son las variables libres de cualquiera de los términos t_i.
4. Cláusula de clausura: ninguna otra cosa es un término.

El conjunto de fórmulas bien formadas (usualmente llamadas fbf, en inglés wff, o simplemente fórmulas) son definidas recursivamente por las siguientes reglas:

1. Predicados simples y complejos Si P es una relación de aridad n ≥ 1 y los a_i son términos entonces P (a₁,...,a_n) es bien formado. Sus variables libres son la variables libres de cualquiera de sus términos a_i. Si se considera la igualdad parte de la lógica, entonces (a₁ = a₂) está bien formada. Todas esas fórmula se llaman atómicas.
2. Cláusula Inductiva I: Si φ es una fórmula bien formada, entonces ¬ φ es una fórmula bien formada. Sus variables libres son las variables libres de φ.
3. Cláusula Inductiva II: Si φ y ψ son fórmulas bien formadas, entonces (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) son fórmulas bien formadas. Sus variables libres son las variables libres de φ or ψ.
4. Cláusula Inductiva III: Si φ es una fórmula bien formada, ∀ x φ y ∃ x φ son fórmulas bien formadas, pudiéndose usar cualquier otra variable en lugar de x. Sus variables libres son las variables libres de φ or ψ otra que x. Cualquier instancia de x (u otra variable reemplazando x en esta construcción) se dice ligada (no libre) en ∀ x φ y ∃ x φ.)
5. Cláusula de clausura: Ninguna otra cosa es una fórmula bien formada.

En la práctica, si P es una relación de aridad 2, habitualmente se escribe "a P b" en vez de "P a b"; por ejemplo, 1 < 2 en vez de <(1, 2). Análogamente si f es una función de aridad 2, a veces escribimos "a f b" en vez de "f(a, b)"; por ejemplo, escribimos 1 + 2 en vez de +(1, 2). También es común omitir algunos paréntesis si esto no conduce a una ambigüedad.

A veces es útil expresar que "P(x) se cumple para exactamente un x". Esto se nota habitualmente:

∃!x P(x)

También puede ser expresado como: ∃x (P(x) ∧ ∀y (P(y) → (x = y)))

Substitución

---

Si t es un término y φ(x) es una fórmula posiblemente conteniendo x como una variable libre entonces φ(t) se define como el resultado de reemplazar todas las apariciones libres de x por t, suponiendo que ninguna variable libre en t se vuelva ligada en este proceso. Si alguna variable libre de t se volviera libre, entonces para substituir t por x se necesita cambiar los nombres de las variables ligadas de φ por otros que no coincidan con las variables libres de t. Para ver por qué esta condición es necesaria, consideremos la fórmula φ(x) dada por ∀y y≤x ("x es máximo"). Si t es un término sin y como variable libre, entonces φ(t) dice que t es máximo. Sin embargo, si t es y la fórmula φ(y) es ∀y y≤y lo cual no dice que y es máximo. El problema es que la variable libre y de t (=y) se volvió ligada al substituir y por x φ(x). Luego para formar φ(y) primero debemos cambiar la variable libre y de φ por otra cosa, digamos z. Así φ(y) es entonces ∀z z≤y. Olvidar esta condición es una notoria causa de errores.

Ejemplos: El lenguaje de los grupos abelianos ordenados tiene una constante 0, una función unaria −, una función binaria +, y una relación binaria ≤. Así

• 0, x, y son términos atómicos
• +(x, y), +(x +(y (−z))) son términos, usualmente notado como x + y, x + (y + (−z))
• +(x, y) = 0, ≤ +(x +(y (−z))) +(x, y) son fórmulas atomicas, usualmente notado como x + y = 0, x + y−z ≤ x + y,
• (∀x ∃y ≤ +(x y) z) ∧ (∃x +(x, y) = 0) es una fórmula, usualmente notado como (∀x ∃y x + y ≤ z) ∧ (∃x x + y = 0).

Igualdad

---

Hay varias convenciones diferentes para usar la igualdad (o identidad) en la lógica de primer orden. Esta sección resume las principales. Todas las convenciones dan esencialmente los mismos resultados y difieren principalmente en la terminología.

• La convención más común para igualdad es incluir el símbolo de igualdad como un símbolo lógico primitivo y agregar los axiomas de igualdad a los axiomas de la lógica de primer orden. Los axiomas de igualdad son:

x = x

x = y → f(...,x,...) = f(...,y,...) para cualquier función f

x = y → (P(...,x,...) → P(...,y,...)) para cualquier relación P (incluyendo la igualdad)

• La siguiente convención más común es incluir el símbolo de igualdad como una de las relaciones de la teoría y agregar los axiomas de igualdad a la teoría. En la práctica esta convención es casi indistinguible de la anterior, salvo en el caso inusual de las teorías sin noción de igualdad. Los axiomas son los mismos. La única diferencias es que unos se llaman axiomas lógicos y los otros axiomas de la teoría.
• En las teorías sin funciones y con un número finito de relaciones, es posible definir la igualdad en términos de las relaciones. Esto se hace definiendo que dos términos s y t son iguales si y sólo si ninguna relación presenta cambios reemplazando s por t en cualquier argumento. Por ejemplo, en teoría de conjuntos con una relación ∈, definiríamos s = t como una abreviatura para ∀x (s ∈ x ↔ t ∈ x) ∧ ∀x (x ∈ s ↔ x ∈ t). Esta definición de igualdad automáticamente satisface los axiomas de igualdad.
• En algunas teorías es posible dar definiciones ad hoc para igualdad. Por ejemplo, en una teoría de órdenes parciales con una relación ≤ podríamos definir s = t como una abreviatura para s ≤ t ∧ t ≤ s.

Reglas de Inferencia

---

La regla de inferencia modus ponens es la única requerida de la lógica proposicional para la formalización dada aquí. Esto indica que si se prueba φ y φ → ψ, entonces se puede deducir ψ.

La regla de inferencia llamada Generalización universal es característica del cálculo de predicados. Se puede expresar como

si $\backslash vdash\; \backslash phi$ entonces $\backslash vdash\; \backslash forall\; x\; \backslash ,\; \backslash phi$

donde φ es un teorema del cálculo de predicados ya probado.

Nótese que la regla de generalización es análoga a la regla de necesidad de la lógica modal, que es:

si $\backslash vdash\; P$ entonces $\backslash Box\; P$

Axiomas de cuantificadores

---

Los siguientes cuatro axiomas lógicos caracterizan un cálculo de predicados:

• PRED-1: (∀x Z(x)) → Z(t)
• PRED-2: Z(t) → (∃x Z(x))
• PRED-3: (∀x (W → Z(x))) → (W → ∀x Z(x))
• PRED-4: (∀x (Z(x) → W)) → (∃x Z(x) → W)

Estos son en realidad axiomas esquema: la expresión W representa cualquier fbf en la cual x no está libre y la expresión Z(x) representa cualquier fbf con la convención aditional que Z(t) representa el resultado de substituir el término t por x en Z(x).

Cálculo de predicados

---

El cálculo de predicados es una extensión del cálculo proposicional que define qué es demostrable en lógica de primer orden. Es un sistema formal usado para describir teorías matemáticas. Si el cálculo proposicional se define con un adecuado conjunto de axiomas y la regla de inferencia modus ponens (hay varias formas de hacerlo), entonces el cálculo de predicados se puede definir agregando algunos axiomas adicionales y la regla de inferencia "generalización universal". En particular, para el cálculo de predicados tomamos:

• Todas las tautologías del cálculo proposicional (con las variables proposicionales reemplazadas por fórmulas).
• Los axiomas para cuantificadores dados.
• Los axiomas para igualdad dados, cuando se desea tener la igualdad como concepto lógico.

De esta manera, una sentencia es demostrable en lógica de primer orden si se puede obtener comenzando con los axiomas del cálculo de predicados y aplicando repetidamente las reglas de inferencia "modus ponens" y "cuantificación universal".

Si tenemos una teoría T entonces la sentencia φ se define demostrable en la teoría T si y sólo si para a ∧ b ∧ ... → φ es demostrable en la lógica de primer orden, para algún conjunto finito de axiomas a, b,... de la teoría T.

Un problema aparente con esta definición de demostrabilidad es que parece ser ad hoc: hemos tomado una colección de axiomas y reglas de inferencia aparentemente al azar. No resulta evidente que no hemos olvidado algún axioma o regla esencial. Sin embargo, el teorema de completitud de Gödel nos asegura que esto nos es un problema: el teorema afirma que cualquier enunciado verdadero en todos los modelos es demostrable en lógica de primer orden. En particular, cualquier definición razonable de "demostrable" en lógica de primer orden debe ser equivalente a la dada previamente (aunque es posible que difieran considerablemente las logitudes de las demostraciones según las diferentes definiciones de demostrabilidad).

Hay varias formas diferentes (pero equivalentes) de definir demostrabilidad. La definición dada es un ejemplo típico de cálculo de estilo de Hilbert, el cual tiene tiene varios axiomas diferentes pero muy pocas reglas de inferencia. El cálculo de sequentes es un cálculo de predicados con el estilo de Gentzen. Difiere en el hecho que tiene muy pocos axiomas pero muchas reglas de inferencia.

Equivalencias

$\backslash lnot\; \backslash forall\; x\; \backslash ,\; P(x)\; \backslash Leftrightarrow\; \backslash exists\; x\; \backslash ,\; \backslash lnot\; P(x)$

$\backslash lnot\; \backslash exists\; x\; \backslash ,\; P(x)\; \backslash Leftrightarrow\; \backslash forall\; x\; \backslash ,\; \backslash lnot\; P(x)$

$\backslash forall\; x\; \backslash ,\; \backslash forall\; y\; \backslash ,\; P(x,y)\; \backslash Leftrightarrow\; \backslash forall\; y\; \backslash ,\; \backslash forall\; x\; \backslash ,\; P(x,y)$

$\backslash exists\; x\; \backslash ,\; \backslash exists\; y\; \backslash ,\; P(x,y)\; \backslash Leftrightarrow\; \backslash exists\; y\; \backslash ,\; \backslash exists\; x\; \backslash ,\; P(x,y)$

$\backslash forall\; x\; \backslash ,\; P(x)\; \backslash land\; \backslash forall\; x\; \backslash ,\; Q(x)\; \backslash Leftrightarrow\; \backslash forall\; x\; \backslash ,\; (P(x)\; \backslash land\; Q(x))$

$\backslash exists\; x\; \backslash ,\; P(x)\; \backslash lor\; \backslash exists\; x\; \backslash ,\; Q(x)\; \backslash Leftrightarrow\; \backslash exists\; x\; \backslash ,\; (P(x)\; \backslash lor\; Q(x))$

Reglas de inferencia

$\backslash exists\; x\; \backslash ,\; \backslash forall\; y\; \backslash ,\; P(x,y)\; \backslash Rightarrow\; \backslash forall\; y\; \backslash ,\; \backslash exists\; x\; \backslash ,\; P(x,y)$

$\backslash forall\; x\; \backslash ,\; P(x)\; \backslash lor\; \backslash forall\; x\; \backslash ,\; Q(x)\; \backslash Rightarrow\; \backslash forall\; x\; \backslash ,\; (P(x)\; \backslash lor\; Q(x))$

$\backslash exists\; x\; \backslash ,\; (P(x)\; \backslash land\; Q(x))\; \backslash Rightarrow\; \backslash exists\; x\; \backslash ,\; P(x)\; \backslash land\; \backslash exists\; x\; \backslash ,\; Q(x)$

$\backslash exists\; x\; \backslash ,\; P(x)\; \backslash land\; \backslash forall\; x\; \backslash ,\; Q(x)\; \backslash Rightarrow\; \backslash exists\; x\; \backslash ,\; (P(x)\; \backslash land\; Q(x))$

$\backslash forall\; x\; \backslash ,\; P(x)\; \backslash Rightarrow\; P(c)$ (Si c es una variable, entonces debe no ser ya cuantificada en alguna parte de P(x))

$P(c)\; \backslash Rightarrow\; \backslash exists\; x\; \backslash ,\; P(x)$ (x no debe aparecer libre en P(c))

Teoremas metalógicos de la lógica de primer orden

---

Algunos teoremas metalógicos importantes son los listados a continuación.

1. A diferencia de la lógica proposicional, la lógica de primer orden es indecidible cuando el lenguaje tiene al menos un predicado de aridad de al menos 2. Es decir, no hay un procedimiento de decisión para determinar para una fórmula arbitraria P, si P es válida. Los resultados llegaron independientemente de Church y Turing.
2. El problema de decisión para validez es semidecidible; es decir, existe una máquina de Turing que dada una sentencia cualquiera como input, se detiene si y sólo si la sentencia es válida (verdadera en todos los modelos). Como muestra el teorema de completitud de Gödel, para cualquier fórmula P, si P es válida entonces es demostrable.
3. La lógica de predicados monádica (la lógica de predicados con predicados de aridad 1) es decidible.

Véase también

---

• Teorema de incompletitud de Gödel
• Teorema de completitud de Gödel
• Lista de reglas de inferencia
• Lógica matemática
• Lógica proposicional

Bibliografía

---

• David Hilbert y Wilhelm Ackermann (1928). Grundzüge der theoretischen Logik (Principios de Lógica Teórica). Springer-Verlag, ISBN 0-8218-2024-9.
• Article on classical logic por Stewart Shapiro en la Stanford Encyclopedia of Philosophy, el cual cubre la definición, teoría de modelos y resultados de soundness y completitud para lógica de primer orden caracterizado con un estilo natural de deducción.
• Introduction to mathematical logic por Karl Podnieks.
• Metamath: un proyecto para construir matemática usando un sistema axiomático basado en el cálculo proposicional, cálculo de predicados y teoría de conjuntos.
• Cálculo relacional apunte sobre "Cálculo relacional" por María Mercedes Marqués Andrés, (2001)
• Instituto de Estudios Avanzados Suger Montano de Guatemala apunte curso de 4to Computación "B", maestro del curso Cesar Jimenez publicado por EloElTemerario.

Lógica matemática

Prädikatenlogik | First-order logic | Calcul des prédicats | Elsőrendű logika | Logica del primo ordine | 一階述語論理 | Rachunek predykatów pierwszego rzędu | Логика первого порядка | Predikatlogik | 一阶逻辑