Extensión por definición

En lógica matemática , más específicamente en la teoría de la demostración de teorías de primer orden , una extensión por definición formaliza la introducción de un nuevo símbolo mediante una definición . Por ejemplo, es común en la teoría ingenua de conjuntos introducir un símbolo${\displaystyle \emptyset }$para el conjunto que no tiene ningún miembro. En el contexto formal de las teorías de primer orden, esto se puede hacer agregando a la teoría una nueva constante.${\displaystyle \emptyset }$y el nuevo axioma${\displaystyle \forall x(x\notin \emptyset )}$, lo que significa "para todo x , x no es un miembro de${\displaystyle \emptyset }$Entonces se puede demostrar que hacerlo no añade prácticamente nada a la teoría anterior, como cabría esperar de una definición. Más precisamente, la nueva teoría es una extensión conservadora de la anterior.

Dejar${\displaystyle T}$ser una teoría de primer orden y${\displaystyle \phi (x_{1},\dots ,x_{n})}$una fórmula de${\displaystyle T}$de tal manera que${\displaystyle x_{1}}$, ...,${\displaystyle x_{n}}$son distintos e incluyen las variables libres en${\displaystyle \phi (x_{1},\dots ,x_{n})}$Formular una nueva teoría de primer orden.${\displaystyle T'}$de${\displaystyle T}$agregando un nuevo${\displaystyle n}$-ario símbolo de relación${\displaystyle R}$, los axiomas lógicos que presentan el símbolo${\displaystyle R}$y el nuevo axioma

${\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${\displaystyle \psi }$es una fórmula de${\displaystyle T'}$, dejar${\displaystyle \psi ^{\ast }}$ser la fórmula de${\displaystyle T}$obtenido de${\displaystyle \psi }$reemplazando cualquier ocurrencia de${\displaystyle R(t_{1},\dots ,t_{n})}$por${\displaystyle \phi (t_{1},\dots ,t_{n})}$(cambiando las variables de enlace en${\displaystyle \phi }$si es necesario para que las variables que aparecen en el${\displaystyle t_{i}}$no están obligados en${\displaystyle \phi (t_{1},\dots ,t_{n})}$). Entonces se cumplen las siguientes condiciones:

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

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

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

${\displaystyle \forall x_{1}\dots \forall x_{n}\exists !y\phi (y,x_{1},\dots ,x_{n})}$

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

${\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}$.

Dejar${\displaystyle \psi }$sea ​​cualquier fórmula atómica de${\displaystyle T'}$Definimos la fórmula${\displaystyle \psi ^{\ast }}$de${\displaystyle T}$recursivamente de la siguiente manera. Si el nuevo símbolo${\displaystyle f}$no ocurre en${\displaystyle \psi }$, dejar${\displaystyle \psi ^{\ast }}$ser${\displaystyle \psi }$. De lo contrario, elija una ocurrencia de${\displaystyle f(t_{1},\dots ,t_{n})}$en${\displaystyle \psi }$de tal manera que${\displaystyle f}$no ocurre en los términos${\displaystyle t_{i}}$y dejar${\displaystyle \chi }$se puede obtener de${\displaystyle \psi }$reemplazando esa ocurrencia por una nueva variable.${\displaystyle z}$. Entonces, desde entonces${\displaystyle f}$ocurre en${\displaystyle \chi }$una vez menos que en${\displaystyle \psi }$, la fórmula${\displaystyle \chi ^{\ast }}$ya ha sido definido, y dejamos${\displaystyle \psi ^{\ast }}$ser

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

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

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

La fórmula${\displaystyle \psi ^{\ast }}$se llama traducción de${\displaystyle \psi }$en${\displaystyle T}$. Como en el caso de los símbolos de relación, la fórmula${\displaystyle \psi ^{\ast }}$tiene el mismo significado que${\displaystyle \psi }$pero el nuevo símbolo${\displaystyle f}$ha sido eliminado.

La estructura de este párrafo también funciona para constantes, que pueden considerarse símbolos de funciones 0-arias.

Una teoría de primer orden${\displaystyle T'}$obtenido de${\displaystyle T}$mediante sucesivas introducciones de símbolos de relación y símbolos de función como se indicó anteriormente se denomina extensión por definiciones de${\displaystyle T}$. Entonces${\displaystyle T'}$es una extensión conservadora de${\displaystyle T}$y para cualquier fórmula${\displaystyle \psi }$de${\displaystyle T'}$Podemos formar una fórmula${\displaystyle \psi ^{\ast }}$de${\displaystyle T}$, llamada una traducción de${\displaystyle \psi }$en${\displaystyle T}$, de tal manera que${\displaystyle \psi \leftrightarrow \psi ^{\ast }}$es demostrable en${\displaystyle T'}$. Dicha fórmula no es única, pero se puede demostrar que cualesquiera dos de ellas son equivalentes en T .

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

• Tradicionalmente, la teoría de conjuntos de primer orden ZF tiene${\displaystyle =}$(igualdad) y${\displaystyle \in }$(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.${\displaystyle \subseteq }$, la constante${\displaystyle \emptyset }$, el símbolo de función unaria P (la operación de conjunto potencia ), etc. Todos estos símbolos pertenecen de hecho a extensiones por definiciones de ZF.
• Dejar${\displaystyle T}$Sea T 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 todo x . Por lo tanto, podemos agregar a T una nueva constante e y el axioma     

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

y lo que obtenemos es una extensión por definiciones${\displaystyle T'}$de${\displaystyle T}$. Luego en${\displaystyle T'}$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     ${\displaystyle T''}$obtenido de${\displaystyle T'}$agregando un símbolo de función unaria${\displaystyle f}$y el axioma

${\displaystyle \forall x(x\times f(x)=e\land f(x)\times x=e)}$

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

• Extensión conservadora
• Descripción definitiva
• Cálculo épsilon
• Extensión mediante nuevos nombres de constantes y funciones.

• SC Kleene (1952), Introducción a la metamatemática , 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).