En una prueba o sistema de deducción, hay algunos axiomas y algunas reglas de inferencia. Para tener una pequeña prueba del sistema, son los axiomas definidos para el primitivas (por ejemplo para la negación y la implicación en la lógica proposicional). Ahora, queremos tener un sistema a prueba que demuestra todo demostrable con fórmulas incluyendo las fórmulas no contienen primitivo conectores lógicos (como O en lógica proposicional). La pregunta es si agregamos definiciones para los no-primitivas como axiomas para la prueba del sistema, o tenemos que hacer algo más? En otras palabras, ¿los lógicos aceptar las definiciones de los axiomas?
Respuestas
¿Demasiados anuncios?
Dada una teoría de la $T$, se puede ampliar con las definiciones en dos pasos. Primera ampliar el alfabeto $L(T)$ a un nuevo alfabeto $L'$ que contendrá los nuevos símbolos de constantes, funciones y relaciones que usted necesita. Luego de ampliar las $T$ sí mediante la adición de los axiomas de la siguiente forma.
Deje $\phi(x_1, \dots, x_n)$ ser una fórmula de $T$ con variables libres $x_1, \dots, x_n$ $\psi$ un nuevo símbolo de $n$-ary relación. A continuación, puede añadir un axioma $$\phi(x_1, \dots, x_n) \leftrightarrow \psi(x_1, \dots, x_n).$$ This axiom "defines the meaning of $\psi$". Del mismo modo, usted puede agregar nuevos defininig axiomas para las funciones.
La teoría de la $T'$, con el lenguaje, $L'$ que se obtiene de esta manera se conoce como una extensión de las definiciones de $T$. No es difícil probar que $T'$ es un conservador extensión de $T$; es decir, $T$ $T'$ probar las mismas fórmulas de $L$. En este sentido uno puede hacer preciso el hecho de que las definiciones no añaden nada nuevo a una teoría.
Adam Kahtava
Puntos
383
Sí, absolutamente, puede introducir las definiciones de los axiomas. Eso es lo que Metamath:
http://us.metamath.org/mpegif/mmset.html#definitions
Ver también
http://www.hss.cmu.edu/philosophy/techreports/181_Avigad.pdf
lo que define a un sistema formal con las definiciones:
Ampliamos la base de marco de dos maneras. En primer lugar, se permiten hacer explícitas las definiciones de los nuevos predicados y funciones en el universo de los conjuntos. Y, en segundo lugar, nos permiten función de símbolos para denotar funciones que sólo están parcialmente de- pago de una multa, el uso de una lógica del parcial términos. Llamamos a la resultante sistema formal DZFC .
