Typentheorie

Typentheorie

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

Nach dieser Theorie gibt es einfache Mengen, die nur Urelemente, aber keine Mengen als Elemente enthalten können; Mengen des zweiten Typs können zusätzlich einfache Mengen enthalten, Mengen des dritten Typs zusätzlich Mengen des zweiten Typs usw. Mengen haben also einen höheren Typ als ihre Elemente. Dieses 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.

Die erste einfache Version der Typentheorie formulierte Russell 1903 im Anhang seiner Principles of Mathematics, die zweite komplexere Version 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 (STT) genannt; sie ist hinreichend zur Vermeidung der logischen Paradoxien wie der Russellschen Antinomie, aber nicht für die Lösung der semantischen Paradoxien wie der Grelling-Nelson-Antinomie; dies vermag erst seine signifikant kompliziertere Version 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.

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

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

Literatur

Weblinks


Wikimedia Foundation.

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Typentheorie — Typentheorie,   eine von A. N. Whitehead und B. Russell erarbeitete Axiomatisierung der Mengenlehre mit einem entsprechend formalisierten Aufbau der Logik, die erstmals 1910 13 von ihnen in dem dreibändigen Werk »Principia Mathematica«… …   Universal-Lexikon

  • Typentheorie — Typentheorie, die von Cuvier und Baer aufgestellte Anschauung, daß man das Tierreich nicht (wie die Naturphilosophen taten) entwickelungsgeschichtlich in eine einzige große Reihenfolge (Stufenleiter) anordnen dürfe, sondern mindestens vier Typen… …   Meyers Großes Konversations-Lexikon

  • Typtheorie — Die Typentheorie ist eine von Bertrand Russell entwickelte Form der Mengenlehre, mit der er unter anderem versuchte, die von ihm entdeckte Russellsche Antinomie und andere Widersprüche der naiven Mengenlehre zu beheben. Nach dieser Theorie gibt… …   Deutsch Wikipedia

  • Axiomatische Mengenlehre — Als axiomatische Mengenlehre gilt jede Axiomatisierung der Mengenlehre, die die bekannten Antinomien der naiven Mengenlehre vermeidet. Die verbreitetste Axiomatisierung in der modernen Mathematik ist die Zermelo Fraenkel Mengenlehre mit… …   Deutsch Wikipedia

  • Bertrand Russell, 3. Earl Russell — Bertrand Russell, 1907 Bertrand Arthur William Russell, 3. Earl Russell (* 18. Mai 1872 bei Trellech, Monmouthshire, Wales; † 2. Februar 1970 in Penrhyndeudraeth, Gwynedd, Wales), war ein britischer Philosoph, Mathematiker und Logiker. Zu …   Deutsch Wikipedia

  • Hermann Kolbe — Adolph Wilhelm Hermann Kolbe Adolph Wilhelm Hermann Kolbe (* 27. September 1818 in Elliehausen, heute ein Stadtbezirk von Göttingen; † 25. November 1884 in Leipzig) war ein deutscher Chemiker. Kolbe hat mit der Elektrolyse von Carbonsäuren eine… …   Deutsch Wikipedia

  • Per Martin-Löf — 2004 Per Erik Rutger Martin Löf (* 8. Mai 1942) ist ein schwedischer mathematischer Logiker und Philosoph. Martin Löf war 1964 1965 an der Lomonossow Universität Student von Andrei Kolmogorow, der auch seine Dissertation an der Universität… …   Deutsch Wikipedia

  • Bertrand Russell — Bertrand Russell, 1970 Bertrand Arthur William Russell, 3. Earl Russell (* 18. Mai 1872 bei Trellech, Monmouthshire, Wales; † 2. Februar 1970 in Penrhyndeudraeth, Gwynedd, Wales), war ein britischer Philosoph, Mathem …   Deutsch Wikipedia

  • Charles Frédéric Gerhardt — Portrait von Charles Frédéric Gerhardt Grab von Charles Gerhardt in Straßburg Charles Frédéric Gerhardt (* …   Deutsch Wikipedia

  • Beweisbarkeit — Die Beweistheorie ist ein Teilgebiet der mathematischen Logik, das Beweise als formale mathematische Objekte behandelt. Dies ermöglicht ihre Analyse mit mathematischen Techniken. Beweise werden üblicherweise als induktiv definierte… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”