Typtheorie

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 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.

Die 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 bekannt und als Basis der Mathematik weitgehend anerkannt ist.

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


Weblinks


Wikimedia Foundation.

Игры ⚽ Поможем сделать НИР

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

  • Alpha-Konversion — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen, die Funktionsdefinitionen, das Definieren formaler, sowie das Auswerten und Einsetzen aktueller Parameter regelt. Inhaltsverzeichnis 1 Geschichte 2 Der untypisierte… …   Deutsch Wikipedia

  • Lambda-Ausdruck — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen, die Funktionsdefinitionen, das Definieren formaler, sowie das Auswerten und Einsetzen aktueller Parameter regelt. Inhaltsverzeichnis 1 Geschichte 2 Der untypisierte… …   Deutsch Wikipedia

  • Lambda-Notation — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen, die Funktionsdefinitionen, das Definieren formaler, sowie das Auswerten und Einsetzen aktueller Parameter regelt. Inhaltsverzeichnis 1 Geschichte 2 Der untypisierte… …   Deutsch Wikipedia

  • Lambdakalkül — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen, die Funktionsdefinitionen, das Definieren formaler, sowie das Auswerten und Einsetzen aktueller Parameter regelt. Inhaltsverzeichnis 1 Geschichte 2 Der untypisierte… …   Deutsch Wikipedia

  • Prädikatenlogik höherer Stufe — Unter Logik höherer Stufe (englisch: Higher Order Logic, HOL) versteht man eine Erweiterung der Prädikatenlogik erster Stufe. Sie basiert auf dem typisierten Lambda Kalkül und geht auf Alonzo Churchs Theory of Simple Types zurück. Entwickelt um… …   Deutsch Wikipedia

  • Stufenlogik — Unter Logik höherer Stufe (englisch: Higher Order Logic, HOL) versteht man eine Erweiterung der Prädikatenlogik erster Stufe. Sie basiert auf dem typisierten Lambda Kalkül und geht auf Alonzo Churchs Theory of Simple Types zurück. Entwickelt um… …   Deutsch Wikipedia

  • Lambda-Kalkül — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen. Sie beschreibt Funktionsdefinitionen, das Definieren formaler Parameter sowie das Auswerten und Einsetzen aktueller Parameter. Inhaltsverzeichnis 1 Geschichte 2 Der… …   Deutsch Wikipedia

  • Logik höherer Stufe — Unter Logik höherer Stufe (englisch: Higher Order Logic, HOL) versteht man eine Erweiterung der Prädikatenlogik erster Stufe. Sie basiert auf dem typisierten Lambda Kalkül und geht auf Alonzo Churchs Theory of Simple Types zurück. Entwickelt um… …   Deutsch Wikipedia

  • Einheitstyp — Mit Einheitstyp (engl. unit type) bezeichnet man in der Typtheorie und Informatik denjenigen Typ, der lediglich einen einzigen Wert besitzt. Die Bezeichnungen des Typs reichen je nach Anwendungsgebiet von 1 (Kategorientheorie) über () (Haskell)… …   Deutsch Wikipedia

Share the article and excerpts

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