En lógica matemática , la lógica de función de predicado ( PFL ) es una de varias formas de expresar la lógica de primer orden (también conocida como lógica de predicado ) por medios puramente algebraicos, es decir, sin variables cuantificadas . PFL emplea una pequeña cantidad de dispositivos algebraicos llamados functores de predicado (o modificadores de predicado ) [1] que operan en términos para producir términos. PFL es principalmente la invención del lógico y filósofo Willard Quine .
Motivación
La fuente de esta sección, así como de gran parte de esta entrada, es Quine (1976). Quine propuso el PFL como una forma de algebraizar la lógica de primer orden de una manera análoga a cómo el álgebra de Boole algebraiza la lógica proposicional . Diseñó PFL para tener exactamente el poder expresivo de la lógica de primer orden con identidad . Por lo tanto, las metamatemáticas de PFL son exactamente las de la lógica de primer orden sin letras de predicado interpretadas: ambas lógicas son sólidas , completas e indecidibles . La mayoría de los trabajos que Quine publicó sobre lógica y matemáticas en los últimos 30 años de su vida tocaron el PFL de alguna manera. [ cita requerida ]
Quine tomó "functor" de los escritos de su amigo Rudolf Carnap , el primero en emplearlo en filosofía y lógica matemática , y lo definió de la siguiente manera:
"La palabra functor , gramatical en importancia pero lógica en hábitat ... es un signo que se adhiere a una o más expresiones de una determinada clase gramatical para producir una expresión de una determinada clase gramatical". (Quine 1982: 129)
Otras formas distintas al PFL de algebraizar la lógica de primer orden incluyen:
- Álgebra cilíndrica de Alfred Tarski y sus estudiantes estadounidenses. El álgebra cilíndrica simplificada propuesta en Bernays (1959) llevó a Quine a escribir el artículo que contiene el primer uso de la frase "functor de predicado";
- El álgebra políada de Paul Halmos . En virtud de sus axiomas y primitivos económicos, este álgebra se parece mucho al PFL;
- El álgebra de relaciones algebraiza el fragmento de lógica de primer orden que consiste en fórmulas que no tienen fórmula atómica que se encuentra en el alcance de más de tres cuantificadores . Sin embargo, ese fragmento es suficiente para la aritmética de Peano y la teoría axiomática de conjuntos ZFC ; por tanto, el álgebra de relaciones, a diferencia del PFL, es incompleta . La mayor parte del trabajo sobre álgebra de relaciones desde aproximadamente 1920 ha sido de Tarski y sus estudiantes estadounidenses. El poder del álgebra de relaciones no se puso de manifiesto hasta la monografía Tarski y Givant (1987), publicada después de los tres importantes artículos relacionados con el PFL, a saber, Bacon (1985), Kuhn (1983) y Quine (1976);
- La lógica combinatoria se basa en combinadores , funciones de orden superior cuyo dominio es otro combinador o función, y cuyo rango es otro combinador más. Por lo tanto, la lógica combinatoria va más allá de la lógica de primer orden al tener el poder expresivo de la teoría de conjuntos , lo que hace que la lógica combinatoria sea vulnerable a las paradojas . Un functor de predicado, por otro lado, simplemente mapea predicados (también llamados términos ) en predicados.
PFL es posiblemente el más simple de estos formalismos, pero también el que menos se ha escrito.
Quine tuvo una fascinación de toda la vida por la lógica combinatoria , atestiguada por su introducción a la traducción en Van Heijenoort (1967) del artículo del lógico ruso Moses Schönfinkel fundando la lógica combinatoria. Cuando Quine comenzó a trabajar en serio en PFL, en 1959, la lógica combinatoria se consideró comúnmente un fracaso por las siguientes razones:
- Hasta que Dana Scott comenzó a escribir sobre la teoría modelo de la lógica combinatoria a fines de la década de 1960, casi solo Haskell Curry , sus estudiantes y Robert Feys en Bélgica trabajaron en esa lógica;
- Las formulaciones axiomáticas satisfactorias de la lógica combinatoria tardaron en llegar. En la década de 1930, se encontró que algunas formulaciones de lógica combinatoria eran inconsistentes . Curry también descubrió la paradoja de Curry , peculiar de la lógica combinatoria;
- El cálculo lambda , con el mismo poder expresivo que la lógica combinatoria , fue visto como un formalismo superior.
Formalización de Kuhn
La sintaxis , las primitivas y los axiomas del PFL descritos en esta sección son en gran parte de Steven Kuhn (1983). La semántica de los functores es de Quine (1982). El resto de esta entrada incorpora terminología de Bacon (1985).
Sintaxis
Un término atómico es una letra latina mayúscula, excepto I y S , seguida de un superíndice numérico llamado su grado , o de variables minúsculas concatenadas, conocidas colectivamente como lista de argumentos . El grado de un término transmite la misma información que el número de variables que siguen a una letra de predicado. Un término atómico de grado 0 denota una variable booleana o un valor de verdad . El grado de I es invariablemente 2, por lo que no se indica.
Los functores predicados "combinatorios" (la palabra es de Quine), todos monádicos y peculiares de PFL, son Inv , inv , ∃ , + y p . Un término es un término atómico o se construye mediante la siguiente regla recursiva. Si τ es un término, entonces Inv τ, inv τ, ∃ τ, + τ yp τ son términos. Un funtor con un superíndice n , n un número natural > 1, denota n aplicaciones consecutivas (iteraciones) de ese funtor.
Una fórmula es un término o está definida por la regla recursiva: si α y β son fórmulas, entonces αβ y ~ (α) son igualmente fórmulas. Por tanto, "~" es otro functor monádico, y la concatenación es el único functor de predicado diádico. Quine llamó a estos functores "aléticos". La interpretación natural de "~" es la negación ; el de la concatenación es cualquier conectivo que, cuando se combina con la negación, forma un conjunto funcionalmente completo de conectivos. El conjunto funcionalmente completo preferido de Quine era la conjunción y la negación . Por tanto, los términos concatenados se toman como conjuntos. La notación + es de Bacon (1985); el resto de la notación es de Quine (1976; 1982). La parte alética de PFL es idéntica a los esquemas de términos booleanos de Quine (1982).
Como es bien sabido, los dos functores aléticos podrían ser reemplazados por un solo functor diádico con la siguiente sintaxis y semántica : si α y β son fórmulas, entonces (αβ) es una fórmula cuya semántica es "no (α y / o β) "(ver NAND y NOR ).
Axiomas y semántica
Quine no estableció ni axiomatización ni procedimiento de prueba para PFL. La siguiente axiomatización de PFL, una de las dos propuestas en Kuhn (1983), es concisa y fácil de describir, pero hace un uso extensivo de variables libres y, por lo tanto, no hace plena justicia al espíritu de PFL. Kuhn da otra axiomatización que prescinde de las variables libres, pero que es más difícil de describir y que hace un uso extensivo de functores definidos. Kuhn demostró que sus dos axiomatizaciones de PFL eran sólidas y completas .
Esta sección se basa en los functores de predicados primitivos y algunos definidos. Los functores aléticos pueden axiomatizarse mediante cualquier conjunto de axiomas para la lógica enunciativa cuyas primitivas son la negación y una de ∧ o ∨. De manera equivalente, todas las tautologías de la lógica enunciativa pueden tomarse como axiomas.
La semántica de Quine (1982) para cada functor de predicado se establece a continuación en términos de abstracción (notación del constructor de conjuntos), seguida del axioma relevante de Kuhn (1983) o una definición de Quine (1976). La notacióndenota el conjunto de n -tuplas que satisfacen la fórmula atómica
- La identidad , yo , se define como:
La identidad es reflexiva ( Ixx ), simétrica ( Ixy → Iyx ), transitiva (( Ixy ∧ Iyz ) → Ixz ) y obedece a la propiedad de sustitución:
- El relleno , + , agrega una variable a la izquierda de cualquier lista de argumentos.
- Al recortar , ∃ , se borra la variable situada más a la izquierda en cualquier lista de argumentos.
El recorte habilita dos útiles functores definidos:
- Reflexión , S :
S generaliza la noción de reflexividad a todos los términos de cualquier grado finito mayor que 2. Nota: S no debe confundirse con el combinador primitivo S de la lógica combinatoria.
- Producto cartesiano ,;
Solo aquí, Quine adoptó una notación infija, porque esta notación infija para el producto cartesiano está muy bien establecida en matemáticas. El producto cartesiano permite replantear la conjunción de la siguiente manera:
Reordene la lista de argumentos concatenados para mover un par de variables duplicadas al extremo izquierdo, luego invoque S para eliminar la duplicación. Repetir esto tantas veces como sea necesario da como resultado una lista de argumentos de longitud máxima ( m , n ).
Los siguientes tres functores permiten reordenar listas de argumentos a voluntad.
- La inversión mayor , Inv , rota las variables en una lista de argumentos hacia la derecha, de modo que la última variable se convierte en la primera.
- Inversión menor , inv , intercambia las dos primeras variables en una lista de argumentos.
- La permutación , p , rota desde la segunda hasta la última variable en una lista de argumentos hacia la izquierda, de modo que la segunda variable se convierte en la última.
Dada una lista de argumentos que consta de n variables, p trata implícitamente las últimas n −1 variables como una cadena de bicicleta, y cada variable constituye un eslabón en la cadena. Una aplicación de p hace avanzar la cadena en un eslabón. k aplicaciones consecutivas de p a F n mueve el k variable de 1 a la segunda posición argumento en F .
Cuando n = 2, Inv e inv simplemente intercambian x 1 y x 2 . Cuando n = 1, no tienen ningún efecto. Por tanto, p no tiene efecto cuando n <3.
Kuhn (1983) toma la inversión mayor y la inversión menor como primitivas. La notación p en Kuhn corresponde a inv ; no tiene ninguna analogía con la permutación y, por tanto, no tiene axiomas para ella. Si, siguiendo a Quine (1976), p se toma como primitivo, Inv e inv pueden definirse como combinaciones no triviales de + , ∃ y p iterado .
La siguiente tabla resume cómo los functores afectan los grados de sus argumentos.
Expresión | La licenciatura |
---|---|
ningún cambio | |
norte | |
máx. ( m , n ) |
Reglas
Todas las instancias de una letra de predicado pueden ser reemplazadas por otra letra de predicado del mismo grado, sin afectar la validez. Las reglas son:
- Modus ponens ;
- Sean α y β fórmulas PFL en las queno aparece. Entonces sí es un teorema de PFL, entonces es igualmente un teorema de PFL.
Algunos resultados útiles
En lugar de axiomatizar el PFL, Quine (1976) propuso las siguientes conjeturas como axiomas candidatos.
n -1 iteraciones consecutivas de p restaura el status quo ante :
+ y ∃ se aniquilan entre sí:
|
|
Distribuye Negación más de + , ∃ , y p :
|
|
|
+ Y p se distribuye sobre conjunción:
|
|
La identidad tiene la interesante implicación:
Quine también conjeturó la regla: si es un teorema de PFL, entonces también lo son y .
El trabajo de tocino
Bacon (1985) toma el condicional , la negación , la identidad , el relleno y la inversión mayor y menor como primitivo, y el recorte como se define. Empleando terminología y notación que difieren un poco de lo anterior, Bacon (1985) establece dos formulaciones de PFL:
- Una formulación de deducción natural al estilo de Frederick Fitch . Bacon demuestra que esta formulación es sólida y completa con todo lujo de detalles.
- Una formulación axiomática, que Bacon afirma, pero no prueba, equivalente a la anterior. Algunos de estos axiomas son simplemente conjeturas de Quine reformuladas en la notación de Bacon.
Tocino también:
- Discute la relación de PFL con el término lógica de Sommers (1982), y argumenta que reformular PFL usando una sintaxis propuesta en el apéndice de Lockwood a Sommers, debería hacer que PFL sea más fácil de "leer, usar y enseñar";
- Toca la estructura teórica de grupos de Inv e inv ;
- Menciona que la lógica proposicional , lógica de predicados monádico , la lógica modal S5 , y la lógica booleana de (des) permutadas las relaciones , son todos los fragmentos de PFL.
De la lógica de primer orden al PFL
El siguiente algoritmo está adaptado de Quine (1976: 300-2). Dada una fórmula cerrada de lógica de primer orden , primero haga lo siguiente:
- Adjunte un subíndice numérico a cada letra de predicado, indicando su grado;
- Traducir todos los cuantificadores universales en cuantificadores existenciales y negación;
- Repita todas las fórmulas atómicas de la forma x = y como Ixy .
Ahora aplique el siguiente algoritmo al resultado anterior:
1. Traducir las matrices de los cuantificadores más profundamente anidados a la forma normal disyuntiva , que consiste en disyuntivas de conjunciones de términos, negando los términos atómicos según sea necesario. La subfórmula resultante contiene solo negación, conjunción, disyunción y cuantificación existencial.
2. Distribuya los cuantificadores existenciales sobre los disyuntos en la matriz usando la regla de paso (Quine 1982: 119):
3. Reemplazar conjunción por producto cartesiano , invocando el hecho:
4. Concatenar las listas de argumentos de todos los términos atómicos y mover la lista concatenada al extremo derecho de la subfórmula.
5. Utilice Inv e inv para mover todas las instancias de la variable cuantificada (llámela y ) a la izquierda de la lista de argumentos.
6. Invoque S tantas veces como sea necesario para eliminar todas menos la última instancia de y . Elimine y anteponiendo la subfórmula con una instancia de ∃ .
7. Repita (1) - (6) hasta que se hayan eliminado todas las variables cuantificadas. Elimine cualquier disyunción que caiga dentro del alcance de un cuantificador invocando la equivalencia:
La traducción inversa, del PFL a la lógica de primer orden, se analiza en Quine (1976: 302-4).
El fundamento canónico de las matemáticas es la teoría de conjuntos axiomática , con una lógica de fondo que consiste en una lógica de primer orden con identidad , con un universo de discurso que consiste enteramente en conjuntos. Hay una sola letra predicada de grado 2, interpretada como pertenencia al conjunto. La traducción PFL de la teoría de conjuntos axiomáticos canónicos ZFC no es difícil, ya que ningún axioma de ZFC requiere más de 6 variables cuantificadas. [2]
Ver también
- Lógica algebraica
Notas al pie
- ^ Johannes Stern, Hacia enfoques predicados de la modalidad , Springer, 2015, p. 11.
- ^ Axiomas de Metamath.
Referencias
- Bacon, John, 1985, "La integridad de una lógica de predicado-functor", Journal of Symbolic Logic 50 : 903-26.
- Paul Bernays , 1959, "Uber eine naturliche Erweiterung des Relationenkalkuls" en Heyting, A., ed., Constructivity in Mathematics . Holanda Septentrional: 1–14.
- Kuhn, Steven T. , 1983, " An Axiomatization of Predicate Functor Logic ", Notre Dame Journal of Formal Logic 24 : 233–41.
- Willard Quine , 1976, "Lógica algebraica y functores de predicados" en Ways of Paradox and Other Essays , ed ampliada. Universidad de Harvard. Presione: 283–307.
- Willard Quine, 1982. Methods of Logic , 4ª ed. Universidad de Harvard. Prensa. Cap. 45.
- Sommers, Fred, 1982. La lógica del lenguaje natural . Universidad de Oxford. Prensa.
- Alfred Tarski y Givant, Steven, 1987. Una formalización de la teoría de conjuntos sin variables . AMS .
- Jean Van Heijenoort , 1967. De Frege a Gödel: un libro de consulta sobre lógica matemática . Universidad de Harvard. Prensa.
enlaces externos
- Una introducción a la lógica de predicado-functor (descarga con un clic, archivo PS) por Mats Dahllöf (Departamento de Lingüística, Universidad de Uppsala)