Выдержка из книги
Клини С.К.
Введение в математику
Наша цель при формализации теории - выявить условия, которые определяют, какие предложения имеют место в смысле доказуемости в этой теории ( § 15), или, короче, - дать явное определение понятия доказательства. Мы можем выразить это требование также словами, сказав, что 9t ( x, Y) должен быть эффективно разрешимым метаматематическим предикатом.