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
922
Ну а как назвать исчисления секвенций, кроме как "исчисления секвенций"? Чтобы объяснить, почему "так нельзя", надо объяснить, что делал Генцен 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
658
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
658
Ukraine

(ksmirnov)

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

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

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

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


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

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

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



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

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


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

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