2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1 ... 7, 8, 9, 10, 11
 
 Re: Написал учебник теории категорий
Сообщение15.12.2018, 22:32 


15/12/18
5
Печально, если оно так :-( И при том, что это лучшее, что я встречал среди русскоязычной учебной литературы по основам матлогики, выпущенной в нашем тысячелетии. В других встречается даже такое: термин "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. Но я думал, что это весьма редкие головы.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение15.12.2018, 22:50 
Заслуженный участник


31/12/15

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

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение16.12.2018, 02:29 


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

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

george66 в сообщении #1361570 писал(а):
после неё натуральным выводом называют "то, что у Правица"

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

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

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение16.12.2018, 11:56 
Аватара пользователя


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

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

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

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

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение16.12.2018, 13:03 


15/12/18
5
beroal в сообщении #1361648 писал(а):
Если учатся программисты, то им полезнее практика логики, чем теория, так как они и теорию программирования толком не знают. Теорию логики они просто не переварят.


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

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение16.12.2018, 13:12 
Аватара пользователя


17/04/11
622
Ukraine

(ksmirnov)

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

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

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

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение23.12.2018, 17:11 
Заслуженный участник


31/12/15

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 157 ]  На страницу Пред.  1 ... 7, 8, 9, 10, 11

Модераторы: Модераторы Математики, Супермодераторы



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

Сейчас этот форум просматривают: lel0lel


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

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group