5 votos

¿Por qué puede ' t reemplazamos generalmente inferencia reglas con axiomas?

Hay una gran diferencia en la insuficiencia de los axiomas y la insuficiencia de las reglas de inferencia y la prueba de procedimiento para tener una teoría completa?

Parece que, en muchos casos, la adición de una nueva regla de inferencia o de un nuevo axioma tiene el mismo efecto. Por ejemplo, considere la posibilidad de un lenguaje con 2-colocar las conectivas $\rightarrow, \land$. El lenguaje también tiene una regla de inferencia $a\rightarrow b,a \Longrightarrow b$.

Ahora podemos añadir un nuevo axioma esquemas: $a\land b \rightarrow a$ $a \land b\rightarrow b$ para cualquier fórmula $a,b$. Una alternativa es añadir una nueva reglas de inferencia: $a\land b \Longrightarrow a$$a\land b \Longrightarrow b$. En este caso lo que afirman las teorías son equivalentes, no importa el axiomatization.

En particular, creo que en segundo orden la lógica de algo que nos impide la sustitución de las reglas de inferencia con los axiomas, no importa cómo muchas de las reglas de inferencia son definidos, ya que los de segundo orden a prueba de cálculo es siempre insuficiente (por ciertas teorías). De lo contrario podríamos utilizar siempre la misma prueba de cálculo y se limita a añadir axiomas, y por lo tanto tienen un universal de la prueba procedimiento de comprobación. ¿Por qué la adición de los axiomas en lugar de las reglas de inferencia no?

3voto

DanielV Puntos 11606

Axiomas, Axioma de Esquemas y Reglas de Inferencias son 3 cosas diferentes.

Un axioma es una pieza de datos. Es una propuesta que se presentó a una lógica sin la prueba.

Una Regla de Inferencia (RoI) es un programa. Puede ser pensado como un programa para generar una nueva propuesta a partir de los actuales proposiciones (enumeración); puede ser considerado como un procedimiento de decisión para comprobar si una nueva proposición de la siguiente manera a partir de los actuales proposiciones (verificación).

Un Axioma Esquema es un retorno de la inversión que presenta una countably número infinito de proposiciones. Por lo que la descripción de un axioma esquema de $(A \land B) \to A$ presenta $(X \land X) \to X$, $(x > y \land y > z) \to (x > z)$, etc, todos a la teoría.

Algunas lógicas explícitamente tiene un retorno de la inversión denominado "Proposicional Substition". Esta es la regla de que si usted tiene una expresión proposicional demostrado, cualquier variable proposicional puede ser completamente reemplazado por un arbitrario proposicional expresión. Así, por ejemplo, si usted tiene probada $(X \to X)$, entonces se puede inferir $((A \lor B) \to (A \lor B))$. Jaśkowski hizo que esta regla explícita en su lógica.

En una lógica Proposicional Substition, Axiomas y Axioma Esquema de la misma descripción de inducir la misma teoría. De hecho, la lógica tienden a no molestarse con el Axioma Esquema. En una lógica sin Proposicional Sustitución, entonces los Axiomas y el Axioma Esquema de la misma descripción puede inducir diferentes teorías. Por ejemplo, desde el axioma $X \to X$ no se podía inferir $Y \to Y $ sin Proposicional de Sustitución.

La eliminación de todas RoI (incluso aquellos que no son Axioma Esquema) haría imposible introducir nuevos teoremas de la teoría, por lo que nunca sería capaz de demostrar nada, excepto lo que está explícitamente asumido.

En la moderna lógica, una cuestión caliente tiende a ser en realidad exactamente lo contrario: ¿cómo podemos hacer para que el usuario de una lógica puede introducir nuevas válido retorno de la inversión? Hay una gran cantidad de procedimientos de toma de decisiones para evaluar las propuestas y decidir su corrección mucho más rápido que restringirse a las composiciones de un par de codificado retorno de la inversión, y como formal de las bibliotecas más grandes, esto se convierte en un cuello de botella importante.

i-Ciencias.com

I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.

Powered by:

X