(Оффтоп)
Я много лет не читал детективов. Теперь я изучаю некоторые математические книги как будто читаю детектив.
«... мы теперь обращаемся к рассмотрению
теорий первого порядка ...» Страница 65. Что такое теории первого порядка Мендельсон не рассказывает. Он просто сообщает, чем мы при этом будем пользоваться из уже определённого, забыв при этом про кванторы, (о чем я уже писал). Дальше идет слово: «Аксиомы» и ещё через пару страниц: «теорема», «непротиворечивость» и, наконец, показался значок «
». Никаких упоминаний об этих терминах для исчисления первого порядка нет. И тут-то и разворачивается глава из детектива. Я помню, что все эти термины определялись в исчислении высказываний. Лезу в параграф 4 главы первой. Параграф озаглавлен «Система аксиом для исчисления высказываний» страница 36 и читаю:
«
Формальная (аксиоматическая) теория считается определенной, если выполнены следующие условия:
(1) Задано некоторое счетное множество символов — символов теории
. Конечные последовательности символов теории
называются
выражениями теории
.
(2) Имеется подмножество выражений теории
, называемых
формулами теории
. ...
(3) Выделено некоторое множество формул, называемых
аксиомами теории
. ...
(4) Имеется конечное множество
отношений между формулами, называемых правилами вывода. Для каждого
- существует целое положительное
такое, что для каждого множества, состоящего из
формул, и для каждой формулы
эффективно решается вопрос о том, находятся ли данные
формул в отношении
с формулой
, и если да, то
называется
непосредственным следствием данных
формул по правилу
.»
И вдруг я осознаю, что от начала параграфа и до этого определения и во время этого определения никто не указал, что те из определяемых символов, которые будут буквы обязаны быть пропозициональными буквами. Итак, появились «аксиомы», дальше «теоремы», «вывод», «следствие множества формул», «свойства выводимости». Мне уже стало интересно, ведь, скоро теорема о дедукции, а она для исчисления предикатов выглядит иначе чем для исчисления высказываний. Но в самом конце следующей страницы 37 детектив прервался и громкий голос сказал: «Мы введем теперь формальную аксиоматическую теорию L для исчисления высказываний.» Интересно, если бы автор хотя бы упомянул, говоря теориях первого порядка, о том, что все определения и выводы о понятии формальной (аксиоматической) теории нужно брать в главе об исчислении высказываний, то материал усваивался бы хуже? На днях получу пятое издание посмотрим, что там делается.