stringtranslate.com

Cálculo proposicional

El cálculo proposicional es una rama de la lógica . También se le llama lógica proposicional , lógica de enunciados , cálculo oracional , lógica oracional o, a veces, lógica de orden cero . Se ocupa de proposiciones (que pueden ser verdaderas o falsas) y de 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 llaman 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 ni cuantificadores . Sin embargo, toda la maquinaria de la lógica proposicional está incluida en la lógica de primer orden y en la lógica de orden superior. En este sentido, la lógica proposicional es la base de la lógica de primer orden y de la lógica de orden superior.

Explicación

Los conectivos lógicos se encuentran en los lenguajes naturales. En inglés, algunos ejemplos son "and" ( conjunción ), "o" ( disyunción ), "not" ( negación ) y "if" (pero sólo cuando se usan 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 entonces está nublado.
Premisa 2: Está lloviendo.
Conclusión: está nublado.

Tanto las premisas como la conclusión son proposiciones. Las premisas se dan por sentadas 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 descomponerse mediante conectivos lógicos, esta inferencia se puede reformular 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 se puede afirmar 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 corresponden exactamente con la expresión original en lenguaje natural. No sólo 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 se puede estudiar a través de un sistema formal en el que se pueden interpretar fórmulas de un lenguaje formal 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 utiliza un sistema formal para representar la lógica formal, solo las letras de declaración (generalmente letras romanas mayúsculas 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 está igualmente fuera del sistema formal mismo.

En la lógica proposicional clásica funcional de verdad , se interpreta que las fórmulas tienen precisamente uno de dos valores de verdad posibles , el valor de verdad de verdadero o el valor de verdad de falso . [1] Se mantienen el principio de bivalencia y la ley del tercero excluido . La lógica proposicional funcional de 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ó hasta convertirse en una lógica formal ( lógica estoica ) en el siglo III a. C. [2] y la amplió sus sucesores , los estoicos . La lógica se centró en proposiciones . Este avance fue diferente de la lógica silogística tradicional , que se centraba en los términos . Sin embargo, la mayoría de los escritos originales se perdieron [3] y la lógica proposicional desarrollada por los estoicos ya no se entendió más tarde en la antigüedad. [ cita necesaria ] En consecuencia, el sistema fue esencialmente reinventado por Peter Abelard en el siglo XII. [4]

La lógica proposicional finalmente se perfeccionó utilizando la lógica simbólica . Al matemático de los siglos XVII y XVIII, Gottfried Leibniz, se le atribuye el mérito de ser el fundador de la lógica simbólica por su trabajo con el racionador de cálculo . Aunque su trabajo fue el primero de su tipo, era 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. [5]

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 "los rasgos distintivos de la lógica silogística y la lógica proposicional". [6] En consecuencia, la lógica de predicados marcó el comienzo de una nueva era en la historia de la lógica; sin embargo, todavía se hicieron avances en la lógica proposicional 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 Stanisław Jaśkowski . Los árboles de la verdad fueron inventados por Evert Willem Beth . [7] La ​​invención de las tablas de verdad, sin embargo, es de atribución incierta.

Dentro de las obras de Frege [8] y Bertrand Russell , [9] se encuentran ideas influyentes para la invención de tablas de verdad. La estructura tabular real (formateada como una tabla), en sí misma, generalmente se atribuye a Ludwig Wittgenstein o Emil Post (o a ambos, de forma independiente). [8] 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 , [10] y Ernst Schröder . Otros a los que se les atribuye la estructura tabular incluyen a Jan Łukasiewicz , Alfred North Whitehead , William Stanley Jevons , John Venn y Clarence Irving Lewis . [9] En última instancia, algunos han llegado a la conclusión, como John Shosky, de que "no está nada claro que a una sola persona se le deba dar el título de 'inventor' de las tablas de verdad". [9]

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 interpretarse como equivalencia lógica , en el espacio de expresiones.

Cuando se pretende que el sistema formal sea un sistema lógico , las expresiones deben interpretarse como enunciados, y las reglas, conocidas como reglas de inferencia , normalmente tienen la intención de preservar la verdad. En este contexto, las reglas, que pueden incluir axiomas , se pueden utilizar para derivar ("inferir") fórmulas que representen afirmaciones verdaderas, a partir de fórmulas dadas que representen afirmaciones verdaderas.

El conjunto de axiomas puede ser vacío, un conjunto finito no vacío o un conjunto infinito contable (ver esquema de axiomas ). Una gramática formal define recursivamente 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 consta de:

  1. un conjunto de símbolos primitivos, denominados 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 pueda construirse 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 alguna proposición particular, mientras que las variables proposicionales abarcan el conjunto de todas las proposiciones atómicas. Los esquemas, sin embargo, abarcan todas las proposiciones. Es común representar constantes proposicionales mediante A , B y C , variables proposicionales mediante P , Q y R , y las letras esquemáticas suelen ser letras griegas, con mayor frecuencia φ , ψ y χ .

Conceptos básicos

A continuación se describe un cálculo proposicional estándar. Existen muchas formulaciones diferentes que son 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 mediante 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 afuera está lloviendo. Esto será verdadero ( P ) si está lloviendo afuera y falso en caso contrario ( ¬P ) .

La conjunción de P y Q es verdadera en el caso 1 y falsa en el caso contrario. Donde P es la proposición de que afuera está lloviendo y Q es la proposición de que hay un frente frío sobre Kansas, PQ es cierta cuando afuera está lloviendo y hay un frente frío sobre Kansas. Si afuera no llueve, entonces P ∧ Q es falso; y si no hay un frente frío sobre Kansas, entonces PQ también es falso.

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

Cierre bajo operaciones

La lógica proposicional está cerrada bajo conectivos funcionales de verdad. Es decir, para cualquier proposición φ , ¬ φ también es una proposición. Asimismo, 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 y, por tanto, puede combinarse con otra proposición. Para representar esto, necesitamos usar paréntesis para indicar qué proposición está unida a cuál. Por ejemplo, PQR no es una fórmula bien formada, porque no sabemos si estamos uniendo PQ con R o si estamos uniendo P con QR. Por lo tanto, debemos escribir ( PQ ) ∧ R para representar el primero, o P ∧ ( QR ) para representar el segundo. 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 cumplen 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 los paréntesis. Se puede verificar esto mediante el método de la tabla de verdad mencionado 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 2k filas, y debajo de P se completa 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 decimosextos, y así sucesivamente, hasta que la última constante proposicional varía 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

Luego, el cálculo proposicional define un argumento como una lista de proposiciones. Un argumento válido es una lista de proposiciones, la última de las cuales se deriva del resto (o está implícita en él). Todos los demás argumentos son inválidos. El argumento válido más simple es el modus ponens , un ejemplo del cual es la siguiente lista de proposiciones:

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

Esto se generaliza esquemáticamente. Por lo 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 uno de esos conjuntos), el modus ponens es suficiente para probar todas las demás formas de argumentos en lógica proposicional, por lo que pueden considerarse un derivado. Tenga en cuenta que esto no se aplica a 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 integridad .

La importancia 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 afirma. 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 A. Siempre se supone la reiteración , por lo que . Además, del primer elemento de A , del último elemento, así como del modus ponens, R es una consecuencia, y así . Sin embargo, como no hemos incluido axiomas suficientemente completos, no se puede deducir nada más. Así, 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: [ cita necesaria ]

El lenguaje de , también conocido como su conjunto de fórmulas , fórmulas bien formadas , se define inductivamente mediante 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:

Ejemplo 1. Sistema de axioma simple

Sea , donde , , , se definen de la siguiente manera:

Entonces se define como y se define como .

Este sistema se utiliza en la base de datos de prueba formal Metamath set.mm.

Ejemplo 2. Sistema de deducción natural

Sea , donde , , , se definen de la siguiente manera:

En el siguiente ejemplo de cálculo proposicional, las reglas de transformación deben interpretarse como las reglas de inferencia de un llamado sistema de deducción natural . El sistema particular presentado 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.

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 diez primeros simplemente afirman que podemos inferir ciertas fórmulas bien formadas a partir de otras fórmulas bien formadas. Sin embargo, la última regla utiliza 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 otra fórmula determinada. Dado que las diez primeras reglas no hacen esto, generalmente se describen como reglas no hipotéticas y la última como 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. Teniendo en cuenta la siguiente regla Introducción a la conjunción , sabremos que siempre que Γ tenga más de una fórmula, siempre podremos reducirla de forma segura a una fórmula usando la conjunción. En resumen, 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
De y , inferir .
Eso es, .
Eliminación de negación
De , inferir .
Eso es, .
Eliminación de doble negación
De , inferir p .
Eso es, .
Introducción a la conjunción
De p y q , inferir .
Eso es, .
Eliminación de conjunciones
De , inferir p .
De , infiere q .
Es decir, y .
Introducción a la disyunción
De p , infiere .
De q , infiere .
Es decir, y .
Eliminación de disyunción
De y y , inferir r .
Eso es, .
Introducción bicondicional
De y , inferir .
Eso es, .
Eliminación bicondicional
De , inferir .
De , inferir .
Es decir, y .
Modus ponens (eliminación condicional)
De p y , infiera q .
Eso es, .
Prueba condicional (introducción condicional)
De [aceptar p permite una prueba de q ], inferir .
Eso es, .

Formas de argumentos básicos y derivados.

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

En la discusión que sigue, una prueba se presenta como una secuencia de líneas numeradas, donde 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 comienzo de la secuencia y se marca como una "premisa" en lugar de otra justificación. La conclusión aparece en la última línea. Una demostración 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, consulte árboles de prueba ).

Ejemplo de prueba en sistema de deducción natural.

Interpretar como "Suponiendo A , infiera A ". Leído como "Sin asumir nada, infiere que A implica A ", o "Es una tautología que A implica A ", o "Siempre es cierto que A implica A ".

Ejemplo de 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 deductivo al estilo de Hilbert para el cálculo proposicional clásico.

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 y exhaustividad de las normas.

Las propiedades cruciales de este conjunto de reglas son que son sólidas y completas . Informalmente, 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. Las pruebas de la solidez y completitud de la lógica proposicional no son en sí mismas pruebas de la lógica proposicional; estos son teoremas en ZFC utilizados como metateoría para demostrar propiedades de la lógica proposicional.

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

Definimos cuándo dicha asignación de verdad A satisface una determinada fórmula bien formada con las siguientes reglas:

Con esta definición ahora podemos formalizar lo que significa que una fórmula φ esté implícita en un cierto conjunto S de fórmulas. Informalmente, esto es cierto si en todos los mundos posibles dado el conjunto de fórmulas S la fórmula φ también se cumple. Esto lleva a la siguiente definición formal: Decimos que un conjunto S de fórmulas bien formadas implica (o implica ) semánticamente 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 manera que φ está sintácticamente implicada por S si y sólo 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 efectivamente 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. Sean A, B y C en oraciones. Para " G sintácticamente implica 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 demostración procede por inducción.

  1. Base. Demuestre: Si A es miembro de G , entonces G implica A.
  2. Base. Demuestre: Si A es un axioma, entonces G implica A.
  3. Paso inductivo (inducción en n , la duración de la prueba):
    1. Supongamos para G y A arbitrarios que si G prueba A en n o menos pasos, entonces G implica A.
    2. Para cada posible aplicación de una regla de inferencia en el paso n + 1 , que conduzca a un nuevo teorema B , demuestre que G implica B.

Observe que el Paso Básico II puede omitirse para los sistemas de deducción natural porque no tienen axiomas. Cuando se utiliza, 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 oraciones demostrables más simples de G también están implícitas en G , para cualquier G . (La prueba es simple, ya que el hecho semántico de que un conjunto implica cualquiera de sus miembros también es trivial). El paso inductivo cubrirá sistemáticamente todas las oraciones adicionales que podrían ser demostrables, 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 al supuesto que acabamos de hacer. Suponemos que A es demostrable a partir de G. Así que es también implicada por G. Así que cualquier valoración semántica que haga verdadero a todo G hace verdadero a A. Pero cualquier valoración que haga verdadero a A hace que " A o B " sea verdadero, según la semántica definida para "o". Por lo tanto, cualquier valoración que haga verdadero a todo G 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 lógica semántica. implicación.

Según la definición de demostrabilidad, no hay oraciones demostrables más que por ser miembro de G , un axioma o seguir una regla; entonces, si todo esto está implícito semánticamente, el cálculo de deducción es correcto.

Bosquejo 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 antes.

Queremos mostrar: Si G implica A , entonces G prueba A. Procedemos por contraposición : mostramos en cambio que si G no prueba A entonces G no implica A. Si demostramos que existe un modelo en el que A no se cumple a pesar de que G sea cierto, entonces obviamente G no implica A. La idea es construir tal modelo a partir de nuestra suposición de que G no prueba A.

  1. G no prueba A . (Suposición)
  2. Si G no prueba A , entonces podemos construir un conjunto máximo (infinito) , G , que es un superconjunto de G y que tampoco prueba A.
    1. Coloque un orden (con tipo de orden ω) en todas las oraciones del idioma (por ejemplo, las más cortas primero y las igualmente largas en orden alfabético extendido) y numérelas ( E 1 , E 2 , ...)
    2. Defina una serie G n de conjuntos ( G 0 , G 1 , ...) de forma inductiva:
      1. Si se prueba A , entonces
      2. Si no prueba A , entonces
    3. Definir 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 , ese G n probaría A contrario a la definición de G n ); y
      3. G es un conjunto máximo con respecto a A : sise añadieran más oraciones a G , se probaría A. (Porque si fuera posible agregar más oraciones, deberían haberse agregado 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 veraz . Esto significa que contiene C si y sólo si no contiene ¬C ; Si contiene C y contiene "Si C, entonces B ", también contiene B ; Etcétera. Para demostrar esto, hay que demostrar que el sistema axiomático es lo suficientemente fuerte para lo siguiente:
    • Para cualquier fórmula C y D , si prueba tanto C como ¬C , entonces prueba D. De esto se deduce que un conjunto máximo con respecto a A no puede probar tanto C como ¬C , ya que de lo contrario probaría A.
    • Para cualquier fórmula C y D , si prueba CD y ¬CD , entonces prueba D. Esto se usa, junto con el teorema de deducción , para demostrar que para cualquier fórmula, ella o su negación están en G : Sea B una fórmula que no está en G ; entonces G con la adición de B prueba A . Así, del teorema de deducción se deduce que G prueba BA . Pero supongamos que ¬B tampoco estuviera en G , entonces por la misma lógica G también prueba ¬BA ; pero entonces G prueba A , que ya hemos demostrado que es falso.
    • Para cualquier fórmula C y D , si prueba C y D , entonces prueba CD.
    • Para cualquier fórmula C y D , si prueba C y ¬D , entonces prueba ¬( CD ).
    • Para cualquier fórmula C y D , si prueba ¬C , entonces prueba CD.
    Si operaciones lógicas adicionales (como conjunción y/o disyunción) también son parte del vocabulario, entonces hay requisitos adicionales en el sistema axiomático (por ejemplo, que si prueba C y D , también probaría su conjunción).
  4. Si G es veraz, hay una valoración G -Canónica del lenguaje: una que hace que cada oración en G sea verdadera y todo lo que esté fuera de G sea falso sin dejar de obedecer las leyes de composición semántica del lenguaje. El requisito de que sea veraz es necesario para garantizar que esta asignación de verdad satisfaga las leyes de composición semántica del lenguaje.
  5. Una valoración canónica G hará que nuestro conjunto original G sea todo verdadero y A sea falso.
  6. Si hay una valoración en la que G es verdadera y A es falsa, entonces G no implica (semánticamente) A.

Por lo tanto, todo sistema que tiene modus ponens como regla de inferencia y demuestra los siguientes teoremas (incluidas sus sustituciones) es completo:

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

Ejemplo

Como 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 el 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 puede demostrarse, 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.       (ejemplo 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 integridad 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 utilizamos el método del metateorema del silogismo hipotético como abreviatura de varios pasos de demostración.

Otro esquema para una prueba de integridad.

Si una fórmula es una tautología , entonces existe una tabla de verdad que muestra que cada valoración produce 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 deriva de la verdad o falsedad (según sea apropiado 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 demostrado la tautología dada. Como 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 proposicional funcional de verdad es una asignación a cada símbolo proposicional de uno u otro (pero no ambos) de los valores de verdad verdad ( T ) y falsedad ( F ), y una asignación a los símbolos conectivos de de sus significados veritativos habituales. Una interpretación de un cálculo proposicional funcional de verdad también se puede expresar en términos de tablas de verdad . [14]

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

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

Para la pareja , existen 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 le asigna F y se le asigna T . [14]

Dado que , es decir, tiene innumerables símbolos proposicionales, hay y, por lo tanto , incontables interpretaciones posibles distintas de . [14]

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

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

Algunas consecuencias de estas definiciones:

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 sólo una regla de inferencia.

Axiomas

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

regla de inferencia

La regla de inferencia es modus ponens :

.

Regla de metainferencia

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

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

Este teorema de deducción (DT) no está formulado 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 completitud del cálculo proposicional.

Por otro lado, la DT es tan útil para simplificar el proceso de prueba sintáctica que puede considerarse y utilizarse 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 de cálculo proposicional presentada en este artículo.

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

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

de hecho, la validez del inverso de DT es casi trivial en comparación con la de DT:

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

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

que puede transformarse mediante el inverso del teorema de deducción en

lo que nos dice que la regla de inferencia

es admisible . Esta regla de inferencia es la eliminación de conjunciones , 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 los axiomas ENTONCES-1 y ENTONCES-2 :

Demostrar: (Reflexividad de la implicación).

Prueba:

  1. Axioma ENTONCES-2 con
  2. Axioma ENTONCES-1 con
  3. De (1) y (2) por modus ponens.
  4. Axioma ENTONCES-1 con
  5. De (3) y (4) por modus ponens.

Equivalencia a la lógica ecuacional

El cálculo alternativo anterior es un ejemplo de un sistema de deducción estilo 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 de manera estándar de manera informal en el álgebra de la escuela secundaria, es un tipo de cálculo diferente a 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 en términos que admite sustitución.

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

Tanto en el álgebra booleana como en el de Heyting, se puede utilizar la desigualdad en lugar de la igualdad. La igualdad se puede expresar como un par de desigualdades y . Por el contrario, 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 implicación

.

La diferencia entre implicación y desigualdad o vinculación o es que la primera es interna a la lógica mientras que la segunda es externa. 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 que se estudia 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.

Son posibles traducciones similares pero más complejas hacia y desde la lógica algebraica para los sistemas de deducción natural descritos anteriormente y para el cálculo siguiente . Las implicaciones de este último pueden interpretarse como bivaluadas, pero una interpretación más perspicaz es como un conjunto, cuyos elementos pueden entenderse como pruebas abstractas organizadas como morfismos de una categoría . En esta interpretación, la regla de corte del cálculo secuente corresponde a la composición de la categoría. Las álgebras de Boole y Heyting entran en este cuadro como categorías especiales que tienen como máximo un morfismo por homset, es decir, una prueba por implicación, lo que corresponde a la idea de que lo único que importa es la existencia de pruebas: cualquier prueba servirá 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. Es má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 les extienda 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 correspondientes familias de estructuras de texto. Las exigencias de la computación práctica en lenguajes formales exigen con frecuencia que las cadenas de texto se conviertan en representaciones de estructuras de punteros de gráficos de análisis sintáctico, simplemente como una cuestión de comprobar 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 sobre cuerdas. El mapeo de cadenas a gráficos de análisis se llama análisis y el mapeo inverso de gráficos de análisis a cadenas se logra mediante una operación que se llama atravesar el gráfico.

Otros cálculos lógicos

El cálculo proposicional es el tipo más simple de cálculo lógico que se utiliza actualmente. Se puede ampliar de varias formas. ( El cálculo "silogístico" aristotélico , que ha sido suplantado en gran medida en la lógica moderna, es en algunos aspectos más simple – pero en otros 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 detalles más detallados 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 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 pueden capturarse 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ógica modal y lógica algebraica concierne a la lógica clásica e intuicionista pero con la introducción de un operador unario en las álgebras booleanas o de Heyting, diferente de las operaciones booleanas, que interpreta la modalidad de posibilidad, y en el caso del álgebra de Heyting un segundo operador que interpreta 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 multivaluadas son aquellas que permiten que las oraciones tengan valores distintos de verdadero y falso . (Por ejemplo, ninguno de los dos y ambos son "valores adicionales" 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 una cantidad infinita de valores), la lógica multivaluada se reduce a la lógica clásica; Por lo tanto, las lógicas multivaluadas sólo tienen interés independiente cuando los valores forman un álgebra que no es booleana.

Solucionadores

Una diferencia notable entre el cálculo proposicional y el cálculo de predicados es que la satisfacibilidad de una fórmula proposicional es decidible . [15] Decidir la satisfacibilidad de 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. Trabajos recientes han ampliado los algoritmos de resolución SAT para trabajar con proposiciones que contienen expresiones aritméticas ; Estos son los solucionadores SMT .

Ver también

Niveles lógicos superiores

Temas relacionados

Notas

  1. ^ Formalmente, la regla 2 obtiene fórmulas en notación polaca , es decir, en este ejemplo. Por conveniencia, usaremos la notación infija común en este y en todos los ejemplos siguientes.

Referencias

  1. ^ "Lógica proposicional | Wiki brillante de matemáticas y ciencias". brillante.org . Consultado el 20 de agosto de 2020 .
  2. ^ Bobzien, Susanne (1 de enero de 2016). "Lógica antigua". En Zalta, Edward N. (ed.). La Enciclopedia de Filosofía de Stanford. Laboratorio de Investigación en Metafísica, Universidad de Stanford, a través de la Enciclopedia de Filosofía de Stanford.
  3. ^ "Lógica proposicional | Enciclopedia de Filosofía de Internet" . Consultado el 20 de agosto de 2020 .
  4. ^ Marenbon, John (2007). Filosofía medieval: una introducción histórica y filosófica . Rutledge. pag. 137.
  5. ^ Peckhaus, Volker (1 de enero de 2014). "La influencia de Leibniz en la lógica del siglo XIX". En Zalta, Edward N. (ed.). La Enciclopedia de Filosofía de Stanford. Laboratorio de Investigación en Metafísica, Universidad de Stanford, a través de la Enciclopedia de Filosofía de Stanford.
  6. ^ Hurley, Patricio (2007). Una introducción concisa a la lógica, décima edición . Publicación Wadsworth. pag. 392.
  7. ^ Beth, Evert W.; "Vinculación semántica y derivabilidad formal", serie: Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, Nieuwe Reeks, vol. 18, núm. 13, Holanda del Norte Uitg. Mij., Ámsterdam, 1955, págs. 309–42. Reimpreso en Jaakko Intikka (ed.) The Philosophy of Mathematics , Oxford University Press, 1969
  8. ^ ab Verdad en Frege
  9. ^ abc "Russell: la revista de estudios de Bertrand Russell".
  10. ^ Anellis, Irving H. (2012). "Análisis funcional de verdad de Peirce y el origen de la tabla de verdad". Historia y Filosofía de la Lógica . 33 : 87–97. doi :10.1080/01445340.2011.621702. S2CID  170654885.
  11. ^ Wernick, William (1942) "Conjuntos completos de funciones lógicas", Transactions of the American Mathematical Society 51 , págs.
  12. ^ Usamos para denotar equivalencia de y , es decir, como abreviatura de y .
  13. ^ Toida, Shunichi (2 de agosto de 2009). "Prueba de implicaciones". CS381 Material del curso web de estructuras discretas/matemáticas discretas . Departamento de Ciencias de la Computación, Universidad Old Dominion . Consultado el 10 de marzo de 2010 .
  14. ^ abcdefghijk Cazador, Geoffrey (1971). Metalógica: una introducción a la metateoría de la lógica estándar de primer orden . Prensa de la Universidad de California. ISBN 0-520-02356-0.
  15. ^ WVO Quine, Lógica matemática (1980), p.81. Prensa de la Universidad de Harvard, 0-674-55451-5

Otras lecturas

Obras relacionadas

enlaces externos