Теорема Гёделя. 
Дискретный анализ. 
Формальные системы и алгоритмы

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

В примере 3.31 мы ввели язык формальной арифметики. В него входят формулы в сигнатуре 0? /о, Е? Р2, г/ G Ji, х? + € J~2' В примере 3.33 были выписаны аксиомы формальной арифметики. Выводимые из этих аксиом утверждения называются теоремами формальной арифметики.

Стандартная модель формальной арифметики имеет в качестве области интерпретации множество натуральных чисел N = {0,1,… }, константа 0 интерпретируется как 0 из множества N натуральных чисел, Е как предикат равенства,.

v как функция следования, х как функция умножения, + как функция сложения. Это действительно модель, поскольку легко проверить истинность аксиом. Поэтому все теоремы формальной арифметики истинны в стандартной модели (рассуждение аналогично доказательству корректности исчисления предикатов). Другими словами, формальная арифметика корректна, относительно стандартной модели и, значит, непротиворечива (например, формула Е (0, z/(0)) невыводима, поскольку она интерпретируется как ложное равенство 0 = 1).

Замечание 4.74. Важно отметить, что приведённые выше доводы в пользу корректности и непротиворечивости формальной арифметики опираются на нашу уверенность в том, что содержательно арифметика непротиворечива. Анализ этой правдоподобной гипотезы представляет куда более сложную задачу.