La lógica de primer orden —también llamada lógica de predicados , cálculo de predicados , lógica cuantificacional— es una colección de sistemas formales utilizados en matemáticas , filosofía , lingüística y ciencias de la computación . La lógica de primer orden utiliza variables cuantificadas sobre objetos no lógicos y permite el uso de oraciones que contienen variables. En lugar de proposiciones como «todos los hombres son mortales», en la lógica de primer orden se pueden tener expresiones en la forma «para todo x , si x es un hombre, entonces x es mortal»; donde «para todo x» es un cuantificador, x es una variable y «... es un hombre » y «... es mortal » son predicados. [1] Esto la distingue de la lógica proposicional , que no utiliza cuantificadores ni relaciones ; [2] en este sentido, la lógica proposicional es la base de la lógica de primer orden.
Una teoría sobre un tema, como la teoría de conjuntos, una teoría de grupos [3] o una teoría formal de la aritmética , es habitualmente una lógica de primer orden junto con un dominio específico de discurso (sobre el que se extienden las variables cuantificadas), un número finito de funciones desde ese dominio hasta sí mismo, un número finito de predicados definidos en ese dominio y un conjunto de axiomas que se cree que se cumplen sobre ellos. "Teoría" a veces se entiende en un sentido más formal como simplemente un conjunto de oraciones en lógica de primer orden.
El término "primer orden" distingue la lógica de primer orden de la lógica de orden superior , en la que hay predicados que tienen predicados o funciones como argumentos, o en la que se permite la cuantificación sobre predicados, funciones o ambos. [4] : 56 En las teorías de primer orden, los predicados a menudo se asocian con conjuntos. En las teorías interpretadas de orden superior, los predicados pueden interpretarse como conjuntos de conjuntos.
Existen muchos sistemas deductivos para la lógica de primer orden que son sólidos , es decir, todas las afirmaciones demostrables son verdaderas en todos los modelos; y completos , es decir, todas las afirmaciones que son verdaderas en todos los modelos son demostrables. Aunque la relación de consecuencia lógica es solo semidecidible , se ha avanzado mucho en la demostración automática de teoremas en lógica de primer orden. La lógica de primer orden también satisface varios teoremas metalógicos que la hacen susceptible de análisis en la teoría de la demostración , como el teorema de Löwenheim-Skolem y el teorema de compacidad .
La lógica de primer orden es el estándar para la formalización de las matemáticas en axiomas y se estudia en los fundamentos de las matemáticas . La aritmética de Peano y la teoría de conjuntos de Zermelo-Fraenkel son axiomatizaciones de la teoría de números y la teoría de conjuntos , respectivamente, en lógica de primer orden. Sin embargo, ninguna teoría de primer orden tiene la fuerza para describir de manera única una estructura con un dominio infinito, como los números naturales o la línea real . Los sistemas axiomáticos que describen completamente estas dos estructuras, es decir, los sistemas axiomáticos categóricos , se pueden obtener en lógicas más fuertes como la lógica de segundo orden .
Los fundamentos de la lógica de primer orden fueron desarrollados independientemente por Gottlob Frege y Charles Sanders Peirce . [5] Para una historia de la lógica de primer orden y cómo llegó a dominar la lógica formal, véase José Ferreirós (2001).
Mientras que la lógica proposicional se ocupa de proposiciones declarativas simples, la lógica de primer orden también abarca los predicados y la cuantificación . Un predicado se evalúa como verdadero o falso para una entidad o entidades en el dominio del discurso .
Consideremos las dos oraciones " Sócrates es un filósofo" y " Platón es un filósofo". En la lógica proposicional , estas oraciones en sí mismas son vistas como los individuos de estudio, y podrían ser denotadas, por ejemplo, por variables como p y q . No se las considera como una aplicación de un predicado, como , a ningún objeto particular en el dominio del discurso, sino que se las ve como un enunciado puro que es verdadero o falso. [6] Sin embargo, en la lógica de primer orden, estas dos oraciones pueden formularse como afirmaciones de que un determinado individuo u objeto no lógico tiene una propiedad. En este ejemplo, resulta que ambas oraciones tienen la forma común para algún individuo , en la primera oración el valor de la variable x es "Sócrates", y en la segunda oración es "Platón". Debido a la capacidad de hablar sobre individuos no lógicos junto con los conectivos lógicos originales, la lógica de primer orden incluye la lógica proposicional. [7]
La verdad de una fórmula como " x es un filósofo" depende de qué objeto se denota por x y de la interpretación del predicado "es un filósofo". En consecuencia, " x es un filósofo" por sí solo no tiene un valor de verdad definido de verdadero o falso, y es similar a un fragmento de oración. [8] Las relaciones entre predicados se pueden establecer utilizando conectivos lógicos . Por ejemplo, la fórmula de primer orden "si x es un filósofo, entonces x es un erudito", es un enunciado condicional con " x es un filósofo" como hipótesis y " x es un erudito" como conclusión, que nuevamente necesita la especificación de x para tener un valor de verdad definido.
Los cuantificadores se pueden aplicar a las variables de una fórmula. La variable x en la fórmula anterior se puede cuantificar universalmente, por ejemplo, con la oración de primer orden "Para cada x , si x es un filósofo, entonces x es un erudito". El cuantificador universal "para cada" en esta oración expresa la idea de que la afirmación "si x es un filósofo, entonces x es un erudito" es válida para todas las opciones de x .
La negación de la oración “Para cada x , si x es un filósofo, entonces x es un erudito” es lógicamente equivalente a la oración “Existe x tal que x es un filósofo y x no es un erudito”. El cuantificador existencial “existe” expresa la idea de que la afirmación “ x es un filósofo y x no es un erudito” es válida para alguna elección de x .
Los predicados "es filósofo" y "es erudito" toman cada uno una sola variable. En general, los predicados pueden tomar varias variables. En la oración de primer orden "Sócrates es el maestro de Platón", el predicado "es el maestro de" toma dos variables.
Una interpretación (o modelo) de una fórmula de primer orden especifica lo que significa cada predicado y las entidades que pueden instanciar las variables. Estas entidades forman el dominio del discurso o universo, que normalmente se requiere que sea un conjunto no vacío. Por ejemplo, considere la oración "Existe x tal que x es un filósofo". Esta oración se considera verdadera en una interpretación tal que el dominio del discurso consiste en todos los seres humanos, y que el predicado "es un filósofo" se entiende como "fue el autor de la República ". Es cierto, como lo atestigua Platón en ese texto. [ aclaración necesaria ]
La lógica de primer orden consta de dos partes fundamentales: la sintaxis, que determina qué secuencias finitas de símbolos son expresiones bien formadas en la lógica de primer orden, mientras que la semántica, que determina los significados que se esconden detrás de estas expresiones.
A diferencia de los lenguajes naturales, como el inglés, el lenguaje de la lógica de primer orden es completamente formal, de modo que se puede determinar mecánicamente si una expresión dada está bien formada . Hay dos tipos clave de expresiones bien formadas: los términos , que representan intuitivamente objetos, y las fórmulas , que expresan intuitivamente afirmaciones que pueden ser verdaderas o falsas. Los términos y fórmulas de la lógica de primer orden son cadenas de símbolos , donde todos los símbolos juntos forman el alfabeto del lenguaje.
Como ocurre con todos los lenguajes formales , la naturaleza de los símbolos en sí mismos queda fuera del alcance de la lógica formal; a menudo se los considera simplemente como letras y símbolos 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 siempre representa "y"; nunca se interpreta como "o", que está representado por el símbolo lógico . 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.
Los símbolos lógicos son un conjunto de caracteres que varían según el autor, pero que normalmente incluyen los siguientes: [10]
No todos estos símbolos son necesarios en la lógica de primer orden. Basta con cualquiera de los cuantificadores junto con la negación, la conjunción (o disyunción), las variables, los corchetes y la igualdad.
Otros símbolos lógicos incluyen los siguientes:
Los símbolos no lógicos representan predicados (relaciones), funciones y constantes. Antes era una práctica habitual utilizar un conjunto fijo e infinito de símbolos no lógicos para todos los fines:
Cuando la aridad de un símbolo de predicado o de función queda clara a partir del contexto, a menudo se omite el superíndice n .
En este enfoque tradicional, sólo hay un lenguaje de lógica de primer orden. [13] Este enfoque todavía es común, especialmente en libros de orientación filosófica.
Una práctica más reciente es utilizar diferentes símbolos no lógicos según la aplicación que se tenga en mente. Por lo tanto, se ha vuelto necesario nombrar el conjunto de todos los símbolos no lógicos utilizados en una aplicación particular. Esta elección se realiza a través de una firma . [14]
Las firmas típicas en matemáticas son {1, ×} o simplemente {×} para grupos , [3] o {0, 1, +, ×, <} para cuerpos ordenados . No hay restricciones en el número de símbolos no lógicos. La firma puede estar vacía , ser finita o infinita, incluso incontable . Las firmas incontables aparecen, por ejemplo, en las demostraciones modernas del teorema de Löwenheim-Skolem .
Aunque en algunos casos las firmas pueden implicar cómo deben interpretarse los símbolos no lógicos, la interpretación de los símbolos no lógicos en la firma es independiente (y no necesariamente fija). Las firmas se refieren a la sintaxis, no a la semántica.
En este enfoque, cada símbolo no lógico es de uno de los siguientes tipos:
El enfoque tradicional se puede recuperar en el enfoque moderno, simplemente especificando que la firma "personalizada" consista en las secuencias tradicionales de símbolos no lógicos.
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 utilizar para escribir una gramática formal para términos y fórmulas. Estas reglas son generalmente independientes del contexto (cada producción tiene un solo símbolo en el lado izquierdo), excepto que se puede permitir que el conjunto de símbolos sea infinito y puede haber muchos símbolos de inicio, por ejemplo, las variables en el caso de los términos.
El conjunto de términos se define inductivamente mediante las siguientes reglas: [17]
Sólo las expresiones que pueden obtenerse mediante un número finito de aplicaciones de las reglas 1 y 2 son términos. Por ejemplo, ninguna expresión que incluya un símbolo de predicado es un término.
El conjunto de fórmulas (también llamadas fórmulas bien formadas [18] o WFF ) se define inductivamente mediante las siguientes reglas:
Sólo las expresiones que se pueden obtener mediante un número finito de aplicaciones de las reglas 1 a 5 son fórmulas. Las fórmulas obtenidas a partir de las dos primeras reglas se denominan fórmulas atómicas .
Por ejemplo:
es una fórmula, si f es un símbolo de función unaria, P un símbolo de predicado unario y Q un símbolo de predicado ternario. Sin embargo, no es una fórmula, aunque es una cadena de símbolos del alfabeto.
La función de los paréntesis en la definición es garantizar que cualquier fórmula solo se pueda obtener de una manera: siguiendo la definición inductiva (es decir, existe un árbol de análisis único para cada fórmula). Esta propiedad se conoce como legibilidad única de las fórmulas. Existen muchas convenciones sobre dónde se utilizan los paréntesis en las fórmulas. Por ejemplo, algunos autores utilizan dos puntos o puntos en lugar de paréntesis, o cambian los lugares en los que se insertan los paréntesis. La definición particular de cada autor debe ir acompañada de una prueba de legibilidad única.
Para mayor comodidad, se han desarrollado convenciones sobre la precedencia de los operadores lógicos, para evitar la necesidad de escribir paréntesis en algunos casos. Estas reglas son similares al orden de las operaciones aritméticas. Una convención común es:
Además, se pueden insertar signos de puntuación adicionales que no sean necesarios según la definición para facilitar la lectura de las fórmulas. Así, la fórmula:
Podría escribirse como:
En algunos campos, es habitual utilizar la notación infija para las relaciones y funciones binarias, en lugar de la notación prefija definida anteriormente. Por ejemplo, en aritmética, normalmente se escribe "2 + 2 = 4" en lugar de "=(+(2,2),4)". Es habitual considerar las fórmulas en notación infija como abreviaturas de las fórmulas correspondientes en notación prefija, véase también estructura de términos frente a representación .
Las definiciones anteriores utilizan la notación infija para los conectores binarios como . Una convención menos común es la notación polaca , en la que se escribe , y así sucesivamente delante de sus argumentos en lugar de entre ellos. Esta convención es ventajosa porque permite descartar todos los símbolos de puntuación. Como tal, la notación polaca es compacta y elegante, pero rara vez se utiliza en la práctica porque es difícil de leer para los humanos. En la notación polaca, la fórmula:
se convierte en "∀x∀y→Pfx¬→ PxQfyxz".
En una fórmula, una variable puede aparecer libre o limitada (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 una variable es libre o limitada, luego si un símbolo de variable en general es libre o limitado. Para distinguir diferentes ocurrencias del símbolo idéntico 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 Luego, se dice que una ocurrencia de x está limitada si esa ocurrencia de x se encuentra dentro del alcance de al menos uno de o . Finalmente, x está limitada en φ si todas las ocurrencias de x en φ están limitadas. [8] pp.142--143
Intuitivamente, un símbolo 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 ocurrencia de la variable x es libre mientras que la de y está limitada. Las ocurrencias libres y limitadas de la variable en una fórmula se definen inductivamente de la siguiente manera.
Por ejemplo, en ∀ x ∀ y ( P ( x ) → Q ( x , f ( x ), z )) , x e y aparecen solo cota, [19] z aparece solo libre y w no es ninguno porque no aparece en la fórmula.
Las variables libres y acotadas de una fórmula no necesitan 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 , está acotada.
Una fórmula en lógica de primer orden sin ocurrencias de variables libres se llama oración de primer orden . Estas son las fórmulas que tendrán valores de verdad bien definidos bajo una interpretación. Por ejemplo, si una fórmula como Phil( x ) es verdadera o no debe depender de lo que x representa. Pero la oración ∃ 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 de 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:
Los axiomas para grupos abelianos ordenados se pueden expresar como un conjunto de oraciones en el lenguaje. Por ejemplo, el axioma que establece que el grupo es conmutativo suele escribirse
Una interpretación de un lenguaje de primer orden asigna una denotación a cada símbolo no lógico (símbolo de predicado, símbolo de función o símbolo de constante) en ese lenguaje. También determina un dominio del discurso que especifica el rango de los cuantificadores. El resultado es que a cada término se le asigna un objeto que representa, a cada predicado se le asigna una propiedad de los objetos y a cada oración se le asigna un valor de verdad. De esta manera, una interpretación proporciona significado semántico a los términos, predicados y fórmulas del lenguaje. El estudio de las interpretaciones de los lenguajes formales se llama semántica formal . Lo que sigue es una descripción de la semántica estándar o tarskiana para la lógica de primer orden. (También es posible definir la semántica de juego para la lógica de primer orden , pero además de requerir el axioma de elección , la semántica de juego concuerda con la semántica tarskiana para la lógica de primer orden, por lo que no se elaborará aquí).
La forma más común de especificar una interpretación (especialmente en matemáticas) es especificar una estructura (también llamada modelo ; véase más adelante). La estructura consiste en 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 un enunciado acerca de estos objetos; por ejemplo, enuncia 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 números enteros .
Los símbolos no lógicos se interpretan de la siguiente manera:
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 significados a fórmulas con variables libres, como . El valor de verdad de esta fórmula cambia dependiendo de los valores que denotan x e y .
En primer lugar, la asignación de la variable μ puede extenderse a todos los términos de la lengua, con el resultado de que cada término corresponde a un único elemento del dominio del discurso. Para realizar esta asignación se utilizan las siguientes reglas:
A continuación, a cada fórmula se le asigna un valor de verdad. La definición inductiva que se utiliza para realizar esta asignación se denomina esquema T.
Si una fórmula no contiene variables libres, y también lo es una oración, entonces la asignación inicial de variable no afecta su valor de verdad. En otras palabras, una oración es verdadera según M y si y solo si es verdadera según M y cualquier otra asignación de variable .
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 agrega a la firma una colección de símbolos constantes, uno para cada elemento del dominio del discurso en M ; digamos que para cada d en el dominio el símbolo constante c d es fijo. 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, de la siguiente manera:
Este enfoque alternativo otorga exactamente los mismos valores de verdad a todas las oraciones que el enfoque mediante asignaciones de variables.
Si una oración φ se evalúa como verdadera bajo una interpretación dada M , se dice que M satisface φ; esto se denota [20] . Una oración es satisfacible si hay alguna interpretación bajo la cual es verdadera. Esto es un poco diferente del símbolo de la teoría de modelos, donde denota satisfacibilidad en un modelo, es decir, "hay una asignación adecuada de valores en el dominio de a símbolos variables de ". [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 se dice que una fórmula φ con variables libres , ..., es satisfecha por una interpretación si la fórmula φ sigue siendo verdadera independientemente de qué individuos del dominio del discurso sean asignados a sus variables libres , ..., . Esto tiene el mismo efecto que decir que una fórmula φ se satisface si y solo si se satisface su clausura universal .
Una fórmula es lógicamente válida (o simplemente válida ) si es verdadera en toda interpretación. [22] Estas fórmulas juegan un papel similar a 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 que ψ sea verdadera también hace que φ sea verdadera. En este caso se dice que φ está implícito lógicamente en ψ.
Un enfoque alternativo a la semántica de la lógica de primer orden procede a través del álgebra abstracta . Este enfoque generaliza las álgebras de Lindenbaum-Tarski de la lógica proposicional. Hay tres formas de eliminar variables cuantificadas de la lógica de primer orden que no implican reemplazar cuantificadores con otros operadores de términos que vinculan variables:
Todas estas álgebras son redes que extienden adecuadamente el álgebra de Boole de dos elementos .
Tarski y Givant (1987) demostraron que el fragmento de lógica de primer orden que no tiene ninguna oración atómica que se encuentre en el ámbito 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 parte de la teoría de conjuntos axiomática , incluida la ZFC canónica . 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 firma particular es un conjunto de axiomas , que son oraciones que consisten en símbolos de esa firma. El conjunto de axiomas es a menudo finito o recursivamente enumerable , en cuyo caso la teoría se llama efectiva . Algunos autores requieren que las teorías también incluyan todas las consecuencias lógicas de los axiomas. Se considera que los axiomas se cumplen dentro de la teoría y de ellos se pueden derivar otras oraciones que se cumplen dentro de la teoría.
Una estructura de primer orden que satisface todas las oraciones de una teoría dada se denomina modelo de la teoría. Una clase elemental es el conjunto de todas las estructuras que satisfacen una teoría particular. Estas clases son un tema principal de estudio en la teoría de modelos .
Muchas teorías tienen una interpretación intencionada , un modelo determinado que se tiene en cuenta al estudiar la teoría. Por ejemplo, la interpretación intencionada 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 muestra 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 si no es posible probar una contradicción a partir de los axiomas de la teoría. Una teoría es completa si, para cada fórmula que la acompaña, dicha fórmula o su negación es una consecuencia lógica de los axiomas de la teoría. El teorema de incompletitud de Gödel muestra que las teorías de primer orden eficaces que incluyen una porción suficiente de la teoría de los números naturales nunca pueden ser consistentes y completas.
La definición anterior requiere que el dominio del discurso de cualquier interpretación no esté vacío. Existen configuraciones, como la lógica inclusiva , en las que se permiten dominios vacíos. Además, si una clase de estructuras algebraicas incluye una estructura vacía (por ejemplo, hay un conjunto poset vacío ), esa clase solo puede ser una clase elemental en lógica de primer orden si se permiten dominios vacíos o si se elimina la estructura vacía de la clase.
Sin embargo, los dominios vacíos presentan varias dificultades:
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.
Un sistema deductivo se utiliza para demostrar, sobre una base puramente sintáctica, que una fórmula es una consecuencia lógica de otra fórmula. Existen muchos sistemas de este tipo para la lógica de primer orden, incluidos los sistemas deductivos de estilo Hilbert , la deducción natural , el cálculo secuencial , el método de tablas y la resolución . Estos comparten la propiedad común de que una deducción es un objeto sintáctico finito; el formato de este objeto y la forma en que se construye varían ampliamente. Estas deducciones finitas a menudo se denominan derivaciones en la teoría de la prueba. También se las suele llamar pruebas , pero están completamente formalizadas a diferencia de las pruebas matemáticas del lenguaje natural .
Un sistema deductivo es sólido si cualquier fórmula que pueda derivarse en el sistema es lógicamente válida. A la inversa, un sistema deductivo es completo si toda fórmula lógicamente válida es derivable. Todos los sistemas analizados en este artículo son sólidos y completos. También comparten la propiedad de que es posible verificar efectivamente que una deducción supuestamente válida es en realidad una deducción; tales sistemas de deducción se denominan efectivos .
Una propiedad fundamental de los sistemas deductivos es que son puramente sintácticos, de modo que las derivaciones pueden verificarse sin tener en cuenta ninguna interpretación. Por lo tanto, un argumento sólido es correcto en cualquier interpretación posible del lenguaje, independientemente de que esa interpretación se refiera a matemáticas, economía o alguna otra área.
En general, la consecuencia lógica en lógica de primer orden es sólo semidecidible : si una oración A implica lógicamente una oración B, esto puede descubrirse (por ejemplo, buscando una prueba hasta encontrarla, utilizando algún sistema de prueba efectivo, sólido y completo). Sin embargo, si A no implica lógicamente B, esto no significa que A implique lógicamente la negación de B. No existe ningún procedimiento efectivo que, dadas las fórmulas A y B, decida siempre correctamente si A implica lógicamente B.
Una regla de inferencia establece que, dada una fórmula particular (o un conjunto de fórmulas) con una determinada propiedad como hipótesis, se puede derivar otra fórmula específica (o un conjunto de fórmulas) como conclusión. La regla es válida (o preserva la verdad) si preserva la validez en el sentido de que, siempre que una 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 concluir φ[ t / x ] a partir de φ siempre que ninguna variable libre de t se vuelva acotada durante el proceso de sustitución. (Si alguna variable libre de t se vuelve acotada, entonces para sustituir t por x es necesario primero cambiar las variables acotadas de φ para que difieran de las variables libres de t ).
Para ver por qué es necesaria la restricción de las variables ligadas, considere la fórmula lógicamente válida φ dada por , en la signatura de (0,1,+,×,=) de la aritmética. Si t es el término "x + 1", la fórmula φ[ t / y ] es , que será falsa en muchas interpretaciones. El problema es que la variable libre x de t se ligó durante la sustitución. El reemplazo deseado se puede obtener renombrando la variable ligada x de φ por otra cosa, digamos z , de modo que la fórmula después de la sustitución sea , que nuevamente es lógicamente válida.
La regla de sustitución muestra 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. Tiene limitaciones (definidas sintácticamente) sobre cuándo se puede aplicar, que deben respetarse para preservar la corrección de las derivaciones. Además, como suele suceder, estas limitaciones son necesarias debido a las interacciones entre variables libres y variables ligadas que ocurren durante las manipulaciones sintácticas de las fórmulas involucradas en la regla de inferencia.
Una deducción en un sistema deductivo de estilo Hilbert es 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 consisten en 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 estilo Hilbert tienen una pequeña cantidad de reglas de inferencia, junto con varios esquemas infinitos de axiomas lógicos. Es común tener solo modus ponens y generalización universal como reglas de inferencia.
Los sistemas de deducción natural se parecen a los sistemas de estilo Hilbert en que una deducción es una lista finita de fórmulas. Sin embargo, los sistemas de deducción natural no tienen axiomas lógicos; lo compensan añadiendo reglas de inferencia adicionales que se pueden utilizar para manipular los conectores lógicos en las fórmulas de la prueba.
El cálculo secuencial 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 secuenciales , que son expresiones de la forma:
donde A 1 , ..., A n , B 1 , ..., B k son fórmulas y se utiliza el símbolo del torniquete como puntuación para separar las dos mitades. Intuitivamente, un consecuente expresa la idea que implica .
A diferencia de los métodos que acabamos de describir, las derivaciones en el método de tablas no son listas de fórmulas, sino que una derivación es un árbol de fórmulas. Para demostrar que una fórmula A es demostrable, el método de tablas intenta demostrar que la negación de A es insatisfacible. El árbol de la derivación tiene en su raíz; el árbol se ramifica de una manera que refleja la estructura de la fórmula. Por ejemplo, para demostrar que es insatisfacible se requiere demostrar que C y D son insatisfacibles; esto corresponde a un punto de ramificación en el árbol con padre e hijos C y D.
La regla de resolución es una regla de inferencia única que, junto con la unificación , es válida y completa para la lógica de primer orden. Al igual que con el método de tablas, una fórmula se demuestra mostrando que la negación de la fórmula es insatisfacible. La resolución se utiliza comúnmente en la demostración automática de teoremas.
El método de resolución funciona únicamente con fórmulas que son disyunciones de fórmulas atómicas; las fórmulas arbitrarias deben convertirse primero a esta forma mediante la eskolemización . La regla de resolución establece que a partir de las hipótesis y se puede obtener la conclusión .
Se pueden demostrar muchas identidades que establecen equivalencias entre fórmulas particulares. Estas identidades permiten reorganizar las fórmulas moviendo cuantificadores a través de otros conectores y son útiles para poner fórmulas en forma normal prenex . Algunas identidades demostrables incluyen:
Existen varias convenciones diferentes para utilizar la igualdad (o identidad) en la lógica de primer orden. La convención más común, conocida como lógica de primer orden con igualdad , incluye el símbolo de igualdad como un símbolo lógico primitivo que siempre se interpreta como la relación de igualdad real entre los miembros del dominio del discurso, de modo que los "dos" miembros dados son el mismo miembro. Este enfoque también agrega ciertos axiomas sobre la igualdad al sistema deductivo empleado. Estos axiomas de igualdad son: [26] : 198–200
Se trata de esquemas axiomáticos , cada uno de los cuales especifica un conjunto infinito de axiomas. El tercer esquema se conoce como la ley de Leibniz , "el principio de sustitutividad", "la indiscernibilidad de los idénticos" o "la propiedad de reemplazo". El segundo esquema, que incluye el símbolo de función f , es (equivalente a) un caso especial del tercer esquema, que utiliza la fórmula:
Entonces
Como se da x = y , y f (..., x , ...) = f (..., x , ...) es verdadero por reflexividad, tenemos f (..., x , ...) = f (..., y , ...)
Muchas otras propiedades de igualdad son consecuencias de los axiomas anteriores, por ejemplo:
Un enfoque alternativo considera que la relación de igualdad es 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 firma, los axiomas de igualdad deben ahora agregarse a las teorías en consideración, si se desea, en lugar de considerarse reglas de la lógica. La principal diferencia entre este método y la lógica de primer orden con igualdad es que una interpretación puede ahora interpretar a dos individuos distintos como "iguales" (aunque, por la ley de Leibniz, estos satisfarán exactamente las mismas fórmulas bajo cualquier interpretación). Es decir, la relación de igualdad puede ahora ser interpretada por 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, se utiliza el término modelo normal 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 los modelos normales, por lo que no hay ningún término para un modelo que no sea 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 los 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 tiene 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 más bien como teoremas derivables. Por ejemplo, en teorías sin símbolos de función y 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 no cambia al cambiar s por t en cualquier argumento.
Algunas teorías permiten otras definiciones ad hoc de igualdad:
Una de las razones para utilizar la lógica de primer orden, en lugar de la lógica de orden superior , es que la lógica de primer orden tiene muchas propiedades metalógicas que las lógicas más fuertes no tienen. Estos resultados se refieren a propiedades generales de la lógica de primer orden en sí, en lugar de propiedades de teorías individuales. Proporcionan herramientas fundamentales para la construcción de modelos de teorías de primer orden.
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 está capturada por 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 serán en general de cardinalidad arbitrariamente grande, y por lo tanto la consecuencia lógica no puede verificarse efectivamente comprobando cada modelo. Sin embargo, es posible enumerar todas las derivaciones finitas y buscar una derivación de ψ a partir de φ. Si ψ está implícito lógicamente por φ, tal derivación eventualmente se encontrará. Por lo tanto, la consecuencia lógica de primer orden es semidecidible : es posible hacer una enumeración efectiva de todos los pares de oraciones (φ, ψ) tales que ψ sea 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 hay un procedimiento de decisión que determine si 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 Entscheidungsproblem planteado por David Hilbert y Wilhelm Ackermann en 1928. Sus pruebas demuestran una conexión entre la irresolubilidad del problema de decisión para la lógica de primer orden y la irresolubilidad del problema de 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ádicos , que es lógica de primer orden restringida a símbolos de predicado 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 descriptivas .
El teorema de Löwenheim–Skolem muestra que si una teoría de cardinalidad de primer orden λ tiene un modelo infinito, entonces tiene modelos de cada cardinalidad infinita mayor o igual a λ. Uno de los primeros resultados en teoría de modelos , implica que no es posible caracterizar la contabilidad o incontabilidad en un lenguaje de primer orden con una firma contable. Es decir, no hay 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 contable (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 línea 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 línea real es infinita, cualquier teoría satisfecha por la línea real también lo es 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 paradoja de Skolem .
El teorema de compacidad establece que un conjunto de oraciones de primer orden tiene un modelo si y solo si cada subconjunto finito de él tiene un modelo. [29] 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 un número finito de esos axiomas. Este teorema fue demostrado por primera vez por Kurt Gödel como consecuencia del teorema de completitud, pero se han obtenido muchas demostraciones adicionales con el tiempo. Es una herramienta central en la teoría de modelos, que proporciona un método fundamental para construir modelos.
El teorema de compacidad tiene un efecto limitante sobre qué conjuntos de estructuras de primer orden son clases elementales. Por ejemplo, el teorema de compacidad implica que cualquier teoría que tenga modelos finitos arbitrariamente grandes tiene un modelo infinito. Por lo tanto, la clase de todos los grafos finitos no es una clase elemental (lo mismo se aplica a muchas otras estructuras algebraicas).
También existen limitaciones más sutiles de la lógica de primer orden que están implícitas en el teorema de compacidad. Por ejemplo, en informática, muchas situaciones pueden modelarse como un grafo dirigido de estados (nodos) y conexiones (aristas dirigidas). Validar un sistema de este tipo puede requerir demostrar que no se puede llegar a ningún estado "malo" desde ningún estado "bueno". Por tanto, se busca determinar si los estados bueno y malo están en diferentes componentes conectados del grafo. Sin embargo, el teorema de compacidad se puede utilizar para demostrar que los grafos conectados 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 . Sin embargo, la conexidad se puede expresar en la lógica de segundo orden , pero no solo con cuantificadores de conjuntos existenciales, ya que también goza de compacidad.
Per Lindström demostró que las propiedades metalógicas que acabamos de analizar caracterizan en realidad a la lógica de primer orden en el sentido de que ninguna lógica más fuerte puede tener 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:
Aunque la lógica de primer orden es suficiente para formalizar gran parte de las matemáticas y se utiliza habitualmente en informática y otros campos, tiene ciertas limitaciones, entre ellas, limitaciones en su expresividad y limitaciones en los fragmentos de lenguajes naturales que puede describir.
Por ejemplo, la lógica de primer orden es indecidible, lo que significa que es imposible crear un algoritmo de decisión sólido, completo y de terminación para la demostrabilidad. Esto ha llevado al estudio de fragmentos decidibles interesantes, como C 2 : lógica de primer orden con dos variables y los cuantificadores de conteo y . [30]
El teorema de Löwenheim-Skolem muestra que si una teoría de primer orden tiene cualquier modelo infinito, entonces tiene 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 hay ninguna teoría de primer orden cuyo único modelo tenga el conjunto de números naturales como su dominio, o cuyo único modelo tenga el conjunto de números reales como su dominio. 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 los números reales [ aclaración necesaria ] . Sin embargo, esta expresividad tiene un costo metalógico: por el teorema de Lindström , el teorema de compacidad y el teorema de Löwenheim-Skolem descendente 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 por ejemplo "cada persona que vive en Perth vive en Australia". Por lo tanto, la lógica de primer orden se utiliza como base para los 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 que sea apropiado como instrumento para el análisis del lenguaje natural necesita una estructura mucho más rica que la lógica de predicados de primer orden”. [31]
Existen muchas variantes de la lógica de primer orden. Algunas de ellas no son esenciales en el sentido de que simplemente cambian la notación sin afectar la semántica. Otras modifican el poder expresivo de manera más significativa, al extender la semántica mediante cuantificadores adicionales u otros símbolos lógicos nuevos. Por ejemplo, las lógicas infinitarias permiten fórmulas de tamaño infinito, y las lógicas modales añaden símbolos de posibilidad y necesidad.
La lógica de primer orden se puede estudiar en lenguajes con menos símbolos lógicos que los descritos anteriormente:
Restricciones como estas son útiles como técnica para reducir el número de reglas de inferencia o esquemas axiomáticos en sistemas deductivos, lo que conduce a pruebas más breves de resultados metalógicos. El costo de las restricciones es que se vuelve más difícil expresar enunciados en lenguaje natural en el sistema formal en cuestión, porque los conectores lógicos utilizados en los enunciados en lenguaje natural deben reemplazarse por sus definiciones (más largas) en términos de la colección restringida de conectores lógicos. De manera similar, las derivaciones en los sistemas limitados pueden ser más largas que las derivaciones en sistemas que incluyen conectores adicionales. Por lo tanto, existe una disyuntiva entre la facilidad de trabajar dentro del sistema formal y la facilidad de probar resultados sobre el sistema formal.
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 es suficiente 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 que se extienden todos los cuantificadores. La lógica de primer orden multiordenada permite que las variables tengan diferentes tipos , que tienen diferentes dominios. Esto también se llama lógica de primer orden tipificada , y los tipos se denominan tipos (como en tipo de datos ), pero no es lo mismo que la teoría de tipos de primer orden . La lógica de primer orden multiordenada se utiliza a menudo en el estudio de la aritmética de segundo orden . [33]
Cuando sólo 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. [34] : 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 los símbolos de predicado y y el axioma:
Entonces, los elementos que satisfacen se consideran elementos del primer tipo y los elementos que satisfacen se consideran 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, para decir que hay un elemento del primer tipo que satisface la fórmula , se escribe:
Se pueden agregar cuantificadores adicionales a la lógica de primer orden.
La lógica infinitesimal permite oraciones infinitamente largas. Por ejemplo, se puede permitir la conjunción o disyunción de infinitas fórmulas, o la cuantificación sobre infinitas 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 infinitesimal 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 firmas generalizadas en las que se permite que los símbolos de función y relación tengan aridades infinitas, o en las que los cuantificadores pueden vincular infinitas variables. Debido a 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, en lugar de con las cadenas que se analizan.
Las lógicas infinitarias más estudiadas se denotan como L αβ , donde α y β son cada uno 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 hay un suministro ilimitado de variables. De manera 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 contables .
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 en el alcance de cualquier cuantificador cuando una fórmula aparece como una subfórmula de otra. [35] En otras lógicas infinitarias, una subfórmula puede estar en el 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 de puntos fijos extiende la lógica de primer orden añadiendo el cierre bajo los puntos menos fijos de los operadores positivos. [36]
La característica distintiva de la lógica de primer orden es que se pueden cuantificar los individuos, pero no los predicados.
es una fórmula legal de primer orden, pero
No lo es, en la mayoría de las formalizaciones de la lógica de primer orden. La lógica de segundo orden extiende la lógica de primer orden añadiendo este último tipo de cuantificación. Otras lógicas de orden superior permiten la cuantificación sobre tipos incluso superiores a 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 tanto, el "primero" en la lógica de primer orden describe el tipo de objetos que se pueden cuantificar.
A diferencia de la lógica de primer orden, para la que se estudia solo una semántica, existen varias semánticas posibles para la lógica de segundo orden. La semántica más comúnmente empleada 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 lógica 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, es posible crear sistemas axiomáticos en lógica de segundo orden que caractericen de manera única a los números naturales y a la línea real. El costo de esta expresividad es que las lógicas de segundo orden y de orden superior tienen 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 cuando se generalizan a lógicas de orden superior con semántica completa.
La demostración automática de teoremas se refiere al desarrollo de programas informáticos que buscan y encuentran derivaciones (pruebas formales) de teoremas matemáticos. [37] Encontrar derivaciones es una tarea difícil porque el espacio de búsqueda puede ser muy grande; una búsqueda exhaustiva de cada derivación posible es teóricamente posible pero computacionalmente inviable para muchos sistemas de interés en matemáticas. Por lo tanto, se desarrollan funciones heurísticas complicadas para intentar encontrar una derivación en menos tiempo que una búsqueda a ciegas. [38]
El área relacionada con la verificación automática de pruebas utiliza programas informáticos para comprobar que las pruebas creadas por humanos son correctas. A diferencia de los comprobadores de teoremas automatizados complicados, los sistemas de verificación pueden ser lo suficientemente pequeños como para que su exactitud pueda comprobarse tanto a mano como mediante la verificación automática de software. Esta validación del verificador de pruebas es necesaria para dar confianza en que cualquier derivación etiquetada como "correcta" lo es realmente.
Algunos verificadores de pruebas, como Metamath , insisten en tener una derivación completa como entrada. Otros, como Mizar e Isabelle , toman un boceto de prueba bien formateado (que aún puede ser muy largo y detallado) y completan las piezas faltantes haciendo búsquedas de prueba simples o aplicando procedimientos de decisión conocidos: la derivación resultante luego es verificada por un pequeño "núcleo" central. Muchos de estos sistemas están destinados principalmente al uso interactivo por parte de matemáticos humanos: estos se conocen como asistentes de prueba . También pueden usar lógicas formales que son más fuertes que la lógica de primer orden, como la teoría de tipos. Debido a que una derivación completa de cualquier resultado no trivial en un sistema deductivo de primer orden será extremadamente larga para que la escriba un humano, [39] los resultados a menudo se formalizan como una serie de lemas, para los cuales se pueden construir derivaciones por separado.
Los probadores de teoremas automáticos también se utilizan para implementar la verificación formal en informática. En este contexto, los probadores de teoremas se utilizan para verificar la corrección de los programas y del hardware, como los procesadores, con respecto a una especificación formal . Debido a que este tipo de análisis requiere mucho tiempo y, por lo tanto, es costoso, generalmente se reserva para proyectos en los que un mal funcionamiento tendría graves consecuencias humanas o financieras.
Para el problema de verificación de modelos , se conocen algoritmos eficientes para decidir si una estructura finita de entrada satisface una fórmula de primer orden, además de los límites de complejidad computacional : consulte Verificación de modelos § Lógica de primer orden .
![{\displaystyle (\lno [\para todo xP(x)])\para \existe x[\lno P(x)].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7b34883b819ec8da58478c3cf001a557826a8bb9)
![{\displaystyle (\para todo x\para todo y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \para todo x\,\para todo y\,\mathop {+} (x,y)=0)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/540d5b5e22885c61946b05841d437c576e4c3b8c)
![{\displaystyle (\para todo x)(\para todo y)[x+y=y+x].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1649ba2cb0d9003b8558c4449aa8c137d6b4c1e6)
![{\displaystyle \para todo x\para todo y[\para todo z(z\en x\Leftrightarrow z\en y)\Rightarrow x=y]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ead06cc9bbab4a341137f21ec450deea1a63209)
![{\displaystyle \para todo x\para todo y[\para todo z(z\en x\flecha izquierda derecha z\en y)\flecha derecha \para todo z(x\en z\flecha izquierda derecha y\en z)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/44b1e8b20e39514ecabe08db08307aeb674e9878)
