¿Probar la solidez de la lógica proposicional sin usar la inducción?

Question

¿Probar la solidez de la lógica proposicional sin usar la inducción?

lógica
Matemáticas
redacción de pruebas
solución-verificación
cálculo proposicional

Diez de cuatro

Quiero probar la solidez de la lógica proposicional sin usar la inducción. Creo que puedo hacerlo a través de un proceso que es básicamente una introducción universal (es decir, demostrar algo sobre un miembro arbitrario e inferir que se aplica universalmente). Como ejemplo de este enfoque, elegí una nueva regla de inferencia para probar.

Mis preguntas:

¿Es válido mi enfoque?
¿Es correcta mi prueba?
¿Es fácil de entender y seguir?
¿Necesito agregar más/menos detalles?
¿De qué otra manera puedo mejorarlo?

Prueba

queremos mostrar que $\boxed{\dfrac{\Gamma_1 ,\,\phi\vdash\psi\quad\Gamma_2,\,\lnot\phi\vdash\psi}{\Gamma_1 ,\,\Gamma_2\vdash\psi}}\def\pa {((\Gamma_1\land\phi)\longrightarrow\psi)} \def\pb {((\Gamma_2\land\lnot\phi)\longrightarrow\psi)} \def\ca {((\Gamma_1\land\Gamma_2)\longrightarrow\psi)} \def\lto {\longrightarrow} \def\val#1{V_\mathscr{I}( #1 )} \def\pli {\text{PL-interpretation, $ $\mathscr{I}$},} \def\inp{\mathscr{I}}$ es una regla de inferencia que preserva la verdad sin utilizar la inducción. Para hacerlo, convertiremos la regla en un esquema de axioma y mostraremos que es válida.

Reglas de conversión

simbolos

"," y el " $\quad$ "convertir a conjunción
" $\vdash$ " y el vinculum se convierte en implicación
$\Gamma$ , con o sin subíndice, es un conjunto finito de wffs unidos, por lo que es simplemente un wff con sus propias reglas de valoración

Valoración de $\Gamma$

$\val{\Gamma}=1$ si, para todos $\gamma\in\Gamma$ , es el caso que $\val{\gamma}=1$ y $\Gamma\neq\emptyset$

Conversión

$\Gamma_1 ,\,\phi\vdash\psi:= \pa$
$\Gamma_2,\,\lnot\phi\vdash\psi:= \pb$
$\Gamma_1 ,\,\Gamma_2\vdash\psi:= \ca$
Poniéndolo todo junto, la regla se convierte en - $\boxed{((\pa\land\pb)\lto\ca)}$

Prueba de que el esquema del axioma es válido

Supongamos por reducción que $\val {((\pa\land\pb)\lto\ca)}=0$
De (1) se sigue que $\val {\ca}=0$
De (2) se sigue que $\val{\Gamma_1}=1$ , $\val{\Gamma_2}=1$ , y $\val{\psi}=0$
De (1) se sigue que $\val{\pa}=1$
De (3) y (4) se sigue que $\val{\phi}=0$
De (5) se sigue que $\val{\lnot\phi}=1$
De (1) se sigue que $\val{\pb}=1$
De (3) y (6) se sigue que $\val{\pb}=0$ , que contradice (7) $\boxed{}$

Prueba de ejemplo

$\begin{array}{lrcll} 1.&\phi&\vdash &\phi &\text{RA}\\ 2.&\phi&\vdash &\lnot\psi\lor\phi &\text{1, $\lor$I}\\ 3.&\phi&\vdash &\psi\to\phi &\text{2, Abbrv}\\ 4.&\phi&\vdash & (\phi\to\psi)\lor(\psi\to\phi) &\text{3, $\lor$ I}\\ 5.&\lnot\phi&\vdash &\lnot\phi &\text{RA}\\ 6.&\lnot\phi&\vdash &\lnot\phi\lor\psi &\text{5, $\lor$I}\\ 7.&\lnot\phi&\vdash &\phi\to\psi &\text{6, Abbrv}\\ 8.&\lnot\phi&\vdash & (\phi\to\psi)\lor(\psi\to\phi) &\text{7, $\lor$ I}\\ 9.&\emptyset &\vdash & (\phi\to\psi)\lor(\psi\to\phi) &\text{4, 8 New Rule}\\ \end{array}$

Mauro ALLEGRANZA

... siempre que

Γ_{i}

$\Gamma_i$ son conjuntos finitos de fórmulas, de lo contrario

Γ_{i} \land ϕ

$\Gamma_i \land \phi$ no es una fórmula.

Diez de cuatro

@Mauro ALLEGRANZA, lo he mencionado explícitamente

Γ

$\Gamma$ es un conjunto finito, pero podría llamar más la atención si aclara las cosas.

Mauro ALLEGRANZA

Pero este es el punto clave: si el número de casos es finito , no necesitamos inducción. Es suficiente comprobarlos uno por uno.

Diez de cuatro

@Mauro ALLEGRANZA, si bien cada instancia de sustitución se compone de un número finito de wffs, hay un número infinito de instancias de sustitución, aunque

mohottnad

Para probar el teorema de solidez de la oración en cuestión, normalmente necesitamos usar RAA para probar la solidez de cada conectivo lógico caso por caso. Dado que cada conectivo tiene un significado diferente, ¿cuál es el principio más importante sobre el cual puede afirmar que su única regla de inferencia universal puede garantizar que cada fila de la tabla de verdad de cada conectivo actúe exactamente de acuerdo con su definición respectiva? El famoso conectivo XOR, por ejemplo, tiene una regla de eliminación muy peculiar, ¿cómo su teoría propuesta puede garantizar que no actúe como si la regla de eliminación incorrecta habitual imitara el silogismo de la disyunción?

Diez de cuatro

@mohottnad, tal como está, cada regla de inferencia que quisiera incluir en su sistema debería probarse individualmente. No es un ejemplo arbitrario de todas las reglas, es un ejemplo arbitrario de esa regla en particular . Habiendo dicho todo eso, el codificador en mí está intrigado 🤔 Creo que puedo probar algo sobre las tuplas, luego solo traduzco las reglas. Sin embargo, no veo cómo puedo evitar la etapa de traducción.

mohottnad

¿Está invocando la famosa máxima del Tao Te Ching "El Tao produjo Uno; Uno produjo Dos; Dos produjo Tres; Tres produjo Todas las cosas"? Para mí, esto suena solo a inducción matemática, que es una regla de inferencia estructural deductiva aceptada o un esquema de axioma, entonces, ¿cómo podemos evitarlo si la prueba depende de la complejidad de su formación?

Diez de cuatro

@mohottnad ese no es el caso, no. Lo que he mostrado, y lo que debería mostrarse para cada regla de inferencia de la misma manera para terminar la prueba, es que la versión del esquema de axioma de esa regla es válida. Esto nos permite inferir que todas las instancias de sustitución de ese esquema son válidas. Dicho de otra manera, estamos mostrando aproximadamente que algunos

Φ c \to Ψ c

$\Phi c \to \Psi c$ es un teorema. Los teoremas no tienen dependencias, lo que hace que c sea arbitrario, lo que nos permite aplicar UI y obtener

\forall x [Φ x \to Ψ x]

$\forall x [\Phi x \to \Psi x]$ . No estamos mostrando que si los pasos anteriores son válidos y 1 paso más es válido, entonces todos los pasos son válidos

mohottnad

El enfoque teórico del modelo de la función de asignación de valoración para probar el teorema de solidez se puede ver más claramente, ya que necesitamos verificar cada regla sintáctica de deducción natural para que cada conector conserve el orden del modelo de un retículo de álgebra booleana. Por supuesto, puede usar el esquema de axioma en lugar de la regla de inferencia como el esquema de axioma de inducción de PA con el estilo de Hilbert, pero aquí en este fondo, todavía se requiere una prueba por inducción en la altura de este enrejado. Hay una interfaz de usuario, pero no hay una regla de HI (introducción de altura), ya que la altura no es un dominio del discurso que contenga términos...

Diez de cuatro

@mohottnad Soy consciente de que existen celosías booleanas, y eso es todo 😆 Sin embargo, suena interesante, así que siéntase libre de publicar una respuesta que muestre exactamente dónde se debe usar la inducción. De vuelta al territorio con el que estoy más familiarizado... la valoración procede bajo el supuesto de que wffs juega bien y se puede sustituir 🤔 Hmm... desde la longitud de la prueba hasta la longitud de la cadena con sustitución. Me pregunto si eso coincide con el HI que mencionaste.

Respuestas (1)

¿Probar la solidez de la lógica proposicional sin usar la inducción?

... siempre que $\Gamma_i$ son conjuntos finitos de fórmulas, de lo contrario $\Gamma_i \land \phi$ no es una fórmula.
@Mauro ALLEGRANZA, lo he mencionado explícitamente $\Gamma$ es un conjunto finito, pero podría llamar más la atención si aclara las cosas.
Pero este es el punto clave: si el número de casos es finito , no necesitamos inducción. Es suficiente comprobarlos uno por uno.
@Mauro ALLEGRANZA, si bien cada instancia de sustitución se compone de un número finito de wffs, hay un número infinito de instancias de sustitución, aunque
Para probar el teorema de solidez de la oración en cuestión, normalmente necesitamos usar RAA para probar la solidez de cada conectivo lógico caso por caso. Dado que cada conectivo tiene un significado diferente, ¿cuál es el principio más importante sobre el cual puede afirmar que su única regla de inferencia universal puede garantizar que cada fila de la tabla de verdad de cada conectivo actúe exactamente de acuerdo con su definición respectiva? El famoso conectivo XOR, por ejemplo, tiene una regla de eliminación muy peculiar, ¿cómo su teoría propuesta puede garantizar que no actúe como si la regla de eliminación incorrecta habitual imitara el silogismo de la disyunción?
@mohottnad, tal como está, cada regla de inferencia que quisiera incluir en su sistema debería probarse individualmente. No es un ejemplo arbitrario de todas las reglas, es un ejemplo arbitrario de esa regla en particular . Habiendo dicho todo eso, el codificador en mí está intrigado 🤔 Creo que puedo probar algo sobre las tuplas, luego solo traduzco las reglas. Sin embargo, no veo cómo puedo evitar la etapa de traducción.
¿Está invocando la famosa máxima del Tao Te Ching "El Tao produjo Uno; Uno produjo Dos; Dos produjo Tres; Tres produjo Todas las cosas"? Para mí, esto suena solo a inducción matemática, que es una regla de inferencia estructural deductiva aceptada o un esquema de axioma, entonces, ¿cómo podemos evitarlo si la prueba depende de la complejidad de su formación?
@mohottnad ese no es el caso, no. Lo que he mostrado, y lo que debería mostrarse para cada regla de inferencia de la misma manera para terminar la prueba, es que la versión del esquema de axioma de esa regla es válida. Esto nos permite inferir que todas las instancias de sustitución de ese esquema son válidas. Dicho de otra manera, estamos mostrando aproximadamente que algunos $\Phi c \to \Psi c$ es un teorema. Los teoremas no tienen dependencias, lo que hace que c sea arbitrario, lo que nos permite aplicar UI y obtener $\forall x [\Phi x \to \Psi x]$ . No estamos mostrando que si los pasos anteriores son válidos y 1 paso más es válido, entonces todos los pasos son válidos
El enfoque teórico del modelo de la función de asignación de valoración para probar el teorema de solidez se puede ver más claramente, ya que necesitamos verificar cada regla sintáctica de deducción natural para que cada conector conserve el orden del modelo de un retículo de álgebra booleana. Por supuesto, puede usar el esquema de axioma en lugar de la regla de inferencia como el esquema de axioma de inducción de PA con el estilo de Hilbert, pero aquí en este fondo, todavía se requiere una prueba por inducción en la altura de este enrejado. Hay una interfaz de usuario, pero no hay una regla de HI (introducción de altura), ya que la altura no es un dominio del discurso que contenga términos...
@mohottnad Soy consciente de que existen celosías booleanas, y eso es todo 😆 Sin embargo, suena interesante, así que siéntase libre de publicar una respuesta que muestre exactamente dónde se debe usar la inducción. De vuelta al territorio con el que estoy más familiarizado... la valoración procede bajo el supuesto de que wffs juega bien y se puede sustituir 🤔 Hmm... desde la longitud de la prueba hasta la longitud de la cadena con sustitución. Me pregunto si eso coincide con el HI que mencionaste.

mohottnad · Answer 1

Es más fácil usar el modelo de celosía del álgebra de Heyting para comprender la prueba de inducción habitual sobre la altura de las derivaciones de solidez tanto en la lógica intuicionista como en la clásica. Y toda álgebra booleana es un álgebra de Heyting que también es distributiva.

En matemáticas, un álgebra de Heyting (también conocida como álgebra pseudo-booleana) es un retículo acotado (con operaciones de unión y encuentro escritas ∨ y ∧ y con el elemento mínimo 0 y el elemento máximo 1) equipado con una operación binaria a → b de implicación tal que (c ∧ a) ≤ b es equivalente a c ≤ (a → b).

En el enlace hay un diagrama de celosía, cada regla de deducción natural de cada conectivo se puede verificar para preservar el orden de dicha celosía de acuerdo con las definiciones de formación de celosía. Pero aún necesita escalar la red para obtener una derivación arbitraria con pasos finitos. Pero esta altura en la red no corresponde a las entidades o términos del dominio del discurso de tal estructura, por lo que no se puede invocar la "introducción universal" como regla de inferencia de deducción natural. Volviendo al territorio con su función de valoración, esta complejidad de altura corresponde al paso individual de su prueba que no es una entidad de su dominio de discurso (por lo tanto, no hay una introducción universal aplicable aquí), por lo que la inducción parece necesaria aquí.

Gracias por eso, jugaré 😊 La regla de inferencia que elegí es bastante útil para probar teoremas. Algo es un teorema si contiene alguna wff separada de su negación. Como tal teorema se puede construir tanto a partir de su wff como de su negación a través de la introducción de la disyunción. Darnos cuenta de eso nos permite evitar molestias, como múltiples aplicaciones de RAA, y hace que la prueba sea más corta y legible. Aunque sería muy difícil de manejar, creo que en realidad puede probar todos los teoremas en PL
Estoy entendiendo esto un poco. Sin embargo, ¿no hay pasos en mi sistema de prueba traducido? Todo lo que hay es esquema axiomático y sustitución, que, dicho sea de paso, toda prueba estándar de solidez da por sentado. Para un estilo hilbert estándar, el caso base muestra que el esquema de axioma es válido, exactamente como lo he hecho, y el paso inductivo, que se basa en la sustitución para mostrar todas las instancias en las que se puede aplicar MP, es válido: hemos terminado con el esquema del axioma. Una prueba en mi sistema es básicamente una composición de funciones poco común. Es la interfaz de usuario en wffs que se puede sustituir
@TenO'Four gracias por la elaboración de su esquema de sustitución. Ciertamente puede llamar a su versión como una especie de "recursión" o "inducción" en wffs que se pueden sustituir. En la lógica, la interfaz de usuario se extiende estrictamente sobre variables de dominio, no wffs. Lo siento, todavía no entiendo completamente su regla estructural especial de cálculo secuente (su disyunción negada favorita, ¿tiene algún nombre?), y mucho menos convertida en esquema de axioma, pero me parece que tiene sentido. Imagine que un robot asistente de prueba hace su trabajo para demostrar la solidez de una fórmula arbitraria, creo que todavía se necesita la recursividad en el sistema de Hilbert.
Sin embargo, ¿las metavariables toman wffs como entrada? De cualquier manera, creo que la sustitución debe probarse, y bien podría ser que haya movido las cosas de "longitud de la prueba" a "longitud de la cadena". La idea general de esto es un esquema al que puedo traducir idiomas, probar mecánicamente la solidez allí y luego, en virtud de la equivalencia, haber probado la solidez en el idioma original. Lo que has compartido ha sido muy útil, gracias 😊 Lo he editado en una prueba de ejemplo usando la regla. No tiene nombre, pero creo que "verificador de teoremas" resume lo que hace.

¿Probar la solidez de la lógica proposicional sin usar la inducción?

Diez de cuatro

Mis preguntas:

Prueba

Reglas de conversión

simbolos

Valoración de $\Gamma$

Conversión

Prueba de que el esquema del axioma es válido

Prueba de ejemplo

Mauro ALLEGRANZA

Diez de cuatro

Mauro ALLEGRANZA

Diez de cuatro

mohottnad

Diez de cuatro

mohottnad

Diez de cuatro

mohottnad

Diez de cuatro

Respuestas (1)

mohottnad

Diez de cuatro

Diez de cuatro

mohottnad

Diez de cuatro

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

Si P entonces Q es verdadero y también lo es P. Entonces Q no es necesariamente verdadero, ¿verdad?

¿Es la manipulación de una igualdad trivial una prueba lógicamente válida de una fórmula?

Pruebas usando tautologías

¿Cómo puedo hacer que las pruebas con fórmulas largas sean más legibles sin sacrificar la claridad?

Al reemplazar las variables de la proposición por su negación y cambiar los valores de verdad de todas las prop. variables, mostrar v(ϕ)=v∗(ϕ∗)v(ϕ)=v∗(ϕ∗)v(\phi)=v^(\phi^)

¿Toda prueba por contradicción puede también demostrarse sin contradicción?

¿Se puede usar esta proposición para probar un enunciado iff?

¿Es verdadera la siguiente generalización de la desigualdad de Cauchy-Schwarz?

Algunas pruebas de teoría de conjuntos

¿Probar la solidez de la lógica proposicional sin usar la inducción?

Diez de cuatro

Mis preguntas:

Prueba

Reglas de conversión

simbolos

Valoración deΓ Γ \Gamma

Conversión

Prueba de que el esquema del axioma es válido

Prueba de ejemplo

Mauro ALLEGRANZA

Diez de cuatro

Mauro ALLEGRANZA

Diez de cuatro

mohottnad

Diez de cuatro

mohottnad

Diez de cuatro

mohottnad

Diez de cuatro

Respuestas (1)

mohottnad

Diez de cuatro

Diez de cuatro

mohottnad

Diez de cuatro

Valoración de $\Gamma$