Decidir si es cierto que<\/p>\n
\nExiste una Universidad tal que si en dicha Universidad se celebra el D\u00eda Mundial de la L\u00f3gica (DML), entonces en todas las Universidades se celebra el DML.\n<\/p><\/blockquote>\n
En la formalizaci\u00f3n usar C(x) para representar que en la Universidad x se celebra el DML.<\/p>\n
Soluciones<\/h4>\n
\ntheory Celebracion_del_DML\nimports Main\n\nbegin\n\n(* 1\u00aa soluci\u00f3n (autom\u00e1tica) *)\nlemma \"\u2203x. (C x \u27f6 (\u2200y. C y))\"\n by simp\n\n(* 2\u00aa soluci\u00f3n (estructurada) *)\nlemma \"\u2203x. (C x \u27f6 (\u2200y. C y))\"\nproof -\n have \"\u00ac (\u2200y. C y) \u2228 (\u2200y. C y)\" ..\n then show \"\u2203x. (C x \u27f6 (\u2200y. C y))\"\n proof \n assume \"\u00ac (\u2200y. C y)\"\n then have \"\u2203y. \u00ac(C y)\" by simp\n then obtain a where \"\u00ac C a\" ..\n then have \"C a \u27f6 (\u2200y. C y)\" by simp\n then show \"\u2203x. (C x \u27f6 (\u2200y. C y))\" ..\n next\n assume \"\u2200y. C y\"\n then show \"\u2203x. (C x \u27f6 (\u2200y. C y))\" by simp\n qed\nqed\n\n(* 3\u00aa soluci\u00f3n (detallada con lemas auxiliares) *)\n\nlemma aux1:\n assumes \"\u00ac (\u2200y. C y)\"\n shows \"\u2203y. \u00ac(C y)\"\nproof (rule ccontr)\n assume \"\u2204y. \u00ac C y\"\n have \"\u2200y. C y\"\n proof \n fix a\n show \"C a\"\n proof (rule ccontr)\n assume \"\u00ac C a\"\n then have \"\u2203y. \u00ac C y\" by (rule exI)\n with \u2039\u2204y. \u00ac C y\u203a show False by (rule notE)\n qed \n qed\n with assms show False by (rule notE)\nqed\n\nlemma aux2:\n assumes \"\u00acP\"\n shows \"P \u27f6 Q\"\nproof\n assume \"P\"\n with assms show \"Q\" by (rule notE)\nqed\n\nlemma aux3:\n assumes \"\u2204x. P x\"\n shows \"\u2200x. \u00ac P x\"\nproof\n fix a\n show \"\u00ac P a\"\n proof \n assume \"P a\"\n then have \"\u2203x. P x\" by (rule exI)\n with assms show False by (rule notE)\n qed \nqed\n\nlemma aux4:\n assumes \"Q\"\n shows \"\u2203x. (P x \u27f6 Q)\"\nproof (rule ccontr)\n assume \"\u2204x. (P x \u27f6 Q)\"\n then have \"\u2200x. \u00ac (P x \u27f6 Q)\" by (rule aux3)\n then have \"\u00ac (P a \u27f6 Q)\" by (rule allE)\n moreover\n have \"P a \u27f6 Q\"\n proof\n assume \"P a\"\n show \"Q\" using assms by this\n qed\n ultimately show False by (rule notE)\nqed\n\nlemma \"\u2203x. (C x \u27f6 (\u2200y. C y))\"\nproof -\n have \"\u00ac (\u2200y. C y) \u2228 (\u2200y. C y)\" ..\n then show \"\u2203x. (C x \u27f6 (\u2200y. C y))\"\n proof \n assume \"\u00ac (\u2200y. C y)\"\n then have \"\u2203y. \u00ac(C y)\" by (rule aux1)\n then obtain a where \"\u00ac C a\" by (rule exE)\n then have \"C a \u27f6 (\u2200y. C y)\" by (rule aux2)\n then show \"\u2203x. (C x \u27f6 (\u2200y. C y))\" by (rule exI)\n next\n assume \"\u2200y. C y\"\n then show \"\u2203x. (C x \u27f6 (\u2200y. C y))\" by (rule aux4)\n qed\nqed\n\nend\n<\/pre>\nNota<\/h4>\n
\n
- Se pueden a\u00f1adir otras soluciones en los comentarios.\n
- El c\u00f3digo se debe escribir entre una l\u00ednea con <pre lang=\u00bbisar\u00bb> y otra con <\/pre>\n<\/ul>\n
Pensamiento<\/h4>\n
\nSi as\u00ed fue, as\u00ed pudo ser; si as\u00ed fuera, as\u00ed podr\u00eda ser; pero como no es, no es. Eso es l\u00f3gica. <\/p>\n
Lewis Carroll\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"
Decidir si es cierto que Existe una Universidad tal que si en dicha Universidad se celebra el D\u00eda Mundial de la L\u00f3gica (DML), entonces en todas las Universidades se celebra el DML. En la formalizaci\u00f3n usar C(x) para representar que en la Universidad x se celebra el DML. Soluciones theory Celebracion_del_DML imports Main begin (* 1\u00aa soluci\u00f3n (autom\u00e1tica) *) lemma \u00ab\u2203x. (C x \u27f6 (\u2200y. C y))\u00bb by simp (* 2\u00aa soluci\u00f3n (estructurada) *) lemma \u00ab\u2203x. (C x \u27f6 (\u2200y. C y))\u00bb proof – have \u00ab\u00ac (\u2200y. C y) \u2228 (\u2200y. C y)\u00bb .. then show \u00ab\u2203x. (C x \u27f6 (\u2200y. C y))\u00bb proof assume \u00ab\u00ac (\u2200y. C y)\u00bb then have \u00ab\u2203y. \u00ac(C y)\u00bb by simp then obtain a where \u00ab\u00ac C a\u00bb .. then…<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[103],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/96"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=96"}],"version-history":[{"count":29,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/96\/revisions"}],"predecessor-version":[{"id":192,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/96\/revisions\/192"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=96"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=96"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=96"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}