In diesem Text untersuchen wir die Logik des formalisierten Beweisbarkeitsprädikates. Wir geben eine Definition dieses Prädikates. Wir definieren die Begriffe von immer beweisbaren und immer wahren Sätzen der Peano Arithmetik. Wir führen das modal-logische System GL ein. In Kapitel 2 befassen wir uns mit den Klassen immer beweisbarer und immer wahrer Sätze, die ohne Prädikate gebildet werden können. Wir zeigen, dass GL erstere Klasse vollständig axiomatisiert. Aus GL gewinnen wir das System GLS und zeigen, dass dieses zweitere Klasse vollständig axiomatisiert. In Kapitel 3 befassen wir uns mit den Klassen immer beweisbarer und immer wahrer Sätze, die mit Prädikaten gebildet werden können. Wir suchen Systeme, die diese Klassen axiomatisieren. Wir zeigen, dass es keine solchen Systeme gibt.

In this text we investigate the logic of the formal provability predicate. A definition of this predicate is given. The notions of the classes of always provable and always true sentences of PA - Peano Arithmetic - are defined. We introduce the modal system GL. In chapter 2 we show that in the propositional case that system completely axiomatizes the class of always provable sentences. From there we introduce the system GLS and show that this system does the same for the class of always true sentences. In chapter 3 we investigate the same question, but this time for the quantificational case. Our results are negative. There are no systems that axiomatize the class of the always true or the always provable sentences.