Новый учебник "Логика в категориях", первая глава

[george66]

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

https://www.mediafire.com/file/npll35f8 ... 3.pdf/file

https://www.mediafire.com/file/wl7gs4l9 ... 2.pdf/file

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

[SomePupil]

george66, и чего жалуются, интересно? Все понятно. В принципе, читается за час.

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

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

Можно примеры верификации "больших" доказательств и пример какой-то одной трудности, который "сидит в печенках" специалистов? Я слышал только про проверку доказательства теоремы Фейта-Томпсона. Есть ли более обозримые проверенные доказательства? Желательно нетривиальные.

-- 02.11.2023, 13:52 --

(Оффтоп)

И, скажите-ка,"Жуаялем" Вы обозвали не Andre Joyal часом? По-русски это имя пишется как Андре Жойал, Жоял или, на худой конец, Жойяль, но никак не Жуаял.

[george66]

По поводу печёнок, вот обзор разных способов представлять связывание переменных
https://jesper.sikanda.be/posts/1001-sy ... tions.html
Ещё раз: доказывать что-то про обычную подстановку адски трудно (смотрите теорему 1.32 в новом учебнике, расшифрованную мной из книги Карри-Фейса). Про обозначения и подстановку де Брёйна доказывать легко, но человек ими пользоваться может только с большим трудом. Равносильность обычной и де Брёйновской подстановки не доказана, видимо, никем, кроме меня (и никем не опубликована). Делаются попытки сделать какой-то гибрид из обычных и де Брёйновских обозначений, попыток много, обзор по ссылке, там формализация соответствующих типов данных для пруфчекера Agda и список статей, где читать подробности
https://researchr.org/bibliography/vari ... blications
Большие примеры -- для какого пруфчекера и по какой математической теме? Я пруфчекингом почти не занимаюсь, но имею опыт работы с Coq и Metamath. Metamath проще (хотя использует причудливую формализацию логики кванторов по техническим причинам), на сайте Metamath выложены доказательства огромного числа теорем (тысяч двадцать), в том числе про Гильбертовы пространства (создатель Metamath занимался квантовой логикой)
https://us.metamath.org/
Понимаете, "обозримых" доказательств для пруфчекера не бывает (это типа как читать чужой программный код).

[SomePupil]

(Оффтоп)

А, впрочем, Вы художник, называйте как хотите. По Вашему написанию "Жуаяля" я нашёл Ваши записи в ЖЖ; полезная штука, однако, эта авторская транскрипция...

[dgwuqtj]

Я только начал читать, вроде хорошо написано и читается легко. Мне больше нравится первая версия шрифта, странно брать разный шрифт для метапеременных для переменных и метапеременных для термов, и из контекста легко отличить метапеременные от $v_i$. Единственно, что странно смотрится $*$ как операция умножения.

[svv]

(SomePupil)

Это же нормальное французское чтение. Вот послушайте, как они произносят royal (руаяль) и loyal (люаяль). А в статье в первой же строке дана транскрипция фамилии.
Французский прекрасен.

[george66]

dgwuqtj в сообщении #1615806 писал(а):

Мне больше нравится первая версия шрифта, странно брать разный шрифт для метапеременных для переменных и метапеременных для термов, и из контекста легко отличить метапеременные от $v_i$

Дело в том, что я хочу в следующих главах использовать $x,y,z$ в качестве обычных переменных, поэтому хотел бы другой шрифт для метапеременных. Кроме того, по опыту чтения таких текстов (глаза сильно устают) рубленый шрифт ненамного, но явно легче читать. Но это не принципиально.

[Mirage_Pick]

george66, а можно ли каким-нибудь естественным образом интерпретировать категорию, дуальную к Вашей, где все стрелки, соответствующие подстановкам, будут обращены вспять, и $\mathcal I$ будет начальным, а не финальным, объектом?

-- 09.11.2023, 19:50 --

george66, и доказательство теоремы 1.32 определенно заслуживает отдельного раздела.

-- 09.11.2023, 20:03 --

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

Я пруфчекингом почти не занимаюсь.

А зря! Тем более, имея опыт работы с пруфчекерами. Все индуктивные рассуждения, где скрупулезно рассматриваете случаи, когда "доказательство может заканчиваться одним из правил $(\rho), (\sigma), (\tau),\ldots$" тысячи их!, и где рассмотрение большинства правил тривиально, сам Бог велел скормить какому-нибудь пруфчекеру, чтобы вместо, как Вы выразились, "14 страниц мрачных вычислений", можно было предъявить симпатичную программу. В книжке, кстати, случаи правил, рассмотрение которых занимает пару строк, можно опустить без ущерба (наоборот, с пользой) для понимания.

[george66]

Mirage_Pick в сообщении #1617110 писал(а):

george66, а можно ли каким-нибудь естественным образом интерпретировать категорию, дуальную к Вашей, где все стрелки, соответствующие подстановкам, будут обращены вспять, и $\mathcal I$ будет начальным, а не финальным, объектом?

Сразу не соображу. А зачем? Кажется, что-то подобное есть в "Справочной книге по математической логике", там в первом томе есть глава про интерпретации в категориях, но она слишком абстрактно завёрнута (на мой взгляд). В общем, если дана теория (вообще говоря, с несколькими сортами переменных - по действительным числам, натуральным, ещё чему-нибудь), можно саму теорию превратить в категорию и затем строить её модели как "правильные отображения" этой категории в Set (или ещё во что-нибудь вместо Set). Модели сами образуют категорию и какая-то двойственность (Йонеды) там возникает (кажется, между исходной теорией-категорией и категорией её "конечно представленных моделей"). Не уверен, что от этого прибавляется знаний.
По поводу теоремы 1.32 - очень надеюсь когда-нибудь сам доказать её попроще и тогда раздел не понадобится. Кстати, в книге Карри и Фейса она занимает страницы три, в результате её приходится буквально расшифровывать.
Я пытался формализовать свои результаты в Coq (а также Lean и Metamath), но скоро упёрся в проблемы самого Coq. У меня есть некий тип $B$ (на самом деле это тип лямбда-термов) и тип $A n$ зависящий от натурального параметра $n:nat$ (это лямбда-термы, содержащие ровно $n$ лямбд, этот тип хитрым путём определяю независимо, что удобно для определения подстановки). Я хочу доказать, что $B$ есть дизъюнктное объединение ($\Sigma$) всех $A n$. Строю три (естественные) функции

$foo (n:nat) (a: A n) : B$
$rank (b:B) : nat$
$bar (b:B) : A (rank\, b)$

Доказываю взаимную обратность (что они дают изоморфизм $B$ и $\Sigma A n$)

$forall (b:B), foo (rank\, b) (bar\, b) = b$
$forall (n:nat) (a: A\, n), rank (foo\, n\, a) = n$

Но когда выписываю теорему

$forall (n:nat) (a: A\, n), bar (foo\, n\, a) = a$

Получаю ошибку "The term bar (foo n a) has type A (rang (foo n a)) while it is expected to have type A n".
Спрашиваю на форуме Coq, велят вставить "тип равенства". Пытаюсь это сделать и понимаю, что вместо 14-ти страниц мрачных доказательств получу в несколько раз больше мрачных доказательств, из которых половина не относится к делу, бросаю. На самом деле идеально подошла бы более тупая "экстенсиональная теория типов" и пруфчекер Nuprl, но он, видимо, сдох (на письма не отвечают). От него осталась виртуальная машина, которая стартует больше часа, потому что написана на Lisp. Ещё отдельно можно рассказать про Metamath, но это настолько изысканный мазохизм, что лучше не начинать. В общем, по опыту попыток формализовать в Coq, Metamath и Lean скажу, что хорошего пруфчекера пока нет.
Спасибо, что комментируете!

[george66]

Mirage_Pick в сообщении #1617110 писал(а):

george66, а можно ли каким-нибудь естественным образом интерпретировать категорию, дуальную к Вашей, где все стрелки, соответствующие подстановкам, будут обращены вспять, и $\mathcal I$ будет начальным, а не финальным, объектом?

И, конечно, $\mathcal I$ не является финальным объектом! Финальный объект - это одноэлементное множество, обозначенное единицей 1.

[talash]

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

Я пытался формализовать свои результаты в Coq (а также Lean и Metamath), но скоро упёрся в проблемы самого Coq.

Странная ситуация. Кажется формализации математики должна была привести к возможности точной машинной проверки выкладок. Почему до сих пор с этим проблемы?

[george66]

talash в сообщении #1617609 писал(а):

Странная ситуация. Кажется формализации математики должна была привести к возможности точной машинной проверки выкладок. Почему до сих пор с этим проблемы?

Проверить не проблема, проблема записать:) Во-первых, записывать сложные доказательства в ZF практически невозможно. Вместо теории множеств используют теорию типов. Большинство популярных пруфчекеров (Coq, Isabelle, Lean) дают некоторый "сильно продвинутый функциональный язык программирования". Ты определяешь нужные тебе типы данных, всякие функции между ними и т.д. Специалисты знают, что доказательства и вычисления -- вещи близкородственные и языки для записи доказательств похожи на языки функционального программирования. За таким языком стоит некоторая теория типов, основанная на лямбда-исчислении. Дальше вылезают чисто математические проблемы теории типов, весьма сложные, особенно для типов, зависящих от параметров. В общем, если удобно записывать, то неудобно проверять и наоборот. Особняком стоит пруфчекер Metamath, который даёт самый минимум (чуть улучшенные производящие системы Поста) и ты можешь выписывать любые аксиомы "с нуля". Там свои математические проблемы, приходится формализовать логику кванторов в причудливом виде (при обычной формализации мы пишем "боковые условия" вида "переменная не входит свободно куда-то", Metamath таких условий решительно не понимает).

[Утундрий]

Дилетантский вопрос. Как всё это рифмуется с HoTT?

[george66]

Утундрий в сообщении #1620760 писал(а):

Дилетантский вопрос. Как всё это рифмуется с HoTT?

Никак. HoTT весьма продвинутая теория, а я излагаю азбуку (и не виноват, что она китайская). Если почитать учебник HoTT, там предполагается, что подстановка -- нечто очевидное, о чём долго говорить нечего. Да и в почти любом учебнике чего угодно так предполагается.

[пианист]

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

Да и в почти любом учебнике чего угодно так предполагается.

А есть примеры, где бы это приводило к проблемам?