Cómo obtener pruebas usando el editor de pruebas y el verificador

¿Cómo puedo usar el editor y verificador de prueba de deducción natural o The Logic Daemon para derivar la conclusión dada de la premisa dada?

(∃x) ( Fx ∙ (y) (Fy → y = x) )

/ (∃x) (y) (Fy ≡ y = x)

Me dice que mi premisa no está bien formada. Cualquiera que sepa cómo usar estas herramientas, su ayuda sería muy apreciada.

Respuestas (2)

Para el primer enlace, aquí hay una captura de pantalla de cómo ingresar la premisa y la conclusión:

ingrese la descripción de la imagen aquí

Tenga en cuenta que el botón FOL (Lógica de primer orden) está activado, no el botón TFL (Lógica funcional de verdad). El valor predeterminado es TFL. Eso desencadenaría una premisa que no está bien formada.

Tenga en cuenta que "(y)" se ingresa como "Ay" sin paréntesis y con y "A".

Tenga en cuenta que no hay paréntesis alrededor de "Ex".

Publique un comentario a continuación si algo no está claro.

Aquí hay una finalización de la prueba:

ingrese la descripción de la imagen aquí

Referencia

Editor y comprobador de pruebas de deducción natural JavaScript/PHP estilo Fitch de Kevin Klement http://proofs.openlogicproject.org/

También necesita probar lo contrario para la equivalencia.
@DanChristensen Sí, veo que podría ser necesario un converso aquí. Gracias por mencionarlo.

Uso de DC Proof 2.0 (otro corrector y editor de pruebas)

ingrese la descripción de la imagen aquí

¿Tienes un enlace a esto? También estoy buscando un verificador de pruebas para la lógica modal.
DC Proof 2.0 se basa en la lógica clásica, pero es posible definir sus axiomas en ella. Envíeme una lista completa de sus axiomas y veré qué puedo hacer para ayudarlo a comenzar. Para descargar DC Proof y un enlace de contacto, visite mi página de inicio.
Encontré el enlace en tu perfil y lo descargué. Aquí está el enlace para otros: dcproof.com
@FrankHubeny Aparentemente, la lógica modal es solo un subconjunto funcional de FOL. Vea la respuesta a mi pregunta en math.stackexchange.com/questions/2976552/… Entonces debería poder hacer lógica modal en DC Proof. Solo tiene que evitar o restringir el uso de las diversas reglas de inferencia en el menú Lógica.
La lógica modal tiene sus reglas de inferencia de diamante y caja, pero por lo que he visto que se usa en la Lógica simbólica de Fitch, también tienen reglas de introducción y eliminación. No he comenzado a usar su producto, pero me gustaría familiarizarme con él. Acabo de empezar a seguir tu blog.
@FrankHubeny Probablemente pueda derivar estos axiomas utilizando las representaciones FOL de los operadores de diamantes y cajas en DC Proof.
@FrankHubeny Pude hacerlo ahora. Consulte groups.google.com/forum/#!topic/sci.logic/utNfhBjgowY
Esto es muy interesante. Podría ampliar su comprobador de pruebas para incluir varias lógicas modales.
@FrankHubeny Vea las pruebas en dcproof.com/AxiomOfModalLogicDerived.htm
Estoy realizando los ejercicios en los tutoriales de DC Proof con la intención de usar esto para la lógica modal. Esta podría ser una respuesta a una pregunta que tuve anteriormente:philosofía.stackexchange.com/q/55962/ 29944
Cómo obtener pruebas usando el editor de pruebas y el verificador
RespuestasAquíPolítica de privacidad1y, 0v