s. A: KIuPKB entwickelte in einer einheitIichen Systematik vollstlindige Interpretationen fiir viele Systeme der Modalitatenlogik, die vorber nur syn­ taktisch fixiert waren. Hiermit ergab sich auf dem Wege tiber eine quantoren­ logische Erweiterung des Modalitatensystems S4 zugleich eine Semantik fUr die intuitionistische Priidikatenlogik:. Der vorliegende Ergebnisbericht behandelt im Rahmen der klassischen Priidikatenlogik: zwei Modalitatensysteme, deren aussagenlogische Teile mit den Systemen M von v. WRIGHT und S4 von LEWIS tibereinstimmen. Es gibt verschiedene Moglichkeiten, aussagenlogische Modalitatensysteme quantoren­ logisch zu erweitem. Die hier (...) gewiihlten Erweiterungen sind in einer nabe­ liegenden Weise so vorgenommen, daB die Barcan-Formel (Seite 7) ungiiltig, aber ihre Umkehrung giiltig ist. Fiir die Kripke-Semantik dieser Systeme wird im m. Kapitel ein Voll­ stlindigkeitsbeweis nach den Methoden von KIuPKE [13] durchgefiihrt. Bin einfacherer Vollstiindigkeitsbeweis, der aber wesentIich weniger konstruktiv ist, wird in § 4 in Verallgemeinerung der Methode von HENKIN [7] gegeben. Durch eine Binbettung der intuitionistischen Priidikatenlogik: in das quan­ torenlogische Modalitatensystem S4' flihrt die Semantik des Systems S4' zur Kripke-Semantik der intuitionistischen Priidikatenlogik. Diese Semantik wird im V. Kapitel systematisch behandelt und im VI. Kapitel (iihnlich wie in KIuPKB [J3D mit der Semantik von BETH in Beziehung gebracht. (shrink)

A recursive notation system of a strong segment of ordinals was developped by Jäger [3]. An unessential modified versionT(J) of this notation system was described in [4]. In the following, the well-ordering ofT(J) is proved in a formal system of second order arithmetic with the axiom schema ofΠ 2 1 -comprehension. It follows, that the proof theoretical ordinal ofΠ 2 1 -analysis is greater than the order type ofT(J).

This paper gives a recursive generalization of a strong notation system of ordinals, which was devellopped by Jäger [3]. The generalized systemT(V′) is based on a hierarchy of Veblen-functions for inaccessible ordinals. The definition ofT(V′) assumes the existence of a weak Mahlo-ordinal. The wellordering ofT(V′) is provable in a formal system of second order arithmetic with the axiom schema ofΠ 2 1 -comprehension in a similar way, as it is proved in [6] for the weaker notation systemT(V′).