Prueba de lógica predicada resolver

Proporcione una prueba de lo siguiente usando FOL en forallx

Use el sistema de deducción natural y las estrategias de prueba en forallx para proporcionar una prueba formal de lo siguiente. Proporcione una imagen de su prueba.

∃xFx ∧ ∀yGy ∴ ∃x(Fx ∧ Gx)

¿Qué has probado? ¿Qué reglas crees que se deben usar?
No soy un experto en el sistema de prueba forallx , pero dentro de la deducción natural "estándar", la prueba es un ejercicio "muy sencillo" en la aplicación de reglas de cuantificadores.
No estoy seguro de si trabajar hacia adelante o hacia atrás para derivar la conclusión.
Puede comenzar con la simplificación de la Premisa.
¡Bienvenido a Filosofía SE! Gracias por tu contribución. Tómese un momento para hacer el recorrido o buscar ayuda . Puede realizar búsquedas aquí o buscar aclaraciones adicionales en el metasitio . No olvides que cuando alguien haya respondido a tu pregunta, puedes hacer clic en la flecha para recompensar al colaborador y en la marca de verificación para seleccionar la que creas que es la mejor respuesta.
Esta pregunta es sobre si comprende las reglas de eliminación del cuantificador existencial. Piénselo de esta manera: ¿cómo usaría sus reglas de prueba para seleccionar un término constante particular 'c' tal que 'F (c)'? Luego, una vez que tenga esa 'c', ¿qué más puede hacer con ella y qué podría decirle?

Respuestas (2)

No estoy seguro de si trabajar hacia adelante o hacia atrás para derivar la conclusión.

¿Por qué no los dos? Sabes con qué tienes que empezar y hacia dónde quieres ir.

Su premisa es una conjunción de un existencial y un universal. Mire las reglas de Eliminación de Conjunción, Eliminación Universal y Eliminación Existencial. Vea lo que ese comienzo le da para trabajar.

Tu conclusión es un existencial de una conjunción. Mire las Reglas de Introducción de Conjunción e Introducción Existencial. Encuentra lo que necesitas para llegar al objetivo final.

Puente juntos.

Suponga que ∃xFx ∧ ∀yGy luego demuestre ∃x(Fx ∧ Gx) con base en esta suposición.

Usa la eliminación de conjunciones para derivar ∃xFx de tu suposición. Luego instancia la variable x a una constante, digamos, a.* El resultado es Fa.

Usa la eliminación de conjunciones para derivar ∀yGy de tu suposición inicial. A partir de esto, puede instanciar la variable y en cualquier constante, digamos a.** El resultado es Ga.

Use la introducción de la conjunción para combinar Fa y Ga, el resultado es Fa ∧ Ga.

Use la generalización existencial, con la variable x reemplazando cada ocurrencia de a. El resultado es ∃x(Fx ∧ Gx).

*La constante no se puede usar ya en la prueba. Esto se debe a que ∃ se aplica a algo en el dominio, pero no sabemos exactamente qué. **Los universales se aplican a todo en el dominio, no solo a algo. Eso significa que podemos optar por instanciar y a la constante a.

Prueba de lógica predicada resolver
RespuestasAquíPolítica de privacidad1y, 0v