Lógica de función predicativa

Algebrización de la lógica de primer orden

En lógica matemática , la lógica de funtores de predicados ( LFP ) es una de las diversas formas de expresar la lógica de primer orden (también conocida como lógica de predicados ) por medios puramente algebraicos, es decir, sin variables cuantificadas . La LFP emplea una pequeña cantidad de dispositivos algebraicos llamados funtores de predicados (o modificadores de predicados ) ^[1] que operan sobre términos para producir términos. La LFP es en su mayor parte una 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 la PFL como una forma de algebraizar la lógica de primer orden de una manera análoga a cómo el álgebra de Boole algebra la lógica proposicional . Diseñó la PFL para que tuviera exactamente el poder expresivo de la lógica de primer orden con identidad . Por lo tanto, las metamatemáticas de la PFL son exactamente las de la lógica de primer orden sin letras predicativas 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 tocó la 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 funtor , de significado gramatical pero de significado lógico... es un signo que se une 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 distintas de PFL para algebrar la lógica de primer orden incluyen:

• Álgebra cilíndrica de Alfred Tarski y sus estudiantes americanos. 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 "funtor predicado";
• El álgebra poliádica de Paul Halmos . En virtud de sus primitivos económicos y axiomas , esta álgebra se parece más a 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 y que se encuentran en el alcance de más de tres cuantificadores . Ese fragmento es suficiente, sin embargo, 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 manifiesto 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 tener el poder expresivo de la teoría de conjuntos , lo que hace que la lógica combinatoria sea vulnerable a las paradojas . Un funtor de predicado, por otro lado, simplemente mapea predicados (también llamados términos ) en predicados.

Se podría decir que el PFL es el más simple de estos formalismos, pero también aquel sobre el que menos se ha escrito.

Quine estuvo fascinado 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 fundó la lógica combinatoria. Cuando Quine comenzó a trabajar en PFL en serio, 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 sólo 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 aparecer. 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 , era visto como un formalismo superior.

Formalización de Kuhn

La sintaxis , los primitivos y los axiomas del PFL descritos en esta sección son en gran parte de Steven Kuhn (1983). La semántica de los funtores es de Quine (1982). El resto de esta entrada incorpora cierta 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 en minúscula concatenadas, conocidas colectivamente como una 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 predicativa. Un término atómico de grado 0 denota una variable booleana o un valor de verdad . El grado de I es invariablemente 2 y, por lo tanto, no se indica.

Los funtores predicativos "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 está construido mediante la siguiente regla recursiva. Si τ es un término, entonces Inv τ, inv τ, ∃ τ, + τ y p τ 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 se define por la regla recursiva: si α y β son fórmulas, entonces αβ y ~(α) son igualmente fórmulas. Por lo tanto, "~" es otro funtor monádico, y la concatenación es el único funtor predicativo diádico. Quine llamó a estos funtores "aléticos". La interpretación natural de "~" es negación ; la de 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 conjunción y negación . Por lo tanto, los términos concatenados se toman como unidos. La notación + es de Bacon (1985); todas las demás notaciones son 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 funtores aléticos podrían ser reemplazados por un único funtor 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 propuso ni una axiomatización ni un 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 ofrece 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 funtores definidos. Kuhn demostró que ambas axiomatizaciones de PFL son sólidas y completas .

Esta sección se basa en los funtores predicativos primitivos y algunos definidos. Los funtores aléticos pueden axiomatizarse mediante cualquier conjunto de axiomas de lógica enunciativa cuyos primitivos sean la negación y uno de ∧ o ∨. De manera equivalente, todas las tautologías de lógica enunciativa pueden tomarse como axiomas.

La semántica de Quine (1982) para cada funtor predicado se enuncia a continuación en términos de abstracción (notación de constructor de conjuntos), seguida del axioma relevante de Kuhn (1983) o de 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 , yo , 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}.}$

• 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}.}$

• Al recortar , ∃ , borra la variable 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 funciones definidas ú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. NB: 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}.}$

En este caso, 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 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}.}$

Reordene la lista de argumentos concatenados de modo de desplazar un par de variables duplicadas hacia el extremo izquierdo y luego invoque S para eliminar la duplicación. Si repite esto tantas veces como sea necesario, obtendrá una lista de argumentos con una longitud máxima ( m , n ).

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

• 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.

${\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}.}$

• Inversión menor , inv , intercambia las dos primeras variables en 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 la segunda a la última variable 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, en la que cada variable constituye un eslabón de la cadena. Una aplicación de p hace avanzar 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 ₂ . Cuando n = 1, no tienen efecto. Por lo tanto, p no tiene efecto cuando n < 3.

Kuhn (1983) considera que la inversión mayor y la inversión menor son primitivas. La notación p en Kuhn corresponde a inv ; no tiene análogo para la permutación y, por lo tanto, no tiene axiomas para ella. Si, siguiendo a Quine (1976), p se toma como primitiva, Inv e inv pueden definirse como combinaciones no triviales de + , ∃ y p iterado .

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

Normas

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

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

Algunos resultados útiles

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 entre sí:

${\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 distribuyen 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 }$

El trabajo de Bacon

Bacon (1985) toma el 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 una notación que difieren un poco de las anteriores, 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, que es equivalente a la anterior. Algunos de estos axiomas son simplemente conjeturas de Quine reformuladas en la notación de Bacon.

Tocino también:

• Se analiza la relación del PFL con la lógica de términos de Sommers (1982) y se sostiene que reformular el PFL utilizando una sintaxis propuesta en el apéndice de Lockwood a Sommers debería hacer que el PFL sea más fácil de "leer, usar y enseñar";
• Se aborda la estructura teórica de grupos de Inv e inv ;
• Menciona que la lógica oracional , la lógica de predicados monádicos , la lógica modal S5 y la lógica booleana de relaciones (no)permutadas son todas fragmentos de PFL.

De la lógica de primer orden a PFL

El siguiente algoritmo es una adaptación 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;
• Traducir todos los cuantificadores universales en cuantificadores existenciales y negación;
• Reformular 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 disyunciones 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 utilizando la regla de paso (Quine 1982: 119):

   ${\displaystyle \exists x[\alpha (x)\lor \gamma (x)]\leftrightarrow (\exists x\alpha (x)\lor \exists x\gamma (x)).}$

3. Reemplazar la conjunción por el producto cartesiano , invocando el hecho:
   ${\displaystyle (F^{m}\land G^{n})\leftrightarrow (F^{m}\times G^{n})\leftrightarrow (F^{m}\exists ^{m}G^{n});m<n.}$
4. Concatene las listas de argumentos de todos los términos atómicos y mueva 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 las instancias de y excepto la última . Elimine y anteponiendo a la subfórmula una instancia de ∃ .
7. Repita los pasos (1) a (6) hasta que se hayan eliminado todas las variables cuantificadas. Elimine cualquier disyunción que esté dentro del alcance de un cuantificador invocando la equivalencia:
   ${\displaystyle (\alpha \lor \beta \lor ...)\leftrightarrow \lnot (\lnot \alpha \land \lnot \beta \land ...).}$

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

La base canónica de las matemáticas es la teoría axiomática de conjuntos , con una lógica de fondo que consiste en lógica de primer orden con identidad , con un universo de discurso que consiste enteramente en conjuntos. Hay una única letra predicativa de grado 2, interpretada como pertenencia al conjunto. La traducción PFL de la teoría axiomática de conjuntos canónica ZFC no es difícil, ya que ningún axioma ZFC requiere más de 6 variables cuantificadas. ^[2]

Véase también

• Lógica algebraica

Notas al pie

1. Johannes Stern, Hacia enfoques predicados de la modalidad , Springer, 2015, pág. 11.
2. Axiomas de Metamath.

Referencias

• Bacon, John, 1985, "La completitud de una lógica 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 del functor predicado", Notre Dame Journal of Formal Logic 24 : 233–41.
• Willard Quine , 1976, "Lógica algebraica y funtores predicados" 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 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 . Harvard Univ. Press.

Enlaces externos

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