Pues ya puedes llorar.
Está perfecto.
Gracias!!! No lo podría haber logrado sin su ayuda
.
No te lo tomes a mal (no es nada malo), pero creo que te falta un punto de "madurez matemática" (o lógica, en este caso). Esto quiere decir que te falta un poco de práctica con demostraciones formales de este estilo. En realidad, todas siguen más o menos la misma estructura, y con suficiente práctica no te debería costar mucho hacer demostraciones formales de este nivel de dificultad, incluso debería convertirse en algo más o menos mecánico. La clave está en ser capaz de explicar con palabras la deducción, una vez tienes claro cómo va el argumento traducirlo a reglas a aplicar y demás es lo de menos.
Me cuesta estudiar por mi cuenta. No digo que las demostraciones de esta índole sean difíciles porque es como decís, se puede mecanizar el proceso (son ejemplo de ello Coq o Agda), pero mi problema es que
- No recuerdo la forma correcta quitar un existencial y un para todo.
- No recuerdo todas las distintas reglas de inferencia que me han enseñado.
- No puedo hacer ese papel "inverso" como decís vos que consiste en que si el razonamiento fuese válido, deberíamos poder ir de abajo hacia arriba (lo intenté con esta última deducción empezando de [texx]\exists x(q(x))[/texx] luego [texx]q(\text{Pablo})[/texx] y luego por adición [texx]q(\text{Pablo})\vee r(\text{Pablo})[/texx] pero de ahí ya no sé qué hacer).
- Me cuesta entender a priori si un razonamiento es válido o no (y el temor de perder mucho tiempo tratando de demostrarlo en vano).
- Cuando el razonamiento fuese inválido me cuesta proponer un contraejemplo (aunque últimamente lo he podido "digerir" mucho más así que ahora no me cuesta tanto).
Y eso que te leído decir que "Practicando te va a ir mejor", cosa que comparto a pleno, pero sinceramente es difícil aplicarlo a mí
. Para el resto de mortales sirve, pero a mí me cuesta, porque una vez que creí haber logrado entenderlo ya no necesito practicar más. Raro.
Con demostración aquí me refiero a una demostración formal. Es decir, una demostración del estilo que estás haciendo (aplicando reglas de inferencias y demás) que pruebe que de las tres premisas que tienes se sigue [texx]\neg r[/texx].
Ahh, de acuerdo. Aquí podríamos abrir el juego a cuándo además una prueba es
hiperformal, aunque creo que sería lo mismo que las pruebas de estos 2 razonamientos pero explotando cada axioma tomado (es decir probar con los mínimos conocimientos posibles).
La lógica es muy divertida, a mí también me encanta.
Sobre lo de no ver las similitudes, es cuestión de práctica como te he dicho. Tienes que pasar de fijarte en razonamientos muy concretos de unas proposiciones muy concretas a ver el bosque, es decir, a cuándo te enfrentes con la prueba de algo pensar "ah, quiero probar una conjunción, así que voy a probar cada una de las proposiciones que los componen por separado, voy a mirar qué premisas tengo y puedo usar para ello, etc". A veces también me da la sensación de que eres demasiado formalista y pierdes de vista el significado intuitivo de las cosas. Hay que entender las reglas, por qué funcionan a nivel intutivo, qué significan los conectores a nivel intuitivo, etc. Hay que aprovechar la intuición y el significado de las cosas, es una de las pocas ventajas que tenemos sobre las máquinas.
Es cierto todo lo que decís y lo que decís sobre mí. Como creo saberlo ya no me importa aprender algo nuevo, sino darle un formato homogéneo para todo, y eso me está jugando en contra. Por cierto, ¿me cobrarás la visita al consultorio?
.
En realidad no es que diseñes un lenguaje de programación para demostrar teoremas. Estos lenguajes ya tienen las reglas de la lógica incorporadas y te sirven para hacer lo mismo que hacemos aquí con las demostraciones formales, pero validadas por el programa, de manera que te aseguras de que no has cometido errores o has usado reglas de manera incorrecta.
De todas maneras, aprender algo de Coq o Agda, aunque sea interesante, no es tan fácil y lleva su tiempo.
Sí sí, no me refería a diseñar esos programas sino más bien a cómo usarlos (desde el vamos no tengo conocimientos con Linux o Mac OS así que debería empezar de cero). Me expresé mal.
¿Podrías armar un mini tutorial en este hilo o abrir uno nuevo para ver el funcionamiento o el código fuente de un programa hecho en Coq o Agda que demuestre la validez de alguno de estos 2 razonamientos, por favor? Quizás viéndolo con un caso concreto en esos entornos pueda interesarme más por esos programas y personas que estén en mi misma situación también les sirva. Gracias!
Sobre lo de recopilar axiomas y demás no tienes por qué hacerlo, ya lo han hecho muchos lógicos antes por nosotros. En cualquier libro de lógica puedes encontrar cálculos deductivos con unos pocos axiomas y unas pocas reglas que te permiten demostrar cualquier teorema válido.
¿Qué libros de lógica que traten específicamente este tópico recomendás?
Saludos
