НГУ

17 марта

Мы в общих чертах изучили подход Гёделя к кодированию кортежей
и, основываясь на аналоге китайской теоремы об остатках,
определили в рамках PA функциональный символ eval(s,i) =: s[i],
обладающий упомянутыми выше свойствами (1) и (2).

Стало быть, теперь в PA строго формализовано понятие кортежа
(у которого длина задается переменной, а не метанатуральным числом).

В частности, в рамках PA определима степень, да и многое другое:
например, суммирование и произведение термов по конечным отрезкам.

Следствие: добавление индукции к аксиомам 2^0=1, 2^(x+1)=2*2^x
приводит к (однозначному) определению в PA.

На очереди:
примеры формальных определений в теории множеств,
понятие интерпретации (= внутренней модели) одной теории в другой,
метод доказательства относительной совместности,
основанный на внутренних моделях.

До встречи 24 марта.

24 марта

Построено элиминируемое расширение ZFC,
формализующее употребление термов вида
{x in t(y) : f(x,y,z)}.

Технически аналогичный подход будет использован
при определении понятия внутренней модели.

До встречи 31 марта.

31 марта

Введено понятие интерпретации (внутренней модели) сигнатуры
в элиминируемом расширении теории другой сигнатуры.
Формализовано понятие значения терма в такой интерпретации.

До встречи 7 апреля.

14 апреля

Формализовано понятие истинности формулы во внутренней модели сигнатуры.
Установлены правила подстановки значений термов при вычислении истинности во внутренней модели.
Во внутренней модели сигнатуры истинны все аксиомы исчисления предикатов.
Совокупность формул, истинных во внутренней модели сигнатуры, замкнута относительно правил вывода.
Во внутренней модели сигнатуры истинны все тавтологии исчисления предикатов.
Формализовано понятие внутренней модели одной теории в другой теории.
Во внутренней модели теории истинны все теоремы этой теории.

До встречи 21 апреля.

21 апреля

Истинность во внутренней модели не обязана коммутировать с подстановкой термов:
бывает так, что f(x) истинно при x=1, но f(1) ложно.

Если существует внутренняя модель теории S в непротиворечивой теории,
то теория S непротиворечива.

При построении внутренней модели теории S в теории T
(с целью доказательства относительной совместности S)
можно консервативно расширять T.

Если M — внутренняя модель теории S в непротиворечивой теории T
и в T доказуемо, что f ложно в M, то f недоказуемо в S.

Внутренние модели, зависящие от параметров.
Метод фиксации параметров (консервативное расширение с введением констант).

До встречи 28 апреля.

28 апреля

* Если M - внутренняя модель теории S в теории T и S* - элиминируемое расширение S, то существуют элиминируемое расширение T* теории T и распространение интерпретации M на сигнатуру S* такие, что M является внутренней моделью S* в T*.
* В связи с доказательством предыдущей метатеоремы - наблюдение: не всякая теория допускает элиминируемое расширение с константой.
* Теория BA булевых алгебр, будучи теорией с сигнатурой {<,0,1,or,and,not}, является элиминируемым расширением теории с сигнатурой {<}.
* Понятие внутренней булевозначной модели сигнатуры.
* Определение истинности бескванторных формул во внутренней булевозначной модели сигнатуры.
* Понятие полной внутренней модели BA.
* Определение истинности любых формул во внутренней булевозначной модели сигнатуры с полной моделью BA.

До встречи в следующем семестре.