Set theoretical mathematics in Coq

pages

English

Documents

Écrit par
Carlos Simpson

Publié par
pefav

Lire un extrait

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

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

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

Publié par

pefav

Nombre de lectures

Langue

English

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

Voir

Publié par

pefav

Nombre de lectures

Langue

English

Set-theoreticalmathematicsinCoqCarlosSimpsoncarlos@math.unice.frCNRS,LaboratoireJ.A.DieudonneUniversitedeNice-SophiaAntipolisAbstract:Wegiveabriefdiscussionofsomeoftheissueswhichhaveariseninthecourseofformalizingsomeclassicalset-theoreticalmathematicsintheCoqsystem.Thissproutsfrom,expandsandreplacesachapterofmath.HO/0311260whichwillberemovedinrevision,andalsocontainsasatar-attachmenttothesourceﬁletherevisedandexpandedversionoftheproofdevelopmentwhichhadbeenattachedtomath.HO/0311260.IntroductionThisisanexpandedversionofoneofthechaptersof[?]whichgavesomedetailsaboutthedevelopmentwhichwasattachedtothatsourceﬁle.Thepresentpreprintalsocomeswithadevelopmentattachedtoitssourceﬁle,amodiﬁedversionoftheoneof[?]:foronething,ithasbeentranslatedtoCoqVersion8syntax(withthehelpoftheautomatedtranslationtoolsattachedtoCoqv8);theﬁleshavebeenreorganizedandrenamed;andwehaveplungedfurtherintothenotionsofwell-orderedset,gettingtothetheoremthatanysetcanbewell-ordered,ordinals,theisomorphismbetweenawell-orderedsetanditscorrespondingordinal,thedeﬁnitionofcardinalsandtheBernstein-Cantor-Schroedertheorem(whichwededuceasaneasyconsequenceofthetheoryofordinals).Allofthemathematicswhichwecoverherehasalreadybeenformalizedmanytimesoverindiﬀerentproofsystems,suchasMizar,Isabelle/ZF,andmorerecentlyMetamath,etc...AsfarasIknow,ithasn’tbeenfullydoneinCoqalthoughmanypartshavebeen.Butthatisperhapsanuninterestingdistinction.Thepresentnoteshouldbethoughtofasmoreofanexperimentinaxioms,semantics,style,notationandorganization.Asjustiﬁcationforwhytowriteitup,apartfromthefactthatyouhavetostartsomewhere,therealpointisthatitisimportanttotryavarietyofdiﬀerentpointsofviewonthesamesubject,anditisimportantthateachofusleteverybodyelseknowabouttheseattempts.Inorderfullytograspthewiderangeofproblemswhichareencounteredinformalizingmathematics,weneedtoseewhatitlookslike“fromthe1

Voir