¿Son intercambiables los axiomas y las reglas de inferencia?

Existe una equivalencia entre autómatas celulares y sistemas formales, se puede codificar uno en el otro y viceversa. Pero en los autómatas celulares (CA) las reglas de inferencia son fijas y bastante simples (por ejemplo, la regla 110 universal de dos vecinos, dos estados). Entonces, todas las reglas del sistema formal que se codifica en una regla 110 CA (también un sistema formal) deben codificarse principalmente en la entrada. Y viceversa, si tiene un sistema formal que se parece a la regla 110, puede codificar sus axiomas en reglas de inferencia en un sistema formal diferente.

¿Es esto correcto? ¿Esta intercambiabilidad entre axiomas y reglas tiene algún significado para los fundamentos de la lógica y/o las matemáticas?

Respuestas (2)

En los sistemas de prueba axiomáticos y de deducción natural, los esquemas axiomáticos y las reglas de inferencia son intercambiables, en su mayor parte. En un sistema con modus ponens y un condicional → , por ejemplo, cualquier regla de inferencia de la forma

Λ / Γ
podría ser reemplazado por el esquema del axioma
Λ → Γ
En el primer caso, si tiene Λ , entonces por la regla de inferencia, puedes inferir Γ . En el segundo caso, si tiene Λ , luego crea una instancia del esquema del axioma para producir Λ → Γ y usa modus ponens para inferir Γ . Creo que eso muestra cómo las reglas de inferencia pueden reemplazarse por esquemas de axiomas (siempre que tenga modus ponens o un equivalente).

Reemplazar esquemas de axiomas por reglas de inferencia es un poco más fácil, aunque puede parecer un truco. Si tienes el esquema del axioma

Λ
simplemente reemplácelo por una regla de inferencia sin condiciones previas
/ Λ

Este enfoque debería funcionar independientemente de las particularidades de sus esquemas axiomáticos y reglas de inferencia, ya que verificar si un paso en una derivación es una aplicación válida de una regla de inferencia basada en algún conjunto de premisas no debería ser más o menos difícil que verificar si un fórmula es una instancia de un esquema de axioma.

Hay un pequeño problema en la primera mitad. La regla de inferencia A ⊢ B solo es aplicable si uno puede derivar A , mientras que el axioma A → B debe ser cierto en todos los modelos. Así, si A no es derivable, puede ser que un modelo no satisfaga A → B a pesar de que esas oraciones verdaderas están cerradas bajo la regla de inferencia A ⊢ B . Este fenómeno ocurre en ciertos sistemas formales que surgen en la lógica matemática, aunque es lo suficientemente oscuro como para que los textos introductorios generalmente no lo mencionen.
@CarlMummert, ese es un punto muy interesante. En mi opinión, no conozco ningún sistema de este tipo, pero me interesaría mucho escuchar algunos ejemplos. ¿Es correcta mi intuición de que tales sistemas no tienen un teorema de deducción (dado que, si lo tuvieran, uno podría asumir A , derivar B , y luego, por el teorema de deducción, conclusión A → B )?
Exactamente, estos sistemas no tienen un teorema de deducción.
Mi otro comentario, que eliminé, estaba mal redactado. Dejar A ser C = 0 y B ser d = 1 en el lenguaje de la aritmética con nuevos símbolos constantes C , d . Dejar METRO ser el modelo estándar de la aritmética, con C interpretado como 0 y d interpretado como 0 . Dejar T ser el cierre de PAG A bajo las reglas usuales de inferencia. Entonces T también está cerrado bajo la regla C = 0 ⊢ d = 1 , porque PAG A no puedo probar C = 0 bajo las reglas usuales de inferencia. Por eso METRO es un modelo de T . Pero METRO no es un modelo de PAG A más el axioma adicional C = 0 → d = 1 .
(Pude seguir el primer ejemplo, pero la reescritura también está bien). Entonces, en general, dicho sistema no tendría teoremas de deducción. Parece que este sistema tampoco puede tener una prueba de solidez orientada semánticamente, ya que hay modelos en los que C = 0 / d = 1 introduce oraciones falsas. (Al menos, la solidez de esa regla no se demostrará demostrando que para cada conjunto de fórmulas Φ , Φ ⊨ C = 0 implica Φ ⊨ d = 1 .) Pero, como usted señala, dado que C = 0 no será demostrable , tampoco lo será d = 1 . ¿Se aplica aquí un tipo diferente de solidez?
En general, probar un teorema de solidez con reglas de inferencia adicionales requiere restringir el conjunto de modelos "permitidos" para incluir solo modelos donde las oraciones verdaderas están cerradas bajo las nuevas reglas de inferencia. Esto es automático para el conjunto habitual de reglas de inferencia: todos los modelos funcionan para ellas, según el teorema de completitud habitual. Pero las reglas de inferencia adicionales, como señala, pueden no ser válidas para el conjunto de todos los modelos. El ejemplo que di es un ejemplo de una nueva regla de inferencia que no es sólida, donde la forma habitual del teorema de solidez que cuantifica sobre todos los modelos sería falsa.
Las lógicas modales son un ejemplo en el que el teorema de deducción no se cumple (respondiendo a una pregunta anterior). Por ejemplo, consulte TLA+2 research.microsoft.com/en-us/um/people/lamport/tla/…

Los autómatas celulares se consideran un subconjunto de los sistemas formales, por lo tanto, lo que dice sobre los axiomas y las reglas que son relativos es correcto. De hecho, recuerdo haber leído algo sobre eso hace mucho tiempo en un libro sobre demostración automática de teoremas, pero no puedo recordar los detalles. Con respecto al significado filosófico de esto, mi opinión es que solo muestra cuántas opciones tiene al elegir un sistema formal para codificar su modelo de interés.

¿Son intercambiables los axiomas y las reglas de inferencia?
RespuestasAquíPolítica de privacidad1y, 0v