Es sei eine
-aufzählbare
Satzmenge, die axiomatisiert, und es sei
, ,
eine -Aufzählung von . Es sei
, ,
eine -Aufzählung der prädikatenlogischen Tautologien aus . Wenn ein Satz aus ableitbar ist, so gibt es eine endliche Auswahl aus
(bzw. aus der gewählten Aufzählung)
derart, dass
-
eine prädikatenlogische Tautologie ist. Daher leistet das folgende Verfahren, bei dem wächst, das Gewünschte: Für jedes notiert man die Tautologien in der Form
-
Wenn überhaupt diese Form besitzt, so ist diese eindeutig bestimmt. Danach überprüft man für jedes
,
ob alle zu gehören. Falls ja, und wenn ein Satz ist, so wird notiert. Danach geht man zum nächsten . Wenn man
,
erreicht hat, so geht man zu , wobei man aber wieder bei
anfängt.