Диофантовы уравнения и формальная математика

По теореме Ю.В. Матиясевича, всякое перечислимое множество диофантово; в частности, диофантовым является множество теорем формальной теории. Доказательство этой теоремы конструктивно и позволяет в принципе построить диофантово уравнение, разрешимость которого эквивалентна выводимости в этой теории. Я опишу диофантово уравнение, кодирующее выводимость в аксиоматической теории множеств.