¿Qué sistemas de prueba formales son capaces de probar ∀x∃yx=y∀x∃yx=y\forall x \exists yx = y sin necesidad de aplicar ∀∀\forall-I a ∃yx=y∃yx=y\exists yx = y?

Estoy interesado en algunas cuestiones filosóficas que dependen de si la fórmula abierta ∃ y X = y es una verdad lógica . Estoy asumiendo que algunos sistemas lógicos son intencionados , en el sentido de que las conclusiones de esos sistemas lógicos son aquellas que deben ser refrendadas filosóficamente. Sobre esa suposición, puedo aclarar lo que quiero decir con "verdad lógica". Una verdad lógica es una declaración para la cual hay una prueba en un sistema lógico que se pretende (en el sentido anterior). Por lo tanto, si se pretende la lógica estándar de predicados, la siguiente prueba muestra que ∃ y X = y es una verdad lógica:

  1. X = X (axioma)
  2. ∃ y X = y (1, ∃ -I)

Esta conclusión es filosóficamente problemática para mí. Puesto que pienso que todas las verdades lógicas deben ser consideradas metafísicamente necesarias , esto me compromete a la conclusión de que ◻ ∃ y X = y es una verdad necesaria, que además lleva a la conclusión de que ◻ ∀ X ◻ ∃ y X = y es una verdad lógica. Bien entendido, este es el tipo de conclusión radical que los filósofos/lógicos deberían evitar. Tiene la consecuencia, por ejemplo, de que no hay nada que haya podido dejar de ser algo.

Por lo tanto, quiero un sistema lógico en el que ∃ y X = y nunca aparece como una línea en ninguna prueba. Pero había razones por las que era necesario en la lógica de predicados estándar. El ejemplo principal está en el título de la pregunta. Por lo general, uno debe probar ∃ y X = y "en el camino" para probar ∀ X ∃ y X = y , que es inofensivo, filosóficamente hablando.

∃ y ( X = y ) como tal es una oración abierta que no tiene valor de verdad, para obtener uno X tiene que ser cuantificado. La convención estándar es suponer que las variables no cuantificadas se cuantifican universalmente, lo que las hace tan inofensivas como ∀ X ∃ y ( X = y ) . no estoy seguro de qué ∃ -Quiero decir.
No estoy seguro, pero un sistema de tipo Hilbert podría satisfacer sus requisitos, y uno que no se base en "reglas de generalización", sino que se adhiera más estrictamente a la filosofía del sistema de tipo Hilbert, es decir, tiene esquemas de axioma como ( ∀ X , ∀ y , ϕ ) → ( ∀ X , ϕ [ y := τ ] ) y ( ∀ X , ϕ → ψ ) → [ ( ∀ X , ϕ ) → ( ∀ X , ψ ) ] .
Creo que puede estar combinando problemas técnicos en lógica matemática con problemas filosóficos. Específicamente, como parte de las matemáticas, la lógica matemática es neutral con respecto a sus suposiciones metafísicas. Está haciendo distinciones filosóficas entre variables libres y ligadas que necesita aclarar en términos matemáticos.
No estoy seguro de que esto sea tanto un problema con los sistemas de prueba de primer orden como un problema (filosófico) sobre la lógica modal y lo que significa "metafísicamente necesario". Cuando escribes algo como ∀ X ◻ PAG ( X ) , ¿Qué quieres decir exactamente? Podemos leer esto como "para todo x, es necesario que PAG sostiene de X ". Ok, entonces elegimos algunas x "en este mundo". ¿Es cierto que "en todos los mundos", PAG sostiene de X ? Parece que hay dos formas de lidiar con este problema: Una forma es decidir que por cada X en un mundo, hay una forma canónica de identificar X con un objeto en cualquier mundo accesible. ...
... Entonces el problema de tu pregunta desaparece, porque es muy cierto que "no hay nada que haya podido dejar de ser algo". La otra opción es decidir que ◻ PAG ( X ) no tiene sentido, o que es falso, siempre que haya un mundo accesible que no contenga X . Pero luego tu regla de que cada vez que aceptas φ ( X ) estás comprometido con ◻ φ ( X ) está equivocado.
Sospecho que tendrá más éxito si primero determina por completo cuál quiere que sea su semántica , antes de buscar un sistema de prueba. Evidentemente, su semántica prevista no es la semántica habitual de la lógica de primer orden, sino que simplemente busca aleatoriamente un sistema de prueba donde ∃ y X = y no aparece en esta prueba probablemente no se ajuste mucho mejor a su semántica.
En qué sentido □ ∀ X □ ∃ y X = y es algo que queremos evitar? Deos "no hay nada que podría haber dejado de ser algo" significa que estás interesado en objetos "inexistentes"? Véase Alexius Meinong .
@Conifold, no me preocupa tanto si las fórmulas abiertas como esta tienen un valor de verdad. Estoy más preocupado por las formas en que se les debería permitir vincularse en la lógica modal. Tradicionalmente, la lógica modal tiene la regla de inferencia "K": φ ⊢ ◻ φ . En un sistema de prueba de este tipo, es difícil entender qué significaría decir que todas las fórmulas abiertas están implícitamente vinculadas. Eso invalidaría la siguiente prueba: PAG X ∨ ¬ PAG X ⊢ ◻ ( PAG X ∨ ¬ PAG X ) ⊢ ∀ X ◻ ( PAG X ∨ ¬ PAG X ) .
@AlexKruckman, no creo que aceptar φ ( X ) te compromete a aceptar ◻ φ ( X ) . Más bien, creo que si aceptas φ ( X ) como consecuencia de la lógica, debe aceptar ◻ φ ( X ) como consecuencia de la lógica. Siendo la idea filosófica que, cualquiera que sea la necesidad, se aplica a la lógica; la lógica no podría haber funcionado de otra manera, por lo que sus consecuencias no deberían cambiar entre mundos posibles.
Pero si ∃y(x=y) no tiene valor de verdad, no puede ser una verdad lógica, y mucho menos metafísicamente necesaria. Es solo un bloque de construcción inacabado para una propuesta. Creo que tiene en mente fórmulas de deducción natural instanciadas, donde x es un nombre para el individuo "genérico" en una subdemostración, al final de la cual la variable se cuantifica universalmente. Pero a) las fórmulas instanciadas no tienen el significado que usted objeta, yb) las subpruebas de instanciación se pueden reescribir usando fórmulas cerradas solo incluso en el cálculo de predicados estándar.
Con respecto a que este es un problema filosófico sobre lo que significa "metafísicamente necesario", acepto ese punto. Pero no quiero decir que esto sea solo una pregunta sobre el significado. Creo que realmente hay un problema filosófico profundo en juego cuando se pregunta si, por ejemplo, podría haber menos cosas de las que hay. Sobre el "sentido" pretendido por ◻ φ , La declaración ◻ ∀ X ◻ ∃ y X = y resuelve ese asunto. Si todo es necesariamente algo, entonces no puede haber menos cosas de las que hay...
Me doy cuenta de que no he dicho completamente qué ◻ φ se supone que significa, pero estoy trabajando bajo la suposición de que este problema solo se puede resolver parcialmente al tratar de determinar cuál es la semántica "correcta" y la teoría de prueba para ◻ φ debiera ser.
@EricWofsey, estoy de acuerdo en que la semántica probablemente debería ser lo primero aquí, y tengo una idea bastante buena de lo que creo que debería ser la semántica (algo así como la semántica de Kripke con dominios variables). Pero ahora está el problema de que tengo los comienzos de un sistema de prueba que no es sólido para la semántica. Ese parece ser un problema que necesita ser resuelto.
Hay algo llamado "lógica libre" que te permite hablar de cosas que no necesariamente existen. Eso podría estar en la línea de lo que está buscando. Aparte, lo que llamas "intencionado" generalmente se llama "sonido".
@DanielIV, intencionalmente evité mencionar la lógica libre, principalmente porque no sé lo suficiente al respecto. Mi esperanza era que alguien pudiera explicar cómo se hace para probar ∀ X ∃ y X = y en lógica libre. Pero creo que tienes razón, esa es la solución ordinaria a este problema. Quiero distinguir entre "sonido" e "intencionado", porque estoy más acostumbrado a que la "solidez" sea una característica de un sistema de prueba en relación con la semántica. Eso es ciertamente lo que busco, pero estoy interesado en un sistema de prueba que sea sólido para la semántica "prevista" de la lógica modal.

Respuestas (1)

¿Qué sistemas de prueba formales son capaces de probar ∀x∃yx=y sin necesidad de aplicar ∀ -I a ∃yx=y?

Prueba formal por contradicción en el sistema DC Proof :

prueba formal

La especialización existencial es básicamente la generalización universal. Quiero decir que podrías (en lógica clásica) simplemente ir más allá y eliminar ∀ totalmente reduciéndola a ¬ ∃ ¬ (lo que hiciste como un paso intermedio). Eso se desharía de ∀ introducción seguro.
@DerekElkins tengo una forma de ∀ -Intro en mi sistema. Simplemente no se requiere en esta prueba.
mi punto es que ∀ no se requiere introducción en ninguna prueba dentro de una lógica clásica. (Por supuesto, las presentaciones específicas de la lógica clásica pueden requerirlo, pero siempre puede hacer una pequeña variante para evitar eso). Podría decirse que el OP también debería tener un problema con la negación o la especialización existencial.
¿Qué sistemas de prueba formales son capaces de probar ∀x∃yx=y∀x∃yx=y\forall x \exists yx = y sin necesidad de aplicar ∀∀\forall-I a ∃yx=y∃yx=y\exists yx = y?
RespuestasAquíPolítica de privacidad1y, 0v