> И этот результат тоже не предполагает непротиворечивость известной

Да, конечно.

Я не вполне понимаю, почему это не преобразуется в формальное доказательство отсутствия корней в рамках данной арифметики (и, тем самым, в доказательство противоречивости данной арифметики) следующим способом: рассмотрим арифметику P; из утверждения "неверно, что данный полином не имеет корней" следует, что из P выводим "false"; тем самым из P следует, что из утверждения "неверно, что данный полином не имеет корней" следует "false"; тем самым из P следует, что "данный полином не имеет корней".