НГУ

Форумы НГУ
Текущее время: Пт ноя 24, 2017 8:48 am

Часовой пояс: UTC + 7 часов




Начать новую тему Ответить на тему  [ Сообщений: 51 ]  На страницу Пред.  1, 2, 3, 4
Автор Сообщение
 Заголовок сообщения:
СообщениеДобавлено: Пн мар 17, 2014 5:58 pm 
Не в сети
Опытный автор

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
17 марта

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

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

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

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пн мар 24, 2014 5:16 pm 
Не в сети
Опытный автор

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
24 марта

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пн мар 31, 2014 5:19 pm 
Не в сети
Опытный автор

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
31 марта

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Вт апр 15, 2014 5:55 pm 
Не в сети
Опытный автор

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
14 апреля

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Ср апр 23, 2014 2:09 pm 
Не в сети
Опытный автор

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
21 апреля

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

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

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

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Пн апр 28, 2014 6:04 pm 
Не в сети
Опытный автор

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
28 апреля

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

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


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 51 ]  На страницу Пред.  1, 2, 3, 4

Часовой пояс: UTC + 7 часов


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Перейти:  
Создано на основе phpBB® Forum Software © phpBB Group
Русская поддержка phpBB