Cálculo proposicional - Propositional calculus

El cálculo proposicional es una rama de la lógica . También se llama la lógica proposicional , lógica declaración , cálculo proposicional , lógica proposicional , o, a veces la lógica de orden cero . Se trata de proposiciones (que pueden ser verdaderas o falsas) y relaciones entre proposiciones, incluida la construcción de argumentos basados ​​en ellas. Las proposiciones compuestas se forman conectando proposiciones mediante conectivos lógicos . Las proposiciones que no contienen conectivos lógicos se denominan proposiciones atómicas.

A diferencia de la lógica de primer orden , la lógica proposicional no se ocupa de objetos no lógicos, predicados sobre ellos o cuantificadores . Sin embargo, toda la maquinaria de la lógica proposicional está incluida en la lógica de primer orden y la lógica de orden superior. En este sentido, la lógica proposicional es la base de la lógica de primer orden y la lógica de orden superior.

Explicación

Los conectivos lógicos se encuentran en los lenguajes naturales. En inglés, por ejemplo, algunos ejemplos son "y" ( conjunción ), "o" ( disyunción ), "no" ( negación ) y "si" (pero solo cuando se usa para denotar material condicional ).

El siguiente es un ejemplo de una inferencia muy simple dentro del alcance de la lógica proposicional:

Premisa 1: Si llueve, está nublado.
Premisa 2: Está lloviendo.
Conclusión: está nublado.

Tanto las premisas como la conclusión son proposiciones. Las premisas se dan por sentado, y con la aplicación del modus ponens (una regla de inferencia ), se llega a la conclusión.

Como la lógica proposicional no se ocupa de la estructura de las proposiciones más allá del punto en el que ya no pueden ser descompuestas por conectivos lógicos, esta inferencia puede reformularse reemplazando esos enunciados atómicos con letras de enunciado, que se interpretan como variables que representan enunciados:

Premisa 1:
Premisa 2:
Conclusión:

Lo mismo puede enunciarse sucintamente de la siguiente manera:

Cuando P se interpreta como "Está lloviendo" y Q como "está nublado", se puede ver que las expresiones simbólicas anteriores se corresponden exactamente con la expresión original en lenguaje natural. No solo eso, sino que también se corresponderán con cualquier otra inferencia de esta forma , que será válida sobre la misma base que esta inferencia.

La lógica proposicional puede estudiarse mediante un sistema formal en el que las fórmulas de un lenguaje formal pueden interpretarse para representar proposiciones . Un sistema de axiomas y reglas de inferencia permite derivar ciertas fórmulas. Estas fórmulas derivadas se denominan teoremas y pueden interpretarse como proposiciones verdaderas. Una secuencia construida de tales fórmulas se conoce como derivación o prueba y la última fórmula de la secuencia es el teorema. La derivación puede interpretarse como prueba de la proposición representada por el teorema.

Cuando se usa un sistema formal para representar la lógica formal, solo las letras de declaración (generalmente letras mayúsculas romanas como , y ) se representan directamente. Las proposiciones del lenguaje natural que surgen cuando se interpretan están fuera del alcance del sistema, y ​​la relación entre el sistema formal y su interpretación también está fuera del sistema formal mismo.

En la lógica proposicional funcional de la verdad clásica , las fórmulas se interpretan como si tuvieran precisamente uno de dos posibles valores de verdad , el valor de verdad de verdadero o el valor de verdad de falso . Se defienden el principio de bivalencia y la ley del medio excluido . La lógica proposicional funcional de la verdad definida como tal y los sistemas isomórficos a ella se consideran lógica de orden cero . Sin embargo, también son posibles lógicas proposicionales alternativas. Para obtener más información, consulte Otros cálculos lógicos a continuación.

Historia

Aunque la lógica proposicional (que es intercambiable con el cálculo proposicional) había sido insinuada por filósofos anteriores, Crisipo la desarrolló en una lógica formal ( lógica estoica ) en el siglo III a. C. y la amplió su sucesor estoico . La lógica se centró en proposiciones . Este avance fue diferente de la lógica silogística tradicional , que se centró en los términos . Sin embargo, la mayoría de los escritos originales se perdieron y la lógica proposicional desarrollada por los estoicos ya no se entendió más tarde en la antigüedad. En consecuencia, el sistema fue reinventado esencialmente por Peter Abelard en el siglo XII.

La lógica proposicional finalmente se refinó utilizando la lógica simbólica . Al matemático de los siglos XVII / XVIII, Gottfried Leibniz, se le atribuye el mérito de ser el fundador de la lógica simbólica por su trabajo con el razonador de cálculo . Aunque su trabajo fue el primero de su tipo, fue desconocido para la comunidad lógica en general. En consecuencia, muchos de los avances logrados por Leibniz fueron recreados por lógicos como George Boole y Augustus De Morgan —completamente independientes de Leibniz.

Así como la lógica proposicional puede considerarse un avance de la lógica silogística anterior, la lógica de predicados de Gottlob Frege también puede considerarse un avance de la lógica proposicional anterior. Un autor describe la lógica de predicados como una combinación de "las características distintivas de la lógica silogística y la lógica proposicional". En consecuencia, la lógica de predicados marcó el comienzo de una nueva era en la historia de la lógica; sin embargo, los avances en la lógica proposicional todavía se hicieron después de Frege, incluida la deducción natural , los árboles de verdad y las tablas de verdad . La deducción natural fue inventada por Gerhard Gentzen y Jan Łukasiewicz . Los árboles de la verdad fueron inventados por Evert Willem Beth . La invención de tablas de verdad, sin embargo, es de atribución incierta.

Dentro de las obras de Frege y Bertrand Russell , hay ideas que influyeron en la invención de las tablas de verdad. La estructura tabular real (que tiene el formato de una tabla), en sí misma, generalmente se atribuye a Ludwig Wittgenstein o Emil Post (o ambos, de forma independiente). Además de Frege y Russell, otros a quienes se les atribuye tener ideas que preceden a las tablas de verdad incluyen a Philo, Boole, Charles Sanders Peirce y Ernst Schröder . Otros a quienes se les atribuye la estructura tabular incluyen a Jan Łukasiewicz , Alfred North Whitehead , William Stanley Jevons , John Venn y Clarence Irving Lewis . En última instancia, algunos han llegado a la conclusión, como John Shosky, de que "no está nada claro que a una persona se le deba otorgar el título de 'inventor' de las tablas de verdad".

Terminología

En términos generales, un cálculo es un sistema formal que consta de un conjunto de expresiones sintácticas ( fórmulas bien formadas ), un subconjunto distinguido de estas expresiones (axiomas), más un conjunto de reglas formales que definen una relación binaria específica , destinada a ser interpretado como equivalencia lógica , en el espacio de expresiones.

Cuando se pretende que el sistema formal sea un sistema lógico , las expresiones se interpretan como enunciados y las reglas, conocidas como reglas de inferencia , suelen estar destinadas a preservar la verdad. En este contexto, las reglas, que pueden incluir axiomas , se pueden utilizar para derivar ("inferir") fórmulas que representan enunciados verdaderos, a partir de fórmulas dadas que representan enunciados verdaderos.

El conjunto de axiomas puede estar vacío, un conjunto finito no vacío o un conjunto infinito numerable (ver esquema de axiomas ). Una gramática formal define de forma recursiva las expresiones y fórmulas bien formadas del lenguaje . Además, se puede dar una semántica que defina la verdad y las valoraciones (o interpretaciones ).

El lenguaje de un cálculo proposicional consiste en

  1. un conjunto de símbolos primitivos, conocidos como fórmulas atómicas , marcadores de posición , letras de proposición o variables , y
  2. un conjunto de símbolos de operador, interpretados de diversas formas como operadores lógicos o conectivos lógicos .

Una fórmula bien formada es cualquier fórmula atómica, o cualquier fórmula que se pueda construir a partir de fórmulas atómicas mediante símbolos de operador de acuerdo con las reglas de la gramática.

Los matemáticos a veces distinguen entre constantes proposicionales, variables proposicionales y esquemas. Las constantes proposicionales representan una proposición particular, mientras que las variables proposicionales se extienden sobre el conjunto de todas las proposiciones atómicas. Los esquemas, sin embargo, abarcan todas las proposiciones. Es común representar constantes proposicionales por A , B y C , variables proposicionales por P , Q y R , y las letras esquemáticas son a menudo letras griegas, más a menudo φ , ψ y χ .

Conceptos básicos

A continuación se describe un cálculo proposicional estándar. Existen muchas formulaciones diferentes que son todas más o menos equivalentes, pero difieren en los detalles de:

  1. su lenguaje (es decir, la colección particular de símbolos primitivos y símbolos de operador),
  2. el conjunto de axiomas, o fórmulas distinguidas, y
  3. el conjunto de reglas de inferencia.

Cualquier proposición dada puede representarse con una letra llamada "constante proposicional", análoga a representar un número por una letra en matemáticas (por ejemplo, a = 5 ). Todas las proposiciones requieren exactamente uno de dos valores de verdad: verdadero o falso. Por ejemplo, sea P la proposición de que está lloviendo afuera. Esto será verdadero ( P ) si está lloviendo afuera, y falso en caso contrario ( ¬ P ).

  • Luego definimos los operadores funcionales de verdad , comenzando con la negación. ¬ P representa la negación de P , que puede ser pensado como la negación de P . En el ejemplo anterior, ¬ P expresa que no llueve afuera, o por una lectura más estándar: "No es el caso que llueve afuera". Cuando P es verdadero, ¬ P es falso; y cuando P es falso, ¬ P es verdadero. Como resultado, ¬¬ P siempre tiene el mismo valor de verdad como P .
  • Conjunción es un conectivo verdad-funcional que forma una proposición de dos proposiciones más simples, por ejemplo, P y Q . La conjunción de P y Q se escribe PQ , y expresa que cada uno es verdadero. Leemos PQ como " P y Q ". Para dos proposiciones cualesquiera, hay cuatro posibles asignaciones de valores de verdad:
    1. P es cierto y Q es cierto
    2. P es verdadero y Q es falso
    3. P es falso y Q es verdadero
    4. P es falso y Q es falso
La conjunción de P y Q es verdadera en el caso 1 y falsa en caso contrario. Donde P es la proposición de que está lloviendo afuera y Q es la proposición de que un frente frío está sobre Kansas, PQ es cierto cuando está lloviendo afuera y hay un frente frío sobre Kansas. Si no llueve afuera, entonces P ∧ Q es falso; y si no hay un frente frío sobre Kansas, entonces PQ también es falso.
  • La disyunción se parece a la conjunción en que forma una proposición a partir de dos proposiciones más simples. Lo escribimos PQ , y se lee " P o Q ". Expresa que P o Q son verdaderos. Por lo tanto, en los casos enumerados anteriormente, la disyunción de P con Q es verdadera en todos los casos, excepto en el caso 4. Usando el ejemplo anterior, la disyunción expresa que está lloviendo afuera o hay un frente frío sobre Kansas. (Tenga en cuenta que se supone que este uso de disyunción se asemeja al uso de la palabra inglesa "o". Sin embargo, es más parecido a la palabra inglesa inclusiva "o", que puede usarse para expresar la verdad de al menos una de dos proposiciones. No es como el "o" exclusivo en inglés , que expresa la verdad de exactamente una de dos proposiciones. En otras palabras, el "o" exclusivo es falso cuando tanto P como Q son verdaderas (caso 1). Un ejemplo de la exclusiva o es: puede tener un bagel o un pastel, pero no ambos. A menudo, en lenguaje natural, dado el contexto apropiado, el apéndice "pero no ambos" se omite, pero está implícito. En matemáticas, sin embargo, "o" es siempre inclusivo o; si es exclusivo o, se especificará, posiblemente mediante "xor".)
  • El material condicional también une dos proposiciones más simples, y escribimos PQ , que se lee "si P entonces Q ". La proposición a la izquierda de la flecha se llama antecedente y la proposición a la derecha se llama consecuente. (No existe tal designación para conjunción o disyunción, ya que son operaciones conmutativas). Expresa que Q es verdadero siempre que P es verdadero. Por lo tanto, PQ es verdadero en todos los casos anteriores, excepto en el caso 2, porque este es el único caso en el que P es verdadero pero Q no lo es. Usando el ejemplo, si P entonces Q expresa que si está lloviendo afuera, entonces hay un frente frío sobre Kansas. El condicional material a menudo se confunde con la causalidad física. Sin embargo, el condicional material sólo relaciona dos proposiciones por sus valores de verdad, que no es la relación de causa y efecto. Es polémico en la literatura si la implicación material representa una causalidad lógica.
  • Bicondicional une dos proposiciones más simples, y escribimos PQ , que se lee " P si y solo si Q ". Expresa que P y Q tienen el mismo valor de verdad, y en los casos 1 y 4. " P es verdadero si y sólo si Q " es verdadero, y es falso en caso contrario.

Es muy útil mirar las tablas de verdad para estos diferentes operadores, así como el método de los cuadros analíticos .

Cierre en operaciones

La lógica proposicional se cierra bajo conectivas funcionales de verdad. Es decir, para cualquier proposición φ , ¬ φ también es una proposición. Del mismo modo, para cualquier proposición φ y ψ , φψ es una proposición, y de manera similar para la disyunción, condicional y bicondicional. Esto implica que, por ejemplo, φψ es una proposición, por lo que se puede unir con otra proposición. Para representar esto, necesitamos usar paréntesis para indicar qué proposición se une con cuál. Por ejemplo, PQR no es una fórmula bien formada, debido a que no sabemos si estamos uniéndonos PQ con R o si estamos uniéndonos P con QR . Por lo tanto, debemos escribir ( PQ ) ∧ R para representar el primero, o P ∧ ( QR ) para representar el último. Al evaluar las condiciones de verdad, vemos que ambas expresiones tienen las mismas condiciones de verdad (serán verdaderas en los mismos casos), y además que cualquier proposición formada por conjunciones arbitrarias tendrá las mismas condiciones de verdad, independientemente de la ubicación de los paréntesis. Esto significa que la conjunción es asociativa, sin embargo, no se debe asumir que los paréntesis nunca tienen un propósito. Por ejemplo, la oración P ∧ ( QR ) no tiene las mismas condiciones de verdad de ( PQ ) ∨ R , por lo que son oraciones diferentes que se distinguen solo por el paréntesis. Uno puede verificar esto mediante el método de la tabla de verdad al que se hace referencia anteriormente.

Nota: Para cualquier número arbitrario de constantes proposicionales, podemos formar un número finito de casos que enumeren sus posibles valores de verdad. Una forma sencilla de generar esto es mediante tablas de verdad, en las que se escribe P , Q , ..., Z , para cualquier lista de k constantes proposicionales, es decir, cualquier lista de constantes proposicionales con k entradas. Debajo de esta lista, se escriben 2 k filas, y debajo de P se llena la primera mitad de las filas con verdadero (o T) y la segunda mitad con falso (o F). Debajo de Q, se llena un cuarto de las filas con T, luego un cuarto con F, luego un cuarto con T y el último cuarto con F. La siguiente columna alterna entre verdadero y falso para cada octavo de las filas, luego dieciseisavos, y así sucesivamente, hasta que la última constante proposicional varíe entre T y F para cada fila. Esto dará una lista completa de casos o asignaciones de valores de verdad posibles para esas constantes proposicionales.

Argumento

El cálculo proposicional luego define un argumento como una lista de proposiciones. Un argumento válido es una lista de proposiciones, la última de las cuales se sigue o está implícita en el resto. Todos los demás argumentos son inválidos. El argumento válido más simple es modus ponens , uno de cuyos ejemplos es la siguiente lista de proposiciones:

Esta es una lista de tres proposiciones, cada línea es una proposición y la última se sigue del resto. Las dos primeras líneas se denominan premisas y la última línea la conclusión. Decimos que cualquier proposición C se sigue de cualquier conjunto de proposiciones , si C debe ser verdadera siempre que todos los miembros del conjunto sean verdaderos. En el argumento anterior, para cualquier P y Q , siempre que PQ y P son verdaderas, necesariamente Q es verdadera. Observe que, cuando P es verdadero, no podemos considerar los casos 3 y 4 (de la tabla de verdad). Cuando PQ es cierto, no podemos considerar el caso 2. Esto deja solo el caso 1, en el que Q también es cierto. Por tanto, Q está implícito en las premisas.

Esto se generaliza esquemáticamente. Por tanto, donde φ y ψ pueden ser cualquier proposición,

Otras formas de argumento son convenientes, pero no necesarias. Dado un conjunto completo de axiomas (ver más abajo para uno de esos conjuntos), modus ponens es suficiente para probar todas las demás formas de argumento en lógica proposicional, por lo que pueden considerarse derivadas. Tenga en cuenta que esto no es cierto para la extensión de la lógica proposicional a otras lógicas como la lógica de primer orden . La lógica de primer orden requiere al menos una regla de inferencia adicional para obtener la completitud .

El significado del argumento en lógica formal es que uno puede obtener nuevas verdades a partir de verdades establecidas. En el primer ejemplo anterior, dadas las dos premisas, la verdad de Q aún no se conoce ni se declara. Una vez realizado el argumento, se deduce Q. De esta manera, definimos un sistema de deducción como un conjunto de todas las proposiciones que pueden deducirse de otro conjunto de proposiciones. Por ejemplo, dado el conjunto de proposiciones , podemos definir un sistema de deducción, Γ , que es el conjunto de todas las proposiciones que se siguen de una . La reiteración siempre se asume, por lo . Además, desde el primer elemento de A , último elemento, así como modus ponens, R es una consecuencia, y así . Sin embargo, debido a que no hemos incluido axiomas suficientemente completos, no se puede deducir nada más. Por lo tanto, aunque la mayoría de los sistemas de deducción estudiados en lógica proposicional son capaces de deducir , éste es demasiado débil para probar tal proposición.

Descripción genérica de un cálculo proposicional

Un cálculo proposicional es un sistema formal , donde:

  • El conjunto alfa es un conjunto numerable infinito de elementos llamados símbolos de proposiciones o variables proposicionales . Hablando sintácticamente, estos son los elementos más básicos del lenguaje formal , también conocidos como fórmulas atómicas o elementos terminales . En los ejemplos siguientes, los elementos de suelen ser las letras p , q , r , etc.
  • El conjunto omega Ω es un conjunto finito de elementos llamados símbolos de operador o conectivos lógicos . El conjunto Ω se divide en subconjuntos separados de la siguiente manera:

    En esta partición, está el conjunto de símbolos de operador de

    aridad j .

    En los cálculos proposicionales más familiares, Ω generalmente se divide de la siguiente manera:

    Una convención adoptada con frecuencia trata los valores lógicos constantes como operadores de aridad cero, así:

    Algunos escritores usan la tilde (~) o N, en lugar de ¬ ; y algunos usan v en lugar de así como el
    ampersand (&), el prefijo K, o en lugar de . La notación varía aún más para el conjunto de valores lógicos, con símbolos como {falso, verdadero}, {F, T} o {0, 1} que se ven todos en varios contextos en lugar de .
  • El conjunto zeta es un conjunto finito de reglas de transformación que se denominan reglas de inferencia cuando adquieren aplicaciones lógicas.
  • El conjunto de iotas es un conjunto contable de puntos iniciales que se denominan axiomas cuando reciben interpretaciones lógicas.

El lenguaje de , también conocido como su conjunto de fórmulas , fórmulas bien formadas , se define inductivamente por las siguientes reglas:

  1. Base: cualquier elemento del conjunto alfa es una fórmula de .
  2. Si son fórmulas y está en , entonces es una fórmula.
  3. Cerrado: Nada más es una fórmula de .

La aplicación repetida de estas reglas permite la construcción de fórmulas complejas. Por ejemplo:

  • Según la regla 1, p es una fórmula.
  • Por regla 2, es una fórmula.
  • Según la regla 1, q es una fórmula.
  • Por regla 2, es una fórmula.

Ejemplo 1. Sistema de axiomas simple

Deje , donde , , , se define como sigue:

  • El conjunto alfa es un conjunto infinito contable de símbolos, por ejemplo:
  • De los tres conectivos para conjunción, disyunción e implicación ( , y ), uno puede tomarse como primitivo y los otros dos pueden definirse en términos de él y negación ( ¬ ). Todas las conectivas lógicas se pueden definir en términos de un único operador suficiente . Por supuesto, el bicondicional ( ) se puede definir en términos de conjunción e implicación, con definido como .
    Adoptar la negación y la implicación como las dos operaciones primitivas de un cálculo proposicional equivale a tener la partición de conjuntos omega de la siguiente manera:
  • Un sistema de axiomas propuesto por Jan Łukasiewicz , y utilizado como parte del cálculo proposicional de un sistema de Hilbert , formula un cálculo proposicional en este lenguaje de la siguiente manera. Todos los axiomas son instancias de sustitución de:
  • La regla de inferencia es modus ponens (es decir, a partir de p y , infer q ). Entonces se define como , y se define como . Este sistema se utiliza en la base de datos de pruebas formales set.mm de Metamath .

Ejemplo 2. Sistema de deducción natural

Deje , donde , , , se define como sigue:

  • El conjunto alfa es un conjunto infinito contable de símbolos, por ejemplo:
  • El omega establece las particiones de la siguiente manera:

En el siguiente ejemplo de cálculo proposicional, se pretende que las reglas de transformación se interpreten como las reglas de inferencia de un llamado sistema de deducción natural . El sistema particular que se presenta aquí no tiene puntos iniciales, lo que significa que su interpretación para aplicaciones lógicas deriva sus teoremas de un conjunto de axiomas vacío.

  • El conjunto de puntos iniciales está vacía, es decir, .
  • El conjunto de reglas de transformación , se describe a continuación:

Nuestro cálculo proposicional tiene once reglas de inferencia. Estas reglas nos permiten derivar otras fórmulas verdaderas dado un conjunto de fórmulas que se supone que son verdaderas. Los primeros diez simplemente establecen que podemos inferir ciertas fórmulas bien formadas a partir de otras fórmulas bien formadas. Sin embargo, la última regla usa un razonamiento hipotético en el sentido de que en la premisa de la regla asumimos temporalmente que una hipótesis (no probada) es parte del conjunto de fórmulas inferidas para ver si podemos inferir alguna otra fórmula determinada. Dado que las primeras diez reglas no hacen esto, generalmente se describen como reglas no hipotéticas y la última como una regla hipotética .

Al describir las reglas de transformación, podemos introducir un símbolo de metalenguaje . Básicamente es una abreviatura conveniente para decir "inferir eso". El formato es , en el que Γ es un conjunto (posiblemente vacío) de fórmulas llamadas premisas, y ψ es una fórmula llamada conclusión. La regla de transformación significa que si cada proposición en Γ es un teorema (o tiene el mismo valor de verdad que los axiomas), entonces ψ también es un teorema. Tenga en cuenta que considerando la siguiente regla Introducción a la conjunción , sabremos que cuando Γ tenga más de una fórmula, siempre podremos reducirla de manera segura a una fórmula usando la conjunción. Entonces, para abreviar, a partir de ese momento podemos representar Γ como una fórmula en lugar de un conjunto. Otra omisión por conveniencia es cuando Γ es un conjunto vacío, en cuyo caso Γ puede no aparecer.

Introducción a la negación
Desde e , inferir .
Es decir, .
Eliminación de la negación
De , inferir .
Es decir, .
Eliminación de la doble negación
De , inferir p .
Es decir, .
Introducción a la conjunción
De p y q , infiera .
Es decir, .
Eliminación de conjunciones
De , inferir p .
De , inferir q .
Eso es, y .
Introducción a la disyunción
De p , inferir .
De q , infiera .
Eso es, y .
Eliminación de disyunciones
De y y , infiera r .
Es decir, .
Introducción bicondicional
Desde e , inferir .
Es decir, .
Eliminación bicondicional
De , inferir .
De , inferir .
Eso es, y .
Modus ponens (eliminación condicional)
De p y , infiera q .
Es decir, .
Prueba condicional (introducción condicional)
De [aceptar p permite una prueba de q ], infiera .
Es decir, .

Formas argumentales básicas y derivadas

Nombre Consecuente Descripción
Modus ponens Si p entonces q ; p ; por lo tanto q
Modus Tollens Si p entonces q ; no q ; por lo tanto no p
Silogismo hipotético Si p entonces q ; si q entonces r ; por lo tanto, si p entonces r
Silogismo disyuntivo O bien p o q , o ambos; no p ; por lo tanto, q
Dilema constructivo Si p entonces q ; y si r entonces s ; pero p o r ; por lo tanto q o s
Dilema destructivo Si p entonces q ; y si r entonces s ; pero no q o no s ; por lo tanto no p o no r
Dilema bidireccional Si p entonces q ; y si r entonces s ; pero p o no s ; por lo tanto q o no r
Simplificación p y q son verdaderas; por lo tanto p es cierto
Conjunción p y q son verdaderas por separado; por lo tanto son verdad conjuntamente
Adición p es cierto; por lo tanto, la disyunción ( p o q ) es verdadera
Composición Si p entonces q ; y si p entonces r ; Por lo tanto, si p es cierto, entonces q y r son verdaderas
Teorema de De Morgan (1) La negación de ( p y q ) es equiv. to (no p o no q )
Teorema de De Morgan (2) La negación de ( p o q ) es equiv. to (no py no q )
Conmutación (1) ( P o q ) es equiv. a ( q o p )
Conmutación (2) ( P y q ) es equiv. a ( q y p )
Conmutación (3) ( p es equivalente a q ) es equiv. a ( q es equiv. a p )
Asociación (1) p o ( q o r ) es equiv. a ( p o q ) o r
Asociación (2) p y ( q y r ) es equiv. a ( p y q ) y r
Distribución (1) p y ( q o r ) es equiv. a ( p y q ) o ( p y r )
Distribución (2) p o ( q y r ) es equiv. a ( p o q ) y ( p o r )
Doble negación y p es equivalente a la negación de no p
Transposición Si p, entonces q es equiv. a si no q entonces no p
Implicación material Si p, entonces q es equiv. para no p o q
Equivalencia material (1) ( p sif q ) es equiv. a (si p es verdadero, entonces q es verdadero) y (si q es verdadero, entonces p es verdadero)
Equivalencia material (2) ( p sif q ) es equiv. para ( p y q son true) o (ambos p y q son falsas)
Equivalencia material (3) ( p sif q ) es equivalente a., ambos ( p o no q es verdadero) y (no p o q es verdadero)
Exportación a partir de (si p y q son verdad, entonces r es verdad) podemos probar (si q es cierto, entonces r es verdad, si p es verdadera)
Importación Si p entonces (si q entonces r ) es equivalente a si p y q entonces r
Tautología (1) p es verdadero es equiv. a p es verdadera o p es cierto
Tautología (2) p es verdadero es equiv. a p es verdadero y p es verdadera
Tertium non datur (Ley del medio excluido) p o no p es cierto
Ley de no contradicción p y no p es falso, es un enunciado verdadero

Pruebas en cálculo proposicional

Uno de los usos principales de un cálculo proposicional, cuando se interpreta para aplicaciones lógicas, es determinar relaciones de equivalencia lógica entre fórmulas proposicionales. Estas relaciones se determinan mediante las reglas de transformación disponibles, cuyas secuencias se denominan derivaciones o demostraciones .

En la discusión que sigue, una prueba se presenta como una secuencia de líneas numeradas, y cada línea consta de una única fórmula seguida de una razón o justificación para introducir esa fórmula. Cada premisa del argumento, es decir, un supuesto introducido como hipótesis del argumento, se enumera al principio de la secuencia y se marca como una "premisa" en lugar de otra justificación. La conclusión se enumera en la última línea. Una prueba está completa si cada línea se sigue de las anteriores mediante la aplicación correcta de una regla de transformación. (Para un enfoque contrastante, vea árboles de prueba ).

Ejemplo de prueba en sistema de deducción natural

  • Para ser demostrado que AA .
  • Una posible prueba de esto (que, aunque es válida, contiene más pasos de los necesarios) se puede organizar de la siguiente manera:
Ejemplo de prueba
Número Fórmula Razón
1 premisa
2 De ( 1 ) por introducción de disyunción
3 De ( 1 ) y ( 2 ) por conjunción introducción
4 De ( 3 ) por eliminación de conjunción
5 Resumen de ( 1 ) a ( 4 )
6 De ( 5 ) por prueba condicional

Interprete como "Suponiendo A , infiera A ". Lea como "No asumiendo nada, infiera que A implica A ", o "Es una tautología que A implica A ", o "Siempre es cierto que A implica A ".

Ejemplo de una demostración en un sistema de cálculo proposicional clásico

Ahora demostramos el mismo teorema en el sistema axiomático de Jan Łukasiewicz descrito anteriormente, que es un ejemplo de un sistema clásico de cálculo proposicional , o un sistema deductivo al estilo de Hilbert para el cálculo proposicional.

Los axiomas son:

(A1)
(A2)
(A3)

Y la prueba es la siguiente:

  1.       (instancia de (A1))
  2.       (instancia de (A2))
  3.       (de (1) y (2) por modus ponens )
  4.       (instancia de (A1))
  5.       (de (4) y (3) por modus ponens)

Solidez e integridad de las reglas.

Las propiedades cruciales de este conjunto de reglas son que son sólidas y completas . De manera informal, esto significa que las reglas son correctas y que no se requieren otras reglas. Estas afirmaciones pueden hacerse más formales de la siguiente manera. Tenga en cuenta que las pruebas de la solidez y la integridad de la lógica proposicional no son en sí mismas pruebas en la lógica proposicional; estos son teoremas en ZFC utilizados como metateoría para probar propiedades de la lógica proposicional.

Definimos una asignación de verdad como una función que asigna variables proposicionales a verdadero o falso . De manera informal, tal asignación de verdad puede entenderse como la descripción de un posible estado de cosas (o mundo posible ) donde ciertos enunciados son verdaderos y otros no. La semántica de las fórmulas puede luego formalizarse definiendo para qué "estado de cosas" se consideran verdaderas, que es lo que se hace mediante la siguiente definición.

Definimos cuando tal asignación de verdad A satisface cierta fórmula bien formada con las siguientes reglas:

  • A satisface la variable proposicional P si y solo si A ( P ) = verdadero
  • A satisface ¬ φ si y solo si A no satisface φ
  • A satisface ( φψ ) si y solo si A satisface tanto φ como ψ
  • A satisface ( φψ ) si y solo si A satisface al menos uno de φ o ψ
  • A satisface ( φψ ) si y solo si no es el caso que A satisface φ pero no ψ
  • A satisface ( φψ ) si y solo si A satisface tanto φ como ψ o no satisface ninguno de ellos

Con esta definición podemos ahora formalizar lo que significa que una fórmula φ esté implícita en un determinado conjunto S de fórmulas. Informalmente esto es cierto si en todos los mundos que son posibles dado el conjunto de fórmulas S también se cumple la fórmula φ . Esto conduce a la siguiente definición formal: Decimos que un conjunto S de fórmulas bien formadas implica semánticamente (o implica ) una cierta fórmula bien formada φ si todas las asignaciones de verdad que satisfacen todas las fórmulas en S también satisfacen φ .

Finalmente, definimos la implicación sintáctica de tal manera que φ está implicada sintácticamente por S si y solo si podemos derivarla con las reglas de inferencia que se presentaron anteriormente en un número finito de pasos. Esto nos permite formular exactamente lo que significa que el conjunto de reglas de inferencia sea sólido y completo:

Solidez: Si el conjunto de fórmulas bien formadas S implica sintácticamente la fórmula bien formada φ, entonces S implica semánticamente φ .

Completitud: Si el conjunto de fórmulas bien formadas S implica semánticamente la fórmula bien formada φ, entonces S implica sintácticamente φ .

Para el conjunto de reglas anterior, este es realmente el caso.

Bosquejo de una prueba de solidez

(Para la mayoría de los sistemas lógicos , esta es la dirección de prueba comparativamente "simple")

Convenciones de notación: Sea G una variable que abarca conjuntos de oraciones. Deje que A, B y C se extiendan sobre las oraciones. Para " G implica sintácticamente A " escribimos " G prueba A ". Para " G implica semánticamente A " escribimos " G implica A ".

Queremos mostrar: ( A ) ( G ) (si G prueba A , entonces G implica A ).

Observamos que " G prueba A " tiene una definición inductiva, y eso nos da los recursos inmediatos para demostrar afirmaciones de la forma "Si G prueba A , entonces ...". Entonces nuestra prueba procede por inducción.

  1. Base. Mostrar: Si A es miembro de G , entonces G implica una .
  2. Base. Mostrar: Si A es un axioma, entonces G implica una .
  3. Paso inductivo (inducción en n , la longitud de la prueba):
    1. Supongamos por arbitrario G y A que si G demuestra A en n o menos pasos, a continuación, G implica A .
    2. Para cada posible aplicación de una regla de inferencia en la etapa n + 1 , que conduce a un nuevo teorema B , muestran que G implica B .

Observe que el Paso básico II se puede omitir para los sistemas de deducción natural porque no tienen axiomas. Cuando se usa, el Paso II implica mostrar que cada uno de los axiomas es una verdad lógica (semántica) .

Los pasos básicos demuestran que las sentencias demostrables más simples de G también están implicados por G , para cualquier G . (La prueba es simple, ya que el hecho semántico de que un conjunto implica a cualquiera de sus miembros, también es trivial.) El paso inductivo cubrirá sistemáticamente todas las oraciones adicionales que puedan demostrarse, considerando cada caso en el que podríamos llegar a una conclusión lógica. usando una regla de inferencia, y muestra que si una nueva oración es demostrable, también está lógicamente implícita. (Por ejemplo, podríamos tener una regla que nos diga que de " A " podemos derivar " A o B ". En III.a asumimos que si A es demostrable, está implícito. También sabemos que si A es demostrable, entonces " A o B "es demostrable. Tenemos que demostrar que entonces" A o B "también está implícito. Lo hacemos apelando a la definición semántica y la suposición que acabamos de hacer. A es demostrable a partir de G , suponemos. Así que es también implícito por G. Entonces, cualquier valoración semántica que haga que todo G sea ​​verdadero hace que A sea verdadero. Pero cualquier valoración que haga que A sea ​​verdadero hace que " A o B " sea verdadero, según la semántica definida para "o". Entonces, cualquier valoración que haga que todo G sea verdadero hace que " A o B " sea verdadero. Por lo tanto, " A o B " está implícito.) Generalmente, el paso inductivo consistirá en un análisis largo pero simple, caso por caso, de todas las reglas de inferencia, mostrando que cada una "conserva" la semántica implicación.

Según la definición de demostrabilidad, no hay enunciados demostrables más que por ser miembro de G , un axioma o seguir una regla; de modo que si todos ellos están implícitos semánticamente, el cálculo de deducción es sólido.

Boceto de prueba de integridad

(Esta suele ser la dirección de prueba mucho más difícil).

Adoptamos las mismas convenciones de notación que las anteriores.

Queremos mostrar: Si G implica A , entonces G demuestra una . Procedemos por contraposición : Mostramos vez que si G no no probar un entonces G no no implica una . Si se demuestra que hay un modelo donde A no se sostiene a pesar G ser verdad, entonces, evidentemente, G no implica una . La idea es construir un modelo tal de nuestra misma suposición de que G no prueba una .

  1. G no prueba una . (Suposición)
  2. Si G no prueba A , entonces podemos construir una (infinito) Maximal Conjunto , G * , que es un superconjunto de G y que también no prueba una .
    1. Coloque un orden (con el tipo de orden ω) en todas las oraciones en el idioma (por ejemplo, la más corta primero, y las igualmente largas en orden alfabético extendido), y numerelas ( E 1 , E 2 , ...)
    2. Defina una serie G n de conjuntos ( G 0 , G 1 , ...) inductivamente:
      1. Si prueba A , entonces
      2. Si no , no probar una , a continuación,
    3. Defina G como la unión de todos los G n . (Es decir, G es el conjunto de todas las oraciones que están en cualquier G n .)
    4. Se puede demostrar fácilmente que
      1. G contiene (es un superconjunto de) G (por (bi));
      2. G no prueba A (porque la prueba contendría sólo un número finito de oraciones y cuando la última de ellas se introduce en algún G n , G n probaría A contraria a la definición de G n ); y
      3. G * es un conjunto máximo con respecto a A : Si hay más frases lo fueron añadidos a G * , se probarían A . (Porque si fuera posible agregar más oraciones, deberían haber sido agregadas cuando se encontraron durante la construcción del G n , nuevamente por definición)
  3. Si G es un conjunto máximo con respecto a A , entonces es similar a la verdad . Esto significa que contiene C si y solo si no contiene ¬C ; Si contiene C y contiene "Si C, entonces B ", entonces también contiene B ; Etcétera. Para mostrar esto, uno tiene que demostrar que el sistema axiomático es lo suficientemente fuerte para lo siguiente:
    • Para cualquier fórmulas C y D , si se demuestra que tanto C y ¬C , a continuación, se demuestra D . De esto se deduce, que un conjunto máximo con respecto a A no puede demostrar tanto C y ¬C , ya que de lo contrario resultaría A .
    • Para cualquier fórmulas C y D , si se demuestra que tanto CD y ¬CD , a continuación, se demuestra D . Esto se usa, junto con el teorema de la deducción , para mostrar que para cualquier fórmula, o esta o su negación está en G : Sea B una fórmula que no está en G ; entonces G * con la adición de B demuestra A . Así, desde el teorema de la deducción se deduce que G * prueba BA . Pero supongamos que ¬B tampoco están en G , entonces por la misma lógica G también prueba ¬BA ; pero luego G prueba A , que ya hemos demostrado que es falsa.
    • Para cualquier fórmulas C y D , si se demuestra que C y D , a continuación, se demuestra CD .
    • Para cualquier fórmula C y D , si prueba C y ¬D , entonces prueba ¬ ( CD ).
    • Para cualquier fórmulas C y D , si resulta ¬C , a continuación, se demuestra CD .
    Si la operación lógica adicional (como conjunción y / o disyunción) también son parte del vocabulario, entonces hay un requisito adicional en el sistema axiomático (por ejemplo, que si prueba C y D , también probaría su conjunción).
  4. Si G es como una verdad, hay una G -Canónica valoración del lenguaje: una que hace que cada oración en G ∗ sea verdadera y todo lo que esté fuera de G ∗ sea falso mientras se siguen las leyes de la composición semántica en el lenguaje. Tenga en cuenta que el requisito de que sea similar a la verdad es necesario para garantizar que las leyes de la composición semántica en el lenguaje se satisfagan con esta asignación de verdad.
  5. Una valoración canónica G hará que nuestro conjunto original G sea verdadero y que A sea falso.
  6. Si hay una valoración en el que G es verdadera y A es falso, entonces G no (semánticamente) implica A .

Por lo tanto, todo sistema que tenga modus ponens como regla de inferencia y demuestre los siguientes teoremas (incluidas sus sustituciones) está completo:

  • p → (¬p → q)
  • (p → q) → ((¬p → q) → q)
  • p → (q → (p → q))
  • p → (¬q → ¬ (p → q))
  • ¬p → (p → q)
  • p → p
  • p → (q → p)
  • (p → (q → r)) → ((p → q) → (p → r))

Los primeros cinco se utilizan para satisfacer las cinco condiciones en la etapa III anterior, y los últimos tres para demostrar el teorema de la deducción.

Ejemplo

A modo de ejemplo, se puede demostrar que, como cualquier otra tautología, los tres axiomas del sistema de cálculo proposicional clásico descrito anteriormente se pueden probar en cualquier sistema que satisfaga lo anterior, es decir, que tenga modus ponens como regla de inferencia, y demuestre lo anterior. ocho teoremas (incluidas sus sustituciones). De los ocho teoremas, los dos últimos son dos de los tres axiomas; el tercer axioma`` también se puede probar, como mostramos ahora.

Para la prueba, podemos usar el teorema del silogismo hipotético (en la forma relevante para este sistema axiomático), ya que solo se basa en los dos axiomas que ya están en el conjunto de ocho teoremas anterior. La prueba entonces es la siguiente:

  1.       (ejemplo del séptimo teorema)
  2.       (ejemplo del séptimo teorema)
  3.       (de (1) y (2) por modus ponens)
  4.       (ejemplo del teorema del silogismo hipotético)
  5.       (ejemplo del quinto teorema)
  6.       (de (5) y (4) por modus ponens)
  7.       (instancia del segundo teorema)
  8.       (ejemplo del séptimo teorema)
  9.       (de (7) y (8) por modus ponens)
  10.       (ejemplo del octavo teorema)
  11.       (de (9) y (10) por modus ponens)
  12.       (de (3) y (11) por modus ponens)
  13.       (ejemplo del octavo teorema)
  14.       (de (12) y (13) por modus ponens)
  15.       (de (6) y (14) por modus ponens)

Verificación de la completitud del sistema de cálculo proposicional clásico

Ahora verificamos que el sistema de cálculo proposicional clásico descrito anteriormente puede probar los ocho teoremas requeridos mencionados anteriormente. Usamos varios lemas probados aquí :

(DN1) - Doble negación (una dirección)
(DN2) - Doble negación (otra dirección)
(HS1) - una forma de silogismo hipotético
(HS2) - otra forma de silogismo hipotético
(TR1) - Transposición
(TR2) - otra forma de transposición.
(L1)
(L3)

También usamos el método del metateorema del silogismo hipotético como una forma abreviada de varios pasos de prueba.

  • p → (¬p → q) - prueba:
    1.       (instancia de (A1))
    2.       (instancia de (TR1))
    3.       (de (1) y (2) usando el metateorema del silogismo hipotético)
    4.       (instancia de (DN1))
    5.       (instancia de (HS1))
    6.       (de (4) y (5) usando modus ponens)
    7.       (de (3) y (6) usando el metateorema del silogismo hipotético)
  • (p → q) → ((¬p → q) → q) - prueba:
    1.       (instancia de (HS1))
    2.       (instancia de (L3))
    3.       (instancia de (HS1))
    4.       (de (2) y (3) por modus ponens)
    5.       (de (1) y (4) usando el metateorema del silogismo hipotético)
    6.       (instancia de (TR2))
    7.       (instancia de (HS2))
    8.       (de (6) y (7) usando modus ponens)
    9.       (de (5) y (8) usando el metateorema del silogismo hipotético)
  • p → (q → (p → q)) - prueba:
    1.       (instancia de (A1))
    2.       (instancia de (A1))
    3.       (de (1) y (2) usando modus ponens)
  • p → (¬q → ¬ (p → q)) - prueba:
    1.       (instancia de (L1))
    2.       (instancia de (TR1))
    3.       (de (1) y (2) usando el metateorema del silogismo hipotético)
  • ¬p → (p → q) - prueba:
    1.       (instancia de (A1))
    2.       (instancia de (A3))
    3.       (de (1) y (2) usando el metateorema del silogismo hipotético)
  • p → p - prueba dada en el ejemplo de prueba anterior
  • p → (q → p) - axioma (A1)
  • (p → (q → r)) → ((p → q) → (p → r)) - axioma (A2)

Otro esquema para una prueba de integridad

Si una fórmula es una tautología , entonces hay una tabla de verdad para ella que muestra que cada valoración arroja el valor verdadero de la fórmula. Considere tal valoración. Por inducción matemática sobre la longitud de las subfórmulas, demuestre que la verdad o falsedad de la subfórmula se sigue de la verdad o falsedad (según corresponda para la valoración) de cada variable proposicional en la subfórmula. Luego combine las líneas de la tabla de verdad de dos en dos usando "( P es verdadero implica S ) implica (( P es falso implica S ) implica S )". Siga repitiendo esto hasta que se hayan eliminado todas las dependencias de las variables proposicionales. El resultado es que hemos probado la tautología dada. Dado que toda tautología es demostrable, la lógica es completa.

Interpretación de un cálculo proposicional funcional de verdad

Una interpretación de un cálculo de proposiciones verdad-funcional es una asignación a cada símbolo proposicional de de uno o el otro (pero no ambos) de la valores de verdad verdad ( T ) y falsedad ( F ), y una asignación a los símbolos conectivos de de sus significados habituales de verdad-funcional. Una interpretación de un cálculo proposicional funcional de verdad también puede expresarse en términos de tablas de verdad .

Para símbolos proposicionales distintos, hay distintas interpretaciones posibles. Para cualquier símbolo en particular , por ejemplo, existen posibles interpretaciones:

  1. se le asigna T , o
  2. se asigna F .

Para la pareja , hay posibles interpretaciones:

  1. a ambos se les asigna T ,
  2. a ambos se les asigna F ,
  3. se le asigna T y se le asigna F , o
  4. se asigna F y se le asigna T .

Dado que tiene , es decir, innumerablemente muchos símbolos proposicionales, hay , y por lo tanto, incontables posibles interpretaciones distintas de .

Interpretación de una oración de lógica proposicional funcional de verdad

Si φ y ψ son fórmulas de y es una interpretación de, se aplican las siguientes definiciones:

  • Una oración de lógica proposicional es verdadera bajo una interpretación si asigna el valor de verdad T a esa oración. Si una oración es verdadera bajo una interpretación, entonces esa interpretación se llama modelo de esa oración.
  • φ es falso bajo una interpretación si φ no es verdadero bajo .
  • Una oración de lógica proposicional es lógicamente válida si es verdadera bajo todas las interpretaciones.
    φ significa que φ es lógicamente válido.
  • Una oración ψ de lógica proposicional es una consecuencia semántica de una oración φ si no hay una interpretación bajo la cual φ es verdadera y ψ es falsa.
  • Una oración de lógica proposicional es consistente si es verdadera bajo al menos una interpretación. Es inconsistente si no es consistente.

Algunas consecuencias de estas definiciones:

  • Para cualquier interpretación dada, una fórmula dada es verdadera o falsa.
  • Ninguna fórmula es a la vez verdadera y falsa bajo la misma interpretación.
  • φ es falso para una interpretación dada sif es verdadero para esa interpretación; y φ es verdadero bajo una interpretación sif es falso bajo esa interpretación.
  • Si φ y son ambos verdaderos bajo una interpretación dada, entonces ψ es verdadero bajo esa interpretación.
  • Si y , entonces .
  • es cierto en iff φ no es cierto en .
  • es verdadero bajo si si φ no es verdadero bajo o ψ es verdadero bajo .
  • Una oración ψ de lógica proposicional es una consecuencia semántica de una oración φ sif es lógicamente válido , es decir, sif .

Cálculo alternativo

Es posible definir otra versión del cálculo proposicional, que define la mayor parte de la sintaxis de los operadores lógicos mediante axiomas, y que utiliza una sola regla de inferencia.

Axiomas

Sean φ , χ y ψ las fórmulas bien formadas. (Las fórmulas bien formadas en sí mismas no contendrían ninguna letra griega, sino solo letras mayúsculas romanas, operadores conectivos y paréntesis). Entonces los axiomas son los siguientes:

Axiomas
Nombre Esquema de axioma Descripción
ENTONCES-1 Agregar hipótesis χ , introducción de implicaciones
ENTONCES-2 Distribuir hipótesis sobre implicaciones
Y 1 Eliminar conjunción
Y 2  
Y-3 Introducir conjunción
OR-1 Introducir disyunción
O-2  
O-3 Eliminar la disyunción
NO-1 Introducir negación
NO-2 Eliminar la negación
NO-3 Excluida la lógica clásica media
IFF-1 Eliminar la equivalencia
IFF-2  
IFF-3 Introducir equivalencia
  • El axioma THEN-2 puede considerarse una "propiedad distributiva de la implicación con respecto a la implicación".
  • Los axiomas AND-1 y AND-2 corresponden a "eliminación de conjunción". La relación entre AND-1 y AND-2 refleja la conmutatividad del operador de conjunción.
  • Axioma AND-3 corresponde a "introducción de conjunción".
  • Los axiomas OR-1 y OR-2 corresponden a "introducción de disyunción". La relación entre OR-1 y OR-2 refleja la conmutatividad del operador de disyunción.
  • El axioma NOT-1 corresponde a "reductio ad absurdum".
  • Axiom NOT-2 dice que "cualquier cosa puede deducirse de una contradicción".
  • El axioma NOT-3 se llama " tertium non-datur " ( latín : "no se da un tercero") y refleja la valoración semántica de fórmulas proposicionales: una fórmula puede tener un valor de verdad verdadero o falso. No existe un tercer valor de verdad, al menos no en la lógica clásica. Los lógicos intuicionistas no aceptan el axioma NO-3 .

Regla de inferencia

La regla de inferencia es modus ponens :

.

Regla de metainferencia

Sea una demostración representada por una secuencia, con hipótesis a la izquierda del torniquete y la conclusión a la derecha del torniquete. Entonces, el teorema de la deducción se puede establecer de la siguiente manera:

Si la secuencia
se ha demostrado, entonces también es posible demostrar la secuencia
.

Este teorema de deducción (DT) no se formula en sí mismo con cálculo proposicional: no es un teorema de cálculo proposicional, sino un teorema sobre cálculo proposicional. En este sentido, es un metateorema , comparable a los teoremas sobre la solidez o integridad del cálculo proposicional.

Por otro lado, DT es tan útil para simplificar el proceso de prueba sintáctica que puede considerarse y usarse como otra regla de inferencia, que acompaña al modus ponens. En este sentido, DT corresponde a la regla de inferencia de prueba condicional natural que forma parte de la primera versión del cálculo proposicional presentada en este artículo.

Lo contrario de DT también es válido:

Si la secuencia
se ha demostrado, entonces también es posible demostrar la secuencia

de hecho, la validez de la recíproca de DT es casi trivial en comparación con la de DT:

Si
luego
1:
2:
y de (1) y (2) se puede deducir
3:
mediante modus ponens, QED

Lo contrario de DT tiene implicaciones poderosas: puede usarse para convertir un axioma en una regla de inferencia. Por ejemplo, el axioma AND-1,

se puede transformar mediante el inverso del teorema de la deducción en la regla de inferencia

que es la eliminación de conjunción , una de las diez reglas de inferencia utilizadas en la primera versión (en este artículo) del cálculo proposicional.

Ejemplo de prueba

El siguiente es un ejemplo de una demostración (sintáctica), que involucra solo axiomas THEN-1 y THEN-2 :

Demuestre: (Reflexividad de la implicación).

Prueba:

  1. Axiom THEN-2 con
  2. Axiom THEN-1 con
  3. De (1) y (2) por modus ponens.
  4. Axiom THEN-1 con
  5. De (3) y (4) por modus ponens.

Equivalencia a lógicas ecuacionales

El cálculo alternativo anterior es un ejemplo de un sistema de deducción al estilo de Hilbert . En el caso de los sistemas proposicionales, los axiomas son términos construidos con conectivos lógicos y la única regla de inferencia es el modus ponens. La lógica ecuacional, tal como se usa informalmente de manera estándar en el álgebra de la escuela secundaria, es un tipo de cálculo diferente de los sistemas de Hilbert. Sus teoremas son ecuaciones y sus reglas de inferencia expresan las propiedades de la igualdad, es decir, que es una congruencia de términos que admite sustitución.

El cálculo proposicional clásico como se describió anteriormente es equivalente al álgebra de Boole , mientras que el cálculo proposicional intuicionista es equivalente al álgebra de Heyting . La equivalencia se muestra traduciendo en cada dirección los teoremas de los respectivos sistemas. Los teoremas del cálculo proposicional clásico o intuicionista se traducen como ecuaciones de álgebra de Boole o de Heyting, respectivamente. A la inversa, los teoremas del álgebra de Boole o de Heyting se traducen como teoremas de cálculo clásico o intuicionista respectivamente, que es una abreviatura estándar. En el caso del álgebra de Boole también se puede traducir como , pero esta traducción es incorrecta intuicionistamente.

Tanto en el álgebra de Boole como en el de Heyting, la desigualdad se puede utilizar en lugar de la igualdad. La igualdad se puede expresar como un par de desigualdades y . A la inversa, la desigualdad se puede expresar como igualdad o como . La importancia de la desigualdad para los sistemas de estilo Hilbert es que corresponde al símbolo de deducción o vinculación de este último . Una vinculación

se traduce en la versión de desigualdad del marco algebraico como

Por el contrario, la desigualdad algebraica se traduce como la vinculación

.

La diferencia entre implicación y la desigualdad o vinculación o es que el primero es interna a la lógica mientras que el último es externo. La implicación interna entre dos términos es otro término del mismo tipo. La vinculación como implicación externa entre dos términos expresa una metaverdad fuera del lenguaje de la lógica, y se considera parte del metalenguaje . Incluso cuando la lógica en estudio es intuicionista, la implicación normalmente se entiende clásicamente como de dos valores: o el lado izquierdo implica, o es menor o igual al lado derecho, o no lo es.

Traducciones similares pero más complejas ay desde lógicas algebraicas son posibles para los sistemas de deducción natural como se describió anteriormente y para el cálculo secuencial . Las implicaciones de este último pueden interpretarse como de dos valores, pero una interpretación más perspicaz es como un conjunto, cuyos elementos pueden entenderse como pruebas abstractas organizadas como los morfismos de una categoría . En esta interpretación, la regla de corte del cálculo secuencial corresponde a la composición en la categoría. Las álgebras de Boole y de Heyting entran en esta imagen como categorías especiales que tienen como máximo un morfismo por homset, es decir, una prueba por implicación, correspondiente a la idea de que la existencia de pruebas es todo lo que importa: cualquier prueba sirve y no tiene sentido distinguirlas. .

Cálculos gráficos

Es posible generalizar la definición de un lenguaje formal a partir de un conjunto de secuencias finitas sobre una base finita para incluir muchos otros conjuntos de estructuras matemáticas, siempre que se construyan por medios finitos a partir de materiales finitos. Además, muchas de estas familias de estructuras formales son especialmente adecuadas para su uso en lógica.

Por ejemplo, hay muchas familias de gráficos que son análogos lo suficientemente cercanos de los lenguajes formales como para que el concepto de cálculo se extienda a ellos con bastante facilidad y naturalidad. Muchas especies de gráficos surgen como gráficos de análisis sintáctico en el análisis sintáctico de las familias correspondientes de estructuras de texto. Las exigencias de la computación práctica en lenguajes formales frecuentemente exigen que las cadenas de texto se conviertan en interpretaciones de estructura de puntero de gráficos de análisis sintáctico, simplemente como una cuestión de verificar si las cadenas son fórmulas bien formadas o no. Una vez hecho esto, se pueden obtener muchas ventajas al desarrollar el análogo gráfico del cálculo en cuerdas. El mapeo de cadenas a analizar gráficos se llama análisis sintáctico y el mapeo inverso de análisis de gráficos a cadenas se logra mediante una operación que se llama atravesar el gráfico.

Otros cálculos lógicos

El cálculo proposicional se trata del tipo más simple de cálculo lógico en uso actual. Puede ampliarse de varias formas. (El cálculo "silogístico" aristotélico , que ha sido reemplazado en gran medida en la lógica moderna, es en algunos aspectos más simple, pero en otros aspectos más complejo, que el cálculo proposicional). La forma más inmediata de desarrollar un cálculo lógico más complejo es introducir reglas que sean sensible a los detalles más precisos de las oraciones que se utilizan.

La lógica de primer orden (también conocida como lógica de predicados de primer orden) resulta cuando las "oraciones atómicas" de la lógica proposicional se dividen en términos , variables , predicados y cuantificadores , todos manteniendo las reglas de la lógica proposicional con algunas nuevas introducidas. (Por ejemplo, de "Todos los perros son mamíferos" podemos inferir "Si Rover es un perro, entonces Rover es un mamífero"). Con las herramientas de la lógica de primer orden es posible formular una serie de teorías, ya sea con axiomas explícitos o por reglas de inferencia, que en sí mismas pueden tratarse como cálculos lógicos. La aritmética es la más conocida de ellas; otros incluyen la teoría de conjuntos y la mereología . La lógica de segundo orden y otras lógicas de orden superior son extensiones formales de la lógica de primer orden. Por lo tanto, tiene sentido referirse a la lógica proposicional como "lógica de orden cero" , al compararla con estas lógicas.

La lógica modal también ofrece una variedad de inferencias que no se pueden capturar en el cálculo proposicional. Por ejemplo, de "Necesariamente p " podemos inferir que p . De p podemos inferir "Es posible que p ". La traducción entre lógicas modales y lógicas algebraicas concierne a lógicas clásica e intuicionista pero con la introducción de un operador unario en álgebras booleanas o de Heyting, diferente de las operaciones booleanas, interpretando la modalidad de posibilidad, y en el caso del álgebra de Heyting un segundo operador interpretando la necesidad. (para el álgebra de Boole esto es redundante ya que la necesidad es el dual de posibilidad de De Morgan). El primer operador conserva 0 y disyunción mientras que el segundo conserva 1 y conjunción.

Las lógicas de muchos valores son aquellas que permiten que las oraciones tengan valores distintos de verdadero y falso . (Por ejemplo, ninguno y ambos son "valores extra" estándar; la "lógica continua" permite que cada oración tenga cualquiera de un número infinito de "grados de verdad" entre verdadero y falso .) Estas lógicas a menudo requieren dispositivos de cálculo bastante distintos de los proposicionales. cálculo. Cuando los valores forman un álgebra booleana (que puede tener más de dos o incluso infinitos valores), la lógica de muchos valores se reduce a la lógica clásica; Las lógicas de muchos valores son, por tanto, de interés independiente sólo cuando los valores forman un álgebra que no es booleana.

Solucionadores

Encontrar soluciones a las fórmulas lógicas proposicionales es un problema NP-completo . Sin embargo, existen métodos prácticos (por ejemplo, algoritmo DPLL , 1962; algoritmo Chaff , 2001) que son muy rápidos para muchos casos útiles. El trabajo reciente ha extendido los algoritmos de resolución de SAT para trabajar con proposiciones que contienen expresiones aritméticas ; estos son los solucionadores de SMT .

Ver también

Niveles lógicos superiores

Temas relacionados

Referencias

Otras lecturas

  • Brown, Frank Markham (2003), Razonamiento booleano: La lógica de las ecuaciones booleanas , 1ª edición, Kluwer Academic Publishers, Norwell, MA. 2ª edición, Dover Publications, Mineola, NY.
  • Chang, CC y Keisler, HJ (1973), Model Theory , North-Holland, Amsterdam, Países Bajos.
  • Kohavi, Zvi (1978), Switching and Finite Automata Theory , 1ª edición, McGraw – Hill, 1970. 2ª edición, McGraw – Hill, 1978.
  • Korfhage, Robert R. (1974), Estructuras computacionales discretas , Academic Press, Nueva York, NY.
  • Lambek, J. y Scott, PJ (1986), Introducción a la lógica categórica de orden superior , Cambridge University Press, Cambridge, Reino Unido.
  • Mendelson, Elliot (1964), Introducción a la lógica matemática , D. Van Nostrand Company.

Obras relacionadas

enlaces externos