¿Cómo se sabe si A⟹BA⟹BA \implica que B (una implicación) es verdadera sin saber si BBB (el consecuente) es verdadera?

Considere las siguientes declaraciones:

$A$: Adam vive en Boston;$B$: Adam vive en Massachusetts.

Nunca has conocido a Adam antes, y no tienes idea de si las declaraciones$A$o$B$son verdaderas. Pero usted sabe que la declaración$A \Rightarrow B$es verdad. Si ahora les presentara una forma de probar que Adam vivía en Boston, podrían concluir razonablemente que vive en Massachusetts.

Supongo que estarías de acuerdo con una afirmación como "Si llueve, las calles se mojan", ¿verdad?

Ahora bien, antes de aceptar la verdad de ese condicional, ¿miraste por la ventana para ver si en este momento está lloviendo o no, y si en este momento las calles se están mojando o no? No, claramente no.

Sí, es cierto que muchas veces llegamos a la verdad de los condicionales basándonos en la evidencia empírica, es decir, presumiblemente en un montón de casos en los que observamos que el antecedente es verdadero y el consecuente también es verdadero... y también no vemos casos en los que el antecedente es verdadero. verdadero y el consecuente falso. Sin embargo, tales condicionales se establecen mediante un razonamiento no deductivo, sino generalizaciones inductivas u otro razonamiento similar. Entonces, no hay circularidad de razonamiento aquí.

Además, algunos condicionales simplemente se afirman como parte de alguna definición o axioma, por lo que en ese caso cualquier observación de que las declaraciones y sean realmente verdaderas o falsas no se usa en absoluto.

Además, los condicionales suelen formar parte de enunciados universales. De hecho, el 'si llueve, las calles se mojan' también puede verse como tal: es realmente un reclamo universal sobre cualquier lugar y en cualquier momento. Entonces, es realmente el universal lo que estamos estableciendo sobre la base de muchas observaciones, o simplemente lo estamos afirmando como un axioma, y ​​entonces ciertamente no estamos estableciendo la verdad de ese universal condicionado a una sola observación en cuanto a si el antecedente y el consecuente son verdaderas o falsas.

Finalmente, una vez que se establecen los condicionales, podemos simplemente usarlos, sin tener que preocuparnos si el antecedente es realmente verdadero o falso, o si el consecuente es verdadero o falso. Entonces, en la práctica, realmente no hay un problema de huevo y gallina aquí.

La forma en que pensó que funcionaban las matemáticas, o más bien la demostración informal de teoremas, es cómo funciona. La lógica proposicional clásica es un pequeño fragmento de las herramientas de razonamiento utilizadas por los argumentos informales típicos y, de manera más general, un enfoque semántico de la lógica no se adapta bien al proceso de prueba, por lo tanto, a la teoría de la prueba.

Hay dos enfoques amplios para comprender la lógica (formal): un enfoque sintáctico o teórico de prueba y un enfoque semántico o teórico de modelos.

El uso de tablas de verdad y funciones de verdad es un enfoque semántico. Aquí interpretamos las fórmulas sintácticas en objetos matemáticos, y luego si la "verdad" de una proposición se convierte en una propiedad del objeto matemático como se interpreta. Por ejemplo, podemos interpretar las proposiciones$A$y$B$como subconjuntos$[\![A]\!]$y$[\![B]\!]$de un conjunto$X$. preguntando si$A\lor B$es "verdadero" se convierte en la afirmación de que$[\![A]\!]\cup[\![B]\!]=X$. Tenga en cuenta que esto no tiene nada que ver con si$A$o$B$son filosóficamente "verdaderos". La interpretación del enunciado es simplemente preguntar si la unión de dos conjuntos es igual a otro. Demostrar o refutar esta afirmación normalmente se hará de manera informal, pero podría hacerse de manera formal, por ejemplo, con la teoría de conjuntos de Zermelo-Fraenkel en este caso. Por supuesto, no podemos usar exactamente el mismo enfoque para probar esta afirmación semántica. Esto lleva al otro enfoque: la teoría de la prueba.

Una forma diferente de entender lo que sucede en la lógica es dar reglas. Aquí las fórmulas sintácticas se quedan en la sintaxis. En cambio, damos reglas que transforman estas fórmulas y llamamos axiomas a ciertas fórmulas. Los teoremas son entonces cualquier fórmula que podamos obtener aplicando las reglas a los axiomas. Esto se parece mucho más al proceso "mecánico" al que aludes. De hecho, esto es lo que hacen los programas de demostración de teoremas. La idea filosófica es que se supone que los axiomas representan cosas que son "verdaderas", y se supone que las reglas "preservan la verdad", pero todo es solo un símbolo. No importa a las reglas si las fórmulas son verdaderas o no, o incluso si son contradictorias. Para la lógica típica, desde el punto de vista de la teoría de la demostración, toda inconsistencia significa que todofórmula se puede llegar a partir de los axiomas por las reglas. (Semánticamente, la inconsistencia generalmente significa que no hay un modelo. En otros enfoques de la semántica, puede significar que solo hay modelos "triviales"). La prueba real es entonces la secuencia de aplicaciones de reglas (válidas) y se llama derivación.

El sistema de prueba que normalmente se presenta primero a los estudiantes es un sistema de prueba estilo Hilbert . Esto es un poco vergonzoso ya que los sistemas de prueba al estilo de Hilbert no son muy fáciles de usar para los humanos. Otros sistemas de prueba incluyen la deducción natural y el cálculo secuente . Personalmente, me gusta usar la deducción natural a través de una lente de Curry-Howard.. Esto lleva a que las pruebas tengan una representación compacta y simple que facilita la manipulación de símbolos. (Las conexiones con la computación también brindan mucha intuición si uno está familiarizado con la programación funcional). Por ejemplo, el uso de modus ponens corresponde solo a la aplicación de funciones. (Desde esta perspectiva, la falta de compatibilidad humana de los sistemas de prueba al estilo de Hilbert es más evidente, ya que corresponden a la lógica combinatorialo cual es muy desagradable de programar). Las pruebas de deducción natural (como su nombre podría sugerir) estaban destinadas a estar más cerca de cómo fluían las pruebas informales. Una vez que tenga una cantidad decente de experiencia con pruebas informales y con sistemas como la deducción natural, en realidad es bastante fácil "leer" incluso la estructura lógica detallada de una prueba informal como una derivación en un sistema similar a la deducción natural.

El enfoque sintáctico proporciona una respuesta directa a sus preocupaciones acerca de la necesidad de conocer el valor de verdad de$B$conocer el valor de verdad de$A\Rightarrow B$usar el modus ponens. Modus ponens es una regla de inferencia, simplemente establece que si tenemos una derivación de$A$(es decir, una secuencia de aplicaciones de reglas válidas) y una derivación de$A\Rightarrow B$, entonces podemos hacer una derivación de$B$. Derivando$A\Rightarrow B$no necesita (y típicamente no requerirá) tener ya una derivación de$B$. En la práctica, las reglas suelen formularse para trabajar sobre fórmulas condicionales. A menudo estos se escriben como por ejemplo$\varphi,\psi\vdash\chi$(aunque esta notación se usa en una variedad de formas diferentes pero relacionadas) que intuitivamente se supone que significa "es probable que$\chi$es cierto si$\varphi$y$\psi$son verdaderas", pero, de nuevo, es solo sintaxis que será manipulada. La lectura intuitiva solo se justifica si las reglas y los axiomas lo permiten. El uso de fórmulas condicionales hace que sea mucho más fácil incluir suposiciones, y también hace que formular las reglas significativamente más simple.

Finalmente, estos dos enfoques de la lógica son diferentes . No está nada claro a priori que conduzcan a la misma noción de "verdad". Los (meta) teoremas de solidez y completitud, por ejemplo, los de FOL , (y la noción más fuerte de una lógica internaque entra en la semántica categórica) son los que los conectan. Pero los teoremas de solidez y completitud son (meta-) teoremas que deben probarse para un sistema de prueba y una semántica dados. No siempre es posible probar ambos (aunque por lo general una violación de la solidez significa que has hecho algo muy malo). En el enfoque sintáctico, una prueba es una derivación y, por lo tanto, verificar las tablas de verdad es simplemente un disparate. Incluso si las tablas de verdad muestran que una fórmula es una tautología, eso en realidad no le proporciona una derivación y, por lo tanto, no tiene ningún uso sintáctico. La prueba (meta-lógica) de la integridad de un sistema de deducción natural para la lógica proposicional clásica con respecto a las tablas de verdad, por ejemplo, necesita mostrar cómo construir una derivación de deducción natural dada una fórmula y una tabla de verdad que muestre que la fórmula es válida. Aparentemente, es bastante común que los enfoques sintáctico y semántico de la lógica se combinen significativamente o al menos no se separen claramente, pero esto genera mucha confusión. (Por ejemplo, si uno pensó que una prueba estaba verificando tablas de verdad, entonces la solidez y la integridad ni siquiera tienen sentido o parecen completamente triviales).

De hecho, podemos probar que la implicación$A\implies B$es verdad sabiendo solo que$A$es falso y nada en absoluto sobre$B$.

La única propiedad de implicación material que requerimos es que, si asume$P$y posteriormente puede derivar$Q$entonces puedes inferir$P \implies Q$. (Se aplican algunas restricciones).

Teorema:

$\neg A \implies [A\implies B]$

Prueba:

1. Suponer$\neg A$

2. Suponer$A$

3. Supongamos (al contrario) que$\neg B$

4. Une (2) y (1) para obtener la contradicción$A \land \neg A$

5. Concluye esto$\neg \neg B$de (3) y (4).

6. Elimina la doble negación de (5) para obtener$B$.

7. Concluye esto$A\implies B$de (2) y (6).

8. Concluir, según se requiere, que$\neg A \implies [A\implies B]$de (1) y (7).

Asimismo, también podemos probar:

$A \land B \implies [A\implies B]$

$A \land \neg B \implies \neg [A \implies B]\space$(requiere regla de desapego también)

De esta manera, podemos justificar la tabla de verdad habitual para la implicación material.

Seguimiento: Otro enfoque: He probado que$[A\implies B] \iff \neg [A \land \neg B]$utilizando reglas de desglose y deducción. A menudo se expresa simplemente como una definición que deja a muchos principiantes rascándose la cabeza.$\neg A \implies [A \implies B]$es un corolario. Vea "Si los cerdos pudieran volar", nuevo hoy en mi blog de matemáticas .

Para responder a la pregunta específica:

cómo en la práctica somos capaces de conocer A⟹B es cierto en el primero.

En general, cuando se le proporciona una Proposición A→B arbitraria , no tiene idea de si la proposición de que A implica materialmente a B es VERDADERA o no. ¡Eso está en debate!

Cuando escribes una prueba, puedes seleccionar cada paso que usas. En cada paso, seleccione A y B para los cuales puede justificar que A→B sea verdadero.

Hay cientos de principios ampliamente aceptados que puedes usar como justificación. Para las tareas escolares, si confías en que alguien ya las ha probado, úsalas. (incluso si no está seguro de cuál es el "nombre" exacto. Pero si se le pregunta sobre algún paso individual, debe poder justificarlo)

Más generalmente:

El término "Tabla de verdad" es una elección de nombre confusa y terrible , en mi opinión.

Peor aún, muchas personas (incluidos los instructores) citarán rutinariamente la "Tabla de verdad" que muestra la relación entre A , B y A→B como una razón que "prueba" que A→B es VERDADERO o FALSO.

Esto demuestra que NO entienden de lo que están hablando.

El símbolo " → ", a menudo traducido como "implica" en inglés, NO tiene el mismo significado en la semántica lógica clásica que la palabra "implica" en inglés estándar. El símbolo es parte de un sistema que utiliza "objetos", "variables", "conectores", "operadores" o "funciones" matemáticos/lógicos con definiciones muy específicas. (Al igual que "+" o "-" tienen una definición específica en matemáticas).

El símbolo " → " se define mejor como el conectivo/operador "Condicional material" o "Implicación material".

" → " se define como un conector entre otros dos "objetos", y se puede pensar que toma "dos entradas". Cada entrada debe evaluarse como VERDADERO o FALSO.

" → " fue luego DEFINIDO para producir, o resolver, UNA salida, ya sea VERDADERO o FALSO.

La DEFINICIÓN del operador " → " ES la tabla de verdad a la que se hace referencia tan a menudo.

Esa tabla anterior ES lo que DEFINE cómo funciona el símbolo " → ", el operador/conectivo "Implicación material" o "Regla de inferencia".

¿Por qué lo eligieron para operar de esa manera? Esa es una explicación más larga, y no pretendo entenderla completamente. Las dos primeras líneas de la tabla tienen un sentido intuitivo completo y se remontan a miles de años atrás a una idea llamada Modus Ponens. ¿Las dos últimas líneas de la tabla? Bueno, tenían sus razones, y la definición es consistente con el resto del sistema.

( Vale la pena señalar que, si bien la tercera línea define que " A→B " es VERDADERO , se llama Verdad Vacua . Cuando A es Falso, estas relaciones NO se usan en la práctica para justificar que " B " es VERDADERO o incluso que " A→B " podría ser VERDADERO. Cuando A es falso, esencialmente no tienes información útil).

La lógica clásica también define el símbolo " ⟷ ", llamado conector/operador "bicondicional material" .

La definición de " ⟷ " en la tabla a continuación se alinea más estrechamente con la comprensión típica de "implica" en inglés.

(*) Ejemplo de una implicación: Si un snack contiene azúcar, será dulce.

Modus ponens nos dice que partimos de la premisa (*), y además sabemos que un snack contiene azúcar, entonces podemos afirmar que el snack será dulce.

El ejemplo de las tablas de verdad y la lógica proposicional oculta la mayor parte de la complejidad de las matemáticas reales, que involucran variables y cuantificadores. Entonces, en lugar de mirar ejemplos un tanto artificiales en lógica proposicional, podemos mirar ejemplos más naturales de las matemáticas reales. Aquí hay un mejor ejemplo de una implicación que podemos demostrar que es verdadera, aunque no sabemos si la hipótesis es verdadera o falsa:

Si$n$es un número natural par entonces$n^2$es un número natural par.

prueba: si$n$es un número natural par, entonces$n = 2m$para algún número natural$m$. Entonces$n^2 = 4m^2 = 2(2m^2)$, entonces$n^2$también es par.

En este caso, no podemos decir si "$n$es un número natural par" es verdadero o falso - no tenemos un valor específico para$n$. En cambio, estamos probando un hecho sobre todos los números naturales simultáneamente (a saber, que si son pares, también lo es su cuadrado). Para probar este tipo de declaración, "asumimos la hipótesis y probamos la conclusión": suponemos que se nos presenta un número par que de otro modo sería desconocido.$n$, y probar que$n^2$también debe ser par.

Los puntos de partida, debajo de todo, son definiciones. La definición de un "número par" nos permite afirmar que si$n$es un número natural par entonces$n = 2m$para algún número natural$m$. Esta ya es una declaración de implicación, pero no la "probamos" por separado porque es simplemente la definición de "par". En cierto sentido, la prueba anterior simplemente demuestra una implicación más complicada al combinar implicaciones más simples que ya se conocían.

Entonces, ¿cómo podríamos aplicar modus ponens en un argumento usando nuestro teorema? Si probamos por separado que algún número particular$C$es par, podemos aplicar modus ponens y nuestro teorema para mostrar que$C^2$también es par. Tendríamos que derivar "$C$es incluso" por separado, por supuesto.

• En la lógica formal,

  $$P\to Q$$ es una función de verdad ; como tal, si es realmente verdadero o falso depende de la combinación particular de valores de verdad de$P$y$Q.$

• En el contexto de las matemáticas, la afirmación

  $$P \implies Q$$ (leer: "$P$implica$Q$”) solo significa que$\mathbf{P\to Q}$ es cierto , es decir, que$Q$La verdad es una consecuencia de$P$es verdad. Para ser claro:$P \implies Q$solo dice que si$P$es cierto, entonces$Q$debe ser cierto

  Tenga en cuenta que esta declaración es útil solo cuando sabemos que$P$es verdad; si sabemos que$P$es falso, o no lo sé$P$el valor de verdad de , entonces$P \implies Q$no nos ayuda a sacar ninguna conclusión.

  Muchos teoremas en Matemáticas tienen esta forma. Al aplicar tal teorema, estamos citando algunos$P \implies Q$declaración, y suponiendo/hipotéticamente (o afirmando, con base en el modelo/escenario) que$P$es cierto, entonces concluye que$Q$por lo tanto debe ser verdadero; tal forma de argumento se llama Modus Ponens .