Extensión por definiciones

En lógica matemática , más concretamente en la teoría de prueba de 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 ingenua de conjuntos introducir un símbolo para el conjunto que no tiene miembros. 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 añade esencialmente nada a la antigua teoría, como debería esperarse de una definición. Más precisamente, la nueva teoría es una extensión conservadora de la antigua. ${\displaystyle \emptyset }$ ${\displaystyle \emptyset }$ ${\displaystyle \forall x(x\notin \emptyset )}$ ${\displaystyle \emptyset }$

Definición de símbolos de relación

Sean una teoría de primer orden y una fórmula de tal que , ..., sean distintas e incluyan las variables libres en . Forme una nueva teoría de primer orden agregando un nuevo símbolo de relación aria , 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 reemplazando cualquier aparición de por (cambiando las variables vinculadas si es necesario para que las variables que aparecen en no estén vinculadas ). Entonces se mantiene 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 probar nuevos teoremas. La fórmula se llama traducción de a . 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.

Sean una teoría de primer orden ( con igualdad ) y una fórmula de tal que , , ..., sean distintas e incluyan 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 todos , ..., , existe una y única tal que . Forme 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 de la siguiente manera. Si el nuevo símbolo no aparece en , sea . De lo contrario, elija una ocurrencia de in tal que no ocurra en los términos y let se obtenga reemplazando esa ocurrencia por una nueva variable . Entonces como ocurre en un tiempo menos que en , la fórmula ya está definida y dejamos que ${\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 aparecen en 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 se mantiene 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 llama 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 funciones 0-arias.

Extensiones por definiciones

Una teoría de primer orden obtenida mediante introducciones sucesivas de símbolos de relación y símbolos de función como se indicó anteriormente se denomina extensión según las definiciones de . Entonces es una extensión conservativa de , y para cualquier fórmula de podemos formar una fórmula de , llamada traducción de en , tal que sea demostrable en . Tal 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, se puede considerar que las fórmulas de abrevian sus traducciones a T . La manipulación de estas abreviaturas como fórmulas reales se justifica entonces por el hecho de que las extensiones mediante 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 del conjunto de potencias ), etc. Todos estos símbolos pertenecen de hecho a extensiones según las 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 elemento único y tal que x × y = y × x = x para cada x . Por lo tanto podemos agregar 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 podemos demostrar 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{ and }}f(x)\times x=e)}$

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

Ver también

• Extensión conservadora
• Extensión por 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.
• J.R. Shoenfield (1967). Lógica matemática , Addison-Wesley Publishing Company (reimpreso en 2001 por AK Peters)