Kategoriale Logik - Categorical logic

Dieser Artikel behandelt die mathematische Logik im Kontext der Kategorientheorie. Für das logische System von Aristoteles siehe Begriff Logik .

Kategorische Logik ist der Zweig der Mathematik, in dem Werkzeuge und Konzepte aus der Kategorientheorie auf das Studium der mathematischen Logik angewendet werden . Es zeichnet sich auch durch seine Verbindungen zur theoretischen Informatik aus . Allgemein ausgedrückt repräsentiert die kategoriale Logik sowohl Syntax als auch Semantik durch eine Kategorie und eine Interpretation durch einen Funktor . Das kategoriale Framework bietet einen reichen konzeptionellen Hintergrund für logische und typtheoretische Konstruktionen. Das Thema ist in diesen Begriffen seit etwa 1970 erkennbar.

Überblick

Es gibt drei wichtige Themen in der kategorialen Herangehensweise an die Logik:

Kategoriale Semantik
Die kategoriale Logik führt den Begriff der in einer Kategorie C bewerteten Struktur mit dem klassischen modelltheoretischen Begriff einer Struktur ein, der in dem speziellen Fall auftritt, in dem C die Kategorie der Mengen und Funktionen ist . Dieser Begriff hat sich als nützlich erwiesen, wenn der mengentheoretische Begriff eines Modells nicht allgemeingültig und/oder unbequem ist. RAG Seelys Modellierung verschiedener imprädikativer Theorien, wie beispielsweise des Systems F, ist ein Beispiel für die Nützlichkeit der kategorialen Semantik.
Es zeigte sich, dass die Konnektoren der präkategorialen Logik mit dem Konzept des adjungierten Funktors besser verstanden wurden und dass auch die Quantoren mit adjungierten Funktoren am besten verstanden wurden.
Interne Sprachen
Dies kann als Formalisierung und Verallgemeinerung des Beweises durch Diagrammverfolgung angesehen werden . Man definiert eine geeignete interne Sprache, die relevante Konstituenten einer Kategorie benennt, und wendet dann kategoriale Semantik an, um Behauptungen in einer Logik über die interne Sprache in entsprechende kategoriale Aussagen umzuwandeln. Dies war am erfolgreichsten in der Theorie der Topos , wo die interne Sprache eines Topos zusammen mit der Semantik der intuitionistischen Logik höherer Ordnung in einem Topos es ermöglicht, über die Objekte und Morphismen eines Topos nachzudenken , "als wären sie Mengen und Funktionen". Dies war erfolgreich im Umgang mit Toposen, die "Mengen" mit Eigenschaften haben, die mit der klassischen Logik nicht kompatibel sind. Ein Paradebeispiel ist Dana Scotts Modell des untypisierten Lambda-Kalküls in Form von Objekten, die sich auf ihren eigenen Funktionsraum zurückziehen. Ein anderes ist das Moggi-Hyland-Modell des Systems F durch eine interne vollständige Unterkategorie des effektiven Topos von Martin Hyland .
Term-Modell-Konstruktionen
In vielen Fällen liefert die kategoriale Semantik einer Logik eine Grundlage, um eine Entsprechung zwischen Theorien in der Logik und Instanzen einer geeigneten Kategorie herzustellen . Ein klassisches Beispiel ist die Übereinstimmung zwischen Theorien von βη - Gleichungslogik über einfach typisierten Lambda - Kalkül und cartesianischen geschlossene Kategorien . Kategorien, die sich aus Theorien über Begriffsmodellkonstruktionen ergeben, können in der Regel bis zur Äquivalenz durch eine geeignete universelle Eigenschaft charakterisiert werden . Dies hat den Beweis metatheoretischer Eigenschaften einiger Logiken durch eine geeignete kategoriale Algebra ermöglicht . Zum Beispiel Freyd gab einen Beweis für die Existenz und disjunction Eigenschaften von intuitionismus auf diese Weise.

Siehe auch

Anmerkungen

Verweise

Bücher
  • Abramski, Samson; Gabbay, Dov (2001). Handbuch der Logik in der Informatik: Logik und algebraische Methoden . Oxford: Oxford University Press. ISBN 0-19-853781-6.
  • Gabbay, Dov (2012). Handbuch der Geschichte der Logik: Mengen und Erweiterungen im zwanzigsten Jahrhundert . Oxford: Sonst. ISBN 978-0-444-51621-3.
  • Kent, Allen; Williams, James G. (1990). Enzyklopädie der Informatik und Technologie . New York: Marcel Dekker Inc. ISBN 0-8247-2272-8.
  • Barr, M. und Wells, C. (1990), Kategorie Theorie für Informatik . Hemel Hempstead , Großbritannien.
  • Lambek, J. und Scott, PJ (1986), Einführung in die kategoriale Logik höherer Ordnung . Cambridge University Press, Cambridge, Großbritannien.
  • Lawvere, FW und Rosebrugh, R. (2003), Sätze für die Mathematik . Cambridge University Press, Cambridge, Großbritannien.
  • Lawvere, FW (2000) und Schanuel, SH , Konzeptuelle Mathematik: Eine erste Einführung in Kategorien . Cambridge University Press, Cambridge, UK, 1997. Nachdruck mit Korrekturen, 2000.

Wegweisende Papiere

  • Lawvere, FW , Funktionelle Semantik algebraischer Theorien . In Proceedings of the National Academy of Sciences 50, Nr. 5 (November 1963), 869-872.
  • Lawvere, FW , Elementare Theorie der Kategorie der Mengen . In Proceedings of the National Academy of Sciences 52 , Nr. 6 (Dezember 1964), 1506-1511.
  • Lawvere, FW , Quantifizierer und Garben . In Proceedings of the International Congress on Mathematics (Nizza 1970) , Gauthier-Villars (1971) 329-334.

Weiterlesen

  • Michael Makkai und Gonzalo E. Reyes, 1977, Kategorische Logik erster Ordnung , Springer-Verlag.
  • Lambek, J. und Scott, PJ, 1986. Einführung in die kategoriale Logik höherer Ordnung . Ziemlich zugängliche Einführung, aber etwas veraltet. Der kategoriale Ansatz zur Logik höherer Ordnung über polymorphe und abhängige Typen wurde weitgehend nach der Veröffentlichung dieses Buches entwickelt.
  • Jacobs, Bart (1999). Kategoriale Logik und Typentheorie . Studium der Logik und der Grundlagen der Mathematik 141. Nordholland, Elsevier. ISBN 0-444-50170-3.Eine umfassende Monographie eines Informatikers; es deckt sowohl Logiken erster und höherer Ordnung als auch polymorphe und abhängige Typen ab. Der Fokus liegt auf der gefaserten Kategorie als universelles Werkzeug in der kategorialen Logik, das im Umgang mit polymorphen und abhängigen Typen notwendig ist.
  • John Lane Bell (2005) Die Entwicklung der kategorialen Logik . Handbuch der philosophischen Logik, Band 12. Springer. Version online verfügbar auf der Homepage von John Bell.
  • Jean-Pierre Marquis und Gonzalo E. Reyes (2012). Die Geschichte der kategorialen Logik 1963–1977 . Handbook of the History of Logic: Sets and Extensions in the Twentieth Century, Band 6, DM Gabbay, A. Kanamori & J. Woods, Hrsg., North-Holland, S. 689–800. Eine vorläufige Version ist unter [1] verfügbar .

Externe Links