Begründung-Logik kann als das explizite Gegenstück von Modallogik gesehen werden. Statt zu sagen "A ist notwendig" ([]A), ist es hier möglich, zu sagen "A ist notwendigerweise wahr wegen t" (t : A), wobei der Begründungsausdruck t sogar aus mehreren Begründungen geformt werden kann. Die formale Verbindung zwischen Modallogik und Begründung-Logik, ist gegeben durch Realisierung. Das ist eine Prozedur, bei der []-s durch Begründungsausdrücke ersetzt werden, wodurch eine Begründungsformel entsteht. Sergei Artemov bewies, dass die Modallogik S4 in die Logic of Proofs LP realisiert werden kann, wobei ein schnittfreier Sequenzenkalkül für S4 verwendet wird. Derzeit wird vermutet, dass es keinen schnittfreien Sequenzenkalkül für S5 gibt. Um S5 syntaktisch in eine Begründung-Logik zu realisieren, muss eine andere Methode gesucht werden. S5 ist in einige seiner Begründung-Gegenstücke realisiert worden, wobei ein Hypersequenzen-System oder ein verschachtelter Sequenzenkalkül sowie verschiedene Realisierungen des negativen Introspektionsaxioms verwendet wurden. In dieser Arbeit wird mit Hilfe eines Hypersequenzenkalküls gezeigt, dass S5 in alle zehn Begründungs-Logik-Gegenstücke realisiert werden kann, die mit diesen verschiedenen Realisierungen des negativen Introspektionsaxioms konstruiert werden können. Um das gleiche Resultat zu bekommen, wenn nicht modulare-verschachtelte Sequenzen wie von Kai Brünnler eingeführt verwendet werden, müssen zu viele ähnliche Falle unterschieden werden, und daher wird das nur für einige weniger standard Realisierungen gemacht. Für die komplette Liste mit Realisierungen wobei verschachtelte Sequenzen verwendet werden, werden die verschachtelte Sequenzenkalküle, eingeführt von Lutz Straßburger, verwendet, dieses Kalkül ist auf grund ihter modularen Nature besser geeignet für dieses Ziel. Diese Modularität macht es möglich die Regeln unabhängig von den anderen Regeln und dementsprechend, von dem Begründungsoperationen die mit die anderen Regeln korrespondieren zu realisieren. Obwohl konzentriert wird auf die Realisierungen von S5, gewährleistet die Modularität von Straßburger's Kalkül, dass die gegebenen Beweise vollständig modulare Realisierungs Sätze für alle Modal-Logiken in des Modalkubus zwischen K und S5 impliziert.
de
Justification logic can be seen as an explicit counterpart of modal logic. Instead of saying "A is necessary" ([]A), it is possible to say "A is necessarily true because of t"(t : A), where the justification term t can even be constructed from more than one justification. The formal way of studying the connection between modal logic and justification logic is called realization, this is a procedure that replaces []-s in a modal formula with terms, to create a justification formula. Sergei Artemov proved that the modal logic S4 is realizable into the logic of proofs LP, using a cut-free sequent system for S4. At the moment, it is believed that there exists no cut-free sequent system for S5. Thus to be able to realize S5 into some justification logic syntactically, another method had to be searched. Using different realizations of the negative introspection axiom, S5 has been realized into some of its justification counterparts by using a hypersequent system or a nested sequent system. In this thesis it will be shown, using hypersequents, that S5 is realizable into any of the ten justification counterparts that can be constructed with these different realizations of the negative introspection axiom and can be found in the literature. In order to establish the same result using non-modular nested sequents as introduced by Kai Brünnler, too many similar cases have to be considered and, therefore, only some of the less standard realizations will be shown. For the complete list of realizations using nested sequents, the nested sequent calculi introduced by Lutz Straßburger will be employed, these calculi are better suited for this purpose due to their modular nature. This modularity makes it possible to realize each rule independent of the other rules and, accordingly, of the justification operations corresponding to the other rules. Even though the focus lies on the realizations of S5, the modularity of Straßburger's calculi ensures that the given proofs imply fully modular realization theorems for all modal logics in the modal cube between K and S5.
