НГУ

Форумы НГУ
Текущее время: Вс сен 24, 2017 12:07 pm

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




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

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
[В ответ на письмо от 11.10.2013, 13:25.]

> Из трех противосубботников трое завтра прийти
> в принципе смогут (единоразово).

Спасибо за отклик.
Тогда договоренность о завтрашней встрече (12-го октября) остается в силе.

> Но, вероятно, уйдут чуть ранее окончания
> чтобы к 12:30 успеть в универ.

А что нам мешает начать в 10:30 -- чтобы закончить в 12 с хвостом?
(Если судить по крестикам в голосовалке, возражений быть не должно.)

Ау, народ, как насчет 10:30?
Ждем возражений, а по умолчанию будем считать, что их нет.
Решение будет принято сегодня в 18:00.


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

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
[Возражения таки поступили.]

Итак, как и было запланировано, встречаемся завтра (12-го октября)
в 11:00 в ауд. 417 Института математики.

По просьбе публики мы сначала определим расписание, потом чуток
поиграем в теорию вычислимости и расстанемся в начале первого —
чтобы дать шанс противосубботникам успеть на занятия в НГУ.


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

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
Итак, сегодня в результате голосования крестиками, ноликами и смайлами,
повлекшего за собой оживленную дискуссию и два дополнительных голосования,
расписание наконец-то определилось. Сам удивляюсь, но оно получилось таким:

суббота, 18:00,
ауд. 417 Института математики

Оставшееся время мы посвятили воспоминаниям о теории вычислимости,
выяснили, что перечислимая контекстно свободная грамматика
способна порождать невычислимый язык, и задались аналогичным
вопросом о вычислимой грамматике, которая вскоре пригодится
при формализации понятия определения в рамках какой-либо теории.

До встречи 19 октября.


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

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

Язык вычислимой контекстно свободной граматики вычислим.
Более того, по данному слову из языка такой грамматики
алгоритмически строится его дерево вывода.
В частности, язык предикатов (вычислимой сигнатуры) вычислим.

Понятия подслова и его входжения в другое слово имеют свои тонкости
и гадости, преодолеваемые должным уточнением понятий
или своевременным применением здравого смысла.
То же относится и к процедуре подстановки термов вместо
свободных вхождений переменных (параметров) в формулы и термы.

Исчисление предикатов (гильбертовского типа, первого порядка,
с равенством) имеет вычислимое множество аксиом и правил вывода.

Теория — множество формул рассматриваемой сигнатуры.
Ее теоремы выводятся из логических аксиом (т.е. аксиом исчисления)
и специальных аксиом теории (т.е. формул самой теории).
Аксиоматика теории — теория с тем же множеством теорем.
Аксиоматизируемая теория — теория, имеющая вычислимую аксиоматику.

Мы остановились на эквивалентности следующих трех свойств теории:
(1) она аксиоматизируема (т.е. имеет вычислимую аксиоматику);
(2) она имеет перечислимую аксиоматику;
(3) множество ее теорем перечислимо.

До встречи 26 октября.


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

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

- модель сигнатуры (алгебраическая система),
- значение терма в модели,
- истинность формулы в модели,
- модель теории,

вспомнили, где и как формулируются и доказываются теоремы...

- о полноте исчисления,
- Гёделя о полноте (в двух формах),
- Мальцева о компактности,

не вспомню что, но что-то еще вспомнили,
и вплотную подошли к формализации понятия определения.

До встречи 2 ноября.


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

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

Занимаемся формализацией понятия определения (в теории).

Простейший вид определения:
расширение сигнатуры одним новым символом и добавление
новых аксиом, определяющих новый символ явно или неявно.

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

Теорема Бета: явная и неявная определимость равносильны.

В арифметике Пеано (включающей принцип индукции)
некоторые вполне безобидные на вид определения
на самом деле не являются определениями. Например,
сложение невозможно определить через остальные операции.
Более простой пример: добавляемые к арифметике аксиомы

f(0) = 0
f(x+1) = f(x)

не определяют унарную операцию f и вовсе не гарантируют,
что f(x) = 0 для всех x.

На очереди формализация более общего понятия определения,
допускающего введение бесконечного набора новых символов.

До встречи 9 ноября.


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

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

Элиминируемое расширение (расширение за счет определений)
аксиоматизируемой теории T сигнатуры S —
это аксиоматизируемая теория T* сигнатуры S*,
консервативно расширяющая T и допускающая элиминацию:
для любой формулы f сигнатуры S* существует формула g сигнатуры S
такая, что T* |- (f <=> g).

Всякое элиминируемое расширение допускает вычислимую элиминацию.

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

Всякое элиминируемое расширение эквивалентно явному.

На очереди: жизненный пример "бесконечного определения",
основные свойства определений, грамматическое расширение языка
за счет обозначений, понятие модели одной теории в другой.

До встречи 30 ноября.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Вс дек 01, 2013 12:14 pm 
Не в сети
Опытный автор

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

Элиминируемое расширение элиминируемого расширения
является элиминируемым расширением.

Объеднение двух независимых элиминируемых расширений
является элиминируемым расширением.

Следующая теорема родилась прямо на спецкурсе:

Если последовательность теорий T=T(0),T(1),...,T(n),... такова,
что T(n+1) — элиминируемое расширение T(n) (для всех n)
и объединение T* теорий T(n) (по всем n) аксиоматизируемо,
то T* является элиминируемым расширением T.

Жизненный пример бесконечного определения — расширение
арифметики введением бесконечного множества констант 1,2,3,...

В самом конце лекции во время рассмотрения другого примера
такого же рода — расширения арифметики термами вида
"сумма t(x) по всем x от 0 до s(y)" — лектора заглючило.

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

До встречи 7 декабря.


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

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

Общий метод придания смысла новым выражениям
(термам или формулам) в рамках какой-либо теории
заключается в добавлении к сигнатуре теории
нового символа для каждого такого выражения
(с арностью, соответствующей списку параметров выражения),
элиминируемом расширении теории, определяющим новые символы,
введением понятия канонического терма
и соглашением о краткой записи канонических термов
(формализуемом на уровне грамматики).

Традиционные индуктивные "определения" таких выражений,
как "x в степени y" или "сумма t(x) по всем x от 0 до y",
в рамках арифметики Пеано не являются определениями.
Например, расширение арифметики Пеано аксиомами
    2^(0) = 1
    2^(x+1) = 2^(x) * 2
не определяет унарный функциональный символ 2^.
В нестандартной модели арифметики Пеано существуют
различные интерпретации символа 2^, удовлетворяющие
указанным аксиомам и такие, что 2^(x) = 0 для некоторых x.

На очереди: доказательство анонсированных теорем,
поиск дополнительных определяющих аксиом,
общий метод формализации индуктивных определений.

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

До встречи 14 декабря


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

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

Порядковая структура любой счетной нестандартной модели PA:
начальный omega-фрагмент, за которым идут Z-фрагменты,
упорядоченные как множество рациональных чисел.

На всякой счетной нестандартной модели PA можно интерпретировать
сложение и умножение континуумом разных способов,
приводящих к попарно неизоморфным моделям PA.
(Это легко доказывается с помощью теоремы Гёделя о неполноте
и теоремы Лёвенгейма -- Скулема о счетных моделях.)

Существует модель PA, имеющая "бесконечно четный" элемент.

Две аксиомы 2^(0) = 1 и 2^(x+1) = 2^(x) * 2 не определяют унарный
функциональный символ 2^ (т.е. не образуют элиминируемое расширение),
так как существует модель PA, которую можно обогатить разными
интепретациями 2^, удовлетворяющими этим двум аксиомам.
Две такие интерпретации легко возникают в любой модели
с "бесконечно четным" элементом, и обе они не индуктивны.

Предположим, что в рамках PA можно определить унарный
функциональный символ 2^, удовлетворяющий тем двум аксиомам.
Тогда, добавив к тем двум аксиомам схему индукции
для расширенной сигнатуры (включающей символ 2^),
мы получим определение, т.е. элиминируемое расширение.

Анонс теоремы. В рамках PA можно определить унарный
функциональный символ 2^, удовлетворяющий тем двум аксиомам.

До встречи 21 декабря.
(Это будет последняя лекция в текущем семестре.)


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

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
Объявляется короткая встреча 25-го февраля (вторник)
с 14:05 до 14:15 в НГУ возле Мальцевской аудитории.

Цель — выбрать день и время первой лекции,
на которой мы, в частности, определим расписание спецкурса.

Предварительные предложения на сей счет можно высказать прямо тут.

P.S. В этом семестре у меня занят вторник с 14:15 до 17:35.


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

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
Очередная лекция спецкурса состоится
14-го марта (пятница) в 16:00
в фойе конференц-зала Института математики
(4-й этаж, после выхода из лифта сразу направо
и по коридору - до конца, в двухстворчатую дверь).

Там мы, в частности, согласуем дальнейшее расписание.


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

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
В результате голосования определилось расписание спецкурса:
понедельник в 14:xx.

Ближайшая лекция состоится
17 марта (понедельник) в 14:30 в Институте математики.
(Аудитория станет известна утром 17 марта.
Соответствующее объявление будет вывешено
на доске объявлений возле вахты Института математики.)

Начиная с 24 марта лекции будут проходить
в НГУ по понедельникам в 14:15.
(Аудитория определится позже.)


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

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

Как мы уже выяснили, аксиомы 2^0=1, 2^(x+1)=2*2^x
не определяют в PA унарную операцию 2^.
(На нестандартной модели PA имеется как минимум
континуум операций, удовлетворяющих этим аксиомам.)
Есть надежда, что определение возникнет,
если к этим аксиомам добавить схему индукции
для расширенной сигнатуры (включающей символ 2^).
Это действительно так, но пока у нас есть лишь надежда,
ибо на нестандартной модели PA не очевидны ни существование,
ни единственность операции с такими свойствами.

Упомянутый выше факт легко доказать, владея арифметической
формулой p(x,y), для которой в PA доказуемо
(A x)(E! y) p(x,y) & p(0,1) & (A x)(A y)( p(x,y) => p(x+1,2y) ).
Нам предстоит обнаружить такую формулу p(x,y).

Успешный опыт определения аналогичной операции в рамках ZFC
наталкивает на мысль о том, что задача может быть решена
после должного кодирования кортежей.

Есть очень простые способы кодирования пар, троек и т.д.,
но они не являются достаточно универсальными,
чтобы привести к требуемой формуле p(x,y).
Нужно изобрести универсальный способ кодирования кортежей,
в котором длина кортежа была бы не метанатуральным числом,
а переменной, "внутренним" параметром формулы.

Текущая цель: определить в PA бинарную операцию eval(s,i),
для удобства обозначаемую через s[i],
со следующим двумя свойствами:

(1) (A x)(E s)( s[0]=x );
(2) (A s)(A n)(A x)(E t)( (A i<n) t[i]=s[i] & t[n]=x ).

Свойства (1) и (2) очень мощны.
В частности, метаиндукцией легко доказать, что они
обеспечивают кодирование кортежей любой стандартной длины:
(A x_0,...,x_n)(E s)( s[0]=x_0 & ... & s[n]=x_n ).

В основе гёделевского кодирования со свойствами (1) и (2)
лежит китайская теорема об остатках.

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


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

Зарегистрирован: Пн май 02, 2005 7:27 pm
Сообщения: 433
Ближайшая лекция состоится 17 марта (понедельник)
в 14:30 в Институте математики в ауд. 417.

Мы хотели было перенести лекции в НГУ,
но оказалось, что там в нужное нам время нет свободной аудитории.

Пока договорились встречаться в ИМ в ауд. 417
по понедельникам в 14:20.


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

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


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

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


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

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