Lógica de primer orden

Como ocurre con todos los lenguajes formales , la naturaleza de los símbolos en sí mismos queda fuera del ámbito de la lógica formal; a menudo se les considera simplemente como letras y signos de puntuación.

Es común dividir los símbolos del alfabeto en símbolos lógicos , que siempre tienen el mismo significado, y símbolos no lógicos , cuyo significado varía según la interpretación. ^{[ 9 ]} Por ejemplo, el símbolo lógico${\displaystyle \land }$siempre representa "y"; nunca se interpreta como "o", que se representa mediante el símbolo lógico.${\displaystyle \lor }$Sin embargo, un símbolo de predicado no lógico como Phil( x ) podría interpretarse como " x es un filósofo", " x es un hombre llamado Philip" o cualquier otro predicado unario dependiendo de la interpretación en cuestión.

Las reglas de formación definen los términos y fórmulas de la lógica de primer orden. ^{[ 16 ]} Cuando los términos y fórmulas se representan como cadenas de símbolos, estas reglas se pueden usar para escribir una gramática formal para términos y fórmulas. Estas reglas son generalmente libres de contexto (cada producción tiene un solo símbolo en el lado izquierdo), excepto que el conjunto de símbolos puede ser infinito y puede haber muchos símbolos iniciales, por ejemplo las variables en el caso de los términos .

En una fórmula, una variable puede aparecer libre o ligada (o ambas). Una formalización de esta noción se debe a Quine: primero se define el concepto de ocurrencia de una variable, luego si una ocurrencia de variable es libre o ligada, y finalmente si un símbolo de variable en su conjunto es libre o ligado. Para distinguir diferentes ocurrencias del mismo símbolo x , cada ocurrencia de un símbolo de variable x en una fórmula φ se identifica con la subcadena inicial de φ hasta el punto en el que aparece dicha instancia del símbolo x . ^{[ 8 ] p.  297} Entonces, se dice que una ocurrencia de x está ligada si esa ocurrencia de x se encuentra dentro del alcance de al menos uno de los${\displaystyle \exists x}$o${\displaystyle \forall x}$Finalmente, x está ligado en φ si todas las ocurrencias de x en φ están ligadas. ^{[ 8 ] págs.  142–143}

Intuitivamente, un símbolo de variable es libre en una fórmula si en ningún punto está cuantificado: ^{[ 8 ] pp.  142–143} en ∀ y P ( x , y ) , la única aparición de la variable x es libre mientras que la de y está ligada. Las apariciones de variables libres y ligadas en una fórmula se definen inductivamente de la siguiente manera.

Fórmulas atómicas

Si φ es una fórmula atómica, entonces x aparece libre en φ si y solo si x aparece en φ . Además, no hay variables ligadas en ninguna fórmula atómica.

Negación

x aparece libre en ¬ φ si y solo si x aparece libre en φ . x aparece ligado en ¬ φ si y solo si x aparece ligado en φ.

Conectores binarios

x aparece libre en ( φ → ψ ) si y solo si x aparece libre en φ o en ψ . x aparece ligado en ( φ → ψ ) si y solo si x aparece ligado en φ o en ψ . La misma regla se aplica a cualquier otro conector binario en lugar de →.

Cuantificadores

x aparece libre en ∀ y φ , si y solo si x aparece libre en φ y x es un símbolo diferente de y . Además, x aparece ligado en ∀ y φ , si y solo si x es y o x aparece ligado en φ . La misma regla se aplica con ∃ en lugar de ∀ .

Por ejemplo, en ∀ x ∀ y ( P ( x ) → Q ( x , f ( x ), z )) , x e y aparecen solo ligados, ^{[ 19 ]} z aparece solo libre y w no es ninguno de los dos porque no aparece en la fórmula.

Las variables libres y ligadas de una fórmula no tienen por qué ser conjuntos disjuntos: en la fórmula P ( x ) → ∀ x Q ( x ) , la primera aparición de x , como argumento de P , es libre mientras que la segunda, como argumento de Q , es ligada.

Una fórmula en lógica de primer orden sin ocurrencias de variables libres se denomina sentencia de primer orden . Estas fórmulas tendrán valores de verdad bien definidos bajo una interpretación. Por ejemplo, que una fórmula como Phil( x ) sea verdadera depende de lo que representa x . Pero la sentencia ∃ x Phil( x ) será verdadera o falsa en una interpretación dada.

En matemáticas, el lenguaje de los grupos abelianos ordenados tiene un símbolo constante 0, un símbolo de función unaria −, un símbolo de función binaria + y un símbolo de relación binaria ≤. Entonces:

• Las expresiones +( x , y ) y +( x , +( y , −( z ))) son términos . Estos se suelen escribir como x + y y x + y − z .
• Las expresiones +( x , y ) = 0 y ≤(+( x , +( y , −( z ))), +( x , y )) son fórmulas atómicas . Estas se suelen escribir como x + y = 0 y x + y − z  ≤ x + y . 
• La expresión${\displaystyle (\forall x\forall y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \forall x\,\forall y\,\mathop {+} (x,y)=0)]}$es una fórmula , que generalmente se escribe como${\displaystyle \forall x\forall y(x+y\leq z)\to \forall x\forall y(x+y=0).}$Esta fórmula tiene una variable libre, z .

Los axiomas para grupos abelianos ordenados pueden expresarse como un conjunto de oraciones en el lenguaje. Por ejemplo, el axioma que establece que el grupo es conmutativo se suele escribir${\displaystyle (\forall x)(\forall y)[x+y=y+x].}$

La forma más común de especificar una interpretación (especialmente en matemáticas) es mediante una estructura (también llamada modelo ; véase más adelante). Esta estructura consta de un dominio de discurso D y una función de interpretación I que asigna símbolos no lógicos a predicados, funciones y constantes.

El dominio del discurso D es un conjunto no vacío de "objetos" de algún tipo. Intuitivamente, dada una interpretación, una fórmula de primer orden se convierte en una afirmación sobre estos objetos; por ejemplo,${\displaystyle \exists xP(x)}$afirma la existencia de algún objeto en D para el cual el predicado P es verdadero (o, más precisamente, para el cual el predicado asignado al símbolo de predicado P por la interpretación es verdadero). Por ejemplo, se puede tomar D como el conjunto de los enteros .

Los símbolos no lógicos se interpretan de la siguiente manera:

• La interpretación de un símbolo de función n -aria es una función de D ⁿ a D . Por ejemplo, si el dominio del discurso es el conjunto de los enteros, un símbolo de función f de aridad 2 puede interpretarse como la función que da la suma de sus argumentos. En otras palabras, el símbolo f está asociado con la función ⁠${\displaystyle I(f)}$⁠ lo cual, en esta interpretación, es una adición.
• La interpretación de un símbolo constante (un símbolo de función de aridad 0) es una función de D ⁰ (un conjunto cuyo único miembro es la tupla vacía ) a D , que puede identificarse simplemente con un objeto en D . Por ejemplo, una interpretación puede asignar el valor${\displaystyle I(c)=10}$al símbolo constante${\displaystyle c}$.
• La interpretación de un símbolo de predicado n -ario es un conjunto de n -tuplas de elementos de D , que dan los argumentos para los cuales el predicado es verdadero. Por ejemplo, una interpretación${\displaystyle I(P)}$Un símbolo de predicado binario P puede ser el conjunto de pares de enteros tales que el primero es menor que el segundo. Según esta interpretación, el predicado P sería verdadero si su primer argumento es menor que su segundo argumento. De forma equivalente, a los símbolos de predicado se les pueden asignar funciones booleanas de D ⁿ a${\displaystyle \{\mathrm {true,false} \}}$.

Una fórmula se evalúa como verdadera o falsa dada una interpretación y una asignación de variable μ que asocia un elemento del dominio del discurso con cada variable. La razón por la que se requiere una asignación de variable es para dar significado a fórmulas con variables libres, como${\displaystyle y=x}$El valor de verdad de esta fórmula cambia dependiendo de los valores que denoten x e y .

En primer lugar, la asignación de variables μ puede extenderse a todos los términos del lenguaje, de modo que cada término se corresponde con un único elemento del dominio del discurso. Para realizar esta asignación se utilizan las siguientes reglas:

• Variables . Cada variable x se evalúa como μ ( x ).
• Funciones . Términos dados${\displaystyle t_{1},\ldots ,t_{n}}$que han sido evaluados a elementos${\displaystyle d_{1},\ldots ,d_{n}}$del dominio del discurso, y un símbolo de función n -aria f , el término${\displaystyle f(t_{1},\ldots ,t_{n})}$evalúa a${\displaystyle (I(f))(d_{1},\ldots ,d_{n})}$.

A continuación, a cada fórmula se le asigna un valor de verdad. La definición inductiva utilizada para realizar esta asignación se denomina esquema T.

• Fórmulas atómicas (1) . Una fórmula${\displaystyle P(t_{1},\ldots ,t_{n})}$se asocia el valor verdadero o falso dependiendo de si${\displaystyle \langle v_{1},\ldots ,v_{n}\rangle \in I(P)}$, dónde${\displaystyle v_{1},\ldots ,v_{n}}$son la evaluación de los términos${\displaystyle t_{1},\ldots ,t_{n}}$y${\displaystyle I(P)}$es la interpretación de${\displaystyle P}$, que por supuesto es un subconjunto de${\displaystyle D^{n}}$.
• Fórmulas atómicas (2) . Una fórmula${\displaystyle t_{1}=t_{2}}$se asigna verdadero si${\displaystyle t_{1}}$y${\displaystyle t_{2}}$evaluar con respecto al mismo objeto del dominio del discurso (véase la sección sobre igualdad más adelante).
• Conectores lógicos . Una fórmula de la forma${\displaystyle \neg \varphi }$,${\displaystyle \varphi \rightarrow \psi }$, etc. se evalúa según la tabla de verdad del conector en cuestión, como en la lógica proposicional.
• Cuantificadores existenciales . Una fórmula${\displaystyle \exists x\varphi (x)}$es cierto según M y${\displaystyle \mu }$si existe una evaluación${\displaystyle \mu '}$de las variables que difieren de${\displaystyle \mu }$como máximo con respecto a la evaluación de x y tal que φ sea verdadero según la interpretación M y la asignación de variables${\displaystyle \mu '}$Esta definición formal capta la idea de que${\displaystyle \exists x\varphi (x)}$es cierto si y solo si hay una manera de elegir un valor para x tal que se satisfaga φ( x ).
• Cuantificadores universales . Una fórmula${\displaystyle \forall x\varphi (x)}$es cierto según M y${\displaystyle \mu }$si φ( x ) es verdadero para cada par compuesto por la interpretación M y alguna asignación de variable${\displaystyle \mu '}$que difiere de${\displaystyle \mu }$como máximo en el valor de x . Esto captura la idea de que${\displaystyle \forall x\varphi (x)}$es verdadero si cada elección posible de un valor para x hace que φ( x ) sea verdadero.

Si una fórmula no contiene variables libres y, por lo tanto, es una oración, entonces la asignación inicial de variables no afecta su valor de verdad. En otras palabras, una oración es verdadera según M y${\displaystyle \mu }$si y solo si es cierto según M y cualquier otra asignación de variables.${\displaystyle \mu '}$.

Existe un segundo enfoque común para definir valores de verdad que no se basa en funciones de asignación de variables. En cambio, dada una interpretación M , primero se añade a la signatura un conjunto de símbolos constantes, uno para cada elemento del dominio de discurso en M ; digamos que para cada d en el dominio se fija el símbolo constante c _d . La interpretación se extiende de modo que cada nuevo símbolo constante se asigna a su elemento correspondiente del dominio. Ahora se define la verdad para fórmulas cuantificadas sintácticamente, como sigue:

• Cuantificadores existenciales (alternativos) . Una fórmula${\displaystyle \exists x\varphi (x)}$es verdadero según M si existe algún d en el dominio del discurso tal que${\displaystyle \varphi (c_{d})}$sostiene. Aquí${\displaystyle \varphi (c_{d})}$es el resultado de sustituir c _d por cada aparición libre de x en φ.
• Cuantificadores universales (alternativos) . Una fórmula${\displaystyle \forall x\varphi (x)}$es cierto según M si, para cada d en el dominio del discurso,${\displaystyle \varphi (c_{d})}$es cierto según M.

Este enfoque alternativo proporciona exactamente los mismos valores de verdad a todas las oraciones que el enfoque mediante la asignación de variables.

Si una sentencia φ se evalúa como verdadera bajo una interpretación dada M , se dice que M satisface φ; esto se denota ^{[ 20 ].}${\displaystyle M\vDash \varphi }$Una oración es satisfacible si existe alguna interpretación bajo la cual sea verdadera. Esto es un poco diferente del símbolo${\displaystyle \vDash }$de la teoría de modelos, donde${\displaystyle M\vDash \phi }$denota satisfacibilidad en un modelo, es decir "hay una asignación adecuada de valores en${\displaystyle M}$dominio de símbolos variables de${\displaystyle \phi }$". ^{[ 21 ]}

La satisfacibilidad de fórmulas con variables libres es más complicada, porque una interpretación por sí sola no determina el valor de verdad de dicha fórmula. La convención más común es que una fórmula φ con variables libres${\displaystyle x_{1}}$, ...,${\displaystyle x_{n}}$Se dice que una interpretación se satisface si la fórmula φ permanece verdadera independientemente de qué individuos del dominio del discurso se asignen a sus variables libres.${\displaystyle x_{1}}$, ...,${\displaystyle x_{n}}$Esto tiene el mismo efecto que decir que una fórmula φ se satisface si y solo si su cierre universal${\displaystyle \forall x_{1}\dots \forall x_{n}\phi (x_{1},\dots ,x_{n})}$está satisfecho.

Una fórmula es lógicamente válida (o simplemente válida ) si es verdadera en cada interpretación. ^{[ 22 ]} Estas fórmulas desempeñan un papel similar al de las tautologías en la lógica proposicional.

Una fórmula φ es una consecuencia lógica de una fórmula ψ si toda interpretación que hace verdadera a ψ también hace verdadera a φ. En este caso, se dice que φ está lógicamente implicada por ψ.

Un enfoque alternativo a la semántica de la lógica de primer orden procede mediante álgebra abstracta . Este enfoque generaliza las álgebras de Lindenbaum-Tarski de la lógica proposicional. Hay tres maneras de eliminar las variables cuantificadas de la lógica de primer orden que no implican reemplazar los cuantificadores con otros operadores de términos de vinculación de variables:

• Álgebra cilíndrica , de Alfred Tarski , et al.;
• Álgebra poliádica , de Paul Halmos ;
• Lógica de funtores de predicados , principalmente de Willard Quine .

Todas estas álgebras son retículos que extienden adecuadamente el álgebra booleana de dos elementos .

Tarski y Givant (1987) demostraron que el fragmento de lógica de primer orden que no tiene ninguna sentencia atómica dentro del alcance de más de tres cuantificadores tiene el mismo poder expresivo que el álgebra de relaciones . ^{[ 23 ] : 32–33} Este fragmento es de gran interés porque es suficiente para la aritmética de Peano y la mayoría de las teorías de conjuntos axiomáticas , incluida la teoría de conjuntos canónica de Zermelo-Fraenkel (ZFC). También demuestran que la lógica de primer orden con un par ordenado primitivo es equivalente a un álgebra de relaciones con dos funciones de proyección de pares ordenados . ^{[ 24 ] : 803}

Una teoría de primer orden de una signatura particular es un conjunto de axiomas , que son enunciados formados por símbolos de dicha signatura. El conjunto de axiomas suele ser finito o recursivamente enumerable , en cuyo caso la teoría se denomina efectiva . Algunos autores exigen que las teorías incluyan también todas las consecuencias lógicas de los axiomas. Se considera que los axiomas son válidos dentro de la teoría y, a partir de ellos, se pueden derivar otros enunciados válidos dentro de la misma.

Una estructura de primer orden que satisface todas las proposiciones de una teoría dada se denomina modelo de dicha teoría. Una clase elemental es el conjunto de todas las estructuras que satisfacen una teoría particular. Estas clases constituyen un tema central de estudio en la teoría de modelos .

Muchas teorías tienen una interpretación prevista , un modelo determinado que se tiene en cuenta al estudiarlas. Por ejemplo, la interpretación prevista de la aritmética de Peano consiste en los números naturales habituales con sus operaciones habituales. Sin embargo, el teorema de Löwenheim-Skolem demuestra que la mayoría de las teorías de primer orden también tendrán otros modelos no estándar .

Una teoría es consistente (dentro de un sistema deductivo ) si no es posible demostrar una contradicción a partir de sus axiomas. Una teoría es completa si, para cada fórmula en su signatura, dicha fórmula o su negación es una consecuencia lógica de sus axiomas. El teorema de incompletitud de Gödel demuestra que las teorías efectivas de primer orden que incluyen una porción suficiente de la aritmética de los números naturales nunca pueden ser a la vez consistentes y completas.

La definición anterior exige que el dominio de discurso de cualquier interpretación no sea vacío. Existen contextos, como la lógica inclusiva , donde se permiten dominios vacíos. Además, si una clase de estructuras algebraicas incluye una estructura vacía (por ejemplo, un conjunto parcialmente ordenado vacío ) , dicha clase solo puede ser una clase elemental en lógica de primer orden si se permiten dominios vacíos o si la estructura vacía se elimina de la clase.

Sin embargo, existen varias dificultades con los dominios vacíos:

• Muchas reglas comunes de inferencia son válidas solo cuando se requiere que el dominio del discurso no esté vacío. Un ejemplo es la regla que establece que${\displaystyle \varphi \lor \exists x\psi }$implica${\displaystyle \exists x(\varphi \lor \psi )}$cuando x no es una variable libre en${\displaystyle \varphi }$Esta regla, que se utiliza para poner fórmulas en forma normal prenexa , es válida en dominios no vacíos, pero no lo es si se permite el dominio vacío.
• La definición de verdad en una interpretación que utiliza una función de asignación de variables no funciona con dominios vacíos, ya que no existen funciones de asignación de variables cuyo rango sea vacío. (De forma similar, no se pueden asignar interpretaciones a símbolos constantes). Esta definición de verdad requiere que se seleccione una función de asignación de variables (μ, como se mencionó anteriormente) antes de poder definir valores de verdad incluso para fórmulas atómicas. Entonces, el valor de verdad de una proposición se define como su valor de verdad bajo cualquier asignación de variables, y se demuestra que este valor de verdad no depende de la asignación elegida. Esta técnica no funciona si no existen funciones de asignación; debe modificarse para adaptarse a dominios vacíos.

Por lo tanto, cuando se permite el dominio vacío, a menudo debe tratarse como un caso especial. Sin embargo, la mayoría de los autores simplemente excluyen el dominio vacío por definición.

Una regla de inferencia establece que, dada una fórmula particular (o un conjunto de fórmulas) con una propiedad determinada como hipótesis, se puede derivar otra fórmula específica (o conjunto de fórmulas) como conclusión. La regla es válida (o preserva la verdad) si mantiene la validez en el sentido de que, siempre que cualquier interpretación satisfaga la hipótesis, esa interpretación también satisface la conclusión.

Por ejemplo, una regla común de inferencia es la regla de sustitución . Si t es un término y φ es una fórmula que posiblemente contenga la variable x , entonces φ[ t / x ] es el resultado de reemplazar todas las instancias libres de x por t en φ. La regla de sustitución establece que para cualquier φ y cualquier término t , se puede deducir φ[ t / x ] a partir de φ siempre que ninguna variable libre de t se vuelva ligada durante el proceso de sustitución. (Si alguna variable libre de t se vuelve ligada, entonces para sustituir t por x es necesario primero cambiar las variables ligadas de φ para que sean diferentes de las variables libres de t ).

Para ver por qué es necesaria la restricción sobre las variables ligadas, considere la fórmula lógicamente válida φ dada por${\displaystyle \exists x(x=y)}$, en la signatura de (0,1,+,×,=) de la aritmética. Si t es el término "x + 1", la fórmula φ[ t / y ] es${\displaystyle \exists x(x=x+1)}$, lo cual será falso en muchas interpretaciones. El problema es que la variable libre x de t se volvió ligada durante la sustitución. El reemplazo deseado se puede obtener renombrando la variable ligada x de φ a otra cosa, digamos z , de modo que la fórmula después de la sustitución sea${\displaystyle \exists z(z=x+1)}$, lo cual, de nuevo, es lógicamente válido.

La regla de sustitución demuestra varios aspectos comunes de las reglas de inferencia. Es completamente sintáctica; se puede determinar si se aplicó correctamente sin recurrir a ninguna interpretación. Presenta limitaciones (definidas sintácticamente) en cuanto a su aplicación, las cuales deben respetarse para preservar la corrección de las derivaciones. Además, como suele ocurrir, estas limitaciones son necesarias debido a las interacciones entre variables libres y ligadas que se producen durante las manipulaciones sintácticas de las fórmulas involucradas en la regla de inferencia.

En un sistema deductivo de Hilbert, una deducción consiste en una lista de fórmulas, cada una de las cuales es un axioma lógico , una hipótesis que se ha asumido para la derivación en cuestión o que se deduce de fórmulas anteriores mediante una regla de inferencia. Los axiomas lógicos constan de varios esquemas axiomáticos de fórmulas lógicamente válidas; estos abarcan una cantidad significativa de lógica proposicional. Las reglas de inferencia permiten la manipulación de cuantificadores. Los sistemas típicos de Hilbert tienen un número reducido de reglas de inferencia, junto con varios esquemas infinitos de axiomas lógicos. Es común que solo se utilicen el modus ponens y la generalización universal como reglas de inferencia.

Los sistemas de deducción natural se asemejan a los sistemas de Hilbert en que una deducción es una lista finita de fórmulas. Sin embargo, los sistemas de deducción natural carecen de axiomas lógicos; lo compensan añadiendo reglas de inferencia adicionales que permiten manipular los conectores lógicos en las fórmulas de la demostración.

El cálculo de secuencias se desarrolló para estudiar las propiedades de los sistemas de deducción natural. ^{[ 25 ]} En lugar de trabajar con una fórmula a la vez, utiliza secuencias , que son expresiones de la forma:

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},}$

donde A ₁ , ..., A _n , B ₁ , ..., B _k son fórmulas y el símbolo del torniquete${\displaystyle \vdash }$se utiliza como signo de puntuación para separar las dos mitades. Intuitivamente, un secuente expresa la idea de que${\displaystyle (A_{1}\land \cdots \land A_{n})}$implica${\displaystyle (B_{1}\lor \cdots \lor B_{k})}$.

A diferencia de los métodos descritos anteriormente, las derivaciones en el método de tableaux no son listas de fórmulas. En cambio, una derivación es un árbol de fórmulas. Para demostrar que una fórmula A es demostrable, el método de tableaux intenta demostrar que la negación de A es insatisfacible. El árbol de la derivación tiene${\displaystyle \lnot A}$en su raíz; el árbol se ramifica de una manera que refleja la estructura de la fórmula. Por ejemplo, para demostrar que${\displaystyle C\lor D}$es insatisfacible requiere demostrar que C y D son insatisfacibles; esto corresponde a un punto de ramificación en el árbol con padre${\displaystyle C\lor D}$y los niños C y D.

La regla de resolución es una regla de inferencia única que, junto con la unificación , es sólida y completa para la lógica de primer orden. Al igual que con el método de los tableaux, una fórmula se demuestra mostrando que su negación es insatisfacible. La resolución se utiliza comúnmente en la demostración automática de teoremas.

El método de resolución funciona solo con fórmulas que son disyunciones de fórmulas atómicas; las fórmulas arbitrarias deben convertirse primero a esta forma mediante la skolemización . La regla de resolución establece que a partir de las hipótesis${\displaystyle A_{1}\lor \cdots \lor A_{k}\lor C}$y${\displaystyle B_{1}\lor \cdots \lor B_{l}\lor \lnot C}$, la conclusión${\displaystyle A_{1}\lor \cdots \lor A_{k}\lor B_{1}\lor \cdots \lor B_{l}}$se puede obtener.

Se pueden demostrar muchas identidades que establecen equivalencias entre fórmulas particulares. Estas identidades permiten reorganizar fórmulas moviendo cuantificadores a través de otros conectores y son útiles para expresar fórmulas en forma normal prenexa . Algunas identidades demostrables incluyen:

${\displaystyle \lnot \forall x\,P(x)\Leftrightarrow \exists x\,\lnot P(x)}$

${\displaystyle \lnot \exists x\,P(x)\Leftrightarrow \forall x\,\lnot P(x)}$

${\displaystyle \forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)}$

${\displaystyle \exists x\,\exists y\,P(x,y)\Leftrightarrow \exists y\,\exists x\,P(x,y)}$

${\displaystyle \forall x\,P(x)\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\land Q(x))}$

${\displaystyle \exists x\,P(x)\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P(x)\lor Q(x))}$

${\displaystyle P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))}$(dónde${\displaystyle x}$no debe ocurrir libre en${\displaystyle P}$)

${\displaystyle P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))}$(dónde${\displaystyle x}$no debe ocurrir libre en${\displaystyle P}$)

Un enfoque alternativo considera la relación de igualdad como un símbolo no lógico. Esta convención se conoce como lógica de primer orden sin igualdad . Si se incluye una relación de igualdad en la signatura, los axiomas de igualdad deben añadirse a las teorías en cuestión, si se desea, en lugar de considerarse reglas lógicas. La principal diferencia entre este método y la lógica de primer orden con igualdad radica en que una interpretación puede ahora considerar a dos individuos distintos como "iguales" (aunque, según la ley de Leibniz, estos satisfarán exactamente las mismas fórmulas bajo cualquier interpretación). Es decir, la relación de igualdad puede interpretarse mediante una relación de equivalencia arbitraria en el dominio del discurso que sea congruente con respecto a las funciones y relaciones de la interpretación.

Cuando se sigue esta segunda convención, el término modelo normal se utiliza para referirse a una interpretación en la que ningún individuo distinto a y b satisface a = b . En la lógica de primer orden con igualdad, solo se consideran modelos normales, por lo que no existe un término para un modelo distinto de un modelo normal. Cuando se estudia la lógica de primer orden sin igualdad, es necesario modificar los enunciados de resultados como el teorema de Löwenheim-Skolem para que solo se consideren modelos normales.

La lógica de primer orden sin igualdad se emplea a menudo en el contexto de la aritmética de segundo orden y otras teorías aritméticas de orden superior, donde la relación de igualdad entre conjuntos de números naturales suele omitirse.

Si una teoría posee una fórmula binaria A ( x , y ) que satisface la reflexividad y la ley de Leibniz, se dice que la teoría tiene igualdad, o que es una teoría con igualdad. La teoría puede no tener todas las instancias de los esquemas anteriores como axiomas, sino como teoremas derivables. Por ejemplo, en teorías sin símbolos de función y con un número finito de relaciones, es posible definir la igualdad en términos de las relaciones, definiendo los dos términos s y t como iguales si cualquier relación permanece inalterada al cambiar s por t en cualquier argumento.

Algunas teorías permiten otras definiciones ad hoc de igualdad:

• En la teoría de órdenes parciales con un símbolo de relación ≤, se podría definir s = t como una abreviatura de s ≤ t.${\displaystyle \wedge }$t ≤ s .
• En la teoría de conjuntos con una relación ∈, se puede definir s = t como una abreviatura de ∀ x ( s ∈ x ↔ t ∈ x ).${\displaystyle \wedge }$∀ x ( x ∈ s ↔ x ∈ t ) . Esta definición de igualdad satisface automáticamente los axiomas de igualdad. En este caso, se debe reemplazar el axioma usual de extensionalidad , que se puede enunciar como${\displaystyle \forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y]}$, con una formulación alternativa${\displaystyle \forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)]}$, que dice que si los conjuntos x e y tienen los mismos elementos, entonces también pertenecen a los mismos conjuntos.

El teorema de completitud de Gödel , demostrado por Kurt Gödel en 1929, establece que existen sistemas deductivos sólidos, completos y efectivos para la lógica de primer orden, y por lo tanto, la relación de consecuencia lógica de primer orden se captura mediante la demostrabilidad finita. Ingenuamente, la afirmación de que una fórmula φ implica lógicamente una fórmula ψ depende de cada modelo de φ; estos modelos tendrán, en general, una cardinalidad arbitrariamente grande, por lo que la consecuencia lógica no puede verificarse eficazmente comprobando cada modelo. Sin embargo, es posible enumerar todas las derivaciones finitas y buscar una derivación de ψ a partir de φ. Si ψ está lógicamente implicada por φ, dicha derivación se encontrará eventualmente. Por lo tanto, la consecuencia lógica de primer orden es semidecidible : es posible realizar una enumeración efectiva de todos los pares de sentencias (φ,ψ) tales que ψ es una consecuencia lógica de  φ.

A diferencia de la lógica proposicional , la lógica de primer orden es indecidible (aunque semidecidible), siempre que el lenguaje tenga al menos un predicado de aridad al menos 2 (distinto de la igualdad). Esto significa que no existe un procedimiento de decisión que determine si las fórmulas arbitrarias son lógicamente válidas. Este resultado fue establecido independientemente por Alonzo Church y Alan Turing en 1936 y 1937, respectivamente, dando una respuesta negativa al problema de decisión planteado por David Hilbert y Wilhelm Ackermann en 1928. Sus demostraciones muestran una conexión entre la irresolubilidad del problema de decisión para la lógica de primer orden y la irresolubilidad del problema de la parada .

Existen sistemas más débiles que la lógica de primer orden completa para los cuales la relación de consecuencia lógica es decidible. Estos incluyen la lógica proposicional y la lógica de predicados monádica , que es lógica de primer orden restringida a símbolos de predicados unarios y sin símbolos de función. Otras lógicas sin símbolos de función que son decidibles son el fragmento protegido de la lógica de primer orden, así como la lógica de dos variables . La clase de fórmulas de primer orden de Bernays-Schönfinkel también es decidible. Los subconjuntos decidibles de la lógica de primer orden también se estudian en el marco de las lógicas de descripción . Véase (Pratt-Hartmann, 2023) para una monografía. ^{[ 29 ]}

Ejemplos de fragmentos decidibles: ^{[ 30 ]}

• C ₂ , FOL con dos variables y cuantificadores de conteo${\displaystyle \exists ^{\geq n}}$y${\displaystyle \exists ^{\leq n}}$. ^{[ 31 ]}
• Fragmento monádico de primer orden (MFO, o fragmento de Löwenheim): FOL sin igualdad, sin símbolos de función y con solo símbolos de predicado unario.
• Fragmento de Löb–Gurevich: FOL sin igualdad, con solo símbolos de función unaria y con solo símbolos de predicado unario.
• Fragmento de Rabin: FOL con igualdad, con exactamente un símbolo de función unaria y con solo símbolos de predicado unarios.
• Fragmento de Bernays–Schönfinkel–Ramsey: todas las oraciones relacionales de primer orden en forma normal prenexa con${\displaystyle \exists ^{*}\forall ^{*}}$prefijo y con igualdad.

El teorema de Löwenheim-Skolem demuestra que si una teoría de primer orden de cardinalidad λ tiene un modelo infinito, entonces tiene modelos de cada cardinalidad infinita mayor o igual que λ. Este es uno de los primeros resultados en teoría de modelos e implica que no es posible caracterizar la numerabilidad o la incontableidad en un lenguaje de primer orden con signatura numerable. Es decir, no existe una fórmula de primer orden φ( x ) tal que una estructura arbitraria M satisfaga φ si y solo si el dominio del discurso de M es numerable (o, en el segundo caso, incontable).

El teorema de Löwenheim-Skolem implica que las estructuras infinitas no pueden axiomatizarse categóricamente en la lógica de primer orden. Por ejemplo, no existe ninguna teoría de primer orden cuyo único modelo sea la recta real: cualquier teoría de primer orden con un modelo infinito también tiene un modelo de cardinalidad mayor que el continuo. Dado que la recta real es infinita, cualquier teoría satisfecha por la recta real también es satisfecha por algunos modelos no estándar . Cuando el teorema de Löwenheim-Skolem se aplica a las teorías de conjuntos de primer orden, las consecuencias no intuitivas se conocen como la paradoja de Skolem .

El teorema de compacidad establece que un conjunto de sentencias de primer orden tiene un modelo si y solo si todo subconjunto finito del mismo tiene un modelo. ^{[ 32 ]} Esto implica que si una fórmula es una consecuencia lógica de un conjunto infinito de axiomas de primer orden, entonces es una consecuencia lógica de algún número finito de esos axiomas. Este teorema fue demostrado por primera vez por Kurt Gödel como consecuencia del teorema de completitud, pero con el tiempo se han obtenido muchas demostraciones adicionales. Es una herramienta fundamental en la teoría de modelos, ya que proporciona un método básico para la construcción de modelos.

El teorema de compacidad limita qué conjuntos de estructuras de primer orden constituyen clases elementales. Por ejemplo, implica que cualquier teoría con modelos finitos arbitrariamente grandes posee un modelo infinito. Por lo tanto, la clase de todos los grafos finitos no es una clase elemental (lo mismo ocurre con muchas otras estructuras algebraicas).

También existen limitaciones más sutiles de la lógica de primer orden que se derivan del teorema de compacidad. Por ejemplo, en informática, muchas situaciones pueden modelarse como un grafo dirigido de estados (nodos) y conexiones (aristas dirigidas). Validar dicho sistema puede requerir demostrar que ningún estado "malo" puede alcanzarse desde ningún estado "bueno". Por lo tanto, se busca determinar si los estados bueno y malo se encuentran en diferentes componentes conexas del grafo. Sin embargo, el teorema de compacidad puede utilizarse para demostrar que los grafos conexos no son una clase elemental en la lógica de primer orden, y no existe una fórmula φ( x , y ) de la lógica de primer orden, en la lógica de grafos , que exprese la idea de que existe un camino de x a y . La conectividad puede expresarse en la lógica de segundo orden , pero no solo con cuantificadores de conjuntos existenciales, como${\displaystyle \Sigma _{1}^{1}}$También se caracteriza por su compacidad.

Per Lindström demostró que las propiedades metalógicas que acabamos de analizar caracterizan la lógica de primer orden en el sentido de que ninguna lógica más fuerte puede poseer también esas propiedades (Ebbinghaus y Flum 1994, Capítulo XIII). Lindström definió una clase de sistemas lógicos abstractos y una definición rigurosa de la fuerza relativa de un miembro de esta clase. Estableció dos teoremas para sistemas de este tipo:

• Un sistema lógico que cumpla con la definición de Lindström, que contenga lógica de primer orden y que satisfaga tanto el teorema de Löwenheim-Skolem como el teorema de compacidad, debe ser equivalente a la lógica de primer orden.
• Un sistema lógico que satisface la definición de Lindström, que posee una relación de consecuencia lógica semidecidible y que satisface el teorema de Löwenheim-Skolem, debe ser equivalente a la lógica de primer orden.

El teorema de Löwenheim-Skolem demuestra que si una teoría de primer orden posee algún modelo infinito, entonces posee modelos infinitos de cada cardinalidad. En particular, ninguna teoría de primer orden con un modelo infinito puede ser categórica . Por lo tanto, no existe ninguna teoría de primer orden cuyo único modelo tenga como dominio el conjunto de los números naturales, ni cuyo único modelo tenga como dominio el conjunto de los números reales. Muchas extensiones de la lógica de primer orden, incluidas las lógicas infinitarias y las lógicas de orden superior, son más expresivas en el sentido de que permiten axiomatizaciones categóricas de los números naturales o reales . Sin embargo, esta expresividad conlleva un coste metalógico: según el teorema de Lindström , el teorema de compacidad y el teorema descendente de Löwenheim-Skolem no pueden cumplirse en ninguna lógica más fuerte que la de primer orden.

La lógica de primer orden es capaz de formalizar muchas construcciones cuantificadoras simples en lenguaje natural, como "toda persona que vive en Perth vive en Australia". Por lo tanto, la lógica de primer orden se utiliza como base para lenguajes de representación del conocimiento , como FO(.) .

Sin embargo, existen características complejas del lenguaje natural que no pueden expresarse mediante la lógica de primer orden. «Cualquier sistema lógico adecuado como instrumento para el análisis del lenguaje natural requiere una estructura mucho más rica que la lógica de predicados de primer orden». ^{[ 33 ]}

La lógica de primer orden puede estudiarse en lenguajes con menos símbolos lógicos que los descritos anteriormente:

• Porque${\displaystyle \exists x\varphi (x)}$puede expresarse como${\displaystyle \neg \forall x\neg \varphi (x)}$, y${\displaystyle \forall x\varphi (x)}$puede expresarse como${\displaystyle \neg \exists x\neg \varphi (x)}$cualquiera de los dos cuantificadores${\displaystyle \exists }$y${\displaystyle \forall }$puede caerse.
• Desde${\displaystyle \varphi \lor \psi }$puede expresarse como${\displaystyle \lnot (\lnot \varphi \land \lnot \psi )}$y${\displaystyle \varphi \land \psi }$puede expresarse como${\displaystyle \lnot (\lnot \varphi \lor \lnot \psi )}$, cualquiera${\displaystyle \vee }$o${\displaystyle \wedge }$puede ser descartado. En otras palabras, es suficiente con tener${\displaystyle \neg }$y${\displaystyle \vee }$, o${\displaystyle \neg }$y${\displaystyle \wedge }$, como los únicos conectores lógicos.
• De igual modo, basta con tener solo${\displaystyle \neg }$y${\displaystyle \rightarrow }$como conectores lógicos, o tener solo el operador de trazo de Sheffer (NAND) o el operador de flecha de Peirce (NOR).
• Es posible evitar por completo los símbolos de función y los símbolos de constante, reescribiéndolos mediante símbolos de predicado de forma apropiada. Por ejemplo, en lugar de usar un símbolo de constante${\displaystyle \;0}$ uno puede usar un predicado ${\displaystyle \;0(x)}$ (interpretado como${\displaystyle \;x=0}$) y reemplazar cada predicado como${\displaystyle \;P(0,y)}$con${\displaystyle \forall x\;(0(x)\rightarrow P(x,y))}$. Una función como${\displaystyle f(x_{1},x_{2},...,x_{n})}$será reemplazado de manera similar por un predicado ${\displaystyle F(x_{1},x_{2},...,x_{n},y)}$interpretado como${\displaystyle y=f(x_{1},x_{2},...,x_{n})}$Este cambio requiere agregar axiomas adicionales a la teoría en cuestión, de modo que las interpretaciones de los símbolos predicativos utilizados tengan la semántica correcta. ^{[ 34 ]}

Restricciones como estas resultan útiles como técnica para reducir el número de reglas de inferencia o esquemas axiomáticos en sistemas deductivos, lo que conduce a demostraciones más breves de resultados metalógicos. El inconveniente de estas restricciones es que dificulta la expresión de enunciados en lenguaje natural dentro del sistema formal en cuestión, ya que los conectores lógicos utilizados en dichos enunciados deben sustituirse por sus definiciones (más extensas) en términos del conjunto restringido de conectores lógicos. Del mismo modo, las derivaciones en sistemas limitados pueden ser más largas que las derivaciones en sistemas que incluyen conectores adicionales. Por lo tanto, existe una compensación entre la facilidad de trabajar dentro del sistema formal y la facilidad de demostrar resultados sobre dicho sistema.

También es posible restringir las aridades de los símbolos de función y de predicado en teorías suficientemente expresivas. En principio, se puede prescindir por completo de funciones de aridad mayor que 2 y de predicados de aridad mayor que 1 en teorías que incluyan una función de emparejamiento . Esta es una función de aridad 2 que toma pares de elementos del dominio y devuelve un par ordenado que los contiene. También basta con tener dos símbolos de predicado de aridad 2 que definan funciones de proyección de un par ordenado a sus componentes. En ambos casos, es necesario que se satisfagan los axiomas naturales para una función de emparejamiento y sus proyecciones.

Las interpretaciones ordinarias de primer orden tienen un único dominio de discurso sobre el cual se extienden todos los cuantificadores. La lógica de primer orden multisortada permite que las variables tengan diferentes tipos , que a su vez tienen diferentes dominios. Esto también se denomina lógica de primer orden tipada , y los tipos se denominan tipos (como en tipo de dato ), pero no es lo mismo que la teoría de tipos de primer orden . La lógica de primer orden multisortada se utiliza a menudo en el estudio de la aritmética de segundo orden . ^{[ 35 ]}

Cuando solo hay un número finito de clases en una teoría, la lógica de primer orden de múltiples clases se puede reducir a la lógica de primer orden de una sola clase. ^{[ 36 ] : 296–299} Se introduce en la teoría de una sola clase un símbolo de predicado unario para cada clase en la teoría de múltiples clases y se añade un axioma que dice que estos predicados unarios dividen el dominio del discurso. Por ejemplo, si hay dos clases, se añaden símbolos de predicado${\displaystyle P_{1}(x)}$y${\displaystyle P_{2}(x)}$y el axioma:

${\displaystyle \forall x(P_{1}(x)\lor P_{2}(x))\land \lnot \exists x(P_{1}(x)\land P_{2}(x))}$.

Entonces los elementos que satisfacen${\displaystyle P_{1}}$se consideran elementos del primer tipo y elementos que satisfacen${\displaystyle P_{2}}$como elementos del segundo tipo. Se puede cuantificar sobre cada tipo utilizando el símbolo de predicado correspondiente para limitar el rango de cuantificación. Por ejemplo, decir que hay un elemento del primer tipo que satisface la fórmula${\displaystyle \varphi (x)}$, escribe uno:

${\displaystyle \exists x(P_{1}(x)\land \varphi (x))}$.

Se pueden agregar cuantificadores adicionales a la lógica de primer orden.

• A veces es útil decir que " P ( x ) se cumple para exactamente un x ", lo que se puede expresar como ∃! x P ( x ) . Esta notación, llamada cuantificación de unicidad , puede tomarse para abreviar una fórmula como ∃ x ( P ( x )${\displaystyle \wedge }$∀ y ( P ( y ) → ( x = y ))) .
• La lógica de primer orden con cuantificadores adicionales incluye nuevos cuantificadores Qx , ..., con significados como "hay muchos x tales que...". Véanse también los cuantificadores ramificados y los cuantificadores plurales de George Boolos y otros.
• Los cuantificadores acotados se utilizan con frecuencia en el estudio de la teoría de conjuntos o la aritmética.

La lógica infinita permite oraciones infinitamente largas. Por ejemplo, se puede permitir la conjunción o disyunción de un número infinito de fórmulas, o la cuantificación sobre un número infinito de variables. Las oraciones infinitamente largas surgen en áreas de las matemáticas como la topología y la teoría de modelos .

La lógica infinita generaliza la lógica de primer orden para permitir fórmulas de longitud infinita. La forma más común en que las fórmulas pueden volverse infinitas es mediante conjunciones y disyunciones infinitas. Sin embargo, también es posible admitir signaturas generalizadas en las que los símbolos de función y relación pueden tener aridades infinitas, o en las que los cuantificadores pueden vincular un número infinito de variables. Dado que una fórmula infinita no puede representarse mediante una cadena finita, es necesario elegir otra representación de fórmulas; la representación habitual en este contexto es un árbol. Por lo tanto, las fórmulas se identifican, esencialmente, con sus árboles de análisis sintáctico, en lugar de con las cadenas que se analizan.

Las lógicas infinitarias más estudiadas se denotan como L _αβ , donde α y β son números cardinales o el símbolo ∞. En esta notación, la lógica ordinaria de primer orden es L _ωω . En la lógica L _∞ω , se permiten conjunciones o disyunciones arbitrarias al construir fórmulas, y existe un suministro ilimitado de variables. De forma más general, la lógica que permite conjunciones o disyunciones con menos de κ constituyentes se conoce como L _κω . Por ejemplo, L _{ω 1 ω} permite conjunciones y disyunciones numerables .

El conjunto de variables libres en una fórmula de L _κω puede tener cualquier cardinalidad estrictamente menor que κ, pero solo un número finito de ellas puede estar dentro del alcance de cualquier cuantificador cuando una fórmula aparece como una subfórmula de otra. ^{[ 37 ]} En otras lógicas infinitas, una subfórmula puede estar dentro del alcance de infinitos cuantificadores. Por ejemplo, en L _κ∞ , un único cuantificador universal o existencial puede vincular arbitrariamente muchas variables simultáneamente. De manera similar, la lógica L _κλ permite la cuantificación simultánea sobre menos de λ variables, así como conjunciones y disyunciones de tamaño menor que κ.

• La lógica intuicionista de primer orden utiliza el razonamiento intuicionista en lugar del clásico; por ejemplo, ¬¬φ no tiene por qué ser equivalente a φ y ¬ ∀x.φ en general no es equivalente a ∃ x.¬φ .
• La lógica modal de primer orden permite describir otros mundos posibles, además del mundo contingentemente verdadero que habitamos. En algunas versiones, el conjunto de mundos posibles varía según el mundo posible que se habite. La lógica modal tiene operadores modales adicionales con significados que pueden caracterizarse informalmente como, por ejemplo, "es necesario que φ" (verdadero en todos los mundos posibles) y "es posible que φ" (verdadero en algún mundo posible). Con la lógica estándar de primer orden, tenemos un único dominio, y a cada predicado se le asigna una extensión. Con la lógica modal de primer orden, tenemos una función de dominio que asigna a cada mundo posible su propio dominio, de modo que cada predicado obtiene una extensión solo en relación con estos mundos posibles. Esto nos permite modelar casos en los que, por ejemplo, Alex es filósofo, pero podría haber sido matemático, o incluso no haber existido. En el primer mundo posible, P ( a ) es verdadero; en el segundo, P ( a ) es falso; y en el tercer mundo posible, no existe ningún a en el dominio.
• Las lógicas difusas de primer orden son extensiones de primer orden de las lógicas difusas proposicionales, en lugar de ser cálculos proposicionales clásicos .

La lógica de punto fijo extiende la lógica de primer orden al agregar el cierre bajo los puntos fijos más pequeños de los operadores positivos. ^{[ 38 ]}

La característica distintiva de la lógica de primer orden es que los individuos pueden cuantificarse, pero no los predicados. Por lo tanto,

${\displaystyle \exists a({\text{Phil}}(a))}$

es una fórmula legal de primer orden, pero

${\displaystyle \exists {\text{Phil}}({\text{Phil}}(a))}$

En la mayoría de las formalizaciones de la lógica de primer orden, esto no es así. La lógica de segundo orden extiende la lógica de primer orden al añadir este último tipo de cuantificación. Otras lógicas de orden superior permiten la cuantificación sobre tipos aún más elevados que los que permite la lógica de segundo orden. Estos tipos superiores incluyen relaciones entre relaciones, funciones de relaciones a relaciones entre relaciones y otros objetos de tipo superior. Por lo tanto, el prefijo "primero" en la lógica de primer orden describe el tipo de objetos que pueden cuantificarse.

A diferencia de la lógica de primer orden, para la cual solo se estudia una semántica, existen varias semánticas posibles para la lógica de segundo orden. La semántica más utilizada para la lógica de segundo orden y de orden superior se conoce como semántica completa . La combinación de cuantificadores adicionales y la semántica completa para estos cuantificadores hace que la lógica de orden superior sea más fuerte que la de primer orden. En particular, la relación de consecuencia lógica (semántica) para la lógica de segundo orden y de orden superior no es semidecidible; no existe un sistema de deducción efectivo para la lógica de segundo orden que sea sólido y completo bajo la semántica completa.

La lógica de segundo orden con semántica completa es más expresiva que la lógica de primer orden. Por ejemplo, en lógica de segundo orden es posible crear sistemas axiomáticos que caracterizan de forma unívoca los números naturales y la recta real. El precio de esta expresividad es que las lógicas de segundo orden y superiores poseen menos propiedades metalógicas atractivas que la lógica de primer orden. Por ejemplo, el teorema de Löwenheim-Skolem y el teorema de compacidad de la lógica de primer orden se vuelven falsos al generalizarse a lógicas de orden superior con semántica completa.