En primer orden la lógica es común (y casi necesario) para introducir nuevos símbolos que han sido definidas en términos de los "fundamentales" símbolos de una teoría dada. Por ejemplo, la firma de la teoría de conjuntos se define a menudo como que sólo contiene una relación binaria símbolo $\in$, pero luego rápidamente se añade la constante símbolo $\emptyset$, binario relación $\subseteq$, unarios función de $\mathcal{P}$, y así sucesivamente. Como otro ejemplo, se puede desarrollar la teoría lineal de pedidos con el orden parcial $\leq$ como el símbolo fundamental, la satisfacción de los axiomas de la reflexividad, antisymmetry, transitividad, y de la totalidad, y, a continuación, defina $x < y$ a la media de $x \leq y \wedge x \neq y$; o se puede empezar con $<$ como el símbolo fundamental, la satisfacción de los axiomas de la irreflexivity, transitividad, y tricotomía y, a continuación, defina $x \leq y$ a la media de $x < y \vee x=y$; el reclamo es que el resultado de la teorías son equivalentes.
Todos ellos parecen lo suficientemente claro, pero estoy tratando de armar un conjunto de reglas sobre cómo hacer esto en general, y no he encontrado un set en los libros que tengo en mi estantería (Srivastava del Curso de Lógica Matemática, Enderton de la Matemática Introducción a la Lógica, y Manin del Curso de Lógica Matemática para los Matemáticos). Aquí es lo que creo que funciona:
- Para definir una nueva constante símbolo $\alpha$, que se caracteriza por la fórmula $\phi(\alpha)$ tener $\alpha$ como la única variable libre, una primera prueba $\exists! x: \phi(x)$. Una fórmula $\psi(\alpha)$ es entonces interpretado $\forall v: (\phi(v) \rightarrow \psi(v))$ donde $v$ no es libre en $\psi$. Como un ejemplo, para definir el símbolo 0 en la teoría de anillos, uno de ellos utiliza la fórmula de $\phi(0)$$\forall x: (x+0=x \wedge 0+x=x)$; el teorema $\forall x: 0 \cdot x = 0$ es entonces interpretado como $$ \forall x: \forall y: [\forall x: (x+y=x \wedge y+x=x) \rightarrow y \cdot x = y]. $$
- Para definir una nueva relación $R(x_1,\dots,x_n)$ cuyas variables libres son un subconjunto de a $\{x_1, \dots, x_n\}$, que se caracteriza por la fórmula $\phi(x_1, \dots,x_n)$, se interpreta cualquier fórmula $\psi$ $R$ mediante la sustitución de cada una de las ocurrencias de $R$$\phi$. Esta es probablemente la más sencilla de las tres reglas. Por ejemplo, si se define el $x < y$ a la media de $x \leq y \wedge x \neq y$, entonces el axioma $\forall x: \forall y: (x < y \vee y < x \vee x \neq y)$ se interpreta como $$ \forall x: \forall y: [(x \leq y \wedge x \neq y) \vee (y \leq x \wedge y \neq x) \vee x=y]. $$
- Para definir una nueva función de $f(x_1,\dots,x_n)$ por la fórmula $\phi(x_1,\dots,x_n,y)$, demuestra los $\forall x_1: \dots \forall x_n: \exists! y: \phi(x_1,\dots,x_n,y)$. Para interpretar fórmulas que involucran $f$, es suficiente por recursión para interpretar fórmulas atómicas $R(t_1,\dots,t_k)$ donde $R$ es una relación y $t_1,\dots,t_k$ son términos. Supongamos que entre los términos de $t_1,\dots,t_k$ hay $m$ apariciones de el símbolo $f$, de la forma$f(a_j^{(1)},\dots,a_j^{(n)})$$j=1,\dots,m$. Deje $v_1, \dots, v_m$ variables que no se utiliza en $t_1,\dots,t_k$. Deje $t_1',\dots,t_k'$ ser los términos obtenidos mediante la sustitución de las apariciones de $f$$v_1,\dots,v_m$. Entonces la fórmula $R(t_1,\dots,t_k)$ se interpreta como $\phi(a_1^{(1)}, \dots, a_1^{(n)},v_1)\wedge \dots \wedge \phi(a_m^{(1)},\dots,a_m^{(n)},v_m) \wedge R(t_1',\dots,t_n')$. Como ejemplo, en el grupo de teoría se usa el teorema de $\forall x: \exists! y: x \cdot y = e$ a definir una única función de $^{-1}$, y el teorema $\forall x: \forall y: (x \cdot y)^{-1} = y^{-1} \cdot x^{-1}$ se interpreta como $$\forall x: \forall y: \exists u: \exists v: \exists w: [(x \cdot y) \cdot u = e \wedge y \cdot v = e \wedge x \cdot w = e \wedge u = v \cdot w ].$$
Preguntas:
- Es esto correcto?
- Es allí una manera más eficiente de hacer esto (especialmente el poco acerca de las funciones)?
