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

[ksmirnov]

Печально, если оно так И при том, что это лучшее, что я встречал среди русскоязычной учебной литературы по основам матлогики, выпущенной в нашем тысячелетии. В других встречается даже такое: термин "valuation" перевели как "валентность" только потому, что англоязычные авторы использовали сокращение "val" (тут тоже ссылку дать не могу ). Ну и несчастный "Шёнфинкель" туда же. Да чего я рассказываю, вы и так лучше понимаете.

ksmirnov в сообщении #1361533 писал(а):

ни в одной известной мне литературе - учебной или в статьях - так не делают

На всякий случай оговорюсь, что сюда попадает и англоязычная литература тоже: Sorensen+Urzyczyn, Girard (правда, эти книги немного не дотянули до нашего тысячелетия), etc. Не думаю, что за 20 лет все сильно поменялось в этом плане (natural vs sequent).

А вообще, проведу "эксперимент": прочитаю студентам (программистам) оба варианта - через специальное исчисление и через гильбертовское. Студенты знают (что-то еще помнят о) гильберта, натуральный вывод и секвенции. Правда, только классическую логику, соответственно, про алгебры Гейтинга они en masse не слышали. Потом можно смотреть, какой вариант лучше вошел в мозг. Так что в плане второго замечания (гильберт vs. спец.) у меня сугубо практический интерес я не великий педагог, но мысли до ребят доносить у меня как-то получается

-- 15.12.2018, 22:49 --

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

Когда объясняешь, что ZF 110 лет, топосы придуманы в 60-е годы, да и сейчас что-то изобретают -- нет, не верят.

??? А как ZF расшифровывается, они знают? В некоторых головах бывает, прости господи, что ZFC - это ZF + Continuum Hypothesis. Но я думал, что это весьма редкие головы.

[george66]

Ну а как назвать исчисления секвенций, кроме как "исчисления секвенций"? Чтобы объяснить, почему "так нельзя", надо объяснить, что делал Генцен 80 лет назад. И хотя так уже давно никто не делает, но всё равно нельзя. Есть классическая книжка Правица "Натуральный вывод", после неё натуральным выводом называют "то, что у Правица". Он действительно "натуральный", то есть простой и естественный, в отличии от любых секвенций. В соседней теме как раз учу секвенциям
topic131109.html

[ksmirnov]

Ммм... Подумал. Врубился, тут термины портят дело.

Да, формально если мы зафиксируем натуральный вывод в форме секвенций и напишем соответствующие правила вывода, это будет в буквальном смысле "исчисление секвенций", только не Генценовское секвенциальное исчисление, а натуральный вывод. В этом буквальном смысле ваш учебник абсолютно корректен. Сложность в том, что когда говорят об интуиционистской или классической логике, под "sequent calculus" понимают именно Генценовское исчисление. Везде и classic sequent calculus или intuitionistic sequent calculus - всегда Gentzen. Я не смог найти опровержение этому в серьезной учебной литературе. Поэтому я считаю, что в данном конкретном случае писать "исчисление секвенций" неудачно.

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

после неё натуральным выводом называют "то, что у Правица"

А вот тут не соглашусь, сейчас термином "natural deduction" называют и "то, что у Правица", и "то, как Генцен записывал свои NL/NK" (еще один термины из 30-х, они еще живые?), и еще разные формы, в зависимости от того, в каком ключе и для каких нужд излагают логику. В этом смысле термину "sequent calculus" повезло больше

BTW, в соседнем топике автор учебника по логике (Кожухов И.Б.) тоже излагает натуральный вывод в форме секвенций, только он нигде не называет это исчислением секвенций. Да и натуральным выводом тоже не называет. Странный учебник, странное изложение. Сугубо мое ИМХО.

[beroal]

ksmirnov в сообщении #1361533 писал(а):

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

Субъективно. В практическом построении доказательств ни система Гильберта, ни (двустороннее) исчисление секвенций не используются. Если учатся программисты, то им полезнее практика логики, чем теория, так как они и теорию программирования толком не знают. Теорию логики они просто не переварят.

ksmirnov в сообщении #1361533 писал(а):

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

О терминах не спорят, а вы с george66 начали делать именно это. Всегда можно выдумать новый термин.

[ksmirnov]

beroal в сообщении #1361648 писал(а):

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

Эх, хотел бы я сам так сказать... В своем курсе я дал программистам задачи на практику: написать простенький солвер для высказываний, и исключительно в виде своего развлечения задачу на совсем страшную для студента-программиста теорию (что-то про компактные пространства - связь логики и топологии из 50-ых годов). Так вот, умные ребята, освоившие несколько языков программирования на более-менее достаточном уровне, радостно пошли разбираться в топологии и в ординалах, вместо того, чтобы на вечер сесть и написать солвер. Солвер написал только один, остальные освоили компакты; некоторые содержательно переварили, не просто тычут палец в распечатку. Это весьма неплохие программисты-практики. Ну вот как оно так получилось? Ну а от совсем практической SMT (Z3) просто сбежали, страшно им это показалось. Может я плохо читаю практику?

[beroal]

(ksmirnov)

ksmirnov в сообщении #1361662 писал(а):

Так вот, умные ребята, освоившие несколько языков программирования на более-менее достаточном уровне, радостно пошли разбираться в топологии и в ординалах, вместо того, чтобы на вечер сесть и написать солвер. Солвер написал только один, остальные освоили компакты; некоторые содержательно переварили, не просто тычут палец в распечатку. Это весьма неплохие программисты-практики.

Очевидно, это не средние программисты. Я говорил о средних. Поэтому забудьте о том, что я говорил.

Кстати, всякие солверы я отношу к теории логики. Практика логики — это просто логическое мышление.

[george66]

Спросил, кстати, Шеня, читал ли он мой учебник - Шень сказал "нет".
Шень и Верещагин - близнецы-братья!
Кто более матери-истории ценен?