Основная семантика интуиционистской логики - семантика миров Крипке. Бонусом рассуждаем о многозначности логики, а также о способах построения других (неклассических) логик.
Эту симантику очень интересно интерпретировать в топосах. Если у нас есть частично упарядоченое множество мы можем посмотреть на него с точки зрения категории где между элементами есть стрелочка если они сравнимы. Тогда формула будет подобьектом какого-то presheaf нашей категории. Так что эту семнатику можно обобщить сперва если взят за domain of presheaf любую маленькую категорию. И можно обобщить ещё больше на либой топос и писать V|-M[a] (M подобьект Х) если а:V->X факториться через М. Так что и тут теория категорий присутствует))
в последующих роликах я как раз пытаюсь рассуждать о том, что разнообразие семантик (и их интерпретаций) очень полезно, т.к. у разных математиков разный мыслительный процесс и система образов, и ваше замечание есть хороший тому пример. я вот как привык когда-то к графам, так и вижу их везде) а кому-то нравятся миры или топосы. Главное, что это все одинаково безупречно работает.
Правильно понимаю, что вводя различие между «выводимо не А» и «не выводимо А» мы как бы помимо true, false добавляем еще и null? Не столкнемся ли мы с проблемой останова, если попробуем реально проверить есть ли Германия в мире Y?
тут скорее не null, а неопределенность (или суперпозиция состояний). это действительно связано с проблемой останова (как и теорема Гёделя) и показывает (алгоритмическую) неразрешимость некоторых формальных систем. Однако в случае модели про Германию в мире Y все же такой проблемы не будет, т.к. саму-то модель мы строим на конечном графе, да еще в рамках классической логики, поэтому там такая проблема не подразумевается. Но не исключено, что можно придумать какой-то пример с неразрешимым множеством вершин графа (миров шкалы Крипке), и тогда уже сама проверка модели на истинность столкнется с проблемой останова.
Эту симантику очень интересно интерпретировать в топосах. Если у нас есть частично упарядоченое множество мы можем посмотреть на него с точки зрения категории где между элементами есть стрелочка если они сравнимы. Тогда формула будет подобьектом какого-то presheaf нашей категории. Так что эту семнатику можно обобщить сперва если взят за domain of presheaf любую маленькую категорию. И можно обобщить ещё больше на либой топос и писать V|-M[a] (M подобьект Х) если а:V->X факториться через М. Так что и тут теория категорий присутствует))
в последующих роликах я как раз пытаюсь рассуждать о том, что разнообразие семантик (и их интерпретаций) очень полезно, т.к. у разных математиков разный мыслительный процесс и система образов, и ваше замечание есть хороший тому пример.
я вот как привык когда-то к графам, так и вижу их везде) а кому-то нравятся миры или топосы. Главное, что это все одинаково безупречно работает.
Правильно понимаю, что вводя различие между «выводимо не А» и «не выводимо А» мы как бы помимо true, false добавляем еще и null? Не столкнемся ли мы с проблемой останова, если попробуем реально проверить есть ли Германия в мире Y?
тут скорее не null, а неопределенность (или суперпозиция состояний). это действительно связано с проблемой останова (как и теорема Гёделя) и показывает (алгоритмическую) неразрешимость некоторых формальных систем. Однако в случае модели про Германию в мире Y все же такой проблемы не будет, т.к. саму-то модель мы строим на конечном графе, да еще в рамках классической логики, поэтому там такая проблема не подразумевается. Но не исключено, что можно придумать какой-то пример с неразрешимым множеством вершин графа (миров шкалы Крипке), и тогда уже сама проверка модели на истинность столкнется с проблемой останова.
@@reisedurchdiemathe суперпозиция состояний, это то, что вы чуть ниже обозначили как аксиому I_n? (Так то понятно, то пример с Германией игрушечный 🙂)
Автор не хотел бы записать какие-то отдельные курсы, посвященные более философским темам? Про формальную онтологию какую-то, к примеру...
сори, но нет, это было бы нечестно по отношению к слушателям, т.к. философия - это совсем не мое. цена таким видео была бы нулевая.