Sistema axiomático (lógica)

Sistema de deducción formal en lógica.

En lógica , especialmente en lógica matemática , un sistema axiomático , a veces llamado sistema deductivo "estilo Hilbert", es un tipo de sistema de deducción formal desarrollado por Gottlob Frege , ^[1] Jan Łukasiewicz , ^[2] Russell y Whitehead, ^{[3 ]} y David Hilbert . ^[3] Estos sistemas deductivos se estudian con mayor frecuencia para la lógica de primer orden , pero también son de interés para otras lógicas.

La mayoría de las variantes de los sistemas axiomáticos adoptan un rumbo característico en la forma en que equilibran el equilibrio entre axiomas lógicos y reglas de inferencia . ^[1] Los sistemas axiomáticos pueden caracterizarse por la elección de un gran número de esquemas de axiomas lógicos y un pequeño conjunto de reglas de inferencia . Los sistemas de deducción natural adoptan el rumbo opuesto, e incluyen muchas reglas de deducción pero muy pocos o ningún esquema de axiomas. Los sistemas axiomáticos más comúnmente estudiados tienen una sola regla de inferencia ( modus ponens , para lógica proposicional  ) o dos (con generalización , para manejar también lógica de predicados ) y varios esquemas de axiomas infinitos. Los sistemas axiomáticos para lógicas modales aléticas , a veces llamados sistemas de Hilbert-Lewis, requieren además la regla de necesidad. Algunos sistemas utilizan una lista finita de fórmulas concretas como axiomas en lugar de un conjunto infinito de fórmulas mediante esquemas de axiomas, en cuyo caso se requiere la regla de sustitución uniforme.

Un rasgo característico de las muchas variantes de los sistemas axiomáticos es que el contexto no cambia en ninguna de sus reglas de inferencia, mientras que tanto la deducción natural como el cálculo secuencial contienen algunas reglas que cambian el contexto. Así, si uno está interesado sólo en la derivabilidad de las tautologías , y no en juicios hipotéticos, entonces puede formalizar el sistema axiomático de tal manera que sus reglas de inferencia contengan sólo juicios de una forma bastante simple. No se puede hacer lo mismo con los otros dos sistemas de deducciones: ^{[ cita necesaria ]} a medida que se cambia el contexto en algunas de sus reglas de inferencia, no se pueden formalizar de modo que se puedan evitar juicios hipotéticos, ni siquiera si queremos usarlos solo para demostrando la derivabilidad de tautologías.

Lógica proposicional

En lógica proposicional , es posible realizar pruebas axiomáticamente, lo que significa que ciertas tautologías se toman como evidentes y otras se deducen de ellas utilizando el modus ponens como regla de inferencia y regla de sustitución . Alternativamente, se utilizan esquemas de axiomas en lugar de axiomas y no se utiliza ninguna regla de sustitución.

fregeBegriffsschrift

Aunque la prueba axiomática se ha utilizado desde el famoso libro de texto griego antiguo , Los Elementos de geometría de Euclides , en lógica proposicional se remonta al Begriffsschrift de Gottlob Frege de 1879 . ^{[4] [5]} El sistema de Frege utilizaba únicamente implicación y negación como conectivos, ^[6] y tenía seis axiomas, ^[5] que eran estos: ^{[7] [8]}

• Proposición 1: ${\displaystyle a\supset (b\supset a)}$
• Proposición 2: ${\displaystyle (c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))}$
• Proposición 8: ${\displaystyle (d\supset (b\supset a))\supset (b\supset (d\supset a))}$
• Proposición 28: ${\displaystyle (b\supset a)\supset (\neg a\supset \neg b)}$
• Proposición 31: ${\displaystyle \neg \neg a\supset a}$
• Proposición 41: ${\displaystyle a\supset \neg \neg a}$

Frege los utilizó junto con el modus ponens y una regla de sustitución (que se utilizó pero nunca se estableció con precisión) para producir una axiomatización completa y consistente de la lógica proposicional funcional de verdad clásica. ^[7]

P de Łukasiewicz2

Jan Łukasiewicz demostró que, en el sistema de Frege, "el tercer axioma es superfluo ya que puede derivarse de los dos axiomas anteriores, y que los tres últimos axiomas pueden sustituirse por una sola frase ". ^[8] Lo cual, sacado de la notación polaca de Łukasiewicz a la notación moderna, significa . De ahí que a Łukasiewicz se le atribuye ^[5] este sistema de tres axiomas: ${\displaystyle CCNpNqCpq}$ ${\displaystyle (\neg p\rightarrow \neg q)\rightarrow (p\rightarrow q)}$

• ${\displaystyle p\to (q\to p)}$
• ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$
• ${\displaystyle (\neg p\to \neg q)\to (q\to p)}$

Al igual que el sistema de Frege, este sistema utiliza una regla de sustitución y utiliza el modus ponens como regla de inferencia. ^[5] Alonzo Church dio exactamente el mismo sistema (con una regla de sustitución explícita) , ^[9] quien se refirió a él como el sistema P _2, ^{[9] [2]} y ayudó a popularizarlo. ^[2]

Forma esquemática de P2

Una representación gráfica del sistema de deducción.

Se puede evitar utilizar la regla de sustitución dando los axiomas en forma esquemática, usándolos para generar un conjunto infinito de axiomas. Por lo tanto, usando letras griegas para representar esquemas (variables metalógicas que pueden representar cualquier fórmula bien formada ), los axiomas se dan como: ^{[4] [2]}

• ${\displaystyle \varphi \to (\psi \to \varphi )}$
• ${\displaystyle (\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))}$
• ${\displaystyle (\neg \varphi \to \neg \psi )\to (\psi \to \varphi )}$

La versión esquemática de P ₂ se atribuye a John von Neumann , ^[5] y se utiliza en la base de datos de prueba formal "set.mm" de Metamath . ^[2] También ha sido atribuido a Hilbert , ^[10] y nombrado en este contexto. ^[10] ${\displaystyle {\mathcal {H}}}$

Ejemplo de prueba en P₂

Como ejemplo, a continuación se proporciona una prueba de en P ₂ . Primero, los axiomas reciben nombres: ${\displaystyle A\to A}$

(A1) ${\displaystyle (p\to (q\to p))}$

(A2) ${\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}$

(A3) ${\displaystyle ((\neg p\to \neg q)\to (q\to p))}$

Y la prueba es la siguiente:

1. ${\displaystyle A\to ((B\to A)\to A)}$       (instancia de (A1))
2. ${\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}$       (instancia de (A2))
3. ${\displaystyle (A\to (B\to A))\to (A\to A)}$       (de (1) y (2) por modus ponens )
4. ${\displaystyle A\to (B\to A)}$       (instancia de (A1))
5. ${\displaystyle A\to A}$       (de (4) y (3) por modus ponens)

Consistencia e integridad de P₂

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:

• A satisface la variable proposicional P si y sólo si A ( P ) = verdadero
• A satisface ¬ φ si y sólo si A no satisface φ
• A satisface ( φ ∧ ψ ) si y sólo si A satisface tanto φ como ψ
• A satisface ( φ ∨ ψ ) si y sólo si A satisface al menos uno de φ o ψ
• A satisface ( φ → ψ ) si y sólo si no se da el caso de que A satisface φ pero no ψ
• A satisface ( φ ↔ ψ ) si y sólo si A satisface tanto φ como ψ o no satisface ninguno de ellos

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 implicado 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". 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 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 ₁ , E ₂ , ...)
   2. Defina una serie G _n de conjuntos ( G ₀ , G ₁ , ...) de forma inductiva:
      1. ${\displaystyle G_{0}=G}$
      2. Si se prueba A , entonces ${\displaystyle G_{k}\cup \{E_{k+1}\}}$ ${\displaystyle G_{k+1}=G_{k}}$
      3. Si no prueba A , entonces ${\displaystyle G_{k}\cup \{E_{k+1}\}}$ ${\displaystyle G_{k+1}=G_{k}\cup \{E_{k+1}\}}$
   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 : si se añadieran más oraciones a G ^∗ , seprobarí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 ; y así sucesivamente. 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 C → D y ¬C → D , entonces prueba D. Esto se utiliza, 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 B → A . Pero supongamos que ¬B tampoco estuviera en G ^∗ , entonces por la misma lógica G ^∗ también prueba ¬B → A ; 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 C → D.
   • Para cualquier fórmula C y D , si prueba C y ¬D , entonces prueba ¬( C → D ).
   • Para cualquier fórmula C y D , si prueba ¬C , entonces prueba C → D.
   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:

• ${\displaystyle p\to (\neg p\to q)}$
• ${\displaystyle (p\to q)\to ((\neg p\to q)\to q)}$
• ${\displaystyle p\to (q\to (p\to q))}$
• ${\displaystyle p\to (\neg q\to \neg (p\to q))}$
• ${\displaystyle \neg p\to (p\to q)}$
• ${\displaystyle p\to p}$
• ${\displaystyle p\to (q\to p)}$
• ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$

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 pueden demostrarse 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 puede demostrarse, como ahora mostramos. ${\displaystyle (\neg q\to \neg p)\to (p\to q)}$

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

1. ${\displaystyle q\to (p\to q)}$       (ejemplo del séptimo teorema)
2. ${\displaystyle (q\to (p\to q))\to ((\neg q\to \neg p)\to (q\to (p\to q)))}$       (ejemplo del séptimo teorema)
3. ${\displaystyle (\neg q\to \neg p)\to (q\to (p\to q))}$       (de (1) y (2) por modus ponens)
4. ${\displaystyle (\neg p\to (p\to q))\to ((\neg q\to \neg p)\to (\neg q\to (p\to q)))}$       (ejemplo del teorema del silogismo hipotético)
5. ${\displaystyle (\neg p\to (p\to q))}$       (ejemplo del quinto teorema)
6. ${\displaystyle (\neg q\to \neg p)\to (\neg q\to (p\to q))}$       (de (5) y (4) por modus ponens)
7. ${\displaystyle (q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))}$       (ejemplo del segundo teorema)
8. ${\displaystyle ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))\to ((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))}$       (ejemplo del séptimo teorema)
9. ${\displaystyle (\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))}$       (de (7) y (8) por modus ponens)
10. ${\displaystyle ((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))\to }$

    ${\displaystyle (((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))))}$       (ejemplo del octavo teorema)

11. ${\displaystyle ((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))}$       (de (9) y (10) por modus ponens)
12. ${\displaystyle (\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))}$       (de (3) y (11) por modus ponens)
13. ${\displaystyle ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))\to (((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q)))}$       (ejemplo del octavo teorema)
14. ${\displaystyle ((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q))}$       (de (12) y (13) por modus ponens)
15. ${\displaystyle (\neg q\to \neg p)\to (p\to q)}$       (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) ${\displaystyle \neg \neg p\to p}$

(DN2) - Doble negación (otra dirección) ${\displaystyle p\to \neg \neg p}$

(HS1) - una forma de silogismo hipotético ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$

(HS2) - otra forma de silogismo hipotético ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$

(TR1) - Transposición ${\displaystyle (p\to q)\to (\neg q\to \neg p)}$

(TR2) - otra forma de transposición. ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$

(L1) ${\displaystyle p\to ((p\to q)\to q)}$

(L3) ${\displaystyle (\neg p\to p)\to p}$

También utilizamos el método del metateorema del silogismo hipotético como abreviatura de varios pasos de demostración.

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

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.

Diferente sistema de prueba axiomática.

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:

• El axioma ENTONCES-2 puede considerarse una "propiedad distributiva de implicación con respecto a implicación".
• Los axiomas AND-1 y AND-2 corresponden a la "eliminación de conjunciones". La relación entre AND-1 y AND-2 refleja la conmutatividad del operador de conjunción.
• El axioma AND-3 corresponde a "introducción de conjunción".
• Los axiomas OR-1 y OR-2 corresponden a la "introducción a la 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".
• El axioma NOT-2 dice que "de una contradicción se puede deducir cualquier cosa".
• El axioma NOT-3 se llama " tertium non datur " ( latín : "no se da un tercio") y refleja la valoración semántica de las 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 NOT-3 .

regla de inferencia

La regla de inferencia es modus ponens :

${\displaystyle {\frac {\phi ,\ \phi \to \chi }{\chi }}}$.

Ejemplo de prueba en los diferentes sistemas axiomáticos.

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). ${\displaystyle A\to A}$

Prueba:

1. ${\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}$

   Axioma ENTONCES-2 con ${\displaystyle \phi =A,\chi =B\to A,\psi =A}$

2. ${\displaystyle A\to ((B\to A)\to A)}$

   Axioma ENTONCES-1 con ${\displaystyle \phi =A,\chi =B\to A}$

3. ${\displaystyle (A\to (B\to A))\to (A\to A)}$

   De (1) y (2) por modus ponens.

4. ${\displaystyle A\to (B\to A)}$

   Axioma ENTONCES-1 con ${\displaystyle \phi =A,\chi =B}$

5. ${\displaystyle A\to A}$

   De (3) y (4) por modus ponens.

metalógico

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

${\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi }$

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

${\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \to \psi }$.

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, 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 de cálculo proposicional presentada en este artículo.

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

Si la secuencia

${\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \to \psi }$

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

${\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi }$

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

Si

${\displaystyle \phi _{1},\ ...,\ \phi _{n}\vdash \chi \to \psi }$

entonces

1: ${\displaystyle \phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi \to \psi }$

2: ${\displaystyle \phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi }$

y de (1) y (2) se puede deducir

3: ${\displaystyle \phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \psi }$

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,

${\displaystyle \vdash \phi \wedge \chi \to \phi ,}$

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

${\displaystyle \phi \wedge \chi \vdash \phi ,}$

lo que nos dice que la regla de inferencia

${\displaystyle {\frac {\phi \wedge \chi }{\phi }}}$

es admisible . Esta regla de inferencia es la eliminación de conjunciones , una de las reglas de inferencia utilizadas en la deducción natural .

Extensiones conservadoras

Es común incluir en un sistema axiomático de lógica sólo axiomas de implicación y negación. Dados estos axiomas, es posible formar extensiones conservadoras del teorema de deducción que permitan el uso de conectivos adicionales. Estas extensiones se llaman conservadoras porque si una fórmula φ que involucra nuevos conectivos se reescribe como una fórmula lógicamente equivalente θ que involucra solo negación, implicación y cuantificación universal, entonces φ es derivable en el sistema extendido si y solo si θ es derivable en el sistema original. . Cuando esté completamente extendido, un sistema axiomático se parecerá más a un sistema de deducción natural .

Cuantificación existencial

• Introducción

${\displaystyle \forall x(\phi \to \exists y(\phi [x:=y]))}$

• Eliminación

${\displaystyle \forall x(\phi \to \psi )\to \exists x(\phi )\to \psi }$donde no es una variable libre de . ${\displaystyle x}$ ${\displaystyle \psi }$

Conjunción y disyunción

• Introducción y eliminación de conjunciones.

introducción: ${\displaystyle \alpha \to (\beta \to \alpha \land \beta )}$

eliminación restante: ${\displaystyle \alpha \wedge \beta \to \alpha }$

derecho de eliminación: ${\displaystyle \alpha \wedge \beta \to \beta }$

• Introducción y eliminación de disyunciones.

introducción a la izquierda: ${\displaystyle \alpha \to \alpha \vee \beta }$

introducción a la derecha: ${\displaystyle \beta \to \alpha \vee \beta }$

eliminación: ${\displaystyle (\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )}$

Metateoremas

Debido a que los sistemas lógicos axiomáticos tienen muy pocas reglas de deducción, es común demostrar metateoremas que muestran que reglas de deducción adicionales no añaden poder deductivo, en el sentido de que una deducción que usa las nuevas reglas de deducción se puede convertir en una deducción que usa solo las reglas de deducción originales. .

Algunos metateoremas comunes de esta forma son:

• El teorema de la deducción : si y sólo si . ${\displaystyle \Gamma ;\phi \vdash \psi }$ ${\displaystyle \Gamma \vdash \phi \to \psi }$
• ${\displaystyle \Gamma \vdash \phi \leftrightarrow \psi }$si y sólo si y . ${\displaystyle \Gamma \vdash \phi \to \psi }$ ${\displaystyle \Gamma \vdash \psi \to \phi }$
• Contraposición: Si entonces . ${\displaystyle \Gamma ;\phi \vdash \psi }$ ${\displaystyle \Gamma ;\lnot \psi \vdash \lnot \phi }$
• Generalización : Si y x no aparecen libres en ninguna fórmula de entonces . ${\displaystyle \Gamma \vdash \phi }$ ${\displaystyle \Gamma }$ ${\displaystyle \Gamma \vdash \forall x\phi }$

Algunos teoremas útiles y sus demostraciones.

A continuación se presentan varios teoremas de lógica proposicional , junto con sus demostraciones (o enlaces a estas demostraciones en otros artículos). Tenga en cuenta que dado que (P1) se puede demostrar utilizando los otros axiomas, de hecho (P2), (P3) y (P4) son suficientes para demostrar todos estos teoremas.

(HS1) - Silogismo hipotético , ver prueba . ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$

(L1) - prueba: ${\displaystyle p\to ((p\to q)\to q)}$

(1)       (instancia de (P3)) ${\displaystyle ((p\to q)\to (p\to q))\to (((p\to q)\to p)\to ((p\to q)\to q))}$

(2)       (instancia de (P1)) ${\displaystyle (p\to q)\to (p\to q)}$

(3)       (de (2) y (1) por modus ponens ) ${\displaystyle ((p\to q)\to p)\to ((p\to q)\to q)}$

(4)       (instancia de (HS1)) ${\displaystyle (((p\to q)\to p)\to ((p\to q)\to q))\to ((p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q)))}$

(5)       (de (3) y (4) por modus ponens) ${\displaystyle (p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q))}$

(6)       (instancia de (P2)) ${\displaystyle p\to ((p\to q)\to p)}$

(7)       (de (6) y (5) por modus ponens) ${\displaystyle p\to ((p\to q)\to q)}$

Los dos teoremas siguientes se conocen juntos como doble negación :

(DN1) ${\displaystyle \neg \neg p\to p}$

(DN2) ${\displaystyle p\to \neg \neg p}$

Ver pruebas .

(L2) - para esta prueba utilizamos el método del metateorema del silogismo hipotético como abreviatura de varios pasos de la prueba: ${\displaystyle (p\to (q\to r))\to (q\to (p\to r))}$

(1)       (instancia de (P3)) ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$

(2)       (instancia de (HS1)) ${\displaystyle ((p\to q)\to (p\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))}$

(3)       (de (1) y (2) utilizando el metateorema del silogismo hipotético) ${\displaystyle (p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))}$

(4)       (instancia de (P3)) ${\displaystyle ((p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r))))\to (((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r))))}$

(5)       (de (3) y (4) usando modus ponens) ${\displaystyle ((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r)))}$

(6)       (instancia de (P2)) ${\displaystyle q\to (p\to q)}$

(7)       (instancia de (P2)) ${\displaystyle (q\to (p\to q))\to ((p\to (q\to r))\to (q\to (p\to q)))}$

(8)       (de (6) y (7) usando modus ponens) ${\displaystyle (p\to (q\to r))\to (q\to (p\to q))}$

(9)       (de (8) y (5) usando modus ponens) ${\displaystyle (p\to (q\to r))\to (q\to (p\to r))}$

(HS2) - una forma alternativa del silogismo hipotético . prueba: ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$

(1)       (instancia de (HS1)) ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$

(2)       (instancia de (L2)) ${\displaystyle ((q\to r)\to ((p\to q)\to (p\to r)))\to ((p\to q)\to ((q\to r)\to (p\to r)))}$

(3) (de (1) y (2) por modus ponens) ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$

(TR1) - Transposición, ver prueba (la otra dirección de transposición es (P4)). ${\displaystyle (p\to q)\to (\neg q\to \neg p)}$

(TR2) - otra forma de transposición; prueba: ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$

(1)       (instancia de (TR1)) ${\displaystyle (\neg p\to q)\to (\neg q\to \neg \neg p)}$

(2)       (instancia de (DN1)) ${\displaystyle \neg \neg p\to p}$

(3)       (instancia de (HS1)) ${\displaystyle (\neg \neg p\to p)\to ((\neg q\to \neg \neg p)\to (\neg q\to p))}$

(4)       (de (2) y (3) por modus ponens) ${\displaystyle (\neg q\to \neg \neg p)\to (\neg q\to p)}$

(5)       (de (1) y (4) utilizando el metateorema del silogismo hipotético) ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$

(L3) - prueba: ${\displaystyle (\neg p\to p)\to p}$

(1)       (instancia de (P2)) ${\displaystyle \neg p\to (\neg \neg (q\to q)\to \neg p)}$

(2)       (instancia de (P4)) ${\displaystyle (\neg \neg (q\to q)\to \neg p)\to (p\to \neg (q\to q))}$

(3)       (de (1) y (2) utilizando el metateorema del silogismo hipotético) ${\displaystyle \neg p\to (p\to \neg (q\to q))}$

(4)       (instancia de (P3)) ${\displaystyle (\neg p\to (p\to \neg (q\to q)))\to ((\neg p\to p)\to (\neg p\to \neg (q\to q)))}$

(5)       (de (3) y (4) usando modos ponens) ${\displaystyle (\neg p\to p)\to (\neg p\to \neg (q\to q))}$

(6)       (instancia de (P4)) ${\displaystyle (\neg p\to \neg (q\to q))\to ((q\to q)\to p)}$

(7)       (de (5) y (6) usando el metateorema del silogismo hipotético) ${\displaystyle (\neg p\to p)\to ((q\to q)\to p)}$

(8)       (instancia de (P1)) ${\displaystyle q\to q}$

(9)       (instancia de (L1)) ${\displaystyle (q\to q)\to (((q\to q)\to p)\to p)}$

(10)       (de (8) y (9) usando modos ponens) ${\displaystyle ((q\to q)\to p)\to p}$

(11)       (de (7) y (10) usando el metateorema del silogismo hipotético) ${\displaystyle (\neg p\to p)\to p}$

Ver también

• Lista de sistemas axiomáticos en lógica.
• deducción natural
• Correspondencia entre Curry y Howard
• Lógica combinatoria

Notas

1. Máté y Ruzsa 1997:129
2. "Proof Explorer - Página de inicio - Metamath". us.metamath.org . Consultado el 2 de julio de 2024 .
3. Craig, Edward (1998). Enciclopedia de Filosofía de Routledge. Taylor y Francisco. pag. 733.ISBN​ 978-0-415-18710-7.
4. Bostock, David (1997). Lógica intermedia . Oxford: Nueva York: Clarendon Press; Prensa de la Universidad de Oxford. págs. 4–5, 8–13, 18–19, 22, 27, 29, 191, 194. ISBN 978-0-19-875141-0.
5. Smullyan, Raymond M. (23 de julio de 2014). Una guía para principiantes de lógica matemática. Corporación de mensajería. págs. 102-103. ISBN 978-0-486-49237-7.
6. Franks, Curtis (2023), "Lógica proposicional", en Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (edición de otoño de 2023), Metaphysics Research Lab, Universidad de Stanford , consultado el 22 de marzo de 2024.
7. Mendelsohn, Richard L. (10 de enero de 2005). La filosofía de Gottlob Frege. Prensa de la Universidad de Cambridge. pag. 185.ISBN​ 978-1-139-44403-3.
8. Łukasiewicz, enero (1970). Jan Lukasiewicz: obras seleccionadas. Holanda del Norte. pag. 136.
9. Iglesia, Alonzo (1996). Introducción a la Lógica Matemática. Prensa de la Universidad de Princeton. pag. 119.ISBN​ 978-0-691-02906-1.
10. Walicki, Michał (2017). Introducción a la lógica matemática (edición ampliada). Nueva Jersey: World Scientific. pag. 126.ISBN​ 978-981-4719-95-7.

Referencias

• Curry, Haskell B.; Robert Feys (1958). Lógica combinatoria vol. I . vol. 1. Ámsterdam: Holanda Septentrional.
• Monje, J. Donald (1976). Lógica Matemática . Textos de Posgrado en Matemáticas. Berlín, Nueva York: Springer-Verlag . ISBN 978-0-387-90170-1.
• Ruzsa, Imre; Máté, András (1997). Bevezetés a modern logikába (en húngaro). Budapest: Osiris Kiadó.
• Tarski, Alfred (1990). Bizonyítás és igazság (en húngaro). Budapest: góndola.Es una traducción al húngaro de los artículos seleccionados de Alfred Tarski sobre la teoría semántica de la verdad .
• David Hilbert (1927) "Los fundamentos de las matemáticas", traducido por Stephan Bauer-Menglerberg y Dagfinn Føllesdal (págs. 464–479). en:
  • van Heijenoort, Jean (1967). De Frege a Gödel: un libro de consulta sobre lógica matemática, 1879-1931 (tercera edición, edición de 1976). Cambridge MA: Harvard University Press. ISBN 0-674-32449-8.
  • Hilbert's 1927, basado en una conferencia anterior sobre "fundamentos" de 1925 (págs. 367-392), presenta sus 17 axiomas: axiomas de implicación #1-4, axiomas sobre & y V #5-10, axiomas de negación #11- 12, su ε-axioma lógico #13, axiomas de igualdad #14-15 y axiomas de números #16-17, junto con los otros elementos necesarios de su "teoría de la prueba" formalista, por ejemplo, axiomas de inducción, axiomas de recursividad, etc; también ofrece una enérgica defensa contra el intuicionismo de LEJ Brouwer. Véanse también los comentarios y la refutación de Hermann Weyl (1927) (págs. 480–484), el apéndice de Paul Bernay (1927) a la conferencia de Hilbert (págs. 485–489) y la respuesta de Luitzen Egbertus Jan Brouwer (1927) (págs. 490–495).
• Kleene, Stephen Cole (1952). Introducción a las metamatemáticas (décima impresión con correcciones de 1971, edición). Ámsterdam Nueva York: Compañía editorial de North Holland. ISBN 0-7204-2103-9.
  • Véase en particular el Capítulo IV Sistema formal (págs. 69–85), donde Kleene presenta los subcapítulos §16 Símbolos formales, §17 Reglas de formación, §18 Variables libres y ligadas (incluida la sustitución), §19 Reglas de transformación (por ejemplo, modus ponens). y de estos presenta 21 "postulados" - 18 axiomas y 3 relaciones de "consecuencia inmediata" divididas de la siguiente manera: Postulados para el cálculo proposicional #1-8, Postulados adicionales para el cálculo de predicados #9-12, y Postulados adicionales para Teoría de números #13-21.

Enlaces externos

• Gaifman, Haim. "Un sistema deductivo tipo Hilbert para lógica oracional, completitud y compacidad" (PDF) .
• Farmer, WM "Lógica proposicional" (PDF) .Describe (entre otros) una parte del sistema de deducción al estilo de Hilbert (restringido al cálculo proposicional ).