Demostrar la reflexividad con el programa Fitch

Question

Estoy tratando de aprender a utilizar el software Fitch de Barwise y Etchemendy para desarrollar pruebas. Estoy tratando de demostrar que $R$ es reflexivo a partir de las siguientes premisas.

Si $R$ es simétrica, transitiva, y si $R$ se refiere a $x$ a algún elemento del dominio, entonces relaciona $x$ a sí mismo. Lo que he formalizado (quizás incorrectamente) como:

En la prueba anterior, he utilizado la consecuencia de primer orden (FO Con) que no me ayuda a entender la prueba en sí. Me gustaría representar la prueba en Fitch sin usar FO Con. Aquí está mi mejor esfuerzo:

Se agradecerá cualquier ayuda para completar esta prueba.

He migrado esta pregunta desde Informática Stack Exchange .

Answer 1

En primer lugar, para demostrar un universal se necesita una estructura de prueba unievrsal, es decir, establecer un $\forall$ Introducir iniciando una subprueba con $a$ como un objeto arbitrario. Por lo tanto, esta es la configuración básica que necesita:

Entonces dentro de esta subprueba puedes obtener el existencial tan importante, y hacer otra subprueba del tipo que ya tienes para eliminar este existencial, pero asegúrate de introducir un $b$ como el testigo de ese existencial:

El resto es más o menos como lo tenías.