Diskussion:Metamath
Letzter Kommentar: vor 7 Jahren von Lambda C in Abschnitt Formulierung
Formulierung
[Quelltext bearbeiten]Der Satz "Jeder Beweis eines entsprechendes Theorems kann bis auf die Axiome und Inferenzregeln von ZFC und Prädikatenlogik zurückverfolgt werden." klingt für mich etwas seltsam. Ich hätte geschrieben "... kann bis auf die Axiome von ZFC und die Interferenzregeln der Prädikatenlogik zurückverfolgt werden". Oder ist gemeint "... kann bis auf die Axiome von ZFC und die Axiome und Interferenzregeln der Prädikatenlogik zurückverfolgt werden"? --Digamma (Diskussion) 21:26, 4. Mai 2017 (CEST)
- Ich habe das mal Deinen Vorschlag entsprechend angepasst, meine Version war da nicht ganz präzise formuliert. Letzteres war gemeint, da set.mm auch die Sätze des Prädikatenkalkül selbst enthält, für welches wiederrum auch die Axiome des (Standard) Prädikatenkalküls benötigt werden. Tatsächlich verwendet Metamath für die Mathematik zusätzlich noch das Tarski-Grothendieck Axiom (http://us.metamath.org/mpegif/mmset.html#axioms), da sonst wohl die Kategorientheorie nicht integrierbar ist (Ich meine zwar bereits was über eine Integration der Kategorientheorie in die Mathematik auf Basis von ZFC alleine gelesen zu haben, tut aber hier nichts zur Sache.). --Lambda (Diskussion) 23:20, 4. Mai 2017 (CEST)