Typentheorie und Metapher

Meiner Erfahrung nach sind Lehrbücher und einführendes Material zur Typentheorie (oder zu konstruktiven Logiksystemen) bemerkenswert frei von Metaphern. Ich habe in diesen Bereichen nie einen Einführungstext gefunden, der ähnlich vorgegangen ist wie in anderen Bereichen der Logik, basierend auf der Mengenlehre, wo Sie das Thema "intuitiv" (metaphorisch) einführen und allmählich zu abstrakteren und trockeneren Ansätzen übergehen können .

Meine Frage ist, ob dies ein wesentliches linguistisches Merkmal der Behandlung der Typentheorie in Texten ist (mit anderen Worten, die Undurchlässigkeit gegenüber Metaphern ist ein erkenntnistheoretisches Problem), oder ob es sich nur um eine vorzuziehende, empfehlenswerte theoretische Strategie handelt.

Russell gibt einige interessante "konkrete" Analogien in seiner Behandlung, nicht wahr? (Der Regimentsfriseur zum Beispiel rasiert jeden, der sich nicht selbst rasiert – also wer rasiert den Barbier?)
Diese Geschichte hängt mit dem Paradoxon zusammen, dem er bei der Arbeit an seiner „Principia Mathematica“ begegnete. Es wirkte sich auf die Abhandlung von Frege über die Grundlagen der Arithmetik aus und zeigte, dass seine Axiome Widersprüchlichkeiten hervorriefen. Die Typentheorie wurde von Russell vorgeschlagen, um solche Fallstricke zu vermeiden, aber meine Frage konzentriert sich auf neuere Literatur.

Antworten (1)

Ich bezweifle, dass dies etwas Wesentliches für die Typentheorie an sich ist; aber mehr aufgrund der allgegenwärtigen Art des mathematischen und wissenschaftlichen Schreibens; Die Kunst der Ausstellung ist meiner Meinung nach allmählich verloren gegangen.

Lagrange zum Beispiel war stolz darauf, dass seine mathematischen Arbeiten keine Diagramme enthielten. Vladimir Arnold hatte sich über eine exzessive Bourbakiste Herangehensweise an die Mathematik beschwert, die, anstatt die Hauptideen zu verdeutlichen und die Bedeutung auszuschildern, alles unter einer dicken Verkrustung von Formalismus versteckte; die meisten verbargen, dass wenig von zusätzlicher Bedeutung gesagt wurde.

Bestimmte Typtheorien beziehen sich auf bestimmte Kategorien – zum Beispiel der einfach typisierte Lambda-Kalkül auf geschlossene kartesische Kategorien, und einige davon können natürlicher als String-Diagramme dargestellt werden; und diese können auf natürliche Weise topologisch verstanden werden.

Ich würde argumentieren, dass dies eine Art schematische Analogie ist.

In der Mengenlehre sind Elemente und Mengen grundlegend; und der Begriff einer Funktion wird abgeleitet; Die Topos-Theorie nimmt Mengen und Funktionen (dh Objekte und Morphismen) als Grundlage; und Elemente als abgeleitet: Lawvere sagte, er wolle Mengenlehre ohne Elemente machen.

Dies ist nicht ganz eine Metapher oder gar eine Analogie, aber es funktioniert ziemlich gut in der Art und Weise, wie es die Mengenlehre „auf den Kopf stellt“; etwa so, wie der Marxismus als Wirtschaftsphilosophie Hegel „auf den Kopf gestellt“ hat. Man könnte es einen Slogan nennen; vielleicht sogar ein "Leitbild".

Ja, die Verbindung zwischen Typentheorie und Kategorientheorie erlaubt es uns, uns mit Diagrammen von Objekten und Pfeilen auszudrücken, aber das sind keine konzeptuellen Metaphern, zumindest nicht in diesem Zusammenhang.
Ich glaube, dass mathematisches Denken im Allgemeinen mit konzeptuellen Metaphern in Verbindung gebracht werden kann (ich folge George Lakoff und Rafael Núñez in dieser Annahme: en.wikipedia.org/wiki/Where_Mathematics_Comes_From ), aber ich würde gerne wissen, ob konstruktive Logik eine Ausnahme sein könnte. Auch wenn dem so ist, glaube ich fest daran, dass das Thema schon immer zu dogmatisch dargestellt wurde, auch von Autoren, die angeblich für Anfänger schreiben.
Sicherlich sind Diagramme keine Metaphern; aber sie sind manchmal eine bessere Anordnung von Informationen, die ein besseres Verständnis ermöglichen.
Die oben erwähnten String-Diagramme sind nicht die gleichen wie die üblichen kategorientheoretischen Diagramme; schau dir das an ; tatsächlich erinnere ich mich, eine sehr kurze Beschreibung der linearen Logik durch die Metapher eines Menüs in einem französischen Restaurant gesehen zu haben; das passt wahrscheinlich besser zu deiner Frage.
Vielleicht, weil die konstruktive Logik gegen die klassische Mainstream-Logik verstößt; dass der Schreibstil dogmatisch wird; Außerdem arbeiten weniger Leute damit, so dass die allgemeinen Ideen, die nicht allgemein verstanden werden und auf die man sich nicht verlassen kann, immer wieder erklärt werden müssen; zum Beispiel „kennt“ jeder Mathematiker die Mengenlehre, ohne ZFC zu kennen; Sie können sehr weit gehen, wenn Sie nur die Metapher der Venn-Diagramme verwenden.
Typentheorie und Metapher
AntwortenHierDatenschutz-Bestimmungen1y, 0v