Во всякой достаточно богатой непротиворечивой теории первого порядка (в частности, во всякой непротиворечивой теории, включающей формальную арифметику), существует такая замкнутая формула F, что ни F, ни не являются выводимыми в этой теории. То есть: в любой достаточно сложной непротиворечивой теории существует утверждение, которое средствами самой теории невозможно ни доказать, ни опровергнуть.