Begründungslogik

2023 Autor: Noah Black | [email protected]. Zuletzt bearbeitet: 2023-11-26 16:05

Dies ist eine Datei im Archiv der Stanford Encyclopedia of Philosophy. Autoren- und Zitierinfo | Freunde PDF Vorschau | InPho-Suche | PhilPapers Bibliographie

Erstveröffentlichung Mi 22. Juni 2011; inhaltliche Überarbeitung Mi 20.07.2011

Sie können sagen: „Ich weiß, dass Abraham Lincoln ein großer Mann war.”Im Gegenzug werden Sie möglicherweise gefragt, woher Sie das wissen. Sie würden mit ziemlicher Sicherheit nicht semantisch im Hintikka-Stil antworten, dass Abraham Lincoln in allen Situationen groß war, die mit Ihrem Wissen vereinbar waren. Stattdessen würden Sie eher sagen: „Ich habe in mehreren Büchern über Abraham Lincolns Größe gelesen und neben anderen Menschen Fotos von ihm gesehen. „Man bescheinigt Wissen, indem man einen Grund, eine Rechtfertigung angibt. Die Hintikka-Semantik erfasst Wissen als wahren Glauben. Die Rechtfertigungslogik liefert die fehlende dritte Komponente von Platons Charakterisierung des Wissens als gerechtfertigten wahren Glauben.

1. Warum Begründungslogik?
- 1.1 Epistemische Tradition
- 1.2 Tradition der mathematischen Logik
2. Die Grundkomponenten der Rechtfertigungslogik
- 2.1 Die Sprache der Rechtfertigungslogik
- 2.2 Grundlegende Begründungslogik J ₀
- 2.3 Logisches Bewusstsein und konstante Spezifikationen
- 2.4 Faktivität
- 2.5 Positive Selbstbeobachtung
- 2.6 Negative Selbstbeobachtung
3. Semantik
- 3.1 Mögliche weltweite Rechtfertigungsmodelle für J.
- 3.2 Schwache und starke Vollständigkeit
- 3.3 Die Single-Agent-Familie
- 3.4 Single World Justification Models
4. Realisierungssätze
5. Verallgemeinerungen
- 5.1 Explizites und implizites Wissen mischen
- 5.2 Mögliche weltweite Rechtfertigungsmodelle für mehrere Agenten
6. Russells Beispiel: Induzierte Faktivität
7. Selbstreferenzialität von Rechtfertigungen
8. Quantifizierer in der Begründungslogik
9. Historische Notizen
Literaturverzeichnis
Akademische Werkzeuge
Verwandte Einträge
Andere Internetquellen

1. Warum Begründungslogik?

Rechtfertigungslogiken sind epistemische Logiken, die es ermöglichen, Wissens- und Glaubensmodalitäten in Rechtfertigungsbegriffe zu „entfalten“: Anstelle von □ X schreibt man t: X und liest es als „X ist durch den Grund t gerechtfertigt“. Man kann sich traditionelle Modaloperatoren als implizite Modalitäten und Begründungsbegriffe als ihre expliziten Ausarbeitungen vorstellen, die die Modallogik durch feinkörnigere epistemische Maschinen ergänzen. Die Familie der Begründungsbegriffe hat Struktur und Funktionsweise. Die Wahl der Operationen führt zu unterschiedlichen Begründungslogiken. Für alle gängigen epistemischen Logiken können ihre Modalitäten vollständig in eine explizite Rechtfertigungsform gebracht werden. In dieser Hinsicht enthüllt und verwendet die Rechtfertigungslogik den expliziten, aber verborgenen Inhalt der traditionellen epistemischen Modallogik.

Die Begründungslogik entstand als Teil eines erfolgreichen Projekts zur Bereitstellung einer konstruktiven Semantik für intuitionistische Begründungsbegriffe, die alle bis auf die grundlegendsten Merkmale mathematischer Beweise abstrahierten. Beweise sind Rechtfertigungen in vielleicht ihrer reinsten Form. Anschließend wurden Begründungslogiken in die formale Erkenntnistheorie eingeführt. Dieser Artikel beschreibt den allgemeinen Bereich der derzeit verstandenen Rechtfertigungslogik. Es werden ihre Beziehungen zu herkömmlichen Modallogiken erörtert. Neben technischen Maschinen wird in dem Artikel untersucht, inwiefern die Verwendung expliziter Begründungsbegriffe eine Reihe traditioneller philosophischer Probleme beleuchtet. Das Thema als Ganzes befindet sich noch in der aktiven Entwicklung. Was hier präsentiert wird, ist eine Momentaufnahme davon zum Zeitpunkt des Schreibens.

Die Wurzeln der Rechtfertigungslogik lassen sich auf viele verschiedene Quellen zurückführen, von denen zwei ausführlich erörtert werden: Erkenntnistheorie und mathematische Logik.

1.1 Epistemische Tradition

Die Eigenschaften von Wissen und Glauben sind zumindest seit von Wright und Hintikka (Hintikka 1962, von Wright 1951) Gegenstand formaler Logik. Wissen und Glaube werden beide auf eine Weise als Modalitäten behandelt, die heute sehr vertraut ist - epistemische Logik. Aber von Platons drei Kriterien für Wissen, gerechtfertigt, wahr, Glaube (Gettier 1963, Hendricks 2005), funktioniert die epistemische Logik wirklich nur mit zwei von ihnen. Mögliche Welten und Ununterscheidbarkeitsmodell glauben - man glaubt, was unter allen Umständen für möglich gehalten wird. Faktizität bringt eine Richtigkeitskomponente ins Spiel - wenn etwas in der tatsächlichen Welt nicht so ist, kann es nicht erkannt, sondern nur geglaubt werden. Es gibt jedoch keine Darstellung für die Rechtfertigungsbedingung. Dennoch,Der modale Ansatz war bemerkenswert erfolgreich bei der Entwicklung einer umfassenden mathematischen Theorie und Anwendung (Fagin, Halpern, Moses und Vardi 1995, van Ditmarsch, van der Hoek und Kooi 2007). Trotzdem ist es nicht das ganze Bild.

Die modale Herangehensweise an die Logik des Wissens basiert gewissermaßen auf dem universellen Quantifizierer: X ist in einer Situation bekannt, in der X in allen Situationen wahr ist, die von dieser nicht zu unterscheiden sind. Begründungen hingegen bringen einen existenziellen Quantifizierer ins Bild: X ist in einer Situation bekannt, wenn in dieser Situation eine Begründung für X vorliegt. Diese universelle / existenzielle Dichotomie ist Logikern vertraut - in formalen Logiken gibt es einen Beweis für eine Formel X, wenn und nur wenn X in allen Modellen für die Logik wahr ist. Man betrachtet Modelle als inhärent nicht konstruktiv und Beweise als konstruktive Dinge. Man wird nicht viel falsch machen, wenn man an Rechtfertigungen im Allgemeinen genauso denkt wie an mathematische Beweise. In der Tat wurde die erste Rechtfertigungslogik explizit entwickelt, um mathematische Beweise in der Arithmetik zu erfassen.etwas, das in Abschnitt 1.2 weiter besprochen wird.

In der Begründungslogik gibt es neben der Kategorie der Formeln eine zweite Kategorie von Begründungen. Begründungen sind formale Begriffe, die aus Konstanten und Variablen unter Verwendung verschiedener Operationssymbole aufgebaut sind. Konstanten stellen Rechtfertigungen für allgemein akzeptierte Wahrheiten dar - typisch Axiome. Variablen bezeichnen nicht spezifizierte Begründungen. Unterschiedliche Begründungslogiken unterscheiden sich darin, welche Operationen zulässig sind (und auch auf andere Weise). Wenn t ein Begründungsterm und X eine Formel ist, ist t: X eine Formel und soll gelesen werden:

t ist eine Rechtfertigung für X.

Eine Operation, die allen Rechtfertigungslogiken gemeinsam ist, ist die Anwendung, die wie eine Multiplikation geschrieben ist. Die Idee ist, wenn s eine Rechtfertigung für A → B ist und t eine Rechtfertigung für A ist, dann ist [s ⋅ t] eine Rechtfertigung für B ^[1]. Das heißt, die Gültigkeit von Folgendem wird allgemein angenommen:

(1)	s:(A → B) → (t: A → [s ⋅ t]: B).

Dies ist die explizite Version der üblichen Verteilung von Wissensoperatoren und Modaloperatoren im Allgemeinen über alle Implikationen hinweg:

(2)	□ (A → B) → (□ A → □ B).

Tatsächlich steckt Formel (2) hinter vielen Problemen der logischen Allwissenheit. Es wird behauptet, dass ein Agent alles weiß, was durch das Wissen des Agenten impliziert wird. Während im Prinzip Erkennbarkeit, Konsequenz, unter Konsequenz geschlossen wird, kann dies nicht für eine plausible Version des tatsächlichen Wissens gesagt werden. Die Unterscheidung zwischen (1) und (2) kann in einer Diskussion des paradigmatischen Red Barn-Beispiels von Goldman und Kripke ausgenutzt werden; Hier ist eine vereinfachte Version der Geschichte aus (Dretske 2005).

Angenommen, ich fahre durch ein Viertel, in dem ohne mein Wissen Pappmaché-Scheunen verstreut sind, und ich sehe, dass das Objekt vor mir eine Scheune ist. Weil ich Scheunen vor mir habe, glaube ich, dass das Objekt vor mir eine Scheune ist. Unsere Intuitionen legen nahe, dass ich die Scheune nicht kenne. Aber jetzt nehmen wir an, dass die Nachbarschaft keine falschen roten Scheunen hat, und ich bemerke auch, dass das Objekt vor mir rot ist, also weiß ich, dass eine rote Scheune da ist. Diese Gegenüberstellung, eine rote Scheune zu sein, die ich kenne, führt dazu, dass es eine Scheune gibt, was ich nicht tue, „ist eine Verlegenheit“.

In der ersten Formalisierung des Red Barn-Beispiels wird die logische Ableitung in einer grundlegenden Modallogik durchgeführt, in der □ als "Glaubens" -Modalität interpretiert wird. Dann werden einige der Vorkommen von □ gemäß der Problembeschreibung extern als „Wissen“interpretiert. Sei B der Satz "das Objekt vor mir ist eine Scheune" und sei R der Satz "das Objekt vor mir ist rot".

□ B, 'Ich glaube, dass das Objekt vor mir eine Scheune ist'
□ (B ∧ R), 'Ich glaube, dass das Objekt vor mir eine rote Scheune ist'.

Auf der Metalebene ist 2 tatsächlich Wissen, während nach der Problembeschreibung 1 kein Wissen ist.

□ (B ∧ R → B), eine Wissensbehauptung eines logischen Axioms

Innerhalb dieser Formalisierung scheint der epistemische Verschluss in seiner modalen Form (2) verletzt zu sein: Zeile 2, □ (B ∧ R) und Zeile 3, □ (B ∧ R → B) sind Fälle von Wissen, während □ B (Zeile) 1) ist kein Wissen. Die modale Sprache hier scheint nicht zur Lösung dieses Problems beizutragen.

Betrachten Sie als nächstes das Beispiel der Roten Scheune in der Begründungslogik, in dem t: F als "Ich glaube F aus Grund t" interpretiert wird. Sei u eine spezifische individuelle Rechtfertigung für den Glauben, dass B und v für den Glauben, dass B ∧ R. Außerdem sei a eine Rechtfertigung für die logische Wahrheit B ∧ R → B. Dann ist die Liste der Annahmen:

u: B, 'u ist ein Grund zu der Annahme, dass das Objekt vor mir eine Scheune ist'
v:(B ∧ R), 'v ist ein Grund zu der Annahme, dass das Objekt vor mir eine rote Scheune ist'
a:(B ∧ R → B).

Auf der Metaebene besagt die Problembeschreibung, dass 2 und 3 Fälle von Wissen und nicht nur Glaube sind, während 1 Glaube ist, der kein Wissen ist. So lautet die formale Argumentation:

a:(B ∧ R → B) → (v:(B ∧ R) → [a ⋅ v]: B) nach Prinzip (1);
v:(B ∧ R) → [a ⋅ v]: B von 3 und 4 nach Aussagenlogik;
[a ⋅ v]: B aus 2 und 5 nach Aussagenlogik.

Beachten Sie, dass Schlussfolgerung 6 [a ⋅ v]: B und nicht u: B ist; epistemischer Verschluss gilt. Durch Argumentation in der Begründungslogik wurde der Schluss gezogen, dass [a ⋅ v]: B ein Fall von Wissen ist, dh 'Ich kenne B aus Grund a ⋅ v'. Die Tatsache, dass u: B kein Wissensfall ist, beeinträchtigt das Schließungsprinzip nicht, da letzteres Wissen speziell für [a ⋅ v]: B beansprucht. Nachdem ich eine rote Fassade beobachtet habe, kenne ich zwar B, aber dieses Wissen hat nichts mit 1 zu tun, was eher ein Fall von Glauben als von Wissen bleibt. Die Formalisierung der Rechtfertigungslogik repräsentiert die Situation fair.

Die Verfolgung von Begründungen stellt die Struktur des Red Barn-Beispiels auf eine Weise dar, die von herkömmlichen epistemischen Modalwerkzeugen nicht erfasst wird. Die Formalisierung der Rechtfertigungslogik modelliert, was in einem solchen Fall zu geschehen scheint. Die Schließung des Wissens unter logischer Konsequenz bleibt erhalten, obwohl "Scheune" nicht wahrnehmbar bekannt ist. ^[2]

1.2 Tradition der mathematischen Logik

Nach Brouwer bedeutet Wahrheit in der konstruktiven (intuitionistischen) Mathematik die Existenz eines Beweises, vgl. (Troelstra und van Dalen 1988). In den Jahren 1931–34 gaben Heyting und Kolmogorov eine informelle Beschreibung der beabsichtigten beweisbasierten Semantik für die intuitionistische Logik (Kolmogorov 1932, Heyting 1934), die heute als Brouwer-Heyting-Kolmogorov (BHK) -Semantik bezeichnet wird. Gemäß den BHK-Bedingungen ist eine Formel "wahr", wenn sie einen Beweis hat. Darüber hinaus ist ein Beweis einer zusammengesetzten Aussage auf folgende Weise mit Beweisen seiner Komponenten verbunden:

ein Beweis von A ∧ B besteht aus einem Beweis von Satz A und einem Beweis von Satz B;
ein Beweis von A ∨ B wird gegeben, indem entweder ein Beweis von A oder ein Beweis von B vorgelegt wird;
ein Beweis von A → B ist eine Konstruktion, die Beweise von A in Beweise von B umwandelt;
Falschheit ⊥ ist ein Satz, der keinen Beweis hat, ¬ A ist eine Abkürzung für A → ⊥.

Kolmogorov schlug ausdrücklich vor, dass die beweisähnlichen Objekte in seiner Interpretation („Problemlösungen“) aus der klassischen Mathematik stammen (Kolmogorov 1932). In der Tat ist es aus grundlegender Sicht wenig sinnvoll, die oben genannten „Beweise“als Beweise in einem intuitionistischen System zu verstehen, das diese Bedingungen spezifizieren sollen.

Der grundlegende Wert der BHK-Semantik besteht darin, dass sie informell, aber eindeutig vorschlägt, Rechtfertigungen, hier mathematische Beweise, als Objekte mit Operationen zu behandeln.

In (Gödel 1933) unternahm Gödel den ersten Schritt zur Entwicklung einer rigorosen beweisbasierten Semantik für den Intuitionismus. Gödel betrachtete die klassische Modallogik S4 als einen Kalkül, der die Eigenschaften der Beweisbarkeit beschreibt:

Axiome und Regeln der klassischen Aussagenlogik;
□ (F → G) → (□ F → □ G);
□ F → F;
□ F → □□ F;
Notwendigkeitsregel: Wenn ⊢ F, dann ⊢ □ F.

Basierend auf Brouwers Verständnis der logischen Wahrheit als Beweisbarkeit definierte Gödel eine Übersetzung tr (F) der Satzformel F in der intuitionistischen Sprache in die Sprache der klassischen Modallogik: tr (F) wird erhalten, indem jeder Subformel von F die Beweisbarkeit vorangestellt wird Modalität □. Informell gesehen wird, wenn das übliche Verfahren zur Bestimmung der klassischen Wahrheit einer Formel auf tr (F) angewendet wird, die Beweisbarkeit (nicht die Wahrheit) jeder der Subformeln von F in Übereinstimmung mit Brouwers Ideen getestet. Aus Gödels Ergebnissen und der McKinsey-Tarski-Arbeit zur topologischen Semantik für die Modallogik folgt, dass die Übersetzung tr (F) eine korrekte Einbettung des Intuitionistic Propositional Calculus (IPC) in S4 liefert, dh eine Einbettung der intuitionistischen Logik in die klassische Logik vom Nachweisbarkeitsbetreiber erweitert.

(3)	Wenn IPC F beweist, beweist S4 tr (F).

Dennoch wurde Gödels ursprüngliches Ziel, die intuitionistische Logik in Bezug auf die klassische Beweisbarkeit zu definieren, nicht erreicht, da die Verbindung von S4 mit dem üblichen mathematischen Begriff der Beweisbarkeit nicht hergestellt wurde. Darüber hinaus stellte Gödel fest, dass die einfache Idee, die Modalität □ F als F in einem gegebenen formalen System T zu interpretieren, dem zweiten Unvollständigkeitssatz von Gödel widersprach. Tatsächlich kann □ (□ F → F) in S4 durch die Regel der Notwendigkeit aus dem Axiom □ F → F abgeleitet werden. Andererseits wandelt die Interpretation der Modalität □ als Prädikat der formalen Beweisbarkeit in Theorie T und F als Widerspruch diese Formel in eine falsche Aussage um, dass die Konsistenz von T in T intern nachweisbar ist.

Die Situation nach (Gödel 1933) kann durch die folgende Abbildung beschrieben werden, in der 'X ↪ Y' als 'X wird in Y interpretiert' gelesen werden sollte.

IPC ↪ S4 ↪? ↪ KLASSISCHE BEWEISE

In einem öffentlichen Vortrag in Wien im Jahr 1938 stellte Gödel fest, dass unter Verwendung des Formats expliziter Beweise:

(4)	t ist ein Beweis von F.

kann bei der Interpretation seines Beweisbarkeitskalküls S4 helfen (Gödel 1938). Leider blieb Gödels Werk (Gödel 1938) bis 1995 unveröffentlicht. Zu diesem Zeitpunkt war die Gödelsche Logik der expliziten Beweise bereits wiederentdeckt und als Logic of Proofs LP axiomatisiert und mit Vollständigkeitssätzen versehen, die sie sowohl mit S4 als auch mit klassischen Beweisen verbinden (Artemov) 1995).

Die Logic of Proofs LP wurde die erste in der Justification Logic-Familie. Beweisbegriffe in LP sind nichts anderes als BHK-Begriffe, die als klassische Beweise verstanden werden. Mit LP erhielt die propositionale intuitionistische Logik die gewünschte strenge BHK-Semantik:

IPC ↪ S4 ↪ LP ↪ KLASSISCHE BEWEISE

Weitere Informationen zur Tradition der mathematischen Logik finden Sie in Abschnitt 1 des ergänzenden Dokuments Some More Technical Matters.

2. Die Grundkomponenten der Rechtfertigungslogik

In diesem Abschnitt werden die Syntax und Axiomatik der gängigsten Systeme der Rechtfertigungslogik vorgestellt.

2.1 Die Sprache der Rechtfertigungslogik

Um eine formale Darstellung der Rechtfertigungslogik zu erstellen, muss eine grundlegende strukturelle Annahme getroffen werden: Rechtfertigungen sind abstrakte Objekte, auf denen Struktur und Operationen basieren. Ein gutes Beispiel für Rechtfertigungen sind formale Beweise, die seit langem Gegenstand mathematischer Logik und Informatik sind (vgl. Abschnitt 1.2).

Die Rechtfertigungslogik ist ein formaler logischer Rahmen, der epistemische Aussagen t: F enthält und für 't eine Rechtfertigung für F' steht. Die Begründungslogik analysiert nicht direkt, was es für t bedeutet, F über das Format t: F hinaus zu rechtfertigen, sondern versucht, diese Beziehung axiomatisch zu charakterisieren. Dies ähnelt der Art und Weise, wie die Boolesche Logik ihre Konnektiva behandelt, beispielsweise die Disjunktion: Sie analysiert nicht die Formel p ∨ q, sondern nimmt bestimmte logische Axiome und Wahrheitstabellen zu dieser Formel an.

Es werden mehrere Entwurfsentscheidungen getroffen. Begründungslogik beginnt mit der einfachsten Basis: der klassischen Booleschen Logik, und das aus guten Gründen. Begründungen stellen selbst auf einfachster Ebene eine hinreichend ernsthafte Herausforderung dar. Die paradigmatischen Beispiele von Russell, Goldman-Kripke, Gettier und anderen können mit Boolean Justification Logic behandelt werden. Der Kern der epistemischen Logik besteht aus modalen Systemen mit einer klassischen booleschen Basis (K, T, K4, S4, K45, KD45, S5 usw.), und jedem von ihnen wurde ein entsprechender Begleitlogik-Begleiter bereitgestellt, der auf der booleschen Logik basiert. Schließlich wird nicht immer davon ausgegangen, dass Rechtfertigungen sachlich sind. Dies ermöglicht es, das Wesentliche von erkenntnistheoretischen Diskussionen zu erfassen, bei denen es um Glaubensfragen und nicht um Wissensfragen geht.

Die grundlegende Operation für Rechtfertigungen sind Anwendung und Summe. Die Anwendungsoperation nimmt die Begründungen s und t und erzeugt eine Begründung s ⋅ t, so dass, wenn s:(F → G) und t: F, dann [s ⋅ t]: G. Symbolisch

s:(F → G) → (t: F → [s ⋅ t]: G)

Dies ist eine grundlegende Eigenschaft von Rechtfertigungen, die in kombinatorischer Logik und λ-Kalkül (Troelstra und Schwichtenberg 1996), Brouwer-Heyting-Kolmogorov-Semantik (Troelstra und van Dalen 1988), Kleene-Realisierbarkeit (Kleene 1945), der Logik der Beweise LP usw..

Zwei beliebige Begründungen können sicher zu etwas mit einem breiteren Anwendungsbereich kombiniert werden. Dies erfolgt mit der Operationssumme '+'. Wenn s: F, dann bleibt der kombinierte Beweis s + t, was auch immer Beweis t sein mag, eine Rechtfertigung für F. Genauer gesagt nimmt die Operation '+' die Rechtfertigungen s und t und erzeugt s + t, was eine Rechtfertigung für alles ist, was durch s oder durch t gerechtfertigt ist.

s: F → [s + t]: F und t: F → [s + t]: F.

Als Motivation könnte man sich s und t als zwei Bände einer Enzyklopädie und s + t als die Menge dieser beiden Bände vorstellen. Stellen Sie sich vor, einer der Bände, z. B. s, enthält eine ausreichende Begründung für einen Satz F, dh s: F ist der Fall. Dann enthält die größere Menge s + t auch eine ausreichende Begründung für F, [s + t]: F. In der Logic of Proofs LP, Abschnitt 1.2, kann 's + t' als Verkettung der Beweise s und t interpretiert werden.

2.2 Grundlegende Begründungslogik J ₀

Begründungsbegriffe werden aus den Begründungsvariablen x, y, z, … und den Begründungskonstanten a, b, c, … (mit Indizes i = 1, 2, 3, …, die weggelassen werden, wenn es sicher ist) mittels der Operationen erstellt. ⋅ 'und' + '. Ausführlichere Logiken, die im Folgenden betrachtet werden, ermöglichen auch zusätzliche Operationen für Rechtfertigungen. Konstanten bezeichnen atomare Rechtfertigungen, die das System nicht analysiert; Variablen bezeichnen nicht spezifizierte Begründungen. Die Grundlogik der Rechtfertigungen, J _0, wird durch Folgendes axiomatisiert.

Klassische Logik

Klassische Satzaxiome und die Regel Modus Ponens

Anwendung Axiom

s:(F → G) → (t: F → [s ⋅ t]: G),

Summenaxiome

s: F → [s + t]: F, s: F → [t + s]: F.

J ₀ ist die Logik allgemeiner (nicht unbedingt faktischer) Rechtfertigungen für einen absolut skeptischen Agenten, für den keine Formel nachweislich gerechtfertigt ist, dh J ₀ leitet t: F für kein t und F ab. Ein solches Mittel ist jedoch in der Lage, relative Rechtfertigungsschlussfolgerungen der Form zu ziehen

Wenn x: A, y: B,…, z: C halten, dann t: F.

Mit dieser Kapazität kann J ₀ andere Justification Logic-Systeme in seiner Sprache angemessen emulieren.

2.3 Logisches Bewusstsein und konstante Spezifikationen

Das Prinzip des logischen Bewusstseins besagt, dass logische Axiome von Amts wegen gerechtfertigt sind: Ein Agent akzeptiert logische Axiome als gerechtfertigt (einschließlich derjenigen, die Rechtfertigungen betreffen). Wie bereits erwähnt, kann das logische Bewusstsein in einigen epistemischen Situationen zu stark sein. Die Begründungslogik bietet jedoch den flexiblen Mechanismus der konstanten Spezifikationen, um unterschiedliche Schattierungen des logischen Bewusstseins darzustellen.

Natürlich unterscheidet man zwischen einer Annahme und einer berechtigten Annahme. In der Begründung werden Logikkonstanten verwendet, um Begründungen von Annahmen in Situationen darzustellen, in denen sie nicht weiter analysiert werden. Angenommen, es ist zu postulieren, dass ein Axiom A für den Wissenden gerechtfertigt ist. Man postuliert einfach e ₁: A für einige Beweiskonstanten e ₁ (mit Index 1). Wenn weiterhin postuliert werden soll, dass dieses neue Prinzip e ₁: A ebenfalls gerechtfertigt ist, kann man e ₂:(e ₁: A) für eine Konstante e ₂ postulieren(mit Index 2). Und so weiter. Das Verfolgen von Indizes ist nicht erforderlich, aber einfach und hilft bei Entscheidungsverfahren (Kuznets 2008). Die Menge aller Annahmen dieser Art für eine gegebene Logik wird als konstante Spezifikation bezeichnet. Hier ist die formale Definition:

Eine konstante Spezifikation CS für eine gegebene Rechtfertigungslogik L ist eine Menge von Formeln der Form

e _n: e _{n −1}:…: e ₁: A (n ≥ 1),

wobei A ein Axiom von L ist und e ₁, e ₂,…, e _n ähnliche Konstanten mit den Indizes 1, 2,…, n sind. Es wird angenommen, dass CS alle Zwischenspezifikationen enthält, dh wann immer e _n: e _{n −1}:…: e ₁: A in CS ist, dann ist e _{n −1}:…: e ₁: A auch in CS.

Es gibt eine Reihe von besonderen Bedingungen, die in der Literatur für konstante Spezifikationen gelten. Die folgenden sind die häufigsten.

Leer

CS = ∅. Dies entspricht einem absolut skeptischen Agenten. Es läuft darauf hinaus, mit der Logik J _{0 zu arbeiten}.

Endlich

CS ist eine endliche Menge von Formeln. Dies ist ein vollständig repräsentativer Fall, da jede spezifische Ableitung in der Begründungslogik nur eine endliche Menge von Konstanten umfasst.

Axiomatisch angemessen

Jedes Axiom, einschließlich derjenigen, die durch die konstante Spezifikation selbst neu erworben wurden, hat Rechtfertigungen. In der formalen Einstellung gibt es für jedes Axiom A eine Konstante e _1, so dass e ₁: A in CS ist, und wenn e _n: e _{n −1}:…: e ₁: A ∈ CS, dann ist e _{n +1}: e _n: e _{n −1}:…: e ₁: A ∈ CS für jedes n ≥ 1. Axiomatisch geeignete konstante Spezifikationen sind erforderlich, um die am Ende dieses Abschnitts beschriebene Internalisierungseigenschaft sicherzustellen.

Gesamt

Für jedes Axiom A und alle Konstanten e ₁, e ₂,… e _n,

e _n: e _{n −1}:…: e ₁: A ∈ CS.

Der Name TCS ist für die Gesamtkonstantenspezifikation (für eine bestimmte Logik) reserviert. Natürlich ist die Gesamtkonstantenspezifikation axiomatisch angemessen.

Wir können jetzt spezifizieren:

Rechtfertigungslogik mit gegebener konstanter Spezifikation:

Sei CS eine konstante Spezifikation. J _CS ist die Logik J ₀ + CS; Die Axiome sind die von J ₀ zusammen mit den Mitgliedern von CS, und die einzige Inferenzregel ist Modus Ponens. Beachten Sie, dass J ₀ J _{∅ ist}.

Rechtfertigungslogik

J ist die Logik J ₀ + Axiom-Internalisierungsregel. Die neue Regel lautet:

Für jedes Axiom A und alle Konstanten e ₁, e ₂,…, e _n schließen Sie e _n: e _{n −1}:…: e ₁: A.

Letzteres verkörpert die Idee eines uneingeschränkten logischen Bewusstseins für J. Eine ähnliche Regel erschien in der LP Logic of Proofs und wurde auch in Goldmans (Goldman 1967) vorweggenommen. Das logische Bewusstsein, ausgedrückt durch axiomatisch geeignete konstante Spezifikationen, ist eine explizite Inkarnation der Erforderungsregel in der Modallogik: ⊢ F ⇒ ⊢ □ F, jedoch auf Axiome beschränkt. Beachten Sie, dass J mit J _TCS übereinstimmt.

Das Hauptmerkmal von Justification Logic-Systemen ist ihre Fähigkeit, ihre eigenen Ableitungen als nachweisbare Rechtfertigungsaussagen in ihren Sprachen zu verinnerlichen. Diese Eigenschaft wurde in (Gödel 1938) erwartet.

Satz 1: Für jede axiomatisch geeignete konstante Spezifikation _CS genießt J _CS die Internalisierung:

Wenn ⊢ F, dann ⊢ p: F für einen Begründungsterm p.

Beweis. Induktion auf Ableitungslänge. Angenommen, ⊢ F. Wenn F ein Mitglied von J ₀ oder ein Mitglied von CS ist, gibt es eine Konstante e _n (wobei n 1 sein könnte), so dass e _n: F in CS ist, da CS axiomatisch angemessen ist. Dann ist _en: F ableitbar. Wenn F durch Modus Ponens aus X → F und X erhalten wird, dann ist nach der Induktionshypothese ⊢ s:(X → F) und ⊢ t: X für einige s, t. Verwenden des Anwendungsaxioms, [s ⋅ t]: F.

In Abschnitt 2 des ergänzenden Dokuments Some More Technical Matters finden Sie Beispiele für konkrete syntaktische Ableitungen in der Begründungslogik.

2.4 Faktivität

Die Faktivität besagt, dass Rechtfertigungen ausreichen, damit ein Agent auf die Wahrheit schließen kann. Dies ist im Folgenden dargestellt.

Faktivitätsaxiom t: F → F.

Das Faktivitätsaxiom hat eine ähnliche Motivation wie das Wahrheitsaxiom der epistemischen Logik, □ F → F, das allgemein als grundlegende Eigenschaft des Wissens akzeptiert wird.

Im Gegensatz zu den Grundsätzen der Anwendung und der Summe ist die Faktizität von Rechtfertigungen in grundlegenden Begründungslogiksystemen nicht erforderlich, wodurch sie in der Lage sind, sowohl teilweise als auch faktische Rechtfertigungen darzustellen. Das Faktivitätsaxiom erschien in der Logic of Proofs LP, Abschnitt 1.2, als Hauptmerkmal mathematischer Beweise. In dieser Einstellung ist Faktivität eindeutig gültig: Wenn es einen mathematischen Beweis t für F gibt, muss F wahr sein.

Das Faktivitätsaxiom wird für Rechtfertigungen übernommen, die zu Wissen führen. Faktizität allein rechtfertigt jedoch kein Wissen, wie die Gettier-Beispiele (Gettier 1963) gezeigt haben.

Logik faktischer Rechtfertigungen

JT ₀ = J ₀ + Faktivität;

JT = J + Faktorität.

Systeme JT _CS, die den Konstantenspezifikationen _CS entsprechen, sind wie in Abschnitt 2.3 definiert.

2.5 Positive Selbstbeobachtung

Eines der gemeinsamen Prinzipien des Wissens ist das Erkennen von Wissen und das Wissen, dass man weiß. In einer modalen Einstellung entspricht dies □ F → □□ F. Dieses Prinzip hat ein adäquates explizites Gegenstück: Die Tatsache, dass ein Agent t als ausreichenden Beweis für F akzeptiert, dient als ausreichender Beweis für t: F. Oft haben solche „Meta-Beweise“eine physische Form: einen Schiedsrichterbericht, der bestätigt, dass ein Beweis in einem Papier korrekt ist; eine Computerüberprüfungsausgabe mit einem formalen Beweis t von F als Eingabe; ein formaler Beweis, dass t ein Beweis für F usw. ist. Eine positive Introspektionsoperation '!' kann zu diesem Zweck der Sprache hinzugefügt werden; man nimmt dann an, dass der Agent bei gegebenem t eine Rechtfertigung liefert! t von t: F so dass t: F →! t:(t: F). Positive Introspektion in dieser operativen Form erschien zuerst in der Logic of Proofs LP.

Axiom der positiven Selbstbeobachtung: t: F →! t:(t: F).

Wir definieren dann:

J4: = J + positive Selbstbeobachtung;
LP: = JT + positive Selbstbeobachtung. ^[3]

Die Logiken J4 ₀, J4 _CS, LP ₀ und LP _CS werden auf natürliche Weise definiert (vgl. Abschnitt 2.3). Das direkte Analogon von Satz 1 gilt auch für J4 _CS und LP _CS.

In Gegenwart des Axioms der positiven Introspektion kann man den Geltungsbereich der Axiom-Internalisierungsregel auf die Internalisierung von Axiomen beschränken, die nicht die Form e: A haben. So wurde es in LP gemacht: Axiom Internalization kann dann mit !! emuliert werden. e:(! e:(e: A)) anstelle von e ₃:(e ₂:(e ₁: A)) usw. Der Begriff der konstanten Spezifikation kann auch entsprechend vereinfacht werden. Solche Änderungen sind geringfügig und wirken sich nicht auf die Hauptsätze und Anwendungen der Rechtfertigungslogik aus.

2.6 Negative Selbstbeobachtung

(Pacuit 2006, Rubtsova 2006) betrachteten die negative Introspektionsoperation als '?' Dies bestätigt, dass eine gegebene Begründung falsch ist. Eine mögliche Motivation für die Prüfung einer solchen Operation ist, dass die positive Selbstbeobachtungsoperation '!' kann durchaus als in der Lage angesehen werden, schlüssige Überprüfungsurteile über die Gültigkeit von Rechtfertigungsbehauptungen t: F abzugeben. Wenn also t keine Rechtfertigung für F ist, kann ein solches '!' sollte daraus schließen, dass ¬ t: F. Dies ist normalerweise bei Computer-Proof-Verifizierern, Proof-Prüfern in formalen Theorien usw. der Fall. Diese Motivation ist jedoch nuanciert: Die Beispiele für Proof-Verifizierer und Proof-Prüfer arbeiten sowohl mit t als auch mit F als Eingaben, während das Pacuit-Rubtsova-Format? t schlägt vor, dass die einzige Eingabe für '?' ist eine Rechtfertigung t und das Ergebnis? t soll Sätze rechtfertigen ¬ t:F gleichmäßig für alle F s, für die t: F nicht gilt. Eine solche Operation '?' existiert für formale mathematische Beweise seitdem nicht mehr? t sollte dann ein einziger Beweis für unendlich viele Sätze sein: t: F, was unmöglich ist.

Negatives Introspektionsaxiom ¬ t: F →? t: (¬ t: F)

Wir definieren die Systeme:

J45 = J4 + negative Selbstbeobachtung;
JD45 = J45 + ¬ t: ⊥;
JT45 = J45 + Faktivität

und erweitern Sie diese Definitionen natürlich auf J45 _CS, JD45 _CS und JT45 _CS. Das direkte Analogon von Satz 1 gilt für J45 _CS, JD45 _CS und JT45 _CS.

3. Semantik

Die heute übliche Semantik für die Rechtfertigungslogik stammt aus (Fitting 2005). Die verwendeten Modelle werden in der Literatur allgemein als Anpassungsmodelle bezeichnet, werden hier jedoch als mögliche weltweite Rechtfertigungsmodelle bezeichnet. Mögliche Weltbegründungsmodelle sind eine Mischung aus der bekannten möglichen Weltsemantik für die Logik von Wissen und Glauben aufgrund von Hintikka und Kripke mit Maschinen, die für Rechtfertigungsbegriffe spezifisch sind und von Mkrtychev in (Mkrtychev 1997) eingeführt wurden (vgl. Abschnitt 3.4).

3.1 Mögliche weltweite Rechtfertigungsmodelle für J

Um genau zu sein, muss eine Semantik für J _{CS definiert werden}, wobei CS eine konstante Spezifikation ist. Formal ist ein mögliches Modell der Weltbegründungslogik für J _CS eine Struktur M = ⟨G, R, E, V⟩. Davon ist ⟨G, R⟩ ein Standard-K-Rahmen, wobei G eine Menge möglicher Welten ist und R eine binäre Beziehung dazu ist. V ist eine Abbildung von Satzvariablen auf Teilmengen von G, die die atomare Wahrheit in möglichen Welten spezifiziert.

Der neue Gegenstand ist E, eine Beweisfunktion, die ihren Ursprung in (Mkrtychev 1997) hat. Dies ordnet Begründungsbegriffe und Formeln Mengen von Welten zu. Die intuitive Idee ist, wenn die mögliche Welt Γ in E (t, X) ist, dann ist t ein relevanter oder zulässiger Beweis für X in der Welt Γ. Relevante Beweise sollten nicht als schlüssig angesehen werden. Stellen Sie sich das eher als Beweismittel vor, die vor Gericht zugelassen werden können: Dieses Zeugnis, dieses Dokument sollte von einer Jury geprüft werden, ist relevant, aber etwas, dessen wahrheitsbestimmender Status noch zu prüfen ist. Beweisfunktionen müssen bestimmte Bedingungen erfüllen, diese werden jedoch etwas später erläutert.

Bei einem J _CS -Modell der möglichen Weltbegründung M = ⟨G, R, E, V⟩ wird die Wahrheit der Formel X in der möglichen Welt Γ mit M, Γ Γ X bezeichnet und muss die folgenden Standardbedingungen erfüllen:

Für jedes Γ Γ G:

M, Γ Γ P iff Γ Γ V (P) für P ein Satzbuchstabe;

es ist nicht der Fall, dass M, Γ Γ ⊥;

M, Γ Γ X → Y, wenn es nicht der Fall ist, dass M, Γ Γ X oder M, Γ Γ Y.

Diese sagen nur, dass die atomare Wahrheit willkürlich spezifiziert ist und dass sich aussagekräftige Verknüpfungen in jeder Welt wahrheitsfunktional verhalten. Der Schlüsselpunkt ist der nächste.

M, Γ Γ (t: X) genau dann, wenn Γ Γ E (t, X) und für jedes Δ ∈ G mit Γ R Δ haben wir M, Δ ⊩ X

Dieser Zustand besteht aus zwei Teilen. Die Klausel, die verlangt, dass M, Δ ⊩ X für jedes Δ ∈ G ist, so dass Γ R Δ die bekannte Hintikka / Kripke-Bedingung ist, damit X bei Γ geglaubt oder glaubwürdig ist. Die Klausel, die Γ Γ E (t, X) verlangt, fügt hinzu, dass t ein relevanter Beweis für X bei Γ sein sollte. Dann ist t: X informell in einer möglichen Welt wahr, wenn X in dieser Welt im üblichen Sinne der epistemischen Logik glaubwürdig ist, und t ist ein relevanter Beweis für X in dieser Welt.

Es ist wichtig zu erkennen, dass man in dieser Semantik etwas aus einem bestimmten Grund in einer Welt nicht glauben kann, entweder weil es einfach nicht glaubwürdig ist oder weil es ist, aber der Grund nicht angemessen ist.

Einige Bedingungen müssen noch an Beweisfunktionen gestellt werden, und die konstante Spezifikation muss ebenfalls ins Bild gebracht werden. Angenommen, man erhält s und t als Rechtfertigung. Man kann diese auf zwei verschiedene Arten kombinieren: gleichzeitig die Informationen von beiden verwenden; oder verwenden Sie die Informationen von nur einem von ihnen, aber wählen Sie zuerst welche aus. Jedes führt zu einer grundlegenden Operation zu den Begründungsbegriffen ⋅ und +, die axiomatisch in Abschnitt 2.2 eingeführt wird.

Angenommen, s ist ein relevanter Beweis für eine Implikation und t ist ein relevanter Beweis für den Vorgänger. Dann liefern s und t zusammen relevante Beweise für die Konsequenz. Die folgende Bedingung für Beweisfunktionen wird angenommen:

E (s, X → Y) ∩E (t, X) ⊆ E (s ⋅ t, Y)

Mit dieser Bedingung wird die Gültigkeit von

s:(X → Y) → (t: X → [s ⋅ t]: Y)

ist gesichert.

Wenn s und t Beweisstücke sind, könnte man sagen, dass etwas durch eines von s oder t gerechtfertigt ist, ohne sich die Mühe zu machen, anzugeben, welches, und dies wird immer noch ein Beweis sein. Die folgende Anforderung wird an Beweisfunktionen gestellt.

E (s, X) ≤ E (t, X) ≤ E (s + t, X)

Es überrascht nicht, dass beide

s: X → [s + t]: X.

und

t: X → [s + t]: X.

jetzt halt.

Schließlich sollte die Konstante Spezifikation CS berücksichtigt werden. Denken Sie daran, dass Konstanten Gründe für Grundannahmen darstellen sollen, die direkt akzeptiert werden. Ein Modell M = ⟨G, R, E, V⟩ erfüllt die angegebene Konstantspezifikation CS: Wenn c: X ∈ CS, dann ist E (c, X) = G.

Mögliches Weltbegründungsmodell Ein mögliches Weltbegründungsmodell für J _CS ist eine Struktur M = ⟨G, R, E, V⟩, die alle oben aufgeführten Bedingungen erfüllt und die Konstante Spezifikation CS erfüllt.

Trotz ihrer Ähnlichkeiten ermöglichen mögliche weltweite Rechtfertigungsmodelle eine feinkörnige Analyse, die mit Kripke-Modellen nicht möglich ist. Weitere Informationen finden Sie in Abschnitt 3 des ergänzenden Dokuments Some More Technical Matters.

3.2 Schwache und starke Vollständigkeit

Eine Formel X ist in einem bestimmten Modell für J _CS gültig, wenn sie für alle möglichen Welten des Modells gilt. Axiomatik für J _CS wurde in den Abschnitten 2.2 und 2.3 angegeben. Ein Vollständigkeitssatz nimmt nun die erwartete Form an.

Satz 2: Eine Formel X ist in J _CS genau dann beweisbar, wenn X in allen J _CS- Modellen gültig ist.

Der soeben angegebene Vollständigkeitssatz wird manchmal als schwache Vollständigkeit bezeichnet. Es ist vielleicht ein bisschen überraschend, dass es für die Modallogik K wesentlich einfacher zu beweisen ist als die Vollständigkeit. Kommentare zu diesem Punkt folgen. Andererseits ist es sehr allgemein und funktioniert für alle konstanten Spezifikationen.

In (Fitting 2005) wurde auch eine stärkere Version der Semantik eingeführt. Ein Modell M = ⟨G, R, E, V⟩ wird als vollständig erklärend bezeichnet, wenn es die folgende Bedingung erfüllt. Für jedes Γ ∈ G, wenn M, Δ ⊩ X für alle Δ ∈ G, so dass Γ R Δ, dann M, Γ Γ t: X für einen Rechtfertigungsterm t. Es ist zu beachten, dass die Bedingung M, Δ ⊩ X für alle Δ ∈ G, so dass Γ R Δ, die übliche Bedingung ist, dass X bei Γ im Hintikka / Kripke-Sinne glaubwürdig ist. Eine vollständige Erklärung besagt also, dass es eine Rechtfertigung dafür gibt, wenn eine Formel in einer möglichen Welt glaubwürdig ist.

Nicht alle schwachen Modelle erfüllen die vollständig erklärende Bedingung. Modelle, die dies tun, werden als starke Modelle bezeichnet. Wenn die konstante Spezifikation CS so reich ist, dass ein Internalisierungssatz gilt, dann hat man Vollständigkeit in Bezug auf starke Modelle, die CS erfüllen. In einem angemessenen Sinne ist Vollständigkeit in Bezug auf starke Modelle gleichbedeutend mit dem Nachweis der Internalisierung.

Der Vollständigkeitsnachweis in Bezug auf starke Modelle hat eine große Ähnlichkeit mit dem Vollständigkeitsnachweis unter Verwendung kanonischer Modelle für die Modallogik K. Starke Modelle können wiederum verwendet werden, um einen semantischen Beweis des Realisierungssatzes zu liefern (vgl. Abschnitt 4)..

3.3 Die Single-Agent-Familie

Bisher wurde eine mögliche Weltsemantik für eine Rechtfertigungslogik für J, das Gegenstück zu K, diskutiert. Jetzt werden die Dinge erweitert, um Rechtfertigungsanaloga anderer bekannter Modallogiken einzuschließen.

Durch einfaches Hinzufügen der Reflexivität der Zugänglichkeitsrelation R zu den Bedingungen für ein Modell in Abschnitt 3.1 erhält man die Gültigkeit von t: X → X für jedes t und X und erhält eine Semantik für JT, das Rechtfertigungslogik-Analogon der Modallogik T, die schwächste Logik des Wissens. In der Tat, wenn M, Γ Γ t: X, dann ist insbesondere X in jedem Zustand wahr, der von Γ aus zugänglich ist. Da die Zugänglichkeitsrelation reflexiv sein muss, ist M, Γ Γ X. Schwache und starke Vollständigkeitssätze sind mit derselben Maschinerie nachweisbar, die im Fall von J angewendet wurde, und ein semantischer Beweis eines Realisierungssatzes, der JT und T verbindet, ist ebenfalls verfügbar. Gleiches gilt für die unten diskutierten Logiken.

Für eine Begründung analog zu K4 ein zusätzlicher unärer Operator '!' wird dem Begriff Sprache hinzugefügt, siehe Abschnitt 2.5. Denken Sie daran, dass dieser Operator Rechtfertigungen Rechtfertigungen zuordnet, wobei die Idee lautet, dass wenn t eine Rechtfertigung für X ist, dann! t sollte eine Rechtfertigung für t: X sein. Semantisch fügt dies einem Modell M = ⟨G, R, E, V⟩ wie folgt Bedingungen hinzu.

Erstens sollte R natürlich transitiv sein, aber nicht unbedingt reflexiv. Zweitens ist eine Monotoniebedingung für Beweisfunktionen erforderlich:

Wenn Γ R Δ und Γ ∈ E (t, X), dann ist Δ ∈ E (t, X)

Und schließlich ist eine weitere Bedingung für die Beweisfunktion erforderlich.

E (t, X) ⊆ E (! T, t: X)

Diese Bedingungen zusammen ergeben die Gültigkeit von t: X →! t: t: X und erzeugen eine Semantik für J4, ein Rechtfertigungsanalogon von K4, mit einem Realisierungssatz, der sie verbindet. Das Hinzufügen von Reflexivität führt zu einer Logik, die aus historischen Gründen als LP bezeichnet wird.

Man kann auch einen negativen Introspektionsoperator hinzufügen, '?', Siehe Abschnitt 2.6. Modelle für Rechtfertigungslogiken, die diesen Operator enthalten, fügen drei Bedingungen hinzu. Das erste R ist symmetrisch. Zweitens fügt man eine Bedingung hinzu, die als starker Beweis bekannt geworden ist: M, Γ Γ t: X für alle Γ Γ E (t, X). Schließlich gibt es eine Bedingung für die Beweisfunktion:

E (t, X) ⊆ E (? T, ¬ t: X)

Wenn diese Maschinerie zu der für J4 hinzugefügt wird, erhalten wir die Logik J45, ein Begründungsgegenstück von K45. Axiomatische Solidität und Vollständigkeit können nachgewiesen werden. In ähnlicher Weise können verwandte Logiken JD45 und JT45 formuliert werden.

Ein Realisierungssatz unter Berücksichtigung dieses Operators wurde in (Rubtsova 2006) gezeigt.

3.4 Single World Justification Models

Einzelwelt-Rechtfertigungsmodelle wurden erheblich vor den allgemeineren möglichen Weltbegründungsmodellen entwickelt, die wir diskutiert haben (Mkrtychev 1997). Heute können sie am einfachsten als mögliche Weltbegründungsmodelle angesehen werden, die zufällig eine einzige Welt haben. Der Vollständigkeitsnachweis für J und die anderen oben genannten Rechtfertigungslogiken können leicht geändert werden, um die Vollständigkeit in Bezug auf Rechtfertigungsmodelle für eine Welt festzustellen, obwohl dies natürlich nicht das ursprüngliche Argument war. Die Vollständigkeit in Bezug auf Rechtfertigungsmodelle für eine Welt zeigt, dass Informationen über die mögliche Weltstruktur von Rechtfertigungsmodellen zumindest für die bisher diskutierten Logiken vollständig durch die zulässige Beweisfunktion codiert werden können. Mkrtychev verwendete Single-World-Rechtfertigungsmodelle, um die Entscheidbarkeit von LP festzustellen.und andere haben sie grundlegend genutzt, um Komplexitätsgrenzen für Rechtfertigungslogiken festzulegen und um Konservativitätsergebnisse für Rechtfertigungslogiken des Glaubens zu zeigen (Kuznets 2000, Kuznets 2008, Milnikel 2007, Milnikel 2009). Komplexitätsergebnisse wurden ferner verwendet, um das Problem der logischen Allwissenheit anzugehen.

4. Realisierungssätze

Das natürliche modale epistemische Gegenstück zur Beweisaussage t: F ist □ F, gelesen für einige x, x: F. Diese Beobachtung führt zu dem Begriff der vergesslichen Projektion, die jedes Auftreten von t: F durch □ F ersetzt und somit einen Begründungslogiksatz S in einen entsprechenden Modallogiksatz S ^o umwandelt. Die vergessliche Projektion erstreckt sich auf natürliche Weise von Sätzen bis zur Logik.

Offensichtlich können verschiedene Sätze der Rechtfertigungslogik dieselbe vergessliche Projektion haben, daher verliert S ^o bestimmte Informationen, die in S enthalten waren. Es ist jedoch leicht zu beobachten, dass die vergessliche Projektion immer gültige Formeln der Rechtfertigungslogik (z. B. Axiome von J) gültigen Formeln einer entsprechenden epistemischen Logik (in diesem Fall K) zuordnet. Das Umgekehrte gilt auch: Jede gültige Formel der epistemischen Logik ist die vergessliche Projektion einer gültigen Formel der Rechtfertigungslogik. Dies folgt aus dem Korrespondenzsatz 3.

Satz 3: ^Jo = K.

Diese Entsprechung gilt für andere Paare von Rechtfertigungs- und epistemischen Systemen, zum Beispiel J4 und K4 oder LP und S4 und viele andere. In solch einer erweiterten Form zeigt der Korrespondenzsatz, dass wichtige modale Logiken wie K, T, K4, S4, K45, S5 und einige andere genaue Gegenstücke zur Rechtfertigungslogik haben.

Im Zentrum des Korrespondenzsatzes steht der folgende Realisierungssatz.

Satz 4: Es gibt einen Algorithmus, der für jede in K ableitbare Modalformel F jedem Auftreten von Modalität in F Evidenzterme so zuweist, dass die resultierende Formel F ^r in J ableitbar ist. Darüber hinaus weist die Realisierung Evidenzvariablen zu auf das negative Auftreten von Modaloperatoren in F, wodurch das existenzielle Lesen der epistemischen Modalität respektiert wird.

Bekannte Realisierungsalgorithmen, die Evidenzterme in Modalsätzen wiederherstellen, verwenden schnittfreie Ableitungen in den entsprechenden Modallogiken. Alternativ kann der Realisierungssatz semantisch durch die Methode von Fitting oder seine geeigneten Modifikationen aufgestellt werden. Im Prinzip erzeugen diese semantischen Argumente auch Realisierungsverfahren, die auf einer erschöpfenden Suche beruhen.

Es wäre ein Fehler, die Schlussfolgerung zu ziehen, dass jede Modallogik ein vernünftiges Gegenstück zur Rechtfertigungslogik hat. Zum Beispiel enthält die Logik der formalen Beweisbarkeit, GL (Boolos 1993), das Löb-Prinzip:

(5)	□ (□ F → F) → □ F,

die keine epistemisch akzeptable explizite Version zu haben scheint. Betrachten Sie zum Beispiel den Fall, in dem F die Satzkonstante ⊥ für false ist. Wenn ein Analogon von Satz 4 das Löb-Prinzip abdecken würde, gäbe es Rechtfertigungsbegriffe s und t, so dass x:(s: ⊥ → ⊥) → t: ⊥. Dies ist jedoch intuitiv falsch für eine sachliche Rechtfertigung. In der Tat ist s: ⊥ → ⊥ eine Instanz des Faktivitätsaxioms. Wenden Sie die Axiom-Internalisierung an, um c:(s: ⊥ → ⊥) für eine Konstante c zu erhalten. Diese Wahl von c macht den Vorgänger von c:(s: ⊥ → ⊥) → t: ⊥ intuitiv wahr und die Schlussfolgerung falsch ^[4]. Insbesondere gilt das Löb-Prinzip (5) nicht für die Beweisinterpretation (vgl. (Goris 2007) für eine vollständige Darstellung, welche Prinzipien des GL realisierbar sind).

Der Korrespondenzsatz gibt neue Einblicke in die epistemische Modallogik. Insbesondere bietet es eine neue Semantik für die wichtigsten Modallogiken. Zusätzlich zu der traditionellen "universellen" Lesart von □ F im Kripke-Stil, wie sie in allen möglichen Situationen gilt, gibt es jetzt eine strenge "existenzielle" Semantik für □ F, die gelesen werden kann, wenn es einen Zeugen (Beweis, Rechtfertigung) für gibt F.

Die Begründungssemantik spielt in der Modallogik eine ähnliche Rolle wie die Kleene-Realisierbarkeit in der Intuitionistischen Logik. In beiden Fällen ist die beabsichtigte Semantik existenziell: die Brouwer-Heyting-Kolmogorov-Interpretation der intuitionistischen Logik (Heyting 1934, Troelstra und van Dalen 1988, van Dalen 1986) und Gödels Beweisbarkeitslesung von S4 (Gödel 1933, Gödel 1938). In beiden Fällen gibt es eine mögliche Weltsemantik des UniversalenCharakter, der ein hochwirksames und dominantes technisches Werkzeug ist. Es wird jedoch nicht auf den existenziellen Charakter der beabsichtigten Semantik eingegangen. Es bedurfte der Realisierbarkeit von Kleene (Kleene 1945, Troelstra 1998), um die rechnerische Semantik der intuitionistischen Logik und die Logik der Beweise aufzudecken und eine genaue BHK-Semantik der Beweise für die intuitionistische und modale Logik bereitzustellen.

Im epistemischen Kontext fügen die Rechtfertigungslogik und der Korrespondenzsatz der modalen Wissens- und Glaubenslogik eine neue Rechtfertigungskomponente hinzu. Auch diese neue Komponente war in der Tat ein alter und zentraler Begriff, der von etablierten Erkenntnistheoretikern ausführlich diskutiert wurde, aber außerhalb des Rahmens der klassischen erkenntnistheoretischen Logik blieb. Der Korrespondenzsatz besagt, dass Rechtfertigungen mit Systemen im Hintikka-Stil kompatibel sind und daher sicher in die Grundlage für die epistemische Modallogik integriert werden können.

Weitere Informationen zu Realisierungssätzen finden Sie in Abschnitt 4 des ergänzenden Dokuments Einige weitere technische Fragen.

5. Verallgemeinerungen

Bisher wurden in diesem Artikel nur Einzelagenten-Rechtfertigungslogiken berücksichtigt, die der Einzelagenten-Wissenslogik analog sind. Begründungslogik kann als Logik expliziten Wissens betrachtet werden, die sich auf konventionellere Logiken impliziten Wissens bezieht. In der Literatur wurde eine Reihe von Systemen untersucht, die über die oben diskutierten hinausgehen und mehrere Wirkstoffe umfassen oder sowohl implizite als auch explizite Operatoren oder eine Kombination davon aufweisen.

5.1 Explizites und implizites Wissen mischen

Da Rechtfertigungslogiken explizite Rechtfertigungen liefern, während herkömmliche Wissenslogiken einen impliziten Wissensoperator liefern, ist es natürlich, die Kombination beider in einem einzigen System in Betracht zu ziehen. Die häufigste gemeinsame Logik expliziten und impliziten Wissens ist S4LP (Artemov und Nogina 2005). Die Sprache von S4LP ist wie die von LP, jedoch mit einem impliziten Wissensoperator, der entweder K oder □ geschrieben ist. Die Axiomatik ist wie die von LP, kombiniert mit der von S4 für den impliziten Operator, zusammen mit einem Verbindungsaxiom, t: X → □ X, alles, was eine explizite Begründung hat, ist erkennbar.

Semantisch bedürfen mögliche Weltbegründungsmodelle für LP keiner Modifikation, da sie bereits über alle Maschinen von Hintikka / Kripke-Modellen verfügen. Einer modelliert den □ -Operator auf die übliche Weise, wobei nur die Zugänglichkeitsrelation verwendet wird, und einer modelliert die Begründungsbegriffe, wie in Abschnitt 3.1 beschrieben, sowohl unter Verwendung der Zugänglichkeits- als auch der Beweisfunktion. Da die übliche Bedingung, dass □ X in einer Welt wahr ist, eine der beiden Klauseln der Bedingung ist, dass t: X wahr ist, ergibt dies sofort die Gültigkeit von t: X → □ X, und die Solidität folgt leicht. Die axiomatische Vollständigkeit ist ebenfalls recht einfach.

In S4LP wird sowohl implizites als auch explizites Wissen dargestellt, aber in der Semantik eines möglichen Weltbegründungsmodells dient eine einzige Zugänglichkeitsrelation für beide. Dies ist nicht der einzige Weg, dies zu tun. Allgemeiner könnte eine explizite Beziehung zur Zugänglichkeit von Wissen eine angemessene Erweiterung derjenigen für implizites Wissen sein. Dies stellt die Vision von explizitem Wissen dar, strengere Standards für das zu haben, was als bekannt gilt, als das implizites Wissen. Die Verwendung unterschiedlicher Zugänglichkeitsrelationen für explizites und implizites Wissen wird erforderlich, wenn diese epistemischen Begriffe unterschiedlichen logischen Gesetzen folgen, z. B. S5 für implizites Wissen und LP für explizites Wissen. Der Fall von Beziehungen mit mehreren Zugänglichkeiten ist in der Literatur allgemein als Artemov-Fitting-Modelle bekannt, wird hier jedoch als mögliche Weltmodelle mit mehreren Agenten bezeichnet. (vgl. Abschnitt 5.2).

Obwohl die Logik S4LP ganz natürlich erscheint, war ein Realisierungssatz seltsamerweise problematisch: Ein solcher Satz kann nicht bewiesen werden, wenn man auf sogenannten normalen Realisierungen besteht (Kuznets 2010). Die Realisierung impliziter Wissensmodalitäten in S4LP durch explizite Begründungen, die die epistemische Struktur berücksichtigen würden, bleibt eine große Herausforderung in diesem Bereich.

Interaktionen zwischen implizitem und explizitem Wissen können manchmal ziemlich heikel sein. Betrachten Sie als Beispiel das folgende gemischte Prinzip der negativen Selbstbeobachtung (wiederum □ sollte als impliziter epistemischer Operator gelesen werden):

(6)	¬ t: X → □ ¬ t: X.

Aus Sicht der Beweisbarkeit ist es die richtige Form der negativen Selbstbeobachtung. In der Tat sei □ F als F beweisbar und t: F als t ist ein Beweis für F in einer gegebenen formalen Theorie T, z. B. in Peano Arithmetic PA. Dann gibt (6) ein nachweisbares Prinzip an. Wenn t kein Beweis für F ist, kann diese Aussage, da sie entscheidbar ist, innerhalb von T festgestellt werden, daher ist dieser Satz in T beweisbar. Andererseits hängt der Beweis p von 't kein Beweis von F' sowohl von t als auch von F ab, p = p (t, F) und kann nicht nur mit t berechnet werden. In dieser Hinsicht kann □ nicht durch einen bestimmten Beweisbegriff ersetzt werden, der nur von t abhängt, und (6) kann nicht in einem vollständig expliziten Rechtfertigungsformat dargestellt werden.

Die ersten Beispiele für explizite / implizite Wissenssysteme erschienen im Bereich der Beweisbarkeitslogik. In (Sidon 1997, Yavorskaya (Sidon) 2001) wurde ein logisches LPP eingeführt, das die Logik der Beweisbarkeit GL mit der Logik der Beweise LP kombinierte, aber um sicherzustellen, dass das resultierende System wünschenswerte logische Eigenschaften hatte, einige zusätzliche Operationen von außerhalb der ursprünglichen Sprachen von GL und LP wurden hinzugefügt. In (Nogina 2006, Nogina 2007) wurde ein vollständiges logisches System, GLA, für Beweise und Beweisbarkeit in der Summe der Originalsprache von GL und LP angeboten. Sowohl LPP als auch GLA sind in Bezug auf die Klasse der arithmetischen Modelle und auch in Bezug auf die Klasse der möglichen Weltbegründungsmodelle vollständig.

Ein weiteres Beispiel für ein Beweisprinzip, das nicht vollständig explizit gemacht werden kann, ist das Löb-Prinzip (5). Für jedes von LPP und GLA ist es einfach, einen Beweisausdruck l (x) zu finden, so dass

(7)	x: (□ F → F) → l (x): F.

hält. Es gibt jedoch keine Erkenntnis, die alle drei □ s in (5) explizit macht. Tatsächlich ist der Satz realisierbarer Beweisbarkeitsprinzipien der Schnittpunkt von GL und S4 (Goris 2007).

5.2 Mögliche weltweite Rechtfertigungsmodelle für mehrere Agenten

In Multi-Agent-Modellen für mögliche weltweite Rechtfertigungen werden mehrere Zugänglichkeitsbeziehungen mit Verbindungen zwischen ihnen verwendet (Artemov 2006). Die Idee ist, dass es mehrere Agenten gibt, von denen jeder einen impliziten Wissensoperator hat, und dass es Begründungsbegriffe gibt, die jeder Agent versteht. Jeder versteht explizite Gründe; diese belaufen sich auf evidenzbasiertes Allgemeinwissen.

Ein mögliches n-Agent-Weltbegründungsmodell ist eine Struktur ⟨G, R ₁,…, R _n, R, E, V⟩, die die folgenden Bedingungen erfüllt. G ist eine Menge möglicher Welten. Jedes von R ₁,…, R _n ist eine Zugänglichkeitsrelation, eine für jeden Agenten. Diese können je nach Wunsch als reflexiv, transitiv oder symmetrisch angenommen werden. Sie werden verwendet, um implizites Agentenwissen für die Agentenfamilie zu modellieren. Die Zugänglichkeitsrelation R erfüllt die LP-Bedingungen, Reflexivität und Transitivität. Es wird zur Modellierung expliziten Wissens verwendet. E ist eine Beweisfunktion, die die gleichen Bedingungen wie für LP in Abschnitt 3.3 erfüllt. V ordnet Satzbuchstaben wie üblich Weltengruppen zu. Es gibt eine spezielle Bedingung: für jedes i = 1,…, n, R _i ⊆ R.

Wenn M = ⟨G, R ₁, …, R _n, R, E, V⟩ ein Multi-Agent-Modell für eine mögliche Weltbegründung ist, wird mit den meisten von ihnen eine Wahrheit-in-Welt-Beziehung M, Γ Γ X definiert die üblichen Klauseln. Von besonderem Interesse sind folgende:

M, Γ Γ K _i X genau dann, wenn wir für jedes Δ ∈ G mit Γ R _i Δ das M, Δ ⊩ X haben.
M, Γ Γ t: X genau dann, wenn Γ Γ E (t, X) und für jedes Δ ∈ G mit Γ R Δ haben wir M, Δ ⊩ X.

Die Bedingung R _i ⊆ R beinhaltet die Gültigkeit von t: X → K _i X für jeden Agenten i. Wenn es nur einen einzigen Agenten gibt und die Eingabehilfenbeziehung für diesen Agenten reflexiv und transitiv ist, bietet dies eine weitere Semantik für S4LP. Unabhängig von der Anzahl der Agenten akzeptiert jeder Agent explizite Gründe als Wissensgrundlage.

Eine Version von LP mit zwei Agenten wurde in (Yavorskaya (Sidon) 2008) eingeführt und untersucht, obwohl sie auf eine endliche Anzahl von Agenten verallgemeinert werden kann. Dabei hat jeder Agent seinen eigenen Satz von Begründungsoperatoren, Variablen und Konstanten, anstatt wie oben einen einzigen Satz für alle zu haben. Darüber hinaus kann eine eingeschränkte Kommunikation zwischen Agenten zulässig sein, indem ein neuer Operator verwendet wird, mit dem ein Agent die Richtigkeit der Rechtfertigungen des anderen Agenten überprüfen kann. Für die Zwei-Agenten-Logik wurden Versionen sowohl einer einzelnen Welt als auch einer allgemeineren möglichen Weltbegründungssemantik erstellt. Dies beinhaltet eine einfache Erweiterung des Begriffs einer Evidenzfunktion und für mögliche weltweite Rechtfertigungsmodelle unter Verwendung von zwei Zugänglichkeitsrelationen. Realisierungssätze wurden syntaktisch bewiesen,obwohl vermutlich auch ein semantischer Beweis funktionieren würde.

In jüngster Zeit wurde die Rolle öffentlicher Ankündigungen in der Rechtfertigungslogik für mehrere Agenten untersucht (Renne 2008, Renne 2009).

In Abschnitt 5 des ergänzenden Dokuments Some More Technical Matters wird mehr auf den Begriff des evidenzbasierten Allgemeinwissens eingegangen.

6. Russells Beispiel: Induzierte Faktivität

Es gibt eine Technik zur Verwendung der Rechtfertigungslogik, um verschiedene Rechtfertigungen für dieselbe Tatsache zu analysieren, insbesondere wenn einige der Rechtfertigungen sachlich sind und andere nicht. Um die Technik zu demonstrieren, betrachten Sie ein bekanntes Beispiel:

Wenn ein Mann glaubt, dass der Nachname des verstorbenen Premierministers mit einem „B“begann, glaubt er, was wahr ist, da der verstorbene Premierminister Sir Henry Campbell Bannerman war ^[5]. Wenn er jedoch glaubt, dass Herr Balfour der verstorbene Premierminister war ^[6], wird er immer noch glauben, dass der Nachname des verstorbenen Premierministers mit einem „B“begann, aber dieser Glaube, obwohl wahr, würde nicht als Wissen angesehen werden. (Russell 1912)

Wie im Beispiel der Roten Scheune, das in Abschnitt 1.1 erörtert wird, muss man sich hier mit zwei Rechtfertigungen für eine wahre Aussage befassen, von denen eine richtig ist und eine nicht. Sei B ein Satz (Satzatom), w eine bezeichnete Rechtfertigungsvariable für den falschen Grund für B und ra eine bezeichnete Rechtfertigungsvariable für den richtigen (daher faktischen) Grund für B. Dann fordert Russells Beispiel die folgenden Annahmen auf ^[7]:

R = {w: B, r: B, r: B → B}

Etwas entgegen der Intuition kann man logisch die Faktivität von w aus R ableiten:

r: B (Annahme)
r: B → B (Annahme)
B (von 1 und 2 von Modus Ponens)
B → (w: B → B) (Satzaxiom)
w: B → B (von 3 und 4 von Modus Ponens)

Diese Herleitung nutzt jedoch die Tatsache, dass r eine faktische Rechtfertigung für B ist, um auf w: B → B zu schließen, was einen Fall von 'induzierter Faktivität' für w: B darstellt. Die Frage ist, wie man die "reale" Faktivität von r: B von der "induzierten Faktivität" von w: B unterscheiden kann. Hier ist eine Art Wahrheitsverfolgung erforderlich, und die Begründungslogik ist ein geeignetes Werkzeug. Der natürliche Ansatz besteht darin, die Menge der Annahmen ohne r: B zu berücksichtigen, dh

S = {w: B, r: B → B}

und stellen Sie fest, dass die Faktivität von w, dh w: B → B, nicht von S ableitbar ist. Hier ist ein mögliches Weltbegründungsmodell M = (G, R, E, V), in dem S gilt, w: B → B jedoch nicht::

G = { 1 },
R = ∅,
V (B) = ∅ (und damit nicht - 1 ⊩ B),
E (t, F) = { 1 } für alle Paare (t, F) außer (r, B) und
E (r, B) = ∅.

Es ist leicht zu erkennen, dass die Verschlussbedingungen Application und Sum on E erfüllt sind. Bei 1 gilt w: B, dh

1 ⊩ w: B.

da w ein zulässiger Beweis für B bei 1 ist und es keine möglichen Welten gibt, die von 1 aus zugänglich sind. Außerdem,

not- 1 ⊩ r: B.

da nach E r kein zulässiger Beweis für B bei 1 ist. Daher:

1 ⊩ r: B → B.

Andererseits,

not- 1 ⊩ w: B → B.

da B nicht bei 1 hält.

7. Selbstreferenzialität von Rechtfertigungen

Die Realisierungsalgorithmen erzeugen manchmal konstante Spezifikationen, die selbstreferenzielle Rechtfertigungsaussagen c: A (c) enthalten, dh Behauptungen, bei denen die Rechtfertigung (hier c) in dem behaupteten Satz (hier A (c)) auftritt.

Die Selbstreferenzialität von Rechtfertigungen ist ein neues Phänomen, das in der konventionellen Modalsprache nicht vorhanden ist. Solche selbstreferenziellen Behauptungen sind nicht nur faszinierende epistemische Objekte, sondern stellen auch aus semantischer Sicht aufgrund des eingebauten Teufelskreises eine besondere Herausforderung dar. Um c zu bewerten, würde man erwarten, zuerst A zu bewerten und dann c ein Rechtfertigungsobjekt für A zuzuweisen. Dies ist jedoch nicht möglich, da A c enthält, das noch ausgewertet werden muss. Die Frage, ob modale Logik ohne Verwendung von selbstreferenziellen Begründungen realisiert werden kann oder nicht, war in diesem Bereich eine wichtige offene Frage.

Das Hauptergebnis von Kuznets in (Breschnew und Kusnez 2006) besagt, dass die Selbstreferenzialität von Rechtfertigungen bei der Realisierung von S4 in LP unvermeidbar ist. Der aktuelle Stand der Dinge ergibt sich aus dem folgenden Satz von Kuznets:

Satz 5: Selbstreferenzialität kann bei Realisierungen der Modallogiken K und D vermieden werden. Selbstreferenzialität kann bei Realisierungen der Modallogiken T, K4, D4 und S4 nicht vermieden werden.

Dieser Satz legt fest, dass ein System von Begründungsbegriffen für S4 notwendigerweise selbstreferenziell sein wird. Dies führt zu einer ernsthaften, wenn auch nicht direkt sichtbaren Einschränkung der Beweisbarkeitssemantik. Im gödelschen Kontext arithmetischer Beweise wurde das Problem durch eine allgemeine Methode zur Zuordnung der arithmetischen Semantik zu selbstreferenziellen Aussagen c: A (c) gelöst, die besagt, dass c ein Beweis für A (c) ist. In der Logic of Proofs LP wurde es durch eine nicht triviale Fixpunktkonstruktion behandelt.

Selbstreferenzialität gibt eine interessante Perspektive auf Moores Paradoxon. Weitere Informationen finden Sie in Abschnitt 6 des ergänzenden Dokuments.

8. Quantifizierer in der Begründungslogik

Während die Untersuchung der Aussagenbegründungslogik bei weitem nicht abgeschlossen ist, wurden auch sporadische Arbeiten an Versionen erster Ordnung durchgeführt. Quantifizierte Versionen von Modal Logic bieten bereits Komplexitäten, die über die Standardlogik erster Ordnung hinausgehen. Die Quantifizierung hat ein noch breiteres Feld, wenn es um die Rechtfertigungslogik geht. Klassischerweise quantifiziert man über "Objekte", und Modelle sind mit einer Domäne ausgestattet, über die sich Quantifizierer erstrecken. Modal kann man eine einzige Domäne haben, die allen möglichen Welten gemeinsam ist, oder man kann separate Domänen für jede Welt haben. Die Rolle der Barcan-Formel ist hier bekannt. Für die Begründungslogik stehen sowohl konstante als auch unterschiedliche Domänenoptionen zur Verfügung. Darüber hinaus gibt es eine Möglichkeit, die für Modal Logic kein Analogon hat: Man könnte über Rechtfertigungen selbst quantifizieren.

Die ersten Ergebnisse bezüglich der Möglichkeit einer quantifizierten Begründungslogik waren besonders ungünstig. Die arithmetische Beweisbarkeitssemantik für die Logic of Proofs LP verallgemeinert sich natürlich auf eine Version erster Ordnung mit herkömmlichen Quantifizierern und auf eine Version mit Quantifizierern über Proofs. In beiden Fällen wurden Fragen zur Axiomatisierbarkeit negativ beantwortet.

Satz 6: Die Beweislogik erster Ordnung ist nicht rekursiv aufzählbar (Artemov und Yavorskaya (Sidon) 2001). Die Logik von Beweisen mit Quantifizierern über Beweisen ist nicht rekursiv aufzählbar (Yavorsky 2001).

Obwohl eine arithmetische Semantik nicht möglich ist, wurde in (Fitting 2008) eine mögliche Weltsemantik und eine axiomatische Beweistheorie für eine Version von LP mit Quantifizierern angegeben, die sich über Begründungen erstrecken. Solidität und Vollständigkeit wurden bewiesen. An diesem Punkt trennt sich die mögliche Weltsemantik von der arithmetischen Semantik, die möglicherweise einen Grund zur Besorgnis darstellt oder nicht. Es wurde auch gezeigt, dass S4 in die quantifizierte Logik eingebettet wird, indem □ Z übersetzt wird als „es gibt eine Rechtfertigung x, so dass x: Z ^* “, wobei Z ^* die Übersetzung von Z ist. Obwohl diese Logik etwas kompliziert ist, hat sie Anwendung gefunden, z. B. in (Dean und Kurokawa 2009b), wo sie zur Analyse des Wissensparadoxons verwendet wird, obwohl in (Arlo-Costa und Kishida 2009) Einwände gegen diese Analyse erhoben wurden.

Es wurde auch an Versionen von Justification Logic mit Quantifizierern über Objekten gearbeitet, sowohl mit als auch ohne Analogon der Barcan-Formel. Nichts davon wurde veröffentlicht, und es sollte davon ausgegangen werden, dass es noch in Arbeit ist.

9. Historische Notizen

Das ursprüngliche Justification Logic-System, die Logic of Proofs LP, wurde 1995 in (Artemov 1995) eingeführt (vgl. Auch (Artemov 2001)), wo erstmals grundlegende Eigenschaften wie Internalisierung, Realisierung und arithmetische Vollständigkeit festgelegt wurden. LP bot eine beabsichtigte Beweisbarkeitssemantik für Gödels Beweisbarkeitslogik S4 und damit eine Formalisierung der Brouwer-Heyting-Kolmogorov-Semantik für die intuitionistische Aussagenlogik. Die epistemische Semantik und Vollständigkeit (Fitting 2005) wurde erstmals für LP festgelegt. Symbolische Modelle und Entscheidbarkeit für LP gehen auf Mkrtychev zurück (Mkrtychev 1997). Komplexitätsschätzungen erschienen erstmals in (Breschnew und Kusnez 2006, Kusnez 2000, Milnikel 2007). Eine umfassende Übersicht aller Ergebnisse zu Entscheidbarkeit und Komplexität finden Sie in (Kuznets 2008). Systeme J, J4,und JT wurden erstmals in (Breschnew 2001) unter verschiedenen Namen und in einer etwas anderen Umgebung betrachtet. JT45 erschien unabhängig in (Pacuit 2006) und (Rubtsova 2006) und JD45 in (Pacuit 2006). Die Logik der Einschlussbeweise wurde in (Krupski 1997) gefunden. Ein allgemeinerer Ansatz für allgemeines Wissen auf der Grundlage von begründetem Wissen wurde in (Artemov 2006) angeboten. Die Spielesemantik der Rechtfertigungslogik und der dynamischen epistemischen Logik mit Begründungen wurde in (Renne 2008, Renne 2009) untersucht. Zusammenhänge zwischen der Rechtfertigungslogik und dem Problem der logischen Allwissenheit wurden in (Artemov und Kuznets 2009, Wang 2009) untersucht. Der Name Justification Logic wurde in (Artemov 2008) eingeführt, in dem Beispiele von Kripke, Russell und Gettier formalisiert wurden; Diese Formalisierung wurde zur Lösung von Paradoxien, zur Verifizierung,Analyse versteckter Annahmen und Beseitigung von Redundanzen. In (Dean und Kurokawa 2009a) wurde die Rechtfertigungslogik zur Analyse von Paradoxien für Wissen und Erkennbarkeit verwendet.

Literaturverzeichnis

Antonakos, E. (2007). "Gerechtfertigtes und allgemeines Wissen: Begrenzte Konservativität", S. Artemov und A. Nerode (Hrsg.), Logische Grundlagen der Informatik, Internationales Symposium, LFCS 2007, New York, NY, USA, 4.-7. Juni 2007, Proceedings (Lecture Notes in Computer Science: Band 4514), Berlin: Springer, S. 1–11.
Arlo-Costa, H. und K. Kishida (2009). "Drei Beweise und der Wissende in der quantifizierten Logik der Beweise", in Formal Epistemology Workshop / FEW 2009. Proceedings, Carnegie Mellon University, Pittsburgh, PA, USA.
Artemov, S. (1995). „Operational Modal Logic“, Technischer Bericht MSI 95–29, Cornell University.
–––. (2001). „Explizite Beweisbarkeit und konstruktive Semantik“, The Bulletin of Symbolic Logic, 7 (1): 1–36.
–––. (2006). „Begründetes Allgemeinwissen“, Theoretische Informatik, 357 (1–3): 4–22.
–––. (2008). „Die Logik der Rechtfertigung“, The Review of Symbolic Logic, 1 (4): 477–513.
Artemov, S. und R. Kuznets (2009). „Logische Allwissenheit als Problem der rechnerischen Komplexität“, in A. Heifetz (Hrsg.), Theoretische Aspekte von Rationalität und Wissen, Proceedings of the Twelfth Conference (TARK 2009), ACM Publishers, S. 14–23.
Artemov, S. und E. Nogina (2005). „Einführung der Rechtfertigung in die epistemische Logik“, Journal of Logic and Computation, 15 (6): 1059–1073.
Artemov, S. und T. Yavorskaya (Sidon) (2001). „Über die Logik der Beweise erster Ordnung“, Moscow Mathematical Journal, 1 (4): 475–490.
Boolos, G. (1993). Die Logik der Provabilität, Cambridge: Cambridge University Press.
Breschnew, V. (2001). „Über die Logik der Beweise“, in K. Striegnitz (Hrsg.), Proceedings of the Sixth ESSLLI Student Session, 13. Europäische Sommerschule für Logik, Sprache und Information (ESSLLI'01), S. 35–46.
Breschnew, V. und R. Kusnez (2006). „Wissen explizit machen: Wie schwer es ist“, Theoretical Computer Science, 357 (1–3): 23–34.
Cubitt, RP und R. Sugden (2003). „Allgemeinwissen, Bedeutung und Konvention: Eine Rekonstruktion der Spieltheorie von David Lewis“, Economics and Philosophy, 19: 175–210.
Dean, W. und H. Kurokawa (2009a). „Vom Paradox der Erkennbarkeit zur Existenz von Beweisen“, Synthese, 176 (2): 177–225.
–––. (2009b). „Wissen, Beweis und der Wissende“, in A. Heifetz (Hrsg.), Theoretische Aspekte von Rationalität und Wissen, Proceedings of the Twelfth Conference (TARK 2009), ACM Publications, S. 81–90.
Dretske, F. (2005). „Wird Wissen unter bekannten Bedingungen geschlossen? Der Fall gegen die Schließung “, in M. Steup und E. Sosa (Hrsg.), Contemporary Debates in Epistemology, Oxford: Blackwell, S. 13–26.
R. Fagin, Y. Moses J. Halpern und M. Vardi (1995). Argumentation über Wissen, Cambridge, MA: MIT Press.
Fitting, M. (2005). „Die Logik der Beweise, semantisch“, Annals of Pure and Applied Logic, 132 (1): 1–25.
–––. (2006). "Ein Ersatzsatz für LP ", Technischer Bericht TR-2006002, Institut für Informatik, City University of New York.
–––. (2008). „Eine quantifizierte Logik der Beweise“, Annals of Pure and Applied Logic, 152 (1–3): 67–83.
–––. (2009). „Realisierungen und LP “, Annals of Pure and Applied Logic, 161 (3): 368–387.
Gettier, E. (1963). "Ist gerechtfertigtes Glaubenswissen gerechtfertigt?" Analysis, 23: 121–123.
Girard, J.-Y., P. Taylor und Y. Lafont (1989). Beweise und Typen (Cambridge Tracts in Computer Science: Band 7), Cambridge: Cambridge University Press.
Gödel, K. (1933). "Eine Interpretation des intuitionistischen Ängstlichen", Ergebnisse Math. Kolloq. 4: 39–40. Englische Übersetzung in: S. Feferman et al. (Hrsg.), Kurt Gödel Collected Works (Band 1), Oxford und New York: Oxford University Press und Clarendon Press, 1986, S. 301–303.
–––. (1938). "Vortrag bei Zilsel / Vortrag bei Zilsel" (* 1938a), in S. Feferman, JJ Dawson, W. Goldfarb, C. Parsons und R. Solovay (Hrsg.), Unveröffentlichte Essays und Vorträge (Kurt Gödel Collected Works: Volume III), Oxford: Oxford University Press, 1995, S. 86–113.
Goldman, A. (1967). „Eine kausale Bedeutungstheorie“, The Journal of Philosophy, 64: 335–372.
Goodman, N. (1970). „Eine Konstruktionstheorie ist gleichbedeutend mit Arithmetik“, in J. Myhill, A. Kino, und R. Vesley (Hrsg.), Intuitionism and Proof Theory, Amsterdam: Nordholland, S. 101–120.
Goris, E. (2007). "Explizite Beweise in der formalen Beweisbarkeitslogik", S. Artemov und A. Nerode (Hrsg.), Logische Grundlagen der Informatik, Internationales Symposium, LFCS 2007, New York, NY, USA, 4.-7. Juni 2007, Proceedings (ecture Notes in Computer Science: Band 4514), Berlin: Springer, S. 241–253.
Hendricks, V. (2005). Mainstream und formale Erkenntnistheorie, New York: Cambridge University Press.
Heyting, A. (1934). Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie, Berlin: Springer.
Hintikka, J. (1962). Wissen und Glaube, Ithaka: Cornell University Press.
Kleene, S. (1945). „Zur Interpretation der intuitionistischen Zahlentheorie“, The Journal of Symbolic Logic, 10 (4): 109–124.
Kolmogorov, A. (1932). „Zur Deutung der Intuitionistischen Logik“, Mathematische Zeitschrift, 35: 58–65. Englische Übersetzung in VM Tikhomirov (Hrsg.), Ausgewählte Werke von AN Kolmogorov. Band I: Mathematik und Mechanik, Dordrecht: Kluwer, 1991, S. 151–158.
Kreisel, G. (1962). "Grundlagen der intuitionistischen Logik", in E. Nagel, P. Suppes und A. Tarski (Hrsg.), Logik, Methodik und Wissenschaftstheorie. Tagungsband des Internationalen Kongresses 1960, Stanford: Stanford University Press, S. 198–210.
–––. (1965). "Mathematische Logik", in T. Saaty (Hrsg.), Lectures in Modern Mathematics III, New York: Wiley and Sons, S. 95–195.
Krupski, V. (1997). "Operative Logik von Beweisen mit Funktionsbedingung auf Beweisprädikat", S. Adian und A. Nerode (Hrsg.), Logische Grundlagen der Informatik, 4. Internationales Symposium, LFCS'97, Jaroslawl, Russland, 6.-12. Juli 1997, Proceedings (Lecture Notes in Computer Science: Band 1234), Berlin: Springer, S. 167–177.
Kurokawa, H. (2009). "Tableaus und Hypersequenzen für die Rechtfertigungslogik", in S. Artemov und A. Nerode (Hrsg.), Logische Grundlagen der Informatik, Internationales Symposium, LFCS 2009, Deerfield Beach, FL, USA, 3. bis 6. Januar 2009, Proceedings (Lecture Notes in Computer Science: Band 5407), Berlin: Springer, S. 295–308.
Kuznets, R. (2000). "Über die Komplexität der expliziten Modallogik", in P. Clote und H. Schwichtenberg (Hrsg.), Computer Science Logic, 14. Internationaler Workshop, CSL 2000, Jahreskonferenz der EACSL, Fischbachau, 21.-26. August 2000, Proceedings (Lecture Notes in Computer Science: Band 1862), Berlin: Springer, S. 371–383.
–––. (2008). Komplexitätsprobleme in der Rechtfertigungslogik, Dissertation, Institut für Informatik, Graduiertenzentrum der Universität New York.
–––. (2010). "Ein Hinweis auf die Abnormalität der Realisierungen von S4LP ", in K. Brünnler und T. Studer (Hrsg.), Beweis, Berechnung, Komplexität PCC 2010, Internationaler Workshop, Verfahren, IAM Technical Reports IAM-10-001, Institute of Computer Naturwissenschaften und Angewandte Mathematik, Universität Bern.
McCarthy, J., M. Sato, T. Hayashi und S. Igarishi (1978). "Zur Modelltheorie des Wissens", Technischer Bericht STAN-CS-78-667, Institut für Informatik, Stanford University.
Milnikel, R. (2007). „Die Ableitbarkeit in bestimmten Subsystemen der Logik der Beweise ist Π ₂ ^p- vollständig“, Annals of Pure and Applied Logic, 145 (3): 223–239.
–––. (2009). "Konservativität für die Logik des berechtigten Glaubens", S. Artemov und A. Nerode (Hrsg.), Logische Grundlagen der Informatik, Internationales Symposium, LFCS 2009, Deerfield Beach, FL, USA, 3. bis 6. Januar 2009, Proceedings (Lecture Notes in Computer Science: Band 5407), Berlin: Springer, S. 354–364.
Mkrtychev, A. (1997). "Modelle für die Logik der Beweise", S. Adian und A. Nerode (Hrsg.), Logische Grundlagen der Informatik, 4. Internationales Symposium, LFCS'97, Jaroslawl, Russland, 6.-12. Juli 1997, Proceedings (Lecture Anmerkungen in der Informatik: Band 1234), Berlin: Springer, S. 266–275.
Nogina, E. (2006). „Über Logik der Beweise und Beweisbarkeit“, Sommertagung 2005 der Vereinigung für symbolische Logik, Logic Colloquium'05, Athen, Griechenland (28. Juli bis 3. August 2005), The Bulletin of Symbolic Logic, 12 (2): 356.
–––. (2007). „Epistemische Vollständigkeit von GLA “, Jahrestagung 2007 der Association for Symbolic Logic, Universität von Florida, Gainesville, Florida (10. bis 13. März 2007), The Bulletin of Symbolic Logic, 13 (3): 407.
Pacuit, E. (2006). „Ein Hinweis zu einigen expliziten modalen Logiken“, Technischer Bericht PP - 2006–29, Institut für Logik, Sprache und Berechnung, Universität Amsterdam.
Plaza, J. (2007). „Logik der öffentlichen Kommunikation“, Synthese, 158 (2): 165–179.
Renne, B. (2008). Dynamische epistemische Logik mit Begründung, Doktorarbeit, Institut für Informatik, CUNY Graduate Center, New York, NY, USA.
–––. (2009). "Evidence Elimination in Multi-Agent Justification Logic", in A. Heifetz (Hrsg.), Theoretische Aspekte von Rationalität und Wissen, Proceedings of the Twelfth Conference (TARK 2009), ACM Publications, S. 227–236.
Rose, G. (1953). "Aussagenrechnung und Realisierbarkeit", Transactions of the American Mathematical Society, 75: 1–19.
Rubtsova, N. (2006). „Zur Realisierung der S5- Modalität durch Evidence Terms“, Journal of Logic and Computation, 16 (5): 671–684.
Russell, B. (1912). Die Probleme der Philosophie, Oxford: Oxford University Press.
Sidon, T. (1997). "Provabilitätslogik mit Operationen an Beweisen", in S. Adian und A. Nerode (Hrsg.), Logische Grundlagen der Informatik, 4. Internationales Symposium, LFCS'97, Jaroslawl, Russland, 6.-12. Juli 1997, Proceedings (Lecture Anmerkungen in der Informatik: Band 1234), Berlin: Springer, S. 342–353.
Troelstra, A. (1998). „Realisierbarkeit“, S. Buss (Hrsg.), Handbook of Proof Theory, Amsterdam: Elsevier, S. 407–474.
Troelstra, A. und H. Schwichtenberg (1996). Grundlegende Beweistheorie, Amsterdam: Cambridge University Press.
Troelstra, A. und D. van Dalen (1988). Konstruktivismus in der Mathematik (Bände 1, 2), Amsterdam: Nordholland.
van Dalen, D. (1986). „Intuitionistische Logik“, in D. Gabbay und F. Guenther (Hrsg.), Handbuch der Philosophischen Logik (Band 3), Bordrecht: Reidel, S. 225–340.
van Ditmarsch, H., W. van der Hoek und B. Kooi (Hrsg.), (2007). Dynamische epistemische Logik (Synthesebibliothek, Band 337), Berlin: Springer..
von Wright, G. (1951). Ein Essay in Modal Logic, Amsterdam: Nordholland.
Wang, R.-J. (2009). "Wissen, Zeit und logische Allwissenheit", in H. Ono, M. Kanazawa und R. de Queiroz (Hrsg.), Logik, Sprache, Information und Berechnung, 16. Internationaler Workshop, WoLLIC 2009, Tokio, Japan, 21. Juni -24, 2009, Proceedings (Lecture Notes in Artificial Intelligence: Band 5514), Berlin: Springer, S. 394–407.
Yavorskaya (Sidon), T. (2001). „Logik der Beweise und Beweisbarkeit“, Annals of Pure and Applied Logic, 113 (1–3): 345–372.
–––. (2008). „Interacting Explicit Evidence Systems“, Theorie der Computersysteme, 43 (2): 272–293.
Yavorsky, R. (2001). „Provabilitätslogik mit Quantifizierern auf Beweisen“, Annals of Pure and Applied Logic, 113 (1–3): 373–387.

Akademische Werkzeuge

Sep Mann Symbol	Wie man diesen Eintrag zitiert.
Sep Mann Symbol	Vorschau der PDF-Version dieses Eintrags bei den Freunden der SEP-Gesellschaft.
Inpho-Symbol	Schlagen Sie dieses Eintragsthema im Indiana Philosophy Ontology Project (InPhO) nach.
Phil Papers Ikone	Erweiterte Bibliographie für diesen Eintrag bei PhilPapers mit Links zu seiner Datenbank.

Begründungslogik

Inhaltsverzeichnis: