Set theoretical mathematics in Coq

Set theoretical mathematics in Coq

-

Documents
16 pages
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Set-theoretical mathematics in Coq Carlos Simpson CNRS, Laboratoire J.A. Dieudonne Universite de Nice-Sophia Antipolis Abstract: We give a brief discussion of some of the issues which have arisen in the course of formalizing some classical set-theoretical mathematics in the Coq system. This sprouts from, expands and replaces a chapter of math.HO/0311260 which will be removed in revision, and also contains as a tar-attachment to the source file the revised and expanded version of the proof development which had been attached to math.HO/0311260. Introduction This is an expanded version of one of the chapters of [?] which gave some details about the development which was attached to that source file. The present preprint also comes with a development attached to its source file, a modified version of the one of [?]: for one thing, it has been translated to Coq Version 8 syntax (with the help of the automated translation tools attached to Coq v8); the files have been reorganized and renamed; and we have plunged further into the notions of well-ordered set, getting to the theorem that any set can be well-ordered, ordinals, the isomorphism between a well-ordered set and its corresponding ordinal, the definition of cardinals and the Bernstein- Cantor-Schroeder theorem (which we deduce as an easy consequence of the theory of ordinals).

  • intros tactic

  • hilbert's ?-function

  • axiom nat

  • function definition

  • tactic becomes

  • tactics designed


Sujets

Informations

Publié par
Ajouté le 19 juin 2012
Nombre de lectures 20
Langue English
Signaler un abus
Set-theoreticalmathematicsinCoqCarlosSimpsoncarlos@math.unice.frCNRS,LaboratoireJ.A.DieudonneUniversitedeNice-SophiaAntipolisAbstract:Wegiveabriefdiscussionofsomeoftheissueswhichhaveariseninthecourseofformalizingsomeclassicalset-theoreticalmathematicsintheCoqsystem.Thissproutsfrom,expandsandreplacesachapterofmath.HO/0311260whichwillberemovedinrevision,andalsocontainsasatar-attachmenttothesourcefiletherevisedandexpandedversionoftheproofdevelopmentwhichhadbeenattachedtomath.HO/0311260.IntroductionThisisanexpandedversionofoneofthechaptersof[?]whichgavesomedetailsaboutthedevelopmentwhichwasattachedtothatsourcefile.Thepresentpreprintalsocomeswithadevelopmentattachedtoitssourcefile,amodifiedversionoftheoneof[?]:foronething,ithasbeentranslatedtoCoqVersion8syntax(withthehelpoftheautomatedtranslationtoolsattachedtoCoqv8);thefileshavebeenreorganizedandrenamed;andwehaveplungedfurtherintothenotionsofwell-orderedset,gettingtothetheoremthatanysetcanbewell-ordered,ordinals,theisomorphismbetweenawell-orderedsetanditscorrespondingordinal,thedefinitionofcardinalsandtheBernstein-Cantor-Schroedertheorem(whichwededuceasaneasyconsequenceofthetheoryofordinals).Allofthemathematicswhichwecoverherehasalreadybeenformalizedmanytimesoverindifferentproofsystems,suchasMizar,Isabelle/ZF,andmorerecentlyMetamath,etc...AsfarasIknow,ithasn’tbeenfullydoneinCoqalthoughmanypartshavebeen.Butthatisperhapsanuninterestingdistinction.Thepresentnoteshouldbethoughtofasmoreofanexperimentinaxioms,semantics,style,notationandorganization.Asjustificationforwhytowriteitup,apartfromthefactthatyouhavetostartsomewhere,therealpointisthatitisimportanttotryavarietyofdifferentpointsofviewonthesamesubject,anditisimportantthateachofusleteverybodyelseknowabouttheseattempts.Inorderfullytograspthewiderangeofproblemswhichareencounteredinformalizingmathematics,weneedtoseewhatitlookslike“fromthe1