Автор: veprus
Дата сообщения: 16.05.2002 13:38
Если математик, то тогда я буду говорить специальными терминами.
У меня сейчас нет возможности посмотреть русскую литературу, поскольку далеко я от Родины, уверен лишь, что большую часть того, что я здесь сейчас скажу можно найти в учебнике "Математическая логика" Ершова и Палютина.
И так.
Формальная арифметика Пеано есть стандартное исчисление предикатов, плюс набор из 10 аксиом, коммутативность, ассоциативность, существование нуля, существование следующего и т.д. У нас есть набор констант (0), набор функциональных символов, набор переменных, набор предикатных символов.
Определение терма.
1. Константа и переменная суть термы.
2. Если f - n-арный функциональный символ, и x_1,...,x_n - термы, то f(x_1,...,x_n) - терм.
3. Других термов нет.
Определение предиката.
1. Любой терм является предикатом.
2. Если P - n-арный предикатный символ и x_1,...,x_n - термы, то P(x_1,...,x_n) - предикат.
3. Если x - переменная, P - предикат, то {forall}xP и {exist}xP - предикаты.
4. Других предикатов нет.
Предикат считается истинным, если он выполним в данной модели (или, что тоже самое, если он выводим из данной системы аксиом) и ложным в противном случае.
Частично-рекурсивные функции - это функции, получаемые из 3-х базовых с помощью операторов суперпозиции, минимизации и еще какого-то (названия не помню, да это и не важно).
Поскольку все здесь строится очень конкретно, можно ввести нумерацию предикатов, переменных, функций и т.д. Не буду уже рассказывать как. Причем нумерацию взаимнооднозначную, совместно с декодирующей вычислимой функцией.
Теорема Геделя. Не существует частично рекурсивной функции, которая по номеру предиката выдавала бы 0 в том случае, когда он истинный и 1, когда он ложный (немного вольная трактовка но смысл такой).
В различных источниках доказывается эквивалентность частично-рекурсивных функций, машин Тьюринга, машин Проста. Кроме того, любой язык программирования имеет такую штуку (не помню как называется, нечто вроде логической схемы), которая полностью формально описывает язык и позволяет доказать, что он эквивалентен машинам Тьюринга. Я сам в свое время доказывал такую штуку для Паскаля и Пролога. Вообще пролог это в чистом виде исчисление предикатов и потому для него это все очень просто доказывается.
К сожалению, мои студенческие лекции не доступны, а восстановить список литературы по памяти я уже не могу. Точно помню, что лекции на тему пролога были вообще по журналам и какой-то английской книге.
Мораль: Машина НИКОГДА не сможет заменить человека даже в таком простом вопросе, как арифметика. И даже не просто арифметика, а полностью формализованная арифметика Пеано (вообще говоря, она поменьше, чем просто вся арифметика).
будет дружить с вирусняком всяким... 
