Что рассказывал Воеводский в Стекловке
0. Еще из предыдущего доклада (летом 2010 года в Петербурге) мне запомнилась формула: предполагается построить такие основания математики, в которых гомотопическая или бесконечность-категорная (в противоположность теоретико-множественной) точка зрения будет единственно возможной, т.е. действия, не имеющие смысла гомотопически, нельзя будет совершить.
***
1. Компьютерная система Coq формальной верификации программ и доказательств преподается студентам-программистам в Принстонском университете. Володя взял там этот курс, сдавал (и сдал) все экзамены.
2. Система эта основана, среди прочего, на теории типов Мартин-Лёфа, знаменитой своей недоступностью для понимания. Интерпретация этой теории в терминах теории гомотопий (придуманная Awodey, а потом и Володей) проясняет ее.
3. Цель всей этой своей затеи Володя объясняет так: ему присылают статью студента, на рецензию или еще чего, длиной в двести страниц. Он ее читает и обнаруживает на третьей странице ошибку [подразумевается -- с большой вероятностью обессмысливающую последующие 197]. Компьютерная система верификации доказательств поможет авторам математических работ избегать ошибок, а математикам в целом -- убедиться, что все, что они понаписали, является правдой.
4. Формальное доказательство, записанное в "правильной" системе верификации, будет, вероятно, не длиннее, и читать его будет не труднее, чем неформальное доказательство традиционного вида.
5. "Правильная" система формальной верификации (т.е. прежде всего Coq) отличается тем, что она приспособлена как для классической, так и для конструктивной математики. На самом деле [насколько я мог понять Володю] по духу она скорее подходит для конструктивной математики, т.е. у нее есть специфически конструктивистские возможности. Работать в этой системе с классической логикой, аксиомой выбора и т.д. можно, но это подразумевает отказ от использования части возможностей системы.
6. Аргумент в пользу конструктивной математики: не то, чтобы Володя в это верил, но действовать считает полезным в предположении, что стандартные системы оснований математики противоречивы. Если в используемой системе оснований обнаруживается противоречие, классические теоремы и доказательства разрушаются/обессмысливаются в большей степени, чем конструктивистские. [В классической логике из ложного утверждения следует любое. Как я понимаю, в конструктивистской логике из ложного утверждения следует любое, начинающееся с "неверно, что". Т.е. в классической логике если 1=0, то я китайский император. B конструктивистской -- если 1=0, то неверно, что я не китайcкий император (но утверждение, что я китайский император, отсюда не выводится).]
7. Аналогия: когда изобрели письменность, наверное, имевшиеся к тому времени в изобилии специалисты по запоминанию больших объемов информации тоже не одобряли новую технологию. И, конечно, внедрение ее не могло не сопровождаться какими-то потерями.
***
8. Собственно, математическая часть. Фильтрация гомотопических типов топологических пространств по уровням: на уровне 0 -- стягиваемые пространства, на уровне 1 -- пустые и стягиваемые ("истинностные значения": стягиваемое = истина, пустое = ложь), на уровне 2 -- у которых все компоненты связности стягиваемые ("дискретные множества"), на уровне 3 -- пространства, у которых все компоненты связности имеют тип K(π,1) ("нервы группоидов"), и т.д. По определению, пространство находится на уровне n, если для любых двух его точек, пространство путей между ними находится на уровне n−1.
9. Семантическими единицами традиционных логических систем являются 1. термы (символизирующие отображения An → A, где A -- множество модели) и 2. формулы (символизирующие отображения в истинностные значения, т.е. попросту подмножества An). Семантическими единицами "теорий типов" являются 1. контексты и 2. суждения. Контекст -- это что-то вроде "x1 есть объект типа T1, x2 есть объект типа T2(x1) (зависящего от x1), и т.д., xn есть объект типа Tn(x1,...,xn−1)". Суждение есть что-то вроде "в таком-то контексте (как выше), объект r(x1,...,xn) имеет тип R(x1,...,xn)".
10. Традиционная интерпретация сопоставляет контексту башню множеств, отображающихся по цепочке сверху вниз -- энное в эн минус первое (соответствующее контексту длины n−1 -- с отброшенным xn), в эн минус второе, и т.д. Суждению она сопоставляет еще один надстроенный этаж башни вместе с сечением отображения множеств на верхнем этаже. Гомотопическая интерпретация сопоставляет контексту башню расслоений (в смысле теории гомотопий), суждению -- дополнительный этаж башни плюс сечение расслоения на этом этаже.
11. "Аксиома унивалентности" состоит примерно в том, что пространство равенств гомотопически эквивалентно пространству изоморфизмов [что бы это ни значило], формально -- некое расслоение обладает тем свойством, что пространство путей между любыми двумя точками базы гомотопически эквивалентно пространству гомотопических эквивалентностей между слоями. Аксиома унивалентности несовместима с теоретико-множественной интерпретацией теории типов и форсирует гомотопическую интерпретацию (влечет нетривиальность высших гомотопических групп).
12. Замечание о связи теоретико-категорной и гомотопической точек зрения: категория не есть множество с дополнительной структурой, но она есть группоид (своих изоморфизмов) с дополнительной структурой (функтором Mor/Hom из квадрата группоида изоморфизмов в группоид множеств). [Что бесконечность-группоиды суть примерно то же самое, что топологические пространства, все мы слыхали.]
***
1. Компьютерная система Coq формальной верификации программ и доказательств преподается студентам-программистам в Принстонском университете. Володя взял там этот курс, сдавал (и сдал) все экзамены.
2. Система эта основана, среди прочего, на теории типов Мартин-Лёфа, знаменитой своей недоступностью для понимания. Интерпретация этой теории в терминах теории гомотопий (придуманная Awodey, а потом и Володей) проясняет ее.
3. Цель всей этой своей затеи Володя объясняет так: ему присылают статью студента, на рецензию или еще чего, длиной в двести страниц. Он ее читает и обнаруживает на третьей странице ошибку [подразумевается -- с большой вероятностью обессмысливающую последующие 197]. Компьютерная система верификации доказательств поможет авторам математических работ избегать ошибок, а математикам в целом -- убедиться, что все, что они понаписали, является правдой.
4. Формальное доказательство, записанное в "правильной" системе верификации, будет, вероятно, не длиннее, и читать его будет не труднее, чем неформальное доказательство традиционного вида.
5. "Правильная" система формальной верификации (т.е. прежде всего Coq) отличается тем, что она приспособлена как для классической, так и для конструктивной математики. На самом деле [насколько я мог понять Володю] по духу она скорее подходит для конструктивной математики, т.е. у нее есть специфически конструктивистские возможности. Работать в этой системе с классической логикой, аксиомой выбора и т.д. можно, но это подразумевает отказ от использования части возможностей системы.
6. Аргумент в пользу конструктивной математики: не то, чтобы Володя в это верил, но действовать считает полезным в предположении, что стандартные системы оснований математики противоречивы. Если в используемой системе оснований обнаруживается противоречие, классические теоремы и доказательства разрушаются/обессмысливаются в большей степени, чем конструктивистские. [В классической логике из ложного утверждения следует любое. Как я понимаю, в конструктивистской логике из ложного утверждения следует любое, начинающееся с "неверно, что". Т.е. в классической логике если 1=0, то я китайский император. B конструктивистской -- если 1=0, то неверно, что я не китайcкий император (но утверждение, что я китайский император, отсюда не выводится).]
7. Аналогия: когда изобрели письменность, наверное, имевшиеся к тому времени в изобилии специалисты по запоминанию больших объемов информации тоже не одобряли новую технологию. И, конечно, внедрение ее не могло не сопровождаться какими-то потерями.
***
8. Собственно, математическая часть. Фильтрация гомотопических типов топологических пространств по уровням: на уровне 0 -- стягиваемые пространства, на уровне 1 -- пустые и стягиваемые ("истинностные значения": стягиваемое = истина, пустое = ложь), на уровне 2 -- у которых все компоненты связности стягиваемые ("дискретные множества"), на уровне 3 -- пространства, у которых все компоненты связности имеют тип K(π,1) ("нервы группоидов"), и т.д. По определению, пространство находится на уровне n, если для любых двух его точек, пространство путей между ними находится на уровне n−1.
9. Семантическими единицами традиционных логических систем являются 1. термы (символизирующие отображения An → A, где A -- множество модели) и 2. формулы (символизирующие отображения в истинностные значения, т.е. попросту подмножества An). Семантическими единицами "теорий типов" являются 1. контексты и 2. суждения. Контекст -- это что-то вроде "x1 есть объект типа T1, x2 есть объект типа T2(x1) (зависящего от x1), и т.д., xn есть объект типа Tn(x1,...,xn−1)". Суждение есть что-то вроде "в таком-то контексте (как выше), объект r(x1,...,xn) имеет тип R(x1,...,xn)".
10. Традиционная интерпретация сопоставляет контексту башню множеств, отображающихся по цепочке сверху вниз -- энное в эн минус первое (соответствующее контексту длины n−1 -- с отброшенным xn), в эн минус второе, и т.д. Суждению она сопоставляет еще один надстроенный этаж башни вместе с сечением отображения множеств на верхнем этаже. Гомотопическая интерпретация сопоставляет контексту башню расслоений (в смысле теории гомотопий), суждению -- дополнительный этаж башни плюс сечение расслоения на этом этаже.
11. "Аксиома унивалентности" состоит примерно в том, что пространство равенств гомотопически эквивалентно пространству изоморфизмов [что бы это ни значило], формально -- некое расслоение обладает тем свойством, что пространство путей между любыми двумя точками базы гомотопически эквивалентно пространству гомотопических эквивалентностей между слоями. Аксиома унивалентности несовместима с теоретико-множественной интерпретацией теории типов и форсирует гомотопическую интерпретацию (влечет нетривиальность высших гомотопических групп).
12. Замечание о связи теоретико-категорной и гомотопической точек зрения: категория не есть множество с дополнительной структурой, но она есть группоид (своих изоморфизмов) с дополнительной структурой (функтором Mor/Hom из квадрата группоида изоморфизмов в группоид множеств). [Что бесконечность-группоиды суть примерно то же самое, что топологические пространства, все мы слыхали.]