Nuestros investigadores estrellas agotaron sus reservas de café, por su búsqueda noche y día por la solución, hasta que Matías halló la respuesta en Gitea así que hoy la compartimos contigo.
Solución:
Considere el argumento informal ‘Todo el mundo ama la pizza. Cualquiera que ame la pizza ama el helado. Así que a todo el mundo le encanta el helado ‘. ¿Por qué es eso válido?
Aproximadamente: elige a alguien, a quien quieras. Entonces, le encanta la pizza. Y por eso le encantan los helados. Pero sh / e fue elegido arbitrariamente. Así que a todo el mundo le encanta el helado.
Este argumento informal se puede explicar con laboriosa laboriosidad con comentarios explícitos como este:
Todo el mundo ama la pizza. (Eso es dado)
Cualquiera que ame la pizza ama el helado. (Eso también se da)
Toma alguna persona arbitraria, llámala Alice. Entonces Alice ama la pizza (De 1)
Si a Alice le encanta la pizza, le encantan los helados (de 2)
Alice ama el helado (de 3, 4, por modus ponens)
Pero Alice era una persona representativa arbitraria, así que lo que se aplica a ella se aplica a todos: así que a todos les encanta el helado.
Ahora considere el análogo formal de esta demostración (usando $ F $ para “ama la pizza”, etc.)
$ forall xFx quad quad quad quad $ Local
$ forall x (Fx a Gx) quad $ Local
$ Fa quad quad quad quad quad $ Desde 1., Univ. Instanciación
$ (Fa a Ga) quad quad $ Desde 2., Univ. Instanciación
$ Ga quad quad quad quad quad $ De 3, 4 por MP
$ forall xGx quad quad quad quad $ Desde 5, Univ. Generalización
(UG en $ a $ es legimitar como $ a $ no aparece en ningún supuesto del que dependa (5), por lo que se puede pensar que indica un miembro representativo arbitrario del dominio).
Tenga en cuenta que aquí necesitamos algún símbolo que desempeñe el papel de $ a $, No un true constante con una interpretación fija, no una variable limitada, sino (como dice la jerga común) una parámetro que representa, en cierto sentido, un elemento arbitrario del dominio.
Ahora, en algunas sintaxis, las variables $ x $, $ y $ etc. sólo aparecen encuadernados, como parte de oraciones cuantificadas. Y los parámetros son tipográficamente bastante distintos, $ a $ y $ b $, etc. Este es el uso en Gentzen, por ejemplo.
Pero otra tradición (probablemente más común, pero no por esa razón para ser preferida), somos tipográficamente económicos, y reciclamos las mismas letras como ambas. true variables y como parámetros. En otras palabras, permitimos que las mismas letras aparezcan como variables “vinculadas” y como variables “libres”. Entonces la prueba formal se verá así:
$ forall xFx quad quad quad quad $ Local
$ forall x (Fx a Gx) quad $ Local
$ Fx quad quad quad quad quad $ Desde 1., Univ. Instanciación
$ (Fx a Gx) quad quad $ Desde 2., Univ. Instanciación
$ Gx quad quad quad quad quad $ De 3, 4 por MP
$ forall xGx quad quad quad quad $ Desde 5, Univ. Generalización
Sin embargo, se trata de una diferencia superficial: el papel de la variable libre (no consolidada) es como parámetro. Y hemos visto, incluso en argumentos informales, que usamos expresiones como “él / ella” o incluso “Alice” como parámetros. Visto desde esa perspectiva, no debería haber ningún misterio sobre por qué también necesitamos parámetros en una lógica formal. Y en una sintaxis, las variables independientes desempeñan el papel de parámetros.
La lógica categórica implica una forma muy natural de pensar en las variables libres: son solo otro tipo de elemento.
Existe la noción de un “elemento generalizado” de un objeto $ X $ en una categoría, que es simplemente cualquier morfismo cuyo codominio es $ X $. Los elementos ordinarios de conjuntos pueden verse como elementos generalizados, identificando un elemento $ a en X $ con la función
$$ f: varnothing a X: varnothing mapsto a $$
El mapa de identidad en $ X $, interpretado como un elemento generalizado, resulta ser un excelente forma de capturar la noción de una “variable indeterminada” o un “elemento genérico”.
Cuando tenemos una colección de variables libres $ x_1, ldots, x_n $ de nuestro dominio de discurso, y hacemos una interpretación en el conjunto $ U $, las interpretamos como los elementos generalizados correspondientes a los mapas de proyección $ U ^ n a U $.
En consecuencia, podemos interpretar la relación $ R $ como un mapa particular
$$ R: U ^ 2 to text true, textofalse $$
y $ R (x, y) $ es el elemento generalizado correspondiente de $ { text true, texto{falsePS
“¿Cuál es la diferencia entre una variable gratuita y el uso de $ ∃x $ ? Quiero decir, no es $ ∃x $ lo mismo que alguna variable aleatoria? “
Entonces el problema es:
“¿Para qué son realmente útiles las variables libres?”
Creo que puede resultar útil empezar por:
“¿Para qué sirven los cuantificadores?”
Considere un ejemplo de álgebra elemental:
$ (x + y) ^ 2 = x ^ 2 + 2xy + y ^ 2 $.
Por lo general, no usamos cuantificadores para establecer esta “ley”, pero es implícitamente cuantificado universalmente; es decir, el significado “previsto” de la ley es:
por cada dos números $ x $ y $ y $, la identidad anterior se mantiene; es decir
$ para todos x para todos y [(x + y)^2 = x^2 + 2xy + y^2]PS.
Por tanto, podemos pensar que, en la práctica matemática habitual, podemos prescindir del cuantificador universal.
Pero podemos considerar un ejemplo algebraico diferente:
$ x ^ 2-2x + 1 = 0 $.
En este caso, no estamos afirmando que la ecuación sea válida para todos los valores de $ x $.
Cuando preguntamos por las soluciones (si las hay) de ecuaciones, estamos preguntando si la cuantificación existencial de la ecuación es válida, es decir, si
$ existe x (x ^ 2-2x + 1 = 0) $.
La conclusión es que las variables libres en contextos matemáticos “habituales” pueden tratarse como cuantificadas universalmente implícitamente.
En otras palabras, no es posible expresar todos los hechos “interesantes” que queremos expresar simplemente con cuantificadores universales por adelantado.
Sobre:
“$ existe x $ es lo mismo que alguna variable aleatoria “,
tenemos que el cuantificador existencial es necesario para expresar el hecho de que en un determinado “dominio del discurso” hay algunos objetos (al menos uno) que satisfacen una determinada propiedad.
Por ejemplo, tenemos eso en el dominio $ mathbb N $ de numebrs naturales, hay un objeto (un número) que satisface la identidad: $ x = 0 $. Precisamente, el número $ 0 $.
Por lo tanto, tenemos licencia para declarar lo siguiente true hecho sobre $ mathbb N $ :
$ existe x (x = 0) $.
Por supuesto, las variables ligadas se pueden reemplazar sin cambiar el significado de la fórmula; así podemos escribir: $ existe y (y = 0) $, y las dos fórmulas expresan el mismo hecho sobre $ mathbb N $.
Pero tenemos que ocuparnos de las “interacciones” entre cuantificadores; no podemos empezar desde $ existe x (x = 0) $, “instanciarlo existencialmente” (incorrectamente) para derivar, por ejemplo, $ (y = 0) $ y luego aplique UG para concluir con: $ para todo y (y = 0) $, eso es claramente false.
Este tipo de detalles se formalizan con las reglas del sistema de prueba, y diferentes “estilos” de sistema de prueba pueden diferir en los detalles, pero todos deben formalizar nuestra comprensión “intuitiva” de qué tipos de inferencia son “correctos”.
La respuesta de Peter Smith anterior ofrece una hermosa explicación del papel de las variables libres en las pruebas lógicas de primer orden.
Sección de Reseñas y Valoraciones
Nos encantaría que puedieras dar difusión a este tutorial si te valió la pena.