Skip to main content

Institution

Was ist eine Institution?

Der Begriff Institution wurde Ende der 1970er Jahre von den Herren Joseph Goguen und Rod Burstall entwickelt. Diese Bezeichnung versucht, das Wesentliche eines logischen Systems einzufangen.

Die Verwendung einer Institution ermöglicht die Entwicklung von Konzepten für Spezifikationssprachen (zum Beispiel Strukturierung von Spezifikationen, Parametrisierung, Implementierung, Verfeinerung, Entwicklung), Korrekturkalküle und sogar Tools, die völlig unabhängig vom zugrunde liegenden logischen System liegen. Es gibt auch Morphismen, die es ermöglichen, logische Systeme zu verknüpfen und zu übersetzen. Wichtige Anwendungen hierfür sind die Weiterverwendung der logischen Struktur, heterogene Spezifikation und Kombination von Logiken.

Die Verbreitung der Institution-Modelltheorie hat verschiedene Begriffe und Ergebnisse der Modelltheorie verallgemeinert und die Institution selbst hat den Fortschritt der universellen Logik beeinflusst.

Definition

Die Theorie der Institution nimmt nichts über die Natur des logischen Systems an. Das heißt, Modelle und Sätze können beliebige Objekte sein. Die einzige Annahme ist, dass es eine Zufriedenheitsbeziehung zwischen Modellen und Sätzen gibt, die aussagt, ob ein Satz in einem Modell enthalten ist oder nicht. Zufriedenheit ist von Tarskis Wahrheitsdefinition inspiriert, kann aber tatsächlich jede binäre Beziehung sein. Ein entscheidendes Merkmal einer Institution besteht nun darin, dass Modelle, Sätze und deren Zufriedenheit immer als in einem bestimmten Vokabular oder Kontext (als Signatur genannt) bezeichnet werden, da die (nicht logischen) Symbole definiert, die in Sätzen verwendet werden können und die interpretiert werden müssen in Modellen.

Darüber hinaus erlauben Signaturmorphismen das Erweitern von Signaturen, Ändern der Notation und so weiter. Über Signaturen und Signaturmorphismen wird nichts angenommen, außer dass sie zusammengesetzt werden. Dies entspricht einer Kategorie von Signaturen und Morphismen. Schließlich wird angenommen, dass die Signaturmorphismen dazu führen, dass Sätze und Modelle so übersetzt werden, dass die Zufriedenheit erhalten bleibt. Während die Sätze zusammen mit Signaturmorphismen übersetzt werden, werden Modelle gegen Signaturmorphismen übersetzt (oder besser: reduziert).

Die Signatur kann auf ein Modell der (kleineren) Quellensignatur reduziert werden, indem nur einige Komponente des Modells vergessen werden.

Beispiele

Aussagenkalkül

Der Aussagenkalkül ist ein Zweig der Logik. Er wird auch als Aussagenkalkül, Anweisungslogik, Sentential-Kalkül/-Logik oder manchmal auch Logik nullter Ordnung bezeichnet. Er befasst sich mit Sätzen (die wahr oder falsch sein können) und dem Argumentfluss.

Logik erster Ordnung

Die Logik erster Ordnung – auch Prädikatslogik und Prädikatenkalkül erster Ordnung – ist eine Sammlung formaler Systeme, die in der Mathematik, Philosophie, Linguistik und Informatik verwendet werden.

Logik höherer Ordnung

In Mathematik und Logik ist eine Logik höherer Ordnung eine Form von Prädikatenlogik, die sich durch zusätzliche Quantifizierer und manchmal stärkere Semantik von der Logik erster Ordnung unterscheidet. Logiken höherer Ordnung mit ihrer Standardsemantik, aber ihre modelltheoretischen Eigenschaften sind weniger gut als die der Logik erster Ordnung.

Intuitionistische Logik

Intuitionistische Logik, manchmal allgemeiner als konstruktive Logik bezeichnet, bezieht sich auf die Systeme symbolischer Logik, die sich von den Systemen der klassischen Logik dadurch unterscheiden, dass sie den Begriff des konstruktiven Beweises stärker widerspiegeln. Systeme der intuitionistischen Logik enthalten insbesondere nicht das Gesetz der ausgeschlossenen Eliminierung der mittleren und doppelten Negation, die grundlegende Inferenzregeln in der klassischen Logik sind.

Sie haben noch Fragen?

Kontaktieren Sie uns

Kostenloser SEO-Check der OSG