{"id":1587,"date":"2011-09-27T04:59:34","date_gmt":"2011-09-27T04:59:34","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-implementation-of-bourbakis-elements-of-mathematics-in-coq-part-two-ordered-sets-cardinals-integers\/"},"modified":"2011-09-27T05:04:46","modified_gmt":"2011-09-27T05:04:46","slug":"resena-implementation-of-bourbakis-elements-of-mathematics-in-coq-part-two-ordered-sets-cardinals-integers","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-implementation-of-bourbakis-elements-of-mathematics-in-coq-part-two-ordered-sets-cardinals-integers\/","title":{"rendered":"Rese\u00f1a: Implementation of Bourbaki&#8217;s Elements of Mathematics in Coq. Part Two: Ordered Sets, Cardinals, Integers"},"content":{"rendered":"<p>En una <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-implementation-of-bourbakis-elements-of-mathematics-in-coq-part-one-theory-of-sets\/\">entrada anterior<\/a> comentamos el proyecto de formalizaci\u00f3n del libro <a href=\"http:\/\/bit.ly\/qusJYm\">Elements of Mathematics: Theory of Sets<\/a> de N. Bourbaki en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a>.<\/p>\n<p>En dicha entrada comentamos el primer paso del proyecto consistente en la formalizaci\u00f3n de la teor\u00eda de conjuntos correspondiente al cap\u00edtulo II del libro de Bourbaki (p\u00e1ginas 65-130).<\/p>\n<p>La formalizaci\u00f3n del cap\u00edtulo III (p\u00e1ginas 131-256) constituye el contenido del segundo paso. Dicha formalizaci\u00f3n ha sido publicada por <a href=\"http:\/\/www-sop.inria.fr\/members\/Jose.Grimm\/\">Jos\u00e9 Grimm<\/a> en el art\u00edculo <a href=\"http:\/\/hal.inria.fr\/docs\/00\/54\/23\/49\/PDF\/RR-7150-v3.pdf\">Implementation of Bourbaki&#8217;s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers<\/a>. Su resumen es el siguiente   <\/p>\n<blockquote><p>\nWe believe that it is possible to put the whole work of Bourbaki into a computer. One of the objectives of the Gaia project concerns homological algebra (theory as well as algorithms); in a first step we want to implement all nine chapters of the book Algebra. But this requires a theory of sets (with axiom of choice, etc.) more powerful than what is provided by Ensembles; we have chosen the work of Carlos Simpson as basis. This reports lists and comments all definitions and theorems of the Chapter &#8220;Ordered Sets, Cardinals, Integers&#8221;. <\/p>\n<p>Version 3 is based on the Coq ssreflect library. It implements some properties on ordinal numbers. The code (including some exercises) is available on the Web, under <a href=\"http:\/\/www-sop.inria.fr\/apics\/gaia\">http:\/\/www-sop.inria.fr\/apics\/gaia<\/a>.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>En una entrada anterior comentamos el proyecto de formalizaci\u00f3n del libro Elements of Mathematics: Theory of Sets de N. Bourbaki en Coq. En dicha entrada comentamos el primer paso del proyecto consistente en la formalizaci\u00f3n de la teor\u00eda de conjuntos correspondiente al cap\u00edtulo II del libro de Bourbaki (p\u00e1ginas 65-130). La formalizaci\u00f3n del cap\u00edtulo III&#8230;<\/p>\n","protected":false},"author":2,"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,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[184,45,273,285,185],"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\/1587"}],"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=1587"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1587\/revisions"}],"predecessor-version":[{"id":1589,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1587\/revisions\/1589"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1587"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1587"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1587"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}