اكتمال التسلسلات الأولية الذرية

في حساب المتتابعات ، تنص نظرية اكتمال المتتابعات الذرية الأولية على أنه يمكن اشتقاق المتتابعات الأولية $A ⊢ A$ (حيث $A$ صيغة اختيارية ) من المتتابعات الذرية الأولية $p ⊢ p$ (حيث $p$ صيغة ذرية ) . تؤدي هذه النظرية دورًا مشابهًا لتوسيع إيتا في حساب لامدا ، وهي مقابلة لحذف القطع واختزال بيتا . ويمكن عادةً إثباتها بالاستقراء على بنية A ، $وهو$ أسهل بكثير من حذف القطع.