¿Por qué generalmente no podemos reemplazar las reglas de inferencia con axiomas?

¿Hay una gran diferencia en tener axiomas insuficientes y reglas de inferencia/procedimiento de prueba insuficientes para tener una teoría completa?

Parece que en muchos casos agregar una nueva regla de inferencia o un nuevo axioma tiene el mismo efecto. Por ejemplo, considere un idioma con conectores de 2 lugares → , ∧ . El lenguaje también tiene una regla de inferencia. a → b , a ⟹ b .

Ahora podemos agregar un nuevo axioma de esquemas: a ∧ b → a y a ∧ b → b para cualquier fórmula a , b . Una alternativa es agregar una nueva regla de inferencia: a ∧ b ⟹ a y a ∧ b ⟹ b . En este caso afirmo que las teorías son equivalentes sin importar la axiomatización.

En particular, pensaría que en la lógica de segundo orden algo nos impide reemplazar las reglas de inferencia por axiomas, sin importar cuántas reglas de inferencia se definan, ya que se afirma que el cálculo de demostración de segundo orden siempre es insuficiente (para ciertas teorías). De lo contrario, siempre podríamos usar el mismo cálculo de prueba y simplemente agregar axiomas, y así tener un procedimiento de verificación de prueba universal. ¿Por qué falla la adición de axiomas en lugar de reglas de inferencia?

"Ahora podemos agregar nuevos esquemas de axiomas: a∧b→a y a∧b→b para cualquier fórmula a,b. Una alternativa es agregar nuevas reglas de inferencia: a∧b⟹a y a∧b⟹b. En este caso afirmo que las teorías son equivalentes sin importar la axiomatización". No. Si sumas los axiomas ((a∧b)⟹a) y ((a∧b)⟹b), entonces las reglas de inferencia (a∧b)⟹a y (a∧b)⟹b son derivables debido a su regla de desapego de inferencia. Pero, de la regla de separación no se sigue que si agrega las reglas de inferencia anteriores, las fórmulas anteriores son teoremas. En consecuencia, esta pregunta parece al revés. Es "¿por qué no podemos reemplazar los axiomas con reglas?"
No entiendo qué crees que tiene que ver reemplazar las reglas de inferencia con axiomas con completar la lógica de segundo orden. ¿Está proponiendo agregar un nuevo axioma para cada inferencia semánticamente válida?

Respuestas (1)

Los axiomas, los esquemas de axiomas y las reglas de inferencia son 3 cosas diferentes.

Un axioma es un dato. Es una proposición que se introduce en una lógica sin demostración.

Una Regla de Inferencia (RoI) es un programa. Puede pensarse como un programa para generar una nueva proposición a partir de proposiciones existentes (enumeración); puede pensarse como un procedimiento de decisión para verificar si una nueva proposición se sigue de proposiciones existentes (verificación).

Un esquema de axioma es un RoI que introduce un número infinito numerable de proposiciones. Entonces, la descripción de un esquema de axioma como ( A ∧ B ) → A presenta ( X ∧ X ) → X , ( X > y ∧ y > z ) → ( X > z ) , etc, todo a la teoría.

Algunas lógicas tienen explícitamente un RoI denominado "Sustitución proposicional". Esta es la regla de que si tiene una expresión proposicional probada, cualquier variable proposicional puede ser completamente reemplazada por una expresión proposicional arbitraria. Entonces, por ejemplo, si ha probado ( X → X ) , entonces puedes inferir ( ( A ∨ B ) → ( A ∨ B ) ) . Jaśkowski hizo explícita esta regla en su lógica.

En una lógica con sustitución proposicional, los axiomas y el esquema de axiomas de la misma descripción inducen la misma teoría. De hecho, tales lógicas tienden a ni siquiera molestarse con Axiom Schema. En una lógica sin sustitución proposicional, entonces los axiomas y el esquema de axiomas de la misma descripción pueden inducir diferentes teorías. Por ejemplo, del axioma X → X no podrías inferir Y → Y sin sustitución proposicional.

Eliminar todos los RoI (incluso aquellos que no son Axiom Schema) haría imposible introducir nuevos teoremas a la teoría, por lo que nunca podría probar nada excepto lo que se supone explícitamente.

En la lógica moderna, una pregunta candente tiende a ser exactamente lo contrario: ¿cómo podemos hacer que el usuario de una lógica pueda introducir un nuevo RoI válido? Hay muchos procedimientos de decisión que pueden evaluar proposiciones y decidir su corrección mucho más rápido que estar restringidos a composiciones de unos pocos RoI codificados y, a medida que las bibliotecas formales crecen, esto se convierte en un cuello de botella importante.

No entiendo completamente la pregunta (y tampoco creo que OP lo haga), pero estoy bastante seguro de que esta no es una respuesta. Por lo que puedo decir, la verdadera pregunta aquí es "¿qué significa que la lógica de segundo orden no tiene un buen sistema de prueba?".
Él está haciendo 2 preguntas diferentes, la primera mitad y la segunda mitad no están relacionadas en mi opinión. La primera mitad es lo que estoy abordando aquí.
@EricWofsey Eso significa que hay una fórmula que es cierta en todos los modelos, pero que no se puede probar. Esto significa que podemos descubrir nuevas verdades agregando reglas de inferencia. Pero, ¿por qué no conformarse con algunas reglas de inferencia y agregar axiomas según sea necesario? Luego hay un procedimiento de verificación de prueba universal ... y la lógica de segundo orden se comporta más como el primer orden donde solo la incompletitud axiomática es el problema (ya que el cálculo de prueba está completo para FO). Siento que debe haber una razón por la cual agregar axiomas (consistentes) no puede reemplazar la adición de reglas de inferencia, y pregunto por qué.
@Dole: agregar axiomas es completamente intercambiable con agregar reglas de inferencia. A nadie le importa ninguno de los enfoques porque ninguno resuelve el problema real con pruebas en lógica de segundo orden.
Un "procedimiento de verificación de prueba universal" es inútil si ni siquiera puede verificar cuáles son sus axiomas lógicos.
@EricWofsey Agregar axiomas puede ser intercambiable con agregar reglas de inferencia. Pero, eso depende del sistema, ya sea que se mantenga o no.
¿Por qué generalmente no podemos reemplazar las reglas de inferencia con axiomas?
RespuestasAquíPolítica de privacidad1y, 0v