IIRC, im Univalent-Foundations-Programm (per Voevodsky), wird die Kategorientheorie als eine mögliche Art der Evolution oder neuen Welle der Typentheorie dargestellt. Vielleicht ist mein Gedächtnis ausgeschaltet, aber wie auch immer, in nlab sagen sie:
Die Typentheorie und bestimmte Arten der Kategorientheorie sind eng miteinander verwandt. Aufgrund einer Syntax-Semantik-Dualität kann man die Typentheorie als eine formale syntaktische Sprache oder einen Kalkül für die Kategorientheorie betrachten, und umgekehrt kann man sich die Kategorientheorie als Bereitstellung von Semantik für die Typentheorie vorstellen. Die Art der verwendeten Kategorientheorie hängt von der Art der Typentheorie ab; dies erstreckt sich auch auf die Homotopietypentheorie und bestimmte Arten von (∞,1)-Kategorietheorie.
Auch die Namenswahl für die Kategorientheorie, wieder IIRC, bezog sich auf den aristotelischen/kantischen Kategoriengebrauch. Angenommen, Mengen sind Repräsentanten der Erweiterung, während Typen Repräsentanten der Intension sind . (Entschuldigung, ich konnte kein spezifischeres Zitat finden.) In Kantischen Begriffen wären die Kategorien, die auf der Seite der diskursiven Erkenntnis stehen, daher intensionale Funktionen. Dass sie typomorph (?) sein würden, scheint leicht zu folgen, zumindest gemäß der Annahme, die ich gerade früher in diesem Absatz gemacht habe.
Abgesehen davon gibt es für mich aus irgendeinem Grund etwas intuitives, was die Kategorientheorie von der Typentheorie unterscheidet. AFAIK, die Typentheorie wurde als alternative Grundlagen der Mathematik erprobt, fiel aber der Mengenlehre zum Opfer. Dagegen ist die Kategorientheorie ein bis dato durchaus gelungenes Bild einer alternativen Grundlegung der Mathematik.†
Liegt das daran, dass Kategorien keine Typen sind? Was ich dachte, war: Ein Begriff bezieht sich auf eine Menge, wenn die Referenz Elemente enthält; ein Begriff bezieht sich auf einen Typ, wenn die Referenz Tokens hat (ich weiß, dass die Tokenhood-Beziehung nicht in der eigentlichen Typentheorie auftaucht, wie es in diesem anderen Verständnis von Typologie der Fall ist); Wenn die Referenz eines Begriffs jedoch Elemente und Token enthält, bezieht sich dieser Begriff auf eine Kategorie. Was also der Typentheorie fehlt, nämlich eine fundierte Extensionalitätstheorie, wird durch diese kategorientheoretische Dualität wettgemacht. Dann kann die Kategorientheorie die scheinbar mathematischen Qualitäten der Typentheorie neben der mengentheoretischen Semiose in die Musik ihrer Notation einbringen und würde daher die schlichte Mengentheorie als Grundlage der Mathematik leicht ersetzen.
Mein einziger Einwand an dieser Stelle wäre zu sagen: typologische Funktionen verweisen letztlich mehr auf die logische Sphäre††; der eindeutig mathematische Inhalt einer Kategorie wird von den Tatsachen der Elementarheit getragen, in denen die Kategorie vorkommt. In diesem Sinne ist die Tragfähigkeit der Kategorientheorie als hinreichend begründete alternative Grundlage der Mathematik nur eine Illusion. Ehrlich gesagt glaube ich tatsächlich, dass dieser Einwand wahr ist.
† Dies ist vielleicht ironisch, wenn man bedenkt, dass die kantische Verwendung von Kategorien dieses ganz neue (?) Genre der Mathematik ursprünglich motivierte: Nach Kant brauchen wir schließlich reine Extensionsobjekte (Raum und Zeit), um unsere Mathematik angemessen zu begründen; der bloße Begriff der Extensionalität würde nicht ausreichen (mit anderen Worten, die Intensionalität des Begriffs Extension ist keine ausreichende Grundlage für eine vertretbare Mathematik).
†† Die logische Elastizität der Typologie ist also ein Analogon oder eine Ergänzung des logischen Pluralismus.
Wie verstehen Philosophen der Mathematik die Unterschiede zwischen Mengen-, Typen- und Kategorientheorie?
Es hört sich an, als hätten Sie Mühe, die Beziehung zwischen drei grundlegenden Theorien zu verstehen. Die naive Mengenlehre ist die Theorie, die Gottlob Frege historisch verwendet hat , um zu zeigen, dass sich alle Mathematik auf Logik reduziert. Die Typentheorie wurde von Bertrand Russell und anderen vorgeschlagen und entwickelt, um die Mengentheorie einzuschränken, um Russells Paradoxon zu vermeiden, und die dann durch ZF und ZFC ersetzt wurde, aber immer noch bei Computersprachendesignern beliebt ist. Und die Kategorientheorie wurde als Alternative zur ZFC als grundlegende Theorie angeboten, die bei der Analyse der funktionalen Aspekte mathematischer Strukturen mächtig ist und als Abstraktion der Mengenlehre angesehen werden könnte. Alle drei Theorien beziehen sich auf das, was Wikipedia die Curry-Howard-Lambek-Korrespondenz nenntwas vorgibt zu zeigen, inwiefern Beweise, Programme und Kategorientheorie eine Art Isomorphismus sind, und was auf eine tiefere Verbindung zwischen den dreien hindeutet.
Es gibt viele mathematische Theorien, aber die Mengentheorie (ST), die Typentheorie (TT) und die Kategorientheorie (CT) sind wichtig, weil sie grundlegende Fragen aufwerfen und als grundlegende Theorien gelten. Die naive Mengenlehre kann zum Beispiel verwendet werden, um Zahlen und Arithmetik zu definieren. Ein berühmtes Beispiel ist die von Neumann Ordinalzahl . Von Georg Cantor und der Verwendung der Mengenlehre wurde das Argument aufgestellt , dass tatsächliche Unendlichkeiten existieren. Das Problem mit der naiven Mengenlehre besteht darin, dass es möglich ist, einen Widerspruch abzuleiten, wie Russell Frege gezeigt hat, der heute als Russells Paradoxon bekannt ist. Die von Russell angeführte Antwort bestand darin, ein neues System zu entwickeln, um die naive Mengenlehre zu ersetzen, und was er vorschlug, war eine Reihe von Theorien, die Typen zulassen. Aus Linnebos Philosophie der Mathematik , p. 143:
Gödel geht so weit zu behaupten, die Mengenlehre sei „nichts anderes als eine natürliche Verallgemeinerung der Typenlehre, oder besser gesagt, sie ist das, was aus der Typenlehre wird, wenn gewisse überflüssige Beschränkungen beseitigt werden … Eine der „überflüssigen“. Einschränkungen", die Gödel im Sinn hat ... [ist] die Typentheorie kann es einem Individuum nicht erlauben, direkt Mitglied eines Clans zu sein, sondern nur über eine Familie".
Die Kurzversion ist, dass die Typentheorie Russells Paradoxon entgeht, indem sie eine strenge Hierarchie von "Mengen" erstellt, sodass eine Menge kein Mitglied von sich selbst sein kann, was eine Annahme ist, die zu dem Paradoxon führt. Sowohl aus historischen als auch aus technischen Gründen entschieden sich Mathematiker jedoch für die ZF-Theorie und entwickelten sie, wobei sie schließlich ein Axiom der Wahl akzeptierten oder es durch andere erweiterten, wie in NBG:
Die Zermelo-Fraenkel-Mengentheorie soll einen einzigen primitiven Begriff, den einer erblichen, wohlbegründeten Menge, formalisieren, sodass alle Entitäten im Diskursuniversum solche Mengen sind. Daher beziehen sich die Axiome der Zermelo-Fraenkel-Mengentheorie nur auf reine Mengen und verhindern, dass ihre Modelle Urelemente (Elemente von Mengen, die selbst keine Mengen sind) enthalten. Darüber hinaus können echte Klassen (Sammlungen mathematischer Objekte, die durch eine von ihren Mitgliedern geteilte Eigenschaft definiert werden, wobei die Sammlungen zu groß sind, um als Mengen festgelegt zu werden) nur indirekt behandelt werden. Insbesondere lässt die Zermelo-Fraenkel-Mengentheorie weder die Existenz einer universellen Menge (einer Menge, die alle Mengen enthält) noch ein uneingeschränktes Verständnis zu, wodurch Russells Paradoxon vermieden wird.
Die Kategorientheorie ist eine ganz andere Sache und wurde speziell erfunden, um nach Verallgemeinerungen zwischen mathematischen Strukturen zu suchen. Von WP:
Die Kategorientheorie formalisiert die mathematische Struktur und ihre Konzepte in Form eines bezeichneten gerichteten Graphen, der Kategorie genannt wird, dessen Knoten Objekte genannt werden und dessen bezeichnete gerichtete Kanten Pfeile (oder Morphismen) genannt werden. 1 Eine Kategorie hat zwei grundlegende Eigenschaften: die Fähigkeit, die Pfeile assoziativ zusammenzusetzen, und die Existenz eines Identitätspfeils für jedes Objekt. Die Sprache der Kategorientheorie wurde verwendet, um Konzepte anderer Abstraktionen auf hoher Ebene wie Mengen, Ringe und Gruppen zu formalisieren. Informell ist die Kategorientheorie eine allgemeine Theorie der Funktionen ... Samuel Eilenberg und Saunders Mac Lane führten die Konzepte von Kategorien, Funktoren und natürlichen Transformationen von 1942 bis 1945 in ihrem Studium der algebraischen Topologie ein, mit dem Ziel, die erhaltenden Prozesse zu verstehen mathematische Struktur.
Im Gegensatz zum Denken über die Grundlagen als Mengen oder Sammlungen begreift das kategorial-theoretische Denken die Welt der mathematisch abstrakten Objekte als Objekte und Karten. Dadurch lässt sich die Theorie recht gut grafisch als mathematische Graphen ausdrücken . Anstelle von Zugehörigkeit und Äquivalenz als wichtigen Relationen werden Zuordnungen und Ordnung als primär angesehen. Seine theoretischen Verteidiger glauben, dass dies die Mathematik besser zeigt:
Aus Conceptual Mathematics: A First Introduction to Categories , S.3:
Unser Ziel in diesem Buch ist es, die Konsequenzen einer neuen und grundlegenden Einsicht über das Wesen der Mathematik zu untersuchen, die zu besseren Methoden zum Verständnis und zur Verwendung mathematischer Konzepte geführt hat ... Während diese Idee, dass Mathematik verschiedene Kategorien und ihre Beziehungen beinhaltet, hat jahrhundertelang implizit war, gaben Eilenberg und Mac Lane erst 1945 explizite Definitionen ... indem sie viele Jahrzehnte der Analyse der Arbeitsweise der Mathematik und der Beziehungen ihrer Teile zusammenfassten.
Sie haben Recht, dass Mengenlehre, Typenlehre und Kategorienlehre für die Mathematik als Teil einer philosophischen Herausforderung sehr wichtig sind und alle in gewissem Zusammenhang mit grundlegenden Fragen stehen . Denken Sie daran, dass die Grundlagen der Mathematik sehr wichtig sind, um zu erklären, was Mathematik „ist“, was unter Mathematikphilosophen umstritten ist. Logiker, Formalisten, Empiriker, Nominalisten und andere haben sehr unterschiedliche Ansichten darüber, was Mathematik ist und ob abstrakte Objekte objektiv, real und so weiter sind. Ein guter Ausgangspunkt ist „Philosophie der Mathematik“ (SEP). Denken Sie daran, dass die Mengenlehre (über ZFC) für das logistische Programm wichtig ist und die Kategorientheorie Strukturalisten anspricht; sowohl die Frage, „was Mathematik ist“, ist noch immer eine umstrittene Frage.
(Haftungsausschluss: Vor langer Zeit habe ich praktisch im CS-Bereich gearbeitet, nämlich mit Programmiersprachen, die auf der Kategorientheorie (Haskell, OCaml) basieren. Ich könnte mich also irren, aber ich werde meinen gesunden Menschenverstand präsentieren, basierend auf meine Intuition)
Die Kategorientheorie ist meines Erachtens eine Theorie, die auf einer Typentheorie aufbaut. Es geht über die Typentheorie hinaus, da es seine Annahmen auf die Kriterien der Zusammensetzbarkeit und Identität stützt. Kurz gesagt handelt es sich bei der Kategorie um Morphismen (strukturerhaltende „Abbildungen“) zwischen Kategorien. Es implementiert strukturerhaltende Funktionen zwischen verschiedenen Kategorien, dh Mapping, Verkettung oder Verbindung verschiedener Kategorieobjekte.
Die Typentheorie ist meiner Ansicht nach grundlegender. Es bezieht sich auf ein Typsystem, das den Vorgängen Bedeutung verleiht, die an einer bestimmten Entität ausgeführt werden können, aber nicht unbedingt die Vorgänge selbst implementiert.
Die Kategorientheorie verwendet typischerweise ein Typensystem, das auf ihre Objektknoten angewendet wird. Die Typentheorie selbst setzt solche konkreten Objekte nicht zusammen mit den Abbildungen. Meiner Meinung nach ist die Typentheorie abstrakter als das. Die Typentheorie ist eine interne Sprache der Kategorientheorie. In der Kategorientheorie haben Sie beispielsweise Typen wie Functor, Setoid, Monad implementiert. Die Kategorientheorie ist also ein bestimmtes Typensystem, aber die Typentheorie kann weithin verwendet werden, um jedes solche andere System zu implementieren.
Type_theory#Relation_to_category_theory
Wie John Lane Bell schreibt: „ Tatsächlich können Kategorien selbst als Typentheorien einer bestimmten Art angesehen werden ; allein diese Tatsache weist darauf hin, dass die Typentheorie viel enger mit der Kategorientheorie verwandt ist als mit der Mengentheorie.“ Kurz gesagt, eine Kategorie kann als Typentheorie angesehen werden, indem ihre Objekte als Typen (oder Arten) betrachtet werden, dh "Grob gesagt kann eine Kategorie als eine Typentheorie betrachtet werden, die ihrer Syntax beraubt ist."
Hier ist eine weitere Betrachtung der Unterschiede von Mengen/Kategorien/Typen aus der Perspektive eines Mathematikers. Ich denke, das kommt darauf an, was ein praktizierender Mathematiker berücksichtigt, wenn er einen dieser drei verwendet. Entscheidend für die Auswahl eines dieser Begriffe ist die Notwendigkeit, damit umzugehen, was gleich bedeutet.
Zusammenfassung
Logikfunktion. Die Logik berücksichtigt Gleichheit/Identität in vielerlei Hinsicht, aber in der Überschneidung mit der Mathematik beinhaltet sie meistens eine gewisse Variation des Leibnizschen Gesetzes.
x=y wenn für jede Eigenschaft P, P(x) wenn, und nur wenn, P(y).
Logikmangel. Mathematik versucht zu wissen, was alle P bedeuten könnten, sicherlich sieht 1+2 anders aus als 3, aber wir wollen, dass diese "als Zahlen" gleich sind. Wir brauchen also einen Kontext, in dem wir sagen können: "Bis zu diesem Kontext macht Gleichheit dieser Art Sinn". In der Mathematik bekommt ein solches Packen Namen wie "Linien", "Ebenen", "Mengen", "Klassen", "Typen". In dieser Form könnte die Idee unter verschiedenen Namen bis zu Euklids Elementen, aber auch zu Des Cartes' Einführung der xy-Ebene und der grafischen Darstellung von Funktionen als dem, was wir heute {(x,y)|y=f schreiben, behauptet werden (X)}. In dieser Wurzelform ist er weit vom kantischen Einfluss entfernt.
Funktion einstellen. In ZFC sind alle Dinge festgelegt. Mengen enthalten also andere Mengen und so weiter. Es gibt Paradoxien, die durch eine solche Behandlung vermieden werden, aber in der täglichen Arbeit der Mathematik regelt dies die Frage der Gleichheit durch das Axiom der Extensionalität.
Rückzug einstellen. Es strengt die Leichtgläubigkeit an, aus der Sicht der Mathematiker 2, 4/5, Pi und andere Strukturen als Mengen anzunehmen. Mathematiker schreiben munter Mengen als {2, 4/5, pi} und wissen, dass sie sich von {3,7, -9} unterscheiden, ohne sich jemals an die ZFC für Gleichheit zu wenden. Es ist nur so, dass ein Mathematiker, wenn er gezwungen ist zu erklären, dass Gleichheit einen gewissen Sinn macht, auf einige vorhandene Quellen zurückgreifen könnte, die alle diese Zahlen als Mengen modellieren und somit einen Kontext für Gleichheit bieten. Dies ist jedoch nicht unkonstruktiv oder erweiternd, sondern es handelt sich lediglich um versteckte, übersehene oder ignorierte Details, die bei Bedarf wiederhergestellt werden könnten.
Kategorie-Funktion. Ein Hauptproblem, an dessen Lösung die frühe Kategorietheorie interessiert war, bestand darin, verfeinerte Ansichten der Gleichheit zuzulassen, z. B. können Kategorien sagen, dass zwei Dinge isomorph oder "äquivalent" sind, aber diese Bedeutung legt explizite Mechanismen für die Übersetzung von Daten offen. Diese Ansicht unterscheidet sich von Mengen, bei denen nur ein Mechanismus (zweiseitige Mengeneinbeziehung) alle Gleichheit erklärt. Kategorien betonen, wie Daten gleich gemacht werden. In seinen ersten Versionen hing dies letztendlich noch von der Gleichheit in Mengen ab, da Morphismen von Mengen erfasst wurden und dies ermöglichte, dass Begriffe wie fg = h als Mengengleichheit ausgedrückt werden konnten. Aber Kategorien sind eine rekursive algebraische Theorie (die Kategorie der Kategorien macht Sinn, wenn sie verzweigt ist), und heutzutage kann die Gleichheit in Kategorien zu höheren Kategorieausdrücken verfeinert werden, anstatt von Mengen abzuhängen.
[Nebenbei bemerkt, Mathematiker könnten die Ansicht von Kategorien als beschriftete Graphen bestreiten. Sie ähneln eher der Algebra, tatsächlich sind sie formal eine "im Wesentlichen algebraische Theorie" (Peter Fryed). Eine Möglichkeit, dies zu beobachten, besteht darin, dass Graphen im Allgemeinen keine transitiven Relationen sind, aber alle Kategoriediagramme dies sein müssen.]
Kategorie Nachteil. Kategorien, wie Mengen, fordern den Mathematiker erneut auf, alle ihre mentalen Modelle in ein neues, eines der Kategorien, zu übersetzen. Selbst einfache Strukturen wie Ziffern und Ordnungen sollen als Diagramme mit spezifischen Operatoren von Komposition und Identität umgeformt werden. Suchen Sie nach "simplizialen Mengen" und prüfen Sie, ob diese Definition beispielsweise das Konzept eines Simplex geometrisch verbessert. Während also Kategorien die Art und Weise verbessern, zu sagen, dass zwei Dinge „isomorph“ oder „äquivalent“ sind, ist die Übersetzung für andere Dinge künstlich und erzwungen.
Ein weiteres Problem ist die Enge von Morphismen in einer Kategorie, die erforderlich ist, um die Zusammensetzbarkeit zu erzwingen. Zum Beispiel arbeitet das Fach Graphentheorie und allgemeinere Kombinatorik mit einer solchen Vielfalt von Transformationen, oft lokalen oder induktiven Studien, die einfach nicht gut in Kategorien passen, da die Bedeutung von "einem Morphismus" variiert. Selbst grundlegende Konzepte wie die lineare Algebra passen nicht in eine einzige Kategorie, da wir Matrizen (M,N) genauso oft mit der Formel XM=NY wie XMY=N vergleichen, aber erstere ist eine abelsche Kategorie und letztere nicht. Diese Vergleiche koexistieren also in der Theorie, aber nicht in der Kategorie. Wir können also nicht einmal die nützlichste Mathematik studieren, ohne die Daten in mehrere Kategorien zu duplizieren und dann zu postulieren, wie sie nachträglich verbunden werden sollten. Das macht es weniger effektiv als Grundlage. Seltsamerweise
Geben Sie Funktion ein. Eine Haupteigenschaft von Typen ist für viele Mathematiker, die sie verwenden (zugegebenermaßen wenige), dass sie die Daten so belässt, wie sie sind. Es kommentiert (dokumentiert) sie lediglich mit Labels, um den Leser darüber zu informieren, welche Regeln und Zusammenhänge für diese Daten gelten. Der Benutzer kann mit den Daten genau so arbeiten, wie er/sie es möchte. Die Zahl Pi ist beispielsweise eine Dezimalzahl, keine Menge oder ein Objekt in einer Kategorie. Gleichheit von Pi ist als Dezimalzahl.
Geben Sie Rückzug ein. Daten sein zu lassen, was sie sind, bedeutet, dass Sie alle Vereinheitlichungen verlieren, die Mathematik nützlich machen. 4/5 ist jetzt nicht unbedingt gleich 0,80, da diese möglicherweise von verschiedenen Typen kommentiert werden (in einer Curry-Typkonvention). Während Hindley-Milner und andere Typklassen und Verbände usw. bereitgestellt haben, um Typen zu vereinheitlichen, bleibt dies ein expliziter Schritt, der oft die schnellere Argumentation behindern kann, die durch Mengen auf einigen Ebenen ermöglicht wird. Univalenz treibt die Vereinigung auf die Spitze und nähert sich dem an, was mit Mengen gemacht werden kann. Es bleibt abzuwarten, ob die Mathematik diesen Ansatz akzeptiert oder ihn als einen weiteren Fall betrachtet, in dem Sie gezwungen sind, alle Ihre mentalen Modelle in eine andere Form zu übersetzen, um eine begrenzte Kapitalrendite zu erzielen.
In Summe. Mathematiker arbeiten abstrakt (im formalen Sinne, ein Thema durch Regeln einzugrenzen), und diese drei grundlegenden Modelle bieten Möglichkeiten, dies mit einer gewissen Infrastruktur zu tun. Da diese Grundlagen jedoch versuchen, Paradoxien zu vermeiden und Lücken zu füllen, führen sie oft zu Änderungen in unserem Modell, die eigentlich nicht das sind, was wir beabsichtigen. Gleichheit ist ein Ort, an dem wir die Risse beobachten. Hier unterscheiden sich die drei Modelle im Alltag.
Paul Ross
JD
JD
Algeboy
Kristian Berry
Algeboy
Boba-Fit