¿Cuál es la definición de una definición?
En lógica matemática u otros sistemas formales, ¿cuál es la definición de una definición, formalmente?
Si "A" se define como "B", ¿cuál es la definición de "A" como? ¿Involucra tanto a "A" como a "B" (por ejemplo, "A: = B"), o simplemente "B"?
Por ejemplo, en la p126 en §3. Extensiones por definiciones en las interpretaciones sintácticas VIII y formas normales en la lógica matemática de Ebbinghaus , supongamos que$S$ es un conjunto de símbolos (no lógicos),
3.1 Definición. Dejar$\Phi$ ser un conjunto de $S$-frases.
(a) Suponga $P \notin S$ es un $n$-símbolo de relación y $\phi_P(v_0, ... , v_{n-1})$ un $S$-fórmula. Entonces decimos que$$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $$ es un $S$-definicion de $P$ en $\Phi$.
¿A quién llamaré como $S$-definicion de $P$ en $\Phi$:
$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $?
¿Es circular definir $P$ en términos de sí mismo?
Es un $𝑆$-definicion de $𝑃$ en $Φ$ una interpretación del símbolo $P$ como un $S'$-¿frase? (como parte de una interpretación sintáctica de$S'$ en $S'$ ¿sí mismo?)
Es la apariencia de $P$ en su propia definición $∀ 𝑣_0,....∀ 𝑣_{𝑛−1}(𝑃𝑣_0...v_{𝑛−1}↔𝜙_𝑃(𝑣_0,...,𝑣_{𝑛−1}))$, en el mismo sentido que la aparición de $A$ en $𝐴:=𝐵$?
$\phi_P(v_0, ... , v_{n-1})) $? (Supongo$P$ Se define como $\phi_P(v_0, ... , v_{n-1})) $ en $\Phi$.)
$\phi_P$? (Compare eso con el segundo:$P$ en sí mismo no involucra variables)
Consulte ¿Cómo define esta definición un símbolo?$P$ fuera del conjunto de símbolos $S$ como un $S$-¿frase?
Gracias.
Respuestas
Tenemos una firma $S$ y lo extendemos a $S':=S\cup\{P\}$.
los $S$-definicion de $P$ es el $S'$-fórmula $$\forall v_0\dots v_{n-1}: Pv_0\dots v_{n-1}\leftrightarrow \phi_P(v_0,\dots,v_{n-1})$$que puede ser tratado formalmente como un axioma adicional al dado$S$-teoría con la que estamos trabajando, produciendo así un equivalente $S'$-teoría, en la que el símbolo $P$se puede utilizar como abreviatura de la fórmula$\phi_P$.
Por ejemplo, la siguiente fórmula es la definición de la relación de orden habitual $\le$ de enteros no negativos en el idioma $(0,+)$: $$\forall x,y:\ x\le y\,\leftrightarrow\,\exists z: x+z=y$$
A continuación, primero intentaré describir el proceso de una manera más intuitiva y luego abordaré sus preocupaciones sobre la circularidad. Sospecho que el último punto puede ser más útil, así que siéntase libre de leer primero la segunda sección y, en particular, el lema destacado allí creo que será bastante útil.
(Re: tu comentario final, la definición es $(1)$- lo que le dice cómo se comporta el nuevo símbolo, en términos de los viejos símbolos que ya tiene y comprende).
La frase clave aquí es " expansión por definiciones ".
Intuitivamente, tenemos en mente el siguiente proceso:
Comenzando con una firma $S$ y un poco de set $\Phi$ de $S$-oraciones, nos molestan un poco las ineficiencias : hay algunas cosas de las que podemos hablar usando$S$-fórmulas pero solo de forma indirecta. Piense, por ejemplo, en el lenguaje de la teoría de conjuntos,$\{\in\}$: podemos expresar cosas como "$x$ es el producto cartesiano de $y$ y $z$"en este idioma, pero solo a través de fórmulas fastidiosamente largas (es un buen ejercicio para manejar el ejemplo anterior, usando, digamos, pares de Kuratowski).
Entonces, dada nuestra fórmula realmente complicada $\varphi(x_0,...,x_{n-1})$, queremos desarrollar una nueva teoría que sea básicamente la misma que $\Phi$ excepto que además tiene una "abreviatura" para $\varphi$.
Primero, esto significa que queremos ampliar nuestro lenguaje: en lugar de trabajar con $S$ queremos trabajar con $S\cup\{R\}$ para algunos $n$-símbolo de relación $R\not\in S$ que pretendemos servir como abreviatura de $\varphi$.
Ahora tenemos que definir una teoría en este lenguaje más amplio. Esta teoría debería subsumir lo que ya tenemos (es decir,$\Phi$), debe dictar correctamente el comportamiento de $R$ (es decir, digamos que es una abreviatura de $\varphi$) y no debería hacer nada más. Esto nos lleva a considerar la nueva teoría$$\Phi':=\Phi\cup\{\forall x_0,...,x_{n-1}(R(x_0,...,x_{n-1})\leftrightarrow \varphi(x_0,...,x_{n-1})\}.$$
El pasaje de $S,\Phi$y $\varphi$ a $S\cup\{R\}$ y $\Phi'$es una expansión por definiciones . Aquí tenemos una seria redundancia : en un sentido preciso,$\Phi'$ realmente no es mejor que $\Phi$. (Formalmente,$\Phi'$es una extensión conservadora de$\Phi$ en el sentido más fuerte posible: cada modelo de $\Phi$ tiene exactamente una expansión a un modelo de $\Phi'$.) Esto no es sorprendente. Nosotros ya sabíamos que podríamos expresar lo que nos importaba a través$\varphi$, solo queríamos poder hacerlo más rápidamente.
Por cierto, tenga en cuenta que esto sugiere una versión natural "máximamente eficiente" de cualquier teoría: ¡simplemente agregue nuevos símbolos para cada fórmula! Esto se llama morleyización y ocasionalmente es útil (aunque generalmente un poco tonto ).
Bien, ahora ¿qué pasa con la circularidad que le preocupa?
Primero, tenga en cuenta que "$R$"en sí mismo es solo un símbolo. La nueva oración que estamos agregando no es realmente una definición de $R$, sino más bien una definición del significado de $R$, o si prefiere una regla que rija el comportamiento de$R$.
Más en serio, ¡la circularidad nunca es un problema en FOL! La idea clave es la siguiente, que creo que es una desviación importante de las intuiciones que uno podría traer de la programación:
Un conjunto de oraciones de primer orden no crea cosas, las describe .
Específicamente, un conjunto de oraciones de primer orden $\Phi$esculpe una clase particular de estructuras, aquellas sobre las que es una descripción precisa. Por ejemplo, los conjuntos de aspecto posiblemente peligroso$$\{\forall x(P(x)\leftrightarrow P(x))\}$$ y $$\{\forall x(Q(x)\leftrightarrow \neg Q(x))\}$$están perfectamente libres de círculos; son simplemente vacías (= sostienen cada estructura) y contradictorias (= sostienen ninguna estructura) respectivamente.