Изменения
Нет описания правки
Чтобы представить доказательства, мы будем объединять строки вместе так же, как
объединяем символы в строки: <tex>2^{2^3} \cdot 3^{2^5}</tex> — это последовательность из двух строк, первая — это <<"(>>", а вторая — <<")>>".
Теперь мы можем понять, как написать программу, проверяющую корректность доказательства некоторого утверждения в формальной арифметике. Наметим общую идею. Программа будет состоять из набора рекурсивных отношений и функций, каждое из которых выражает некоторое отношение, содержательное для проверки доказательства. Ниже мы покажем идею данной конструкции, приведя несколько из них.
