{"id":1579,"date":"2011-09-26T05:14:55","date_gmt":"2011-09-26T05:14:55","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1579"},"modified":"2011-09-26T05:14:55","modified_gmt":"2011-09-26T05:14:55","slug":"resena-implementation-of-bourbakis-elements-of-mathematics-in-coq-part-one-theory-of-sets","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-implementation-of-bourbakis-elements-of-mathematics-in-coq-part-one-theory-of-sets\/","title":{"rendered":"Rese\u00f1a: Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets"},"content":{"rendered":"

Una de las tareas del razonamiento formalizado consiste en la formalizaci\u00f3n de textos matem\u00e1ticos. Un ejemplo es el art\u00edculo Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets<\/a>.<\/p>\n

El autor del art\u00edculo es Jos\u00e9 Grimm<\/a> (del INRIA Sophia-Antipolis M\u00e9diterran\u00e9e<\/a>) y se ha publicado en el Journal of Formalized Reasoning<\/a>.<\/p>\n

El trabajo se enmarca en el proyecto GAIA<\/a> (Geometry, Algebra, Informatics and Applications), cuyos objetivos son la formalizaci\u00f3n de las demostraciones del la HDR (Habilitation \u00e0 diriger des recherches) de A. Quadrat<\/a>, de las del libro Basic Homological Algebra<\/a> (de M. Scott Osborne) y la demostraci\u00f3n de la correcci\u00f3n de la implementaci\u00f3n de estos teoremas como algoritmos en el sistema OreModules<\/a>. <\/p>\n

Dentro del proyecto GAIA, el contenido del art\u00edculo es el primer paso y, esencialmente consiste en la formalizaci\u00f3n en Coq<\/a> de teoremas del libro Elements of Mathematics: Theory of Sets<\/a> de N. Bourbaki. La formalizaci\u00f3n se basa en la realizada por Carlos Simpson<\/a> y publicada en Set-theoretical mathematics in Coq<\/a>.<\/p>\n

El resumen del art\u00edculo es el siguiente<\/p>\n

\nThis paper presents a formalization of the first book of the series “Elements of Mathematics” by Nicolas Bourbaki, using the Coq proof assistant.<\/p>\n

It discusses formalization of mathematics, and explains in which sense a computer proof of a statement corresponds to a proof in the Bourbaki sense, given that the Coq quantifiers are not defined in terms of Hilbert’s epsilon function. The list of axioms and axiom schemes of Bourbaki is compared to the more usual Zermelo-Fraenkel theory, and to those proposed by Carlos Simpson, which form the basis of the Gaia software. Some basic constructions (union, intersection, product, function, equivalence and order relation) are described, as well as some properties; this corresponds to Sections 1 to 6 of Chapter II, and the first two sections of Chapter III. A commented proof of Zermelo’s theorem is also given. The code (including almost all exercises) is available on the Web, under http:\/\/www-sop.inria.fr\/apics\/gaia.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"

Una de las tareas del razonamiento formalizado consiste en la formalizaci\u00f3n de textos matem\u00e1ticos. Un ejemplo es el art\u00edculo Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets. El autor del art\u00edculo es Jos\u00e9 Grimm (del INRIA Sophia-Antipolis M\u00e9diterran\u00e9e) y se ha publicado en el Journal of Formalized Reasoning. El trabajo…<\/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\/1579"}],"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=1579"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1579\/revisions"}],"predecessor-version":[{"id":1580,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1579\/revisions\/1580"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1579"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1579"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1579"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}