Diskussion:Typentheorie

Weitere Einzelheiten, 1. Absatz

Aktuell heißt es hier:

Mengen des zweiten Typs können zusätzlich einfache Mengen enthalten, Mengen des dritten Typs zusätzlich Mengen des zweiten Typs usw.

Dies gilt für eine 'kumulative' Typentheorie. Man spricht dann nicht vom Typ, sondern von der Stufe bzw. dem Rang einer Menge/eines Urelements. Die Mengenstufen haben eine gewisse Ordnungsstruktur. Ggf. vorhandene Urelemente haben Stufe 0, die Leermenge hat Stufe 1. Die Stufe einer Menge ist immer um 1 höher als das Supremum der Stufen ihrer Elemente. Diessen Existenz wird durch die Forderung der Beschränktheit der Stufen der Elemente gesichert. Die Vereinigung von Mengen unterschiedlich hoher Stufe ist erlaubt. Die Vereinigungsmenge endlich vieler Mengen hat dieselbe Stufe wie die Menge mit der höchsten Stufe (Maximum). Bei der Vereinigung unendlich vieler Mengen tritt an die Stelle des Maximums das Supremum. Die Menge der natürlichen Zahlen ist wie üblich konstruierbar (ohne Urelemente): 0 = {}, 1 = {0} = {{}}, 2 = {0,1} = {{},{{}}}, 3 = {0,1,2}, allg. n+1 = {1,2,3,...n}. Die Menge der Natürlichen Zahlen ist auch die Vereinigung dieser Mengen, N = U N. Ihre Stufe ist die kleinste unendliche Ordinalzahl ω (omega). Immer höhere Stufen sind nach dem sog. Shoenfield-Prinzip definierbar. Dieser Ansatz wurde/wird z. B. von Dieter Klaua verfolgt. Die Axiome der klassischen Mengentheorie (ZF) sind ableitbar. Umgekehrt können die Mengen der klassischen Mengentheorie ZF wegen Fundiertheit mit einer Stufen- oder Rang-Hierarchie versehen werden. Dies zeigt, dass die kumulative Typentheorie (im Wesentlichen) äquivalent zu ZF ist.

Refernz: Dieter Klaua, Mengenlehre, de Gruyter Lehrbuch, Berlin, 1979, ISBN: 3110077264.

Bertrand Russel hat hingegen (zunächst) eine strikte Typentheorie vertreten. Typ 0 haben wieder die Urelemente. Typ 1 haben die einfachen Mengen (engl. sets), die nur Urelemente enthalten. Typ 2 haben die einfachen Mengensysteme (engl. collection sets), die nur(!) Mengen des Typs 1 als Elemente enthalten usw. Jede Potenzmengenbildung führt eine Typstufe höher, die Typen werden also durch die natürlichen Zahlen gekennzeichnet. Zu jedem Typ gibt es eine zugehörige Leermenge!

Im übrigen kann man auch *verschiedene* Grundmengen von Urelementen annehmen, so dass Urelemente verschiedener Grundmengen nicht verträglich sind und zu einer Menge zusammengefasst werden können, neben einer Menge E von Urelementen vom Typ e etwa logische Wahrheitswerte mit Typ t - klassisch T={0,1} oder T={false,true}, in einer Fuzzy-Logik etwa das relle Intervall [0,1]. Als Typen haben wir dann eine Kombination fon e, t, ... mit einer Zahl n=0, 1, 2, 3,... Diese zeigt an, wie oft die Potenzmengenbildung über E, T, ... ausgeführt werden muss. Die Typen bilden also eine unendliche Menge (Typen über einer Urmenge E also ein Modell der nat. Zahlen N). Für alle vorkommenden Typen selbst kann ein Typ type angenommen werden. d

Abgesehen von diesen kann (unter den Objekten selbst) die Menge der natürlichen Zahlen nicht konstruiert werden. Man kann entweder annehmen, dass ein Modell (Trägermenge N) der der natürlichen Zahlen (mit Peano-Axiomen) Teilmenge der Urelemente U ist; oder (zu e, t, ...) einen weiteren Typ nat eines Modells der natürlichen Zahlen (Trägermenge N) hinzufügen.

Weitere Typen werden üblicherweise für die Abbildungen A -> B vorgesehen. Sei a der Typ von A, b der von B, so wird der Typ dieser Abbildungen mit a |-> b (oder <a,b>) bezeichnet. Beispiel die Indikatorfunktionen E -> T mit Typ e |-> t. (Einer Menge X (Teilmenge von E) ist die Indikatorfunktion I_X : x |-> (x ∈ X) eineindeutig zugeordnet.)

Teilweise wurden auch für Relationen eigene Typen angenommen. (Eine zweistellige Relation zw. Elementen der Mengen A und B ist eine Teilmenge der Produktmenge AxB, also wäre a x b der Typ der Paare (α,β) ∈ A X B). Nach Wiener und Haussdorff sind aber geordnete Paare als spezielle Mengen konstruierbar, etwa in der Art (α,β) = {{α},{α,β}} (Kuratowski) oder der Art (α,β) = { { {α}},{{},{β}}} (Wiener), dazu müssen α und β aber denselben Typ, etwa e haben. Tripel, Quadrupel, ... analog. Der Typ a x b ist dann Typ e2 bzw. e3 (einfache Mengensysteme über E). Falls α und b aus verschieden oft iterierten Potenzmengen derselben Grundmenge E stammen, kann man das niedrigere Element α ausreichend oft 'liften' ( {α}, { {α}}, ... ) bis man auf derselben 'Ebene' ist wie b und dann erst das Paar wie oben angegeben bilden.

Geht das auch dann noch, wenn α und β aber aus Grundmengen mit unterschiedl. Typ stammen (oder iterierten Potenzmengen davon), etwa aus E und T??? Wohl kaum - dann wären etwa Paare (x,l) aus E X T nur durch die charakteristische Eigenschaft (a,b) = (c,d) <=> a=c ∧ b=d gekennzeichnet (nicht konstruierbar), mit neuem Typ e x t???

Gibt es einen Experten, der das klären könnte und im Artikel einfließen lassen kann?

Referenzen:

• http://glossar.hs-augsburg.de/Typentheorie
• http://glossar.hs-augsburg.de/Geordnetes_Paar
• http://glossar.hs-augsburg.de/Russellsche_Antinomie - auf cyclische Mengen (mit Antifundierungsaxiomen) und Ackermann-Mengentheorie (mit echten Klassen, d. h. Unmengen, die in anderen Klassen enthalten sind wird nicht eingegangen.

Vielen Dank im voraus!

[[[Benutzer:Ernsts|Ernsts]] (Diskussion) 22:52, 30. Sep. 2013 (CEST)

Link veraltet

---Ich moechte darauf hinweisen dass der Literaturlink tot ist, die verlinkte PDF (http://www.cfh.ufsc.br/~dkrause/pg/cursos/selecaoartigos/Russell(1905).pdf) gibt es nicht mehr. (nicht signierter Beitrag von 185.17.204.5 (Diskussion) 00:14, 11. Apr. 2015 (CEST))

Gelöst: Link repariert per Web-Archiv (Wayback machine) --Ernsts (Diskussion) 19:35, 29. Mai 2018 (CEST)

Russell´sche Typentheorie

Aus meiner (laienhaften) Sicht gibt es drei Fragestellungen:

• Gelingt es Russell mit der Typentheorie die Russellsche Antinomie zu überwinden?

Ja, definitiv. In Russells Typentheorie gibt es Urelemente, die keine Mengen sind, Mengen die solche Urelemente enthalten (= Mengen niedrigster Typstufe), Mengensysteme (= Mengen von Mengen niedrigster Stufe = Mengen zweitniedrigster Stufe) usw. Entscheidend ist, dass die Elemente einer Menge egal welcher Typstufe immer dieselbe (um 1 niedrigere) Stufe haben. Es sind keine Vermischungen wie etwa {a, {a}} erlaubt. Damit gibt es weder die 'Menge aller Mengen' (Allmenge, würde sich selbst als Element enthalten), noch die 'Menge aller Mengen, die sich nicht als Element enthalten' (Russellsche Menge, sozusagen der 'Problembär'). Es hat sich im Lauf der Zeit aber gezeigt, dass die von Russell vorgeschlagenen Einschränkungen der Mengenbildung hinreichend sind, die Russellsche Antinomie zu vermeiden, aber keinesfalls notwendig. Aus mengentheoretischer Sicht gibt es bessere, weniger restriktive Lösungen. Am gebräuchlichsten sind heute Mengentheorien vom Zermelo-Fraenkel-Typ mit oder ohne Urelemente, mit oder ohne Auswahlaxiom. Hier sind zirkelafte Mengen, dis sich selbst direkt oder indirket als Element enthalten (wie die Allmenge), verboten. Die Mengenbildung ist allgemein einer Bechränkung unterworfen. Zusammenfassungen jenseits dieser Beschränkung werden oft als Unmengen (oder eigentliche Klassen) bezeichnet (Allklasse = Klasse aller Mnegen, Klasse der Vektorräume, ...), dabei ist es nicht erlaubt, dass eigentliche Klassen als Elemente irgendwelcher Zusammenfassungen auftreten, also auf der linken Seite der Enthaltensrelation $\in$. Es gibt seitdem sogar verschiedene Mengentheorien mit zirkelhaften Mengen, die die Russellsche Antinomie auf raffinierte Weise vermeiden. Solche Mengen sind beispielsweise geeignet, Bibliotheken oder Datenbanken zu beschreiben, wenn diese einen Katalog bzw. eine Tabelle enthalten, der/die alle Bücher bzw. Tabellen (also auch sich selbst) umfasst.

• Gibt es verbesserte Typentheorien, denen das besser/eleganter etc. gelingt?

Die von Russell zunächst entworfenen Typentheorien mit verzweigten Theorien sind infolge anderer Erkenntnisse teilweise überflüssig geworden (wenn ich es richtig verstanden habe). Allerdings kann man die Typentheorie zu einem ganzen 'Zoo' von Typen weiterentwicken: Warum sollen alle Urelemente als Elemente von Mengen beliebig mischbar vorkommen? Etwa natürliche Zahlen und Wahrheitswerte? Letztere kann man als 0 und 1 verstehen, muss es aber nicht. Aus solchen Basistypen (nat mit Peano-Axiomen, logical mit Boolschen Axiomen) kann man weitere Typen konstruieren, nicht nur nach Russell (per 'Menge von ...' / 'set of'), sondern auch vielleicht als geordnete Paare von Objekten möglicherweise verschiedenen Typs, die lediglich dem Paaraxiom unterworfen sind (Typkonstruktoren). Ganz abgesehen von Funktionstypen (definiert durch Stelligkeit und alle Argumenttypen, sowie den Ergebnistyp). Das wiederum legt nahe, einen Typ 'type' (oft einfach notiert mit '*') einzuführen, dessen Objekte die vorkommenden Typen sind.

• Gibt es unabhängig von dieser Frage in der Mathematik Anwendungsbereiche für Typentheorien?

Ja, das sind vor allem die in den Programmiersprachen üblichen Datentypen. Grundsätzlich gibt es hier eine Reihe von Basistypen (int, chat,...). Viele Programmiersprachen lassen Typkonstruktoren zu, etwa 'struct' oder 'recdord', welche weitgehend geordneten Paaren bzw. Tupeln entsprechen (mit dem Unterschied, dass die Komponenten Namen statt Indexnummern haben), gelegentlich gibt es auch 'setof' (Mengen). Moderne Programmiersprachen fassen dass Vermischungsverbot flexibler. So gibt es Subtypen (etwa a..b Ganzzahlen zwischen a und b einschl., Pascal, Modula2) und abgeleitete Typen ('Klassen' im objektorientierten Sinn). Man versucht so, die Problematik einer 'typeof'-Funktion zu vermeiden (Ergebnistyp: 'type', Argumenttyp: alles vermischt - was eigentlich gegen die 'reine Lehre' ist), und analog der Interpretationsfunktion: Argumenttyp: string (Objektname), Ergebnistyp: alles mögliche). Manchmal muss man eben doch verschiedene Typen mischen. Die Modelltheorie erklärt Typen als Sorten verschiedener Objekte, deren Vermischung zwar erlaubt, aber grundsätzlich (mit klar definierten Ausnahmen) nicht üblich ist (nicht innerhalb des Modells=Miniwelt!).

--Karl-Hagemann (Diskussion) 18:12, 3. Apr. 2016 (CEST)

Antwortversuch: --Ernsts (Diskussion) 22:46, 29. Mai 2018 (CEST)

Russellsche Typentheorie als Überwindung der Russellschen Antinomie

Ich verstehe das so, dass im Rahmen des logizistischen Programms die Russellsche Antinomie auftritt, die ungelöst zur Aufgabe des Logizismus zwingt. Frege verfiel in Depression, Russell entwickelte die Typentheorie.

Kritische Anmerkungen zu Russell:

• "Die Theorie der Typen wurde mit Russells Paradoxie fertig - nicht aber mit der des Epimenides und der Grellings", jedoch "auf Kosten einer künstlich erscheinenden Hierarchie".

(so Hofstädter, Douglas R.: Gödel, Escher, Bach. 5. Auflage. Klett-Cotta, Stuttgart 1985, S. 24) (Meine Anm.: Mit Blick auf den Unvollständigkeitssatz von Gödel ist das vielleicht ja nicht künstlich.)

• Die Russellsche führt zu der Schwierigkeit, wie man dann noch (mit Frege) Zahlen als Klassen von Klassen definieren kann. Russells Lösung war, ein Unendlichkeitsaxiom einzuführen, d.h. hier die Annahme einer unendlichen Anzahl kontingenter Dinge - das überzeugt aber auch nicht jeden.

(Zitat: "Doch nun tauchte eine neue Schwierigkeit auf. Erinnern wir uns daran, dass Frege die Zahl Zwei faktisch als die Klasse aller Paare und die anderen natürlichen Zahlen auf ähnliche Weise definiert hatte. Doch ein Paar ist einfach eine Klasse mit zwei Elementen, sodass die Zahl Zwei nach dieser Erklärung eine Klasse von Klassen ist. Wenn wir die Bildung der Klassen von Klassen einschränken, wie können wir dann die Reihe der natürlichen Zahlen definieren? Russell behielt die Definition der Null als der Klasse, deren einziges Element die Null-Klasse ist, bei. Doch er behandelte die Zahl Eins jetzt als die Klasse aller Klassen, die der Klasse entsprach, deren Elemente (a) Elemente der Null-Klasse sind und (b) irgendein Objekt, das kein Element dieser definierenden Klasse ist. Auf diese Weise können die Zahlen eine nach der anderen definiert werden, und jede Zahl ist eine Klasse von Klassen von Individuen. Die Reihe der natürlichen Zahlen kann auf diese Weise nur dann bis ins Unendliche fortgesetzt werden, wenn die Anzahl der Gegenstände des Universums selbst unendlich ist. Denn wenn es nur n Einzeldinge gibt, dann wird es keine Klassen mit n + 1 Elementen geben und daher keine Kardinalzahl n + 1. Russell akzeptierte dieses Argument und fügte seinen Axiomen daher ein Axiom der Unendlichkeit hinzu, d. h. die Hypothese, dass die Anzahl der Gegenstände im Universum nicht endlich ist. Ob diese Hypothese wahr ist oder nicht: Sie ist gewiss keine Wahrheit der reinen Logik, und daher scheint die Notwendigkeit sie zu postulieren, das logizistische Projekt der Ableitung der Arithmetik aus der Logik zum Scheitern zu verurteilen."

So Anthony Kenny: Geschichte der abendländischen Philosophie. Band IV. Moderne. 2. Auflage. WBG (Wissenschaftliche Buchgesellschaft), Darmstadt 2014, 978-3-534-73858-8, S. 62

--Karl-Hagemann (Diskussion) 18:24, 3. Apr. 2016 (CEST)

Top-Typ, Einheitstyp, Bottom-Typ

Irgendwie vermisse ich diese drei Begriffe hier, sie sollten wenigstens erwähnt/verlinkt werden. Wie seht ihr das? --84.141.125.94 10:17, 30. Jun. 2016 (CEST)

Der Artikel bedarf wohl einer grundsätzlichen Überarbeitung, siehe die Diskussion in der Mathe-QS.--Pugo (Diskussion) 15:52, 29. Sep. 2016 (CEST)

Erwähnung/Links hinzugefügt --Ernsts (Diskussion) 23:14, 29. Mai 2018 (CEST)

Literatur

https://arxiv.org/pdf/1805.05419.pdf Seite 17-20 könnte vielleicht für eine allgemeinverständliche Darstellung von Nutzen sein.—Godung Gwahag (Diskussion) 08:42, 18. Jul. 2019 (CEST)