Begründungslogik

Begründungslogik, im Englischen oft Justification Logic, ist ein logischer Rahmen zur formalen Modellierung von Begründungen für Behauptungen. Im Gegensatz zur herkömmlichen epistemischen Logik, die allein den Operator K kennt, führt Begründungslogik explizite Begründungstermon ein. Formell spricht man von Formeln der Form t:A, was bedeutet, dass der Term t eine Begründung für A liefert. Begründungstermine lassen sich zusammensetzen, wodurch Begründungsketten abgebildet werden können.

Der Sprachaufbau umfasst Begründungstermvariablen, Begründungskonstanten und Operatoren wie · (Anwendung) und + (Summe); in vielen Systemen gibt es weitere Operationen wie ! (Beweisprüfer). Die Axiome regeln, wie Begründungen kombiniert werden können: Aus einer Begründung für A und einer Begründung für A→B folgt eine Begründung für B; Begründungen können durch Addition weiterer Begründungen erweitert werden. Semantische Modelle wie Fitting-Modelle oder Mkrtychenko-Modelle verwenden Evidenzrelationen oder Begründungsmengen, um die Gültigkeit von t:A zu interpretieren. Constant Specifications ordnen Konstanten feste Begründungen zu.

Historisch wurde Begründungslogik von Sergei Artemow in den späten 1990er bis frühen 2000er Jahren eingeführt, um epistemische Aussagen durch explizite Begründungen zu analysieren. Seitdem hat sich das Gebiet als eigenständige Forschungsrichtung in Philosophie, Erkenntnistheorie und Informatik etabliert und findet Anwendung in formalen Beweisstrukturen sowie in sicherheitskritischen Protokollen.

Begründungslogik steht in enger Beziehung zur epistemischen Modallogik: Wissen wird oft als t:A verstanden, wobei geeignete Bedingungen für Begründungen erfüllt sein müssen. Realisationstheoreme zeigen, wie JL-Formeln in modal-logische Systeme wie S4 oder S5 überführt werden können. Kritisch diskutiert werden u.a. die Abhängigkeit von Wahrheit von Begründungen und die damit verbundenen Komplexitätsfragen.