En lógica matemática , más específicamente en la teoría de la prueba de las teorías de primer orden , las extensiones por definiciones formalizan la introducción de nuevos símbolos mediante una definición. Por ejemplo, es común en la teoría de conjuntos ingenua introducir un símbolopara el conjunto que no tiene miembro. En el marco formal de las teorías de primer orden, esto se puede hacer agregando a la teoría una nueva constantey el nuevo axioma , lo que significa "para todo x , x no es miembro de". Entonces se puede probar que hacerlo no añade esencialmente nada a la vieja teoría, como debería esperarse de una definición. Más precisamente, la nueva teoría es una extensión conservadora de la anterior.
Definición de símbolos de relación
Dejar ser una teoría de primer orden yuna fórmula de tal que , ..., son distintas e incluyen las variables libres en. Formar una nueva teoría de primer orden de agregando un nuevo -símbolo de relación , los axiomas lógicos que presentan el símbolo y el nuevo axioma
- ,
llamado el axioma definitorio de.
Si es una fórmula de , dejar ser la fórmula de obtenido de reemplazando cualquier ocurrencia de por (cambiando las variables ligadas en si es necesario para que las variables que ocurren en el no están obligados a ). Entonces la siguiente espera:
- es demostrable en , y
- es una extensión conservadora de.
El hecho de que es una extensión conservadora de muestra que el axioma definitorio de no se puede utilizar para probar nuevos teoremas. La formulase llama una traducción de dentro . Semánticamente, la fórmula tiene el mismo significado que , pero el símbolo definido ha sido eliminado.
Definición de símbolos de función
Dejar ser una teoría de primer orden ( con igualdad ) y una fórmula de tal que , , ..., son distintas e incluyen las variables libres en . Supongamos que podemos probar
en , es decir, para todos , ..., , existe una única y tal que. Formar una nueva teoría de primer orden de agregando un nuevo -símbolo de función de orden , los axiomas lógicos que presentan el símbolo y el nuevo axioma
- ,
llamado el axioma definitorio de.
Dejar ser cualquier fórmula atómica de . Definimos fórmula de recursivamente como sigue. Si el nuevo símbolo no ocurre en , dejar ser . De lo contrario, elija una ocurrencia de en tal que no ocurre en los términos , y deja ser obtenido de reemplazando esa ocurrencia por una nueva variable . Entonces desde ocurre en una vez menos que en , la formula ya ha sido definido, y dejamos ser
(cambiando las variables ligadas en si es necesario para que las variables que ocurren en el no están obligados a ). Para una fórmula general, la formula se forma reemplazando cada aparición de una subfórmula atómica por . Entonces la siguiente espera:
- es demostrable en , y
- es una extensión conservadora de.
La formula se llama una traducción de dentro . Como en el caso de los símbolos de relación, la fórmula tiene el mismo significado que , pero el nuevo símbolo ha sido eliminado.
La construcción de este párrafo también funciona para las constantes, que pueden verse como símbolos de función 0-aria.
Extensiones por definiciones
Una teoría de primer orden obtenido de mediante introducciones sucesivas de símbolos de relación y símbolos de función, como antes, se denomina extensión por las definiciones de. Luego es una extensión conservadora de y para cualquier fórmula de podemos formar una fórmula de , llamado una traducción de dentro , tal que es demostrable en . Tal fórmula no es única, pero dos de ellos se puede resultó ser equivalente en T .
En la práctica, una extensión por definiciones de T no se distingue de la teoría original T . De hecho, las fórmulas depuede ser pensado como abreviando sus traducciones en T . La manipulación de estas abreviaturas como fórmulas reales se justifica entonces por el hecho de que las extensiones por definiciones son conservadoras.
Ejemplos de
- Tradicionalmente, la teoría de conjuntos de primer orden ZF ha (igualdad) y (pertenencia) como sus únicos símbolos de relación primitivos, y sin símbolos de función. En las matemáticas cotidianas, sin embargo, se utilizan muchos otros símbolos, como el símbolo de relación binaria., el constante , el símbolo de función unaria P (la operación de conjunto de potencia ), etc. Todos estos símbolos pertenecen de hecho a extensiones por definiciones de ZF.
- Dejar ser una teoría de primer orden para grupos en los que el único símbolo primitivo es el producto binario ×. En T , podemos probar que existe un elemento único y tal que x × y = y × x = x para cada x . Por lo tanto, podemos agregar a T una nueva constante ey el axioma
- ,
- y lo que obtenemos es una extensión por definiciones de . Entonces en podemos probar que para cada x , existe una y única tal que x × y = y × x = e . En consecuencia, la teoría de primer orden obtenido de agregando un símbolo de función unaria y el axioma
- es una extensión por definiciones de . Por lo general, se denota .
Bibliografía
- SC Kleene (1952), Introducción a las metamatemáticas , D. Van Nostrand
- E. Mendelson (1997). Introducción a la lógica matemática (4ª ed.), Chapman & Hall.
- JR Shoenfield (1967). Lógica matemática , Addison-Wesley Publishing Company (reimpreso en 2001 por AK Peters)