Написал учебник теории категорий

[beroal]

george66 в сообщении #1305151 писал(а):

И учебник, учебник читайте

Вместо учебника скачивается какой-то файл HTML.

[george66]

https://github.com/George66/Textbook/bl ... 8F%209.pdf
А так?

[beroal]

george66 в сообщении #1305259 писал(а):

https://github.com/George66/Textbook/blob/master/%D0%A3%D1%87%D0%B5%D0%B1%D0%BD%D0%B8%D0%BA%20%D0%B2%D0%B5%D1%80%D1%81%D0%B8%D1%8F%209.pdf
А так?

Именно по этой ссылке я скачивал.

[grizzly]

beroal
Перейдите по ссылке на github и найдите прямо над обложкой (справа, сверху) кнопку "Download". У меня по ней нормально скачивается.

[beroal]

grizzly в сообщении #1305272 писал(а):

beroal
Перейдите по ссылке на github и найдите прямо над обложкой (справа, сверху) кнопку "Download". У меня по ней нормально скачивается.

То есть надо открыть документ в браузере. После этого мой Firefox довольно быстро зависает. Но я всё-таки успел скопировать ссылку. Правильная ссылка: https://raw.githubusercontent.com/Georg ... 8F%209.pdf .

[george66]

В крайнем случае могу прислать по почте.

[пианист]

(Оффтоп)

george66 в сообщении #1241695 писал(а):

Про топос графов популярная статья
https://arxiv.org/abs/math/0306394

Прошу прощения за офтоп, но не хочется из-за одного пустякового вопроса создавать тему..
Вопрос по этой статье.
На 3 странице утверждается, что the representable $A$ это вот такой вот граф
$s \stackrel{A}{\to} t$,
где $A$, $s$, $t$ объект и стрелки из категории
$\xymatrix{N\ar@/^10pt/@{->}[rr]^{s} \ar@/_10pt/@{->}[rr]^{t} &&A}$
Собс-но, вопрос, почему/в каком смысле?
Вроде бы, the representable $A$ это функтор, который объект $A$ отображает в множество $\{ A \}$, объект $N$ в множество $\{ s, t \}$, стрелки $A$ и $N$ в тождественные отображения, стрелки $s$ и $t$ в соответствующие отображения $\{ A \}$ в $\{ s, t \}$. Совсем непохоже. Особенно интересно, откуда берется направление дуги в графе, когда $s$ и $t$ в категории совершенно симметричны.

[george66]

Граф (любой) можно изображать двумя способами: как граф и как функтор. Картинка $s\overset{A}{\to} t$ это сам граф (с двумя вершинами $s$ и $t$ и одной стрелкой $A$). Если изобразить его как функтор, это будут два множества $\{A\}$ и $\{s,t\}$ (множество стрелок и множество вершин) и две функции между ними, выдающие по стрелке её начало и конец.

[пианист]

А, ясно, спасибо.

[george66]

Да, и учтите, что шкала у него перевёрнутая (функторы контравариантные, из $\Gamma^{op}$ в $Sets$), поэтому стрелки $s$ и $t$ в шкале идут из множества вершин $N$ во множество стрелок $A$, а не наоборот.

[пианист]

Я уже многажды спотыкался, и планирую это делать снова.

[ksmirnov]

Здравствуйте!

У меня два замечания к главе про логику.

I. В учебнике в главах 15.1 и 15.3 по сути изложен один и тот же натуральный вывод, просто в разных формах.
В современной литературе по логике можно встретить два (как минимум, я больше не встречал) способа изложения натурального вывода - традиционный в виде деревьев формул, и в форме секвенций. Второй вид очень похож на интуиционистское секвенциальное исчисление, их даже легко спутать, но это совершенно разные вещи. Проще всего различить их можно по структуре правил:
1) в натуральном выводе связки добавляются и удаляются из сукцедента. Правила так и называются "правило введения (или удаления) такой-то связки".
2) в секвенциальном исчислении (инт. и класс.) связки добавляются как в антецедент, так и в сукцедент. Правила называются "правило введения такой-то связки в антецедент (или сукцедент)". Для удаления связок можно использовать те же правила, но в обратную сторону. В этом смысле секвенциальное исчисление гораздо более симметрично, чем натуральный вывод. Именно стремление достичь этой симметрии и привело к рождению секвенциальных исчислений (тут по-хорошему я должен дать ссылку на работу Генцена, в которой он подробно излагает эту интуицию, но мне лень искать точное место )

II. В главе 15.4 изложенный специальный вывод очень-очень близок к интуиционистскому Гильбертовскому исчислению высказываний, а именно: тут смешаны в одну кучу аксиомы и понятие вывода из гипотез. Незначительным формальными преобразованиями можно их разделить и получить Гильбертовское исчисление как оно есть.
Откровенно говоря, я впервые здесь встретил такое специальное исчисление, поэтому у меня нет четкого понимания, почему специальное исчисление лучше подходит для изложения введения в BiCCC. BiCCC знаю плохо. Я более-менее знаком с алгебрами Гейтинга, тут мне мой опыт и интуиция подсказывает, что Гильберт подходит лучше. Поэтому я не понимаю, зачем усложнять жизнь и вводить специальное исчисление.

[george66]

Ну, Генцена то я читал. При желании можно и в натуральном выводе (с деревьями) добавлять в антецедент, при этом вывод будет надстраиваться сверху. Но так уже давно не делают (как делал Генцен, при всём к нему почтении), сейчас используют нормализацию выводов вместо устранения сечения, поэтому исчисления Генцена представляют чисто технический интерес. Ту же прекрасную идею воплощают по-другому.
"Специальное исчисление" заимствовано из книги Ламбека и Скотта, оно точно соответствует определению бидекартово замкнутой категории, тем и интересно. Вообще, исчислениям Гильберта больше ста лет (и даже книжке Ламбека и Скотта уже тридцать). А первым работам Мартин-Лёфа 45. А кто это всё прочитает и расскажет другим?
Пародист усталости не знает -
Пишут все, а он один читает
(с) Александр Иванов

[ksmirnov]

george66 в сообщении #1361500 писал(а):

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

Это-то понятно. Может я неудачно изложил идею в предыдущем посте, суть моего замечания к главе 15.3 в другом: зачем называть натуральный вывод, хоть и записанный в форме отношения $\Gamma \vdash A$, секвенциальным исчислением? Во всяком случае, ни в одной известной мне литературе - учебной или в статьях - так не делают. Зато его прямо называют натуральным выводом и иногда явно противопоставляют секвенциальному.

george66 в сообщении #1361500 писал(а):

"Специальное исчисление" заимствовано из книги Ламбека и Скотта, оно точно соответствует определению бидекартово замкнутой категории, тем и интересно.

О, спасибо! Внимательно прочту этот кусок в Lambek J., Scott P.J. Introduction to Higher Order Categorical Logiс.pdf

george66 в сообщении #1361500 писал(а):

Вообще, исчислениям Гильберта больше ста лет (и даже книжке Ламбека и Скотта уже тридцать).

Я сюда приплел Гильбертовское исчисление из педагогических соображений. Современные (!) хорошие учебники по матлогике (напр, Верещагин и Шень, Герасимов, и др.) начинают изложение исчислений именно с Гильберта, несмотря на его почтенный вековой возраст. Он проще и задает хорошую интуицию для дальнейших построений во всех областях логики. Поэтому как минимум студенты в основной своей массе с ним знакомы. Ну ОК, должны быть знакомы. С секвенциями и нат. выводом в этом смысле все хуже. Может я и неправ. YMMV. Пойду Ламбека читать.

[george66]

Дело в том, что наша учебная литература устарела очень сильно. В шкафу на кафедре матлогики МГУ стояли книги Ламбека-Скотта, Фрейда-Щедрова, ещё что-то, я один их и читал (ещё Станислав Баров, но он потом спятил и ничего не написал). А до широких масс математиков то, что делается в основаниях, доходит ещё медленнее. Когда объясняешь, что ZF 110 лет, топосы придуманы в 60-е годы, да и сейчас что-то изобретают -- нет, не верят.
С Верещагиным и Шенем я знаком лично и давно, при всём к ним уважении я сам великий педагог, да. В 1987 году ходил на просеминар по математической логике, его вели Верещагин, Шень и Разборов. Не уверен, что Верещагин читал мой учебник (я ему посылал первые восемь версий, потом спросил -- не читал). Этих людей поздно учить:)