On the concept of relatively uniform realizability of propositional formulas (Q1204621)

Der Autor betrachtet den Begriff \(e\text{r}F\) (die natürliche Zahl \(e\) realisiert die geschlossene arithmetische Formel \(F\)) im Sinne von \textit{S. C. Kleene} ``Introduction to metamathematics'' (1952; Zbl 0047.007). Für eine aussagenlogische Formel \(A(p_ 1, \dots, p_ n)\) sei \(A(F_ 1, \dots, F_ n)\) das Resultat der Substitution von \(p_ 1,\dots,p_ n\) durch arithmetische Formeln \(F_ 1, \dots, F_ n\) in \(A\). \(A(p_ 1, \dots, p_ n)\) heißt realisierbar, wenn es einen Algorithmus gibt, der für geschlossene arithmetische Formeln \(F_ 1, \dots, F_ n\) die natürliche Zahl \(e\) konstruiert, so daß \(e \text{r} A(F_ 1, \dots, F_ n)\). Für eine Klasse \(K\) von geschlossenen arithmetischen Formeln nennt man \(A(p_ 1, \dots, p_ n)\) \(K\)-uniform realisierbar, wenn es eine natürliche Zahl \(e\) gibt, so daß \(e \text{r} A(F_ 1, \dots, F_ n)\) für alle \(F_ 1,\dots, F_ n\in K\). Sei \(L\) die Klasse von Formeln \(\exists x(x+1=n)\), \(n=0,1,2, \dots\;\). Es wird ein Theorem bewiesen, das bestätigt, daß aus der \(L\)-uniformen Realisierbarkeit die Realisierbarkeit nicht folgt.