{"id":3171,"date":"2013-04-02T16:42:57","date_gmt":"2013-04-02T16:42:57","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3171"},"modified":"2013-04-03T13:44:31","modified_gmt":"2013-04-03T13:44:31","slug":"lmf2013-miscelaneas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-miscelaneas\/","title":{"rendered":"LMF2013: Miscel\u00e1neas"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se comentado distintas cuestiones.<\/p>\n<p>En primer lugar, se ha respondido la pregunta de c\u00f3mo demostrar por deducci\u00f3n natural la f\u00f3rmula (\u00acq \u2192 \u00acp) \u2228 (q \u2192 p). Su dificulad est\u00e1 en el uso del principio del tercio excluso y en la demostraci\u00f3n por casos (eliminaci\u00f3n de la disyunci\u00f3n).<\/p>\n<p>En segundo lugar, se ha respondido la pregunta de c\u00f3mo usar lemas auxiliares en las demostraciones con Isabelle\/HOL.<\/p>\n<p>En tercer lugar, se ha comentado que APLI2 s\u00f3lo comprueba que la formalizaci\u00f3n es correcta; pero no que el argumento sea correcto.<\/p>\n<p>En cuarto lugar, se ha explicado c\u00f3mo se puede demostrar autom\u00e1ticamente argumentos que no se puede con el m\u00e9todo auto, pero s\u00ed con metis o meson. Como ejemplo, se ha demostrado el ejercicio 8 de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/LMF2013\/index.php5\/Relaci%C3%B3n_6\">relaci\u00f3n 6<\/a> con metis. <\/p>\n<p>En quinto lugar, se ha explicado c\u00f3mo se puede comprobar que los modelos calculados por QuickCheck son contramodelos. Para ello, se ha usado el ejercicio el ejercicio 13 de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/LMF2013\/index.php5\/Relaci%C3%B3n_6\">relaci\u00f3n 6<\/a>.<\/p>\n<p>Para resaltar la importancia del principio del tercio excluso, se ha demostrado que:<\/p>\n<ul>\n<li>la f\u00f3rmula \u2203x(P(x) \u2192 \u2200yP(y)) es correcta y\n<li>existen dos n\u00fameros irracionales x e y tales que x\u02b8 es racional.\n<\/ul>\n<p>Finalmente, terminamos comentando cuestiones de <a href=\"http:\/\/goo.gl\/e9SK2\">filosof\u00eda de la matem\u00e1tica<\/a>. En particular, sobre el <a href=\"http:\/\/goo.gl\/ahICb\">formalismo<\/a>, el <a href=\"http:\/\/goo.gl\/XR8cT\">intuicionismo<\/a> y el <a href=\"http:\/\/goo.gl\/gBceB\">constructivismo<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se comentado distintas cuestiones. En primer lugar, se ha respondido la pregunta de c\u00f3mo demostrar por deducci\u00f3n natural la f\u00f3rmula (\u00acq \u2192 \u00acp) \u2228 (q \u2192 p). Su dificulad est\u00e1 en el uso del principio del tercio excluso y en la demostraci\u00f3n por casos&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[153,144,202,189],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3171"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3171"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3171\/revisions"}],"predecessor-version":[{"id":3172,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3171\/revisions\/3172"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3171"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3171"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3171"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}