lógica de functores predicados

En lógica matemática , la lógica de functores de predicados ( LFP ) es una de las diversas maneras de expresar la lógica de primer orden (también conocida como lógica de predicados ) mediante métodos puramente algebraicos, es decir, sin variables cuantificadas . La LFP emplea un pequeño número de dispositivos algebraicos llamados functores de predicados (o modificadores de predicados ) ^{[ 1 ]} que operan sobre términos para generar otros términos. La LFP es principalmente una invención del lógico y filósofo Willard Quine .

La fuente de esta sección, así como de gran parte de esta entrada, es Quine (1976). Quine propuso PFL como una forma de algebrizar la lógica de primer orden de manera análoga a como el álgebra booleana algebriza la lógica proposicional . Diseñó PFL para que tuviera exactamente el poder expresivo de la lógica de primer orden con identidad . Por lo tanto, la metamatemática de PFL es exactamente la misma que la de la lógica de primer orden sin letras de predicado interpretadas: ambas lógicas son sólidas , completas e indecidibles . La mayor parte del trabajo que Quine publicó sobre lógica y matemáticas en los últimos 30 años de su vida abordó PFL de alguna manera.

Quine tomó el término "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' , de significado gramatical pero de uso lógico... es un signo que se adjunta a una o más expresiones de un tipo gramatical determinado para producir una expresión de un tipo gramatical determinado." (Quine 1982: 129)

Otras formas de algebrizar la lógica de primer orden, además de PFL, incluyen:

• Álgebra cilíndrica por 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 predicado";
• El álgebra poliádica de Paul Halmos . En virtud de sus primitivas y axiomas económicos , esta álgebra se asemeja más a PFL;
• El álgebra de relaciones algebriza el fragmento de lógica de primer orden que consiste en fórmulas sin fórmula atómica que se encuentre 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 de conjuntos axiomáticos ZFC ; por lo tanto, el álgebra de relaciones, a diferencia de PFL, es incompletable . La mayor parte del trabajo sobre álgebra de relaciones desde aproximadamente 1920 ha sido realizado por Tarski y sus estudiantes estadounidenses. El poder del álgebra de relaciones no se hizo evidente hasta la monografía Tarski y Givant (1987), publicada después de los tres artículos importantes relacionados con 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 poseer el poder expresivo de la teoría de conjuntos , lo que la hace vulnerable a las paradojas . Un functor de predicados, por otro lado, simplemente asigna predicados (también llamados términos ) a predicados.

Podría decirse que PFL es el más sencillo de estos formalismos, pero también el que menos se ha escrito.

Quine sintió fascinación durante toda su vida por la lógica combinatoria , como lo demuestra su introducción a la traducción en Van Heijenoort (1967) del artículo del lógico ruso Moses Schönfinkel que fundaba la lógica combinatoria. Cuando Quine comenzó a trabajar seriamente en PFL, en 1959, la lógica combinatoria era considerada un fracaso por las siguientes razones:

• Hasta que Dana Scott comenzó a escribir sobre la teoría de modelos de la lógica combinatoria a finales 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 descubrió que algunas formulaciones de la 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 considerado un formalismo superior.

La sintaxis , los primitivos y los axiomas de 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).

Un término atómico es una letra latina mayúscula, excepto la I y la S , seguida de un superíndice numérico llamado 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 predicada. Un término atómico de grado 0 denota una variable booleana o un valor de verdad . El grado de la I es invariablemente 2, por lo que no se indica.

Los functores de predicado "combinatorios" (término acuñado por Quine), todos monádicos y propios de PFL, son Inv , inv , ∃ , + y p . Un término es atómico o se construye mediante la siguiente regla recursiva. Si τ es un término, entonces Inv τ, inv τ, ∃ τ, + τ y p τ son términos. Un functor con un superíndice n , donde n es un número natural > 1, denota n aplicaciones consecutivas (iteraciones) de dicho functor.

Una fórmula es un término o se define mediante la regla recursiva: si α y β son fórmulas, entonces αβ y ~(α) también lo son. Por lo tanto, "~" es otro functor monádico, y la concatenación es el único functor predicado diádico. Quine denominó a estos functores "alécticos". La interpretación natural de "~" es la negación ; la de la concatenación es cualquier conector que, al combinarse con la negación, forma un conjunto funcionalmente completo de conectores. El conjunto funcionalmente completo preferido por Quine era la conjunción y la negación . Así, los términos concatenados se toman como conjuntivos. La notación + es de Bacon (1985); toda la demás notación es de Quine (1976; 1982). La parte aléctica de PFL es idéntica a los esquemas de términos booleanos de Quine (1982).

Como es bien sabido, los dos functores alécticos podrían ser reemplazados por un único 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 ).

Quine no estableció ni una axiomatización ni un procedimiento de demostración 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 ofrece otra axiomatización que prescinde de variables libres, pero esta es más difícil de describir y hace un uso extensivo de functores definidos. Kuhn demostró que ambas axiomatizaciones de PFL son correctas y completas .

Esta sección se basa en los functores de predicados primitivos y algunos definidos. Los functores alécticos pueden axiomatizarse mediante cualquier conjunto de axiomas de la lógica sentencial cuyos primitivos sean la negación y uno de los operadores ∧ o ∨. De forma equivalente, todas las tautologías de la lógica sentencial pueden considerarse axiomas.

La semántica de Quine (1982) para cada functor predicado se presenta a continuación en términos de abstracción (notación de constructor de conjuntos), seguida del axioma correspondiente de Kuhn (1983) o una definición de Quine (1976). La notación denota el conjunto de n -tuplas que satisfacen la fórmula atómica.${\displaystyle \{x_{1}\cdots x_{n}:Fx_{1}\cdots x_{n}\}}$${\displaystyle Fx_{1}\cdots x_{n}.}$

• La identidad , I , se define como:

${\displaystyle IFx_{1}x_{2}\cdots x_{n}\leftrightarrow (Fx_{1}x_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{2}\cdots x_{n}){\text{.}}}$

La identidad es reflexiva ( Ixx ), simétrica ( Ixy → Iyx ), transitiva ( ( Ixy ∧ Iyz ) → Ixz ), y obedece la propiedad de sustitución:

${\displaystyle (Fx_{1}\cdots x_{n}\land Ix_{1}y)\rightarrow Fyx_{2}\cdots x_{n}.}$

• El relleno , + , agrega una variable a la izquierda de cualquier lista de argumentos.

${\displaystyle \ +F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{0}x_{1}\cdots x_{n}:F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle +Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}\cdots x_{n}.}$

• El recorte , ∃ , borra la variable situada más a la izquierda en cualquier lista de argumentos.

${\displaystyle \exists F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:\exists x_{1}F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle Fx_{1}\cdots x_{n}\rightarrow \exists Fx_{2}\cdots x_{n}.}$

El recorte permite dos functores definidos útiles:

• Reflexión , S :

${\displaystyle SF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:F^{n}x_{2}x_{2}\cdots x_{n}\}.}$

${\displaystyle SF^{n}\leftrightarrow \exists IF^{n}.}$

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 ,;${\displaystyle \times }$

${\displaystyle F^{m}\times G^{n}\leftrightarrow F^{m}\exists ^{m}G^{n}.}$

Aquí, Quine adoptó la notación infija porque esta notación para el producto cartesiano está muy bien establecida en matemáticas. El producto cartesiano permite reformular la conjunción de la siguiente manera:

${\displaystyle F^{m}x_{1}\cdots x_{m}G^{n}x_{1}\cdots x_{n}\leftrightarrow (F^{m}\times G^{n})x_{1}\cdots x_{m}x_{1}\cdots x_{n}.}$

Reordena la lista de argumentos concatenados de manera que un par de variables duplicadas se desplacen al extremo izquierdo, luego invoca S para eliminar la duplicación. Repitiendo esto tantas veces como sea necesario, se obtiene una lista de argumentos de longitud max( m , n ).

Los siguientes tres functores permiten reordenar las listas de argumentos a voluntad.

• La inversión mayor , Inv , rota las variables de una lista de argumentos hacia la derecha, de modo que la última variable se convierte en la primera.

${\displaystyle \operatorname {Inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{n}x_{1}\cdots x_{n-1}\}.}$

${\displaystyle \operatorname {Inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{n}x_{1}\cdots x_{n-1}.}$

• La inversión menor , inv , intercambia las dos primeras variables de una lista de argumentos.

${\displaystyle \operatorname {inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{2}x_{1}\cdots x_{n}\}.}$

${\displaystyle \operatorname {inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{1}\cdots x_{n}.}$

• La permutación , p , rota las variables desde la segunda hasta la última en una lista de argumentos hacia la izquierda, de modo que la segunda variable se convierte en la última.

${\displaystyle \ pF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{1}x_{3}\cdots x_{n}x_{2}\}.}$

${\displaystyle pFx_{1}\cdots x_{n}\leftrightarrow \operatorname {Inv} \operatorname {inv} Fx_{1}x_{3}\cdots x_{n}x_{2}.}$

Dada una lista de argumentos que consta de n variables, p trata implícitamente las últimas n −1 variables como una cadena de bicicleta, donde cada variable constituye un eslabón en la cadena. Una aplicación de p avanza la cadena un eslabón. k aplicaciones consecutivas de p a F ⁿ mueven la variable k +1 a la segunda posición de argumento en F .

Cuando n = 2, Inv e inv simplemente intercambian x ₁ y x _2. Cuando n = 1, no tienen ningún efecto. Por lo tanto, p no tiene ningún 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 un análogo para la permutación y, por lo tanto, no tiene axiomas para ella. Si, siguiendo a Quine (1976), se toma p como primitiva, Inv e inv pueden definirse como combinaciones no triviales de + , ∃ y p iterada .

La siguiente tabla resume cómo los functores afectan los grados de sus argumentos.

Todas las instancias de una letra predicativa pueden ser reemplazadas por otra letra predicativa del mismo grado, sin afectar la validez. Las reglas son:

• Modus ponens ;
• Sean α y β fórmulas PFL en las que no aparece. Entonces, si es un teorema PFL, entonces también lo es.${\displaystyle x_{1}}$${\displaystyle (\alpha \land Fx_{1}...x_{n})\rightarrow \beta }$${\displaystyle (\alpha \land \exists Fx_{2}...x_{n})\rightarrow \beta }$

En lugar de axiomatizar PFL, Quine (1976) propuso las siguientes conjeturas como axiomas candidatos.

${\displaystyle \exists I}$

n −1 iteraciones consecutivas de p restablecen el status quo ante :

${\displaystyle F^{n}\leftrightarrow p^{n-1}F^{n}}$

+ y ∃ se aniquilan mutuamente:

${\displaystyle {\begin{cases}F^{n}\rightarrow +\exists F^{n}\\F^{n}\leftrightarrow \exists +F^{n}\end{cases}}}$

La negación se distribuye sobre + , ∃ , y p :

${\displaystyle {\begin{cases}+\lnot F^{n}\leftrightarrow \lnot +F^{n}\\\lnot \exists F^{n}\rightarrow \exists \lnot F^{n}\\p\lnot F^{n}\leftrightarrow \lnot pF^{n}\end{cases}}}$

+ y p se distribuye sobre la conjunción:

${\displaystyle {\begin{cases}+(F^{n}G^{m})\leftrightarrow (+F^{n}+G^{m})\\p(F^{n}G^{m})\leftrightarrow (pF^{n}pG^{m})\end{cases}}}$

La identidad tiene una implicación interesante:

${\displaystyle IF^{n}\rightarrow p^{n-2}\exists p+F^{n}}$

Quine también conjeturó la regla: Si α es un teorema PFL, entonces también lo son pα , +α , y . ${\displaystyle \lnot \exists \lnot \alpha }$

Bacon (1985) toma la condicional , la negación , la identidad , el relleno y la inversión mayor y menor como primitivos, y el recorte como definido. Empleando una terminología y notación que difieren un poco de las anteriores, Bacon (1985) establece dos formulaciones de PFL:

• Una formulación deductiva natural al estilo de Frederick Fitch . Bacon demuestra que esta formulación es sólida y completa con todo detalle.
• Una formulación axiomática que Bacon afirma, pero no demuestra, como equivalente a la anterior. Algunos de estos axiomas son simplemente conjeturas de Quine reformuladas con la notación de Bacon.

El tocino también:

• Analiza la relación de PFL con la lógica de términos de Sommers (1982) y argumenta que reformular PFL utilizando 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 sentencial , la lógica de predicados monádicos , la lógica modal S5 y la lógica booleana de relaciones (no) permutadas son todos fragmentos de 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 del predicado, indicando su grado;
• Traduzca todos los cuantificadores universales a cuantificadores existenciales y negación;
• Reformule todas las fórmulas atómicas de la forma x = y como Ixy .

Ahora aplique el siguiente algoritmo al resultado anterior:

La traducción inversa, de PFL a lógica de primer orden, se analiza en Quine (1976: 302–4).

El fundamento canónico de las matemáticas es la teoría axiomática de conjuntos , con una lógica subyacente que consiste en lógica de primer orden con identidad , y un universo de discurso compuesto enteramente por conjuntos. Existe una única letra predicado de grado 2, interpretada como pertenencia a un conjunto. La traducción a lenguaje práctico de la teoría axiomática de conjuntos canónica ZFC no es difícil, ya que ningún axioma de ZFC requiere más de 6 variables cuantificadas. ^{[ 2 ]}

• Lógica algebraica

• Bacon, John, 1985, " La completitud 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, " Una axiomatización de la lógica de functores de predicados ", Notre Dame Journal of Formal Logic 24 : 233–41.
• Willard Quine , 1976, "Lógica algebraica y functores predicativos" en Ways of Paradox and Other Essays , edición revisada y ampliada. Harvard Univ. Press: 283–307.
• Willard Quine, 1982. Métodos de lógica , 4.ª ed. Harvard Univ. Press. Cap. 45.
• Sommers, Fred , 1982. La lógica del lenguaje natural . Oxford Univ. Press.
• Alfred Tarski y Steven Givant, 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 referencia sobre lógica matemática . Harvard Univ. Press.

• Introducción a la lógica de predicados y functores (descarga con un solo clic, archivo PS) por Mats Dahllöf (Departamento de Lingüística, Universidad de Uppsala)