Typentheorie

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche
Racine carrée bleue.svg
Dieser Artikel wurde auf der Qualitätssicherungsseite des Portals Mathematik eingetragen. Dies geschieht, um die Qualität der Artikel aus dem Themengebiet Mathematik auf ein akzeptables Niveau zu bringen.

Bitte hilf mit, die Mängel dieses Artikels zu beseitigen, und beteilige dich bitte an der Diskussion! (Artikel eintragen)

Die Typentheorie ist eine vom Mathematiker Bertrand Russell entwickelte Form der Mengenlehre, mit der er unter anderem versuchte, die von ihm entdeckte Russellsche Antinomie und andere Widersprüche der ursprünglichen oder naiven Mengenlehre zu beheben.

Weitere Einzelheiten[Bearbeiten]

Nach der Typentheorie gibt es einfache Mengen, welche lediglich Urelemente, aber keine Mengen als Elemente enthalten können; Mengen des zweiten Typs können nur einfache Mengen enthalten, Mengen des dritten Typs nur Mengen des zweiten Typs usw. Mengen haben also einen um eins höheren Typ als ihre Elemente. Diese System beruht somit auf einer Stratifikation des Mengenbegriffs und vermeidet dadurch die Russellsche Antinomie, da die Darstellung der Menge aller sich nicht selbst enthaltenden Mengen schon aus syntaktischen Gründen nicht möglich ist, denn die dazu nötigen Aussagen x\in x und x\notin x sind syntaktisch nicht korrekt.

In einer kumulativen Typentheorie können in einer Menge beliebige Mengen niedrigerer Stufe oder Urelemente enthalten sein, wodurch ebenfalls die Russellsche Antinomie vermieden wird.

Die erste einfache Version der Typentheorie formulierte Russell im Jahr 1903 im Anhang seiner Principles of Mathematics, die zweite komplexere Version im Jahr 1908 in Mathematical Logic as based on the Theory of Types. Letztere wurde die Grundlage der berühmten Principia Mathematica, die er nach beinahe zehnjähriger Vorbereitungszeit zusammen mit Alfred North Whitehead ab 1910 veröffentlichte. Die einfache Typentheorie wird seit Ramsey auch Simplified Theory of Types (oder kurz STT) genannt; sie ist hinreichend zur Vermeidung der logischen Widerspruche wie der Russellschen Antinomie, aber nicht für die Lösung der semantischen Widerspruche wie der Grelling-Nelson-Antinomie; dies vermag erst seine wesentlich aufwendigere Ausgabe von 1908, die Ramified Theory of Types (RTT), die „verzweigte“ Typentheorie.

Diese Version der Typentheorie setzte sich wegen ihrer Kompliziertheit und eingeschränkten Leistungsfähigkeit nicht auf Dauer durch. Als bequemer und leistungsfähiger erwies sich die von Ernst Zermelo 1907 entwickelte axiomatische Mengenlehre, die Abraham Fraenkel 1922 erweiterte und die heute als Zermelo-Fraenkel-Mengenlehre, kurz ZF, bekannt und als Basis der Mathematik weitgehend anerkannt ist. Zudem hat man in ZF eine zum Fundierungsaxiom äquivalente von-Neumann-Hierarchie, die eine Art Stratifikation darstellt, aber keine weiteren Restriktionen mit sich bringt. Die Stufen oder Ränge der Mengen entsprechen zudem einer kumulativen Typentheorie.

Eine vereinfachte Variante der Typentheorie entwarf Quine 1937 in seinen New Foundations.

Typentheorien spielen eine wichtige Rolle in der Theorie der Programmiersprache und in darauf basierenden Programmiersprachen und computergestützten Beweissystemen wie Coq und Agda (dependent types).

Literatur[Bearbeiten]

Weblinks[Bearbeiten]