Extensión por definiciones

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 por medio de 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 ningún miembro. En el contexto formal de las teorías de primer orden, esto se puede hacer añadiendo a la teoría una nueva constante y el nuevo axioma , es decir, "para todo x , x no es un miembro de ". Entonces se puede demostrar que al hacerlo no se añade esencialmente nada a la teoría anterior, 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

Sea una teoría de primer orden y una fórmula de tales que , ..., son distintas e incluyen las variables libres en . Forme una nueva teoría de primer orden a partir de agregando un nuevo símbolo de relación -ario , 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 aparecen en no estén ligadas en ). Entonces se cumple lo siguiente: ${\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 se puede utilizar para demostrar nuevos teoremas. La fórmula se denomina 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

Sea 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 demostrar ${\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}\exists !y\phi (y,x_{1},\dots ,x_{n})}$

en , es decir, para todo , ..., , existe un único y tal que . Forme una nueva teoría de primer orden a partir de 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 de la siguiente manera. Si el nuevo símbolo no aparece en , sea . De lo contrario, elija una ocurrencia de en tal que no aparezca en los términos , y sea que se obtenga de reemplazando esa ocurrencia por una nueva variable . Entonces, dado que aparece en una vez menos que en , la fórmula ya ha sido definida, y sea ${\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 ligadas en si es necesario para que las variables que aparecen en no estén ligadas en ). Para una fórmula general , la fórmula se forma reemplazando cada ocurrencia de una subfórmula atómica por . Entonces se cumple lo siguiente: ${\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 denomina traducción de a . Como en el caso de los símbolos de relación, la fórmula tiene el mismo significado que , pero se ha eliminado el nuevo símbolo. ${\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 las anteriores se denomina extensión por definiciones de . Entonces es una extensión conservativa de , y para cualquier fórmula de podemos formar una fórmula de , denominada traducción de en , tal que es demostrable en . Dicha fórmula no es única, pero se puede demostrar que dos de ellas son equivalentes 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 definiciones de T no se distingue de la teoría original T . De hecho, las fórmulas de pueden considerarse como abreviaturas de sus traducciones a 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 ningún símbolo de función. Sin embargo, en las matemáticas cotidianas, 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 de conjuntos potencia ), 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 demostrar que existe un único elemento y tal que x × y = y × x = x para cada x . Por lo tanto, podemos añadir a T una nueva constante e y el axioma ${\displaystyle T}$

${\displaystyle \forall x(x\times e=x{\text{ and }}e\times x=x)}$,

y lo que obtenemos es una extensión por definiciones de . Entonces en podemos demostrar que para cada x , existe un único y tal que x × y = y × x = e . En consecuencia, la teoría de primer orden obtenida de agregando 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{ and }}f(x)\times x=e)}$

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

Véase también

• Extensión conservadora
• Extensión mediante nuevos nombres de constantes y funciones

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)