Extensión por definiciones - Extension by definitions

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ímbolo para 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 constante y el nuevo axioma , que significa "para todo x , x no es miembro de ". Entonces se puede demostrar que hacerlo no agrega 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. ${\ Displaystyle \ emptyset}$${\ Displaystyle \ emptyset}$ ${\ Displaystyle \ forall x (x \ notin \ emptyset)}$${\ Displaystyle \ emptyset}$

Definición de símbolos de relación

Vamos a ser una teoría de primer orden y una fórmula de tal manera que , ..., son distintos e incluyen las variables liberan en . Formar una nueva teoría de primer orden a partir de la adición de un nuevo símbolo de relación -ariana , los axiomas lógicos que presentan el símbolo y el nuevo axioma ${\ Displaystyle T}$${\ Displaystyle \ phi (x_ {1}, \ dots, x_ {n})}$${\ Displaystyle T}$${\ Displaystyle x_ {1}}$${\ Displaystyle x_ {n}}$${\ Displaystyle \ phi (x_ {1}, \ dots, x_ {n})}$${\ Displaystyle T '}$${\ Displaystyle T}$${\ Displaystyle n}$${\ Displaystyle R}$${\ Displaystyle R}$

${\ Displaystyle \ forall x_ {1} \ dots \ forall x_ {n} (R (x_ {1}, \ dots, x_ {n}) \ leftrightarrow \ phi (x_ {1}, \ dots, x_ {n} ))}$,

llamado el axioma definitorio de . ${\ Displaystyle R}$

Si es una fórmula de , sea ​​la fórmula de obtenida 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 ligadas ). Entonces la siguiente espera: ${\ Displaystyle \ psi}$${\ Displaystyle T '}$${\ Displaystyle \ psi ^ {\ ast}}$${\ Displaystyle T}$${\ Displaystyle \ psi}$${\ Displaystyle R (t_ {1}, \ dots, t_ {n})}$${\ Displaystyle \ phi (t_ {1}, \ dots, t_ {n})}$${\ Displaystyle \ phi}$${\ Displaystyle t_ {i}}$${\ Displaystyle \ phi (t_ {1}, \ dots, t_ {n})}$

1. ${\ Displaystyle \ psi \ leftrightarrow \ psi ^ {\ ast}}$es demostrable en , y${\ Displaystyle T '}$
2. ${\ Displaystyle T '}$es una extensión conservadora de .${\ Displaystyle T}$

El hecho de que sea ​​una extensión conservadora de muestra que el axioma definitorio de no puede usarse para probar nuevos teoremas. La fórmula se llama traducción de en . Semánticamente, la fórmula tiene el mismo significado que , pero se ha eliminado el símbolo definido . ${\ Displaystyle T '}$${\ Displaystyle T}$${\ Displaystyle R}$${\ Displaystyle \ psi ^ {\ ast}}$${\ Displaystyle \ psi}$${\ Displaystyle T}$${\ Displaystyle \ psi ^ {\ ast}}$${\ Displaystyle \ psi}$${\ Displaystyle R}$

Definición de símbolos de función

Vamos a ser una teoría de primer orden ( con igualdad ) y una fórmula de tal manera que , , ..., son distintos e incluyen las variables libres en . Supongamos que podemos probar ${\ Displaystyle T}$${\ Displaystyle \ phi (y, x_ {1}, \ dots, x_ {n})}$${\ Displaystyle T}$${\ Displaystyle y}$${\ Displaystyle x_ {1}}$${\ Displaystyle x_ {n}}$${\ Displaystyle \ phi (y, x_ {1}, \ dots, x_ {n})}$

${\ Displaystyle \ forall x_ {1} \ dots \ forall x_ {n} \ existe! y \ phi (y, x_ {1}, \ dots, x_ {n})}$

en , es decir, para todos , ..., existe un único y tal que . Formar una nueva teoría de primer orden agregando un nuevo símbolo de función -aria , los axiomas lógicos que presentan el símbolo y el nuevo axioma ${\ Displaystyle T}$${\ Displaystyle x_ {1}}$${\ Displaystyle x_ {n}}$${\ Displaystyle \ phi (y, x_ {1}, \ dots, x_ {n})}$${\ Displaystyle T '}$${\ Displaystyle T}$${\ Displaystyle n}$${\ Displaystyle f}$${\ Displaystyle f}$

${\ Displaystyle \ forall x_ {1} \ dots \ forall x_ {n} \ phi (f (x_ {1}, \ dots, x_ {n}), x_ {1}, \ dots, x_ {n})}$,

llamado el axioma definitorio de . ${\ Displaystyle f}$

Sea cualquier fórmula atómica de . Definimos la fórmula de recursivamente como sigue. Si el nuevo símbolo no aparece , déjelo estar . De lo contrario, elija una ocurrencia de de tal manera que no se da en los términos , y dejar ser obtenidos a partir de la sustitución de dicha aparición de una nueva variable . Entonces como ocurre en un tiempo menos que en , la fórmula ya está definida, y dejamos ser ${\ Displaystyle \ psi}$${\ Displaystyle T '}$${\ Displaystyle \ psi ^ {\ ast}}$${\ Displaystyle T}$${\ Displaystyle f}$${\ Displaystyle \ psi}$${\ Displaystyle \ psi ^ {\ ast}}$${\ Displaystyle \ psi}$${\ Displaystyle f (t_ {1}, \ dots, t_ {n})}$${\ Displaystyle \ psi}$${\ Displaystyle f}$${\ Displaystyle t_ {i}}$${\ Displaystyle \ chi}$${\ Displaystyle \ psi}$${\ Displaystyle z}$${\ Displaystyle f}$${\ Displaystyle \ chi}$${\ Displaystyle \ psi}$${\ Displaystyle \ chi ^ {\ ast}}$${\ Displaystyle \ psi ^ {\ ast}}$

${\ Displaystyle \ forall z (\ phi (z, t_ {1}, \ dots, t_ {n}) \ rightarrow \ chi ^ {\ ast})}$

(cambiando las variables vinculadas si es necesario para que las variables que ocurren en el no estén vinculadas ). Para una fórmula general , la fórmula se forma reemplazando cada aparición de una subfórmula atómica por . Entonces la siguiente espera: ${\ Displaystyle \ phi}$${\ Displaystyle t_ {i}}$${\ Displaystyle \ phi (z, t_ {1}, \ dots, t_ {n})}$${\ Displaystyle \ psi}$${\ Displaystyle \ psi ^ {\ ast}}$${\ Displaystyle \ chi}$${\ Displaystyle \ chi ^ {\ ast}}$

1. ${\ Displaystyle \ psi \ leftrightarrow \ psi ^ {\ ast}}$es demostrable en , y${\ Displaystyle T '}$
2. ${\ Displaystyle T '}$es una extensión conservadora de .${\ Displaystyle T}$

La fórmula se llama traducción de en . 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. ${\ Displaystyle \ psi ^ {\ ast}}$${\ Displaystyle \ psi}$${\ Displaystyle T}$${\ Displaystyle \ psi ^ {\ ast}}$${\ Displaystyle \ psi}$${\ Displaystyle f}$

La construcción de este párrafo también funciona para constantes, que pueden verse como símbolos de función 0-aria.

Extensiones por definiciones

Una teoría de primer orden obtenida a partir de introducciones sucesivas de símbolos de relación y símbolos de función como anteriormente se denomina extensión por definiciones de . Entonces es una extensión conservadora de , y para cualquier fórmula de podemos formar una fórmula de , llamada traducción de en , tal que se pueda demostrar en . Tal fórmula no es única, pero dos de ellos se puede resultó ser equivalente en T . ${\ Displaystyle T '}$${\ Displaystyle T}$${\ Displaystyle T}$${\ Displaystyle T '}$${\ Displaystyle T}$${\ Displaystyle \ psi}$${\ Displaystyle T '}$${\ Displaystyle \ psi ^ {\ ast}}$${\ Displaystyle T}$${\ Displaystyle \ psi}$${\ Displaystyle T}$${\ Displaystyle \ psi \ leftrightarrow \ psi ^ {\ ast}}$${\ Displaystyle T '}$

En la práctica, una extensión por las definiciones de T no se distingue de la teoría original T . De hecho, las fórmulas de pueden ser considerados 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. ${\ Displaystyle T '}$${\ Displaystyle T '}$

Ejemplos

• Tradicionalmente, la teoría de conjuntos de primer orden ZF tiene (igualdad) y (pertenencia) como sus únicos símbolos de relación primitivos, y no tiene 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 , la constante , el símbolo de función unaria P (la operación del conjunto de potencias ), etc. Todos estos símbolos pertenecen de hecho a extensiones por definiciones de ZF.${\ displaystyle =}$${\ Displaystyle \ in}$${\ Displaystyle \ subseteq}$${\ Displaystyle \ emptyset}$
• Sea 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${\ Displaystyle T}$

${\ Displaystyle \ forall x (x \ times e = x {\ text {y}} e \ times x = x)}$,

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 obtenida al agregar un símbolo de función unaria y el axioma ${\ Displaystyle T '}$${\ Displaystyle T}$${\ Displaystyle T '}$${\ Displaystyle T ''}$${\ Displaystyle T '}$${\ Displaystyle f}$

${\ Displaystyle \ forall x (x \ times f (x) = e {\ text {y}} f (x) \ times x = e)}$

es una extensión por definiciones de . Por lo general, se denota .${\ Displaystyle T}$${\ Displaystyle f (x)}$${\ Displaystyle x ^ {- 1}}$

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)