| Buchprofil | |||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||
|
| Inhalt |
| Ein Fragment der Stärke und mit den beweisbar rekursiven Funktionen von n iterierten induktiven Definitionen erhält man durch die folgende Einschränkung der Prädikatenlogik zweiter Stufe. Die zugrunde liegende Sprache erlaubt nur bis zu n+1 geschachtelte zweitstufige Quantifikationen und diese sind dergestalt, daß keine zweitstufige Variable frei im Gültigkeitsbereich eines anderen zweitstufigen
Quantors vorkommt.
Die beweisbar rekursiven Funktionen werden auch charakterisiert als dasjenige Fragment des polymorphen lambda-Kalküls mit denselben Einschränkungen auf Typvariablen. Die Hinzunahme von Induktion über arithmetische Formeln zu den Fragmenten der Prädikatenlogik zweiter Stufe beeinflußt nur die arithmetischen Konsequenzen dieser Theorien, wohingegen die Hinzunahme voller Induktion die Stärke um eine induktive Definition erhöht. Endlich iterierte induktive Definitionen sind äquivalent zu demjenigen Fragment der Prädikatenlogik zweiter Stufe, das auf eine einzige Prädikatenvariable eingeschränkt ist. |
Copyright 1996-2021 HARLAND media
Dr. Peter E. Harland
Ernst-Thälmann-Str. 16
07747 Jena