По теореме Гёделя о неполноте, в применимости к многочленам от целых переменных, можно утверждать, что существуют многочлены, неравные нулю, и это неравенство нулю, не доказуемо из аксиом арифметики.
В ВТФ такие многочлены могут возникать.
Свойства таких многочленов: они алгоритмически не перечислимы.
Т.е. достаточно чтобы в ВТФ содержались такие многочлены, и тогда ВТФ в результате непротиворечивости арифметики доказуема только после того как будут выявлены все такие многочлены.
Такие многочлены могут возникать при различных степенях, напимер:
при фиксированном