LMF2013: Misceláneas
En la clase de hoy del curso Lógica matemática y fundamentos se comentado distintas cuestiones.
En primer lugar, se ha respondido la pregunta de cómo demostrar por deducción natural la fórmula (¬q → ¬p) ∨ (q → p). Su dificulad está en el uso del principio del tercio excluso y en la demostración por casos (eliminación de la disyunción).
En segundo lugar, se ha respondido la pregunta de cómo usar lemas auxiliares en las demostraciones con Isabelle/HOL.
En tercer lugar, se ha comentado que APLI2 sólo comprueba que la formalización es correcta; pero no que el argumento sea correcto.
En cuarto lugar, se ha explicado cómo se puede demostrar automáticamente argumentos que no se puede con el método auto, pero sí con metis o meson. Como ejemplo, se ha demostrado el ejercicio 8 de la relación 6 con metis.
En quinto lugar, se ha explicado cómo se puede comprobar que los modelos calculados por QuickCheck son contramodelos. Para ello, se ha usado el ejercicio el ejercicio 13 de la relación 6.
Para resaltar la importancia del principio del tercio excluso, se ha demostrado que:
- la fórmula ∃x(P(x) → ∀yP(y)) es correcta y
- existen dos números irracionales x e y tales que xʸ es racional.
Finalmente, terminamos comentando cuestiones de filosofía de la matemática. En particular, sobre el formalismo, el intuicionismo y el constructivismo.