17 марта
Мы в общих чертах изучили подход Гёделя к кодированию кортежей
и, основываясь на аналоге китайской теоремы об остатках,
определили в рамках PA функциональный символ eval(s,i) =: s[i],
обладающий упомянутыми выше свойствами (1) и (2).
Стало быть, теперь в PA строго формализовано понятие кортежа
(у которого длина задается переменной, а не метанатуральным числом).
В частности, в рамках PA определима степень, да и многое другое:
например, суммирование и произведение термов по конечным отрезкам.
Следствие: добавление индукции к аксиомам 2^0=1, 2^(x+1)=2*2^x
приводит к (однозначному) определению в PA.
На очереди:
примеры формальных определений в теории множеств,
понятие интерпретации (= внутренней модели) одной теории в другой,
метод доказательства относительной совместности,
основанный на внутренних моделях.
До встречи 24 марта.
|