ENTSCHEIDBARKEIT DER ARITHMETIK MIT ADDITION UND ORDNUNG I N LOGIKEN MIT VERALLGEMEINERTEN QUANTOREN von HELMUT WOLTER in Berlin (DDR) M. PRESBURGER hat in [4] die Entscheidbarkeit der Arithmetik mit Addition nachgewiesen. I n der vorliegenden Arbeit werden Entscheidbarkeitsuntersuchungen fur arithmetische Theorien mit Addition und Ordnung in Sprachen mit Machtigkeitsquantoren bzw. mit CHANa-Quantor vorgenommen. Hierzu sei I! ein elementarer Formalismus mit einem Zeichen ,,<" fur die Ordnung, einem Zeichen , , = I ' fiir die Identitiit, einem zweistelligen Funktionenzeichen ,, + " fur die Addition und zwei Individuenzeichen ,,O", ,,l" fur Null und Eins. 1st A eine Menge von Ordinalzahlen, dann entstehe 2, aus 2 durch Hinzunahme neuer Quantoren Q, fur oc ELI, wobei Q, als Machtigkeitsquantor ,,cs gibt N , viele" interpretiert wird. 1st d = (a}, dann schreiben wir fiir 2, auch 2,. Aus den Ergebnissen von H. APELT [l] folgt, daB die Theorien der Standardmodelle dtbr Arithmetik der naturlichen Zahlen und der ganzen Zahlen mit Addition und Ordnung in 2, entscheidbar sind. In [5] gab der Verfasser einen Oberblick uber alle widerspruchsfreien und vollstandigen Erweiterungen der elementar-vollstandigen Arithmetik mit Addition und Ordnung in 2, und zeigte, dafl alle diese Erweiterungen mit Elimination der Quantoren entscheidbar sind. I n der vorliegenden Arbeit werden diese Ergebriisse wesentlich verallgemeinert. Wir geben einen uberblick uber alle widerspruchsfrcbicm und vollstandigen Erweiterungen der in Frage stehenden elementar-vollstandigen Arithmetik in 2 , und 2(,,bl und zeigen die Entscheidbarkeit dieser und gewisser verwand t'er Theorien. \Yir betrachten zunachst die elementare Theorie der ganzen Zahlen mit Addition und Ordnung. Bekanntlich besitzt diese Theorie ein vollstandiges elementares Axiomensystem C (vgl. [l]). C ist in 2 , nicht vollstandig, da weder H, = 3zQ,y(O < y < x) noch i H , aus C folgen. Denn im Standardmodell von C (im Bereich der ganzen Zahlen) gilt i H , u n d in allen Nicht-Standardmodellen von C i s t H , gultig. Folglich sindC u {H,} und C w ( i H , } widerspruchsfrei. Dies gilt auch, wenn man Qo durch den &ma-Quantor Qc ersetzt und Modelle der Machtigkeit N, betrachtet. Da fur die entsprechende Logik QC das aufsteigende Theorem von L~WENHEIM-SKOLEM gultig ist (vgl. [3] und [Z I), erhalt man hieraus die Widerspruchsfreiheit von C w ( H a } und C v { i H , } .
EY sei bemerkt, daB wir wie ublich 2 , nur in Modellen der Miichtigkeit 2 u, interpret ieren.
Fur Q, schreiben wir im folgenden einfach Q, was nicht zu Verwechslungen fiihren wird.
Um das Eliminationsverfahren fiir die Arithmetik in 2 , durchfiihren zu ktinnen, erweitern wir 2 , definitorisch durch Hinzunahme der einstelligen Relationenzeichen ,,n 1" fur 2 n < W , eines zweistelligen Relationenzeichens ,, U" und eines zweistelligen Funktionenzeichens ,, -.