NI
Ээээ
Предикаты первого порядка - инфинитарные?
Предикаты первого порядка - инфинитарные?
Size: a a a
2021 August 13
B
Нет
B
Как раз потому, что квантификация описывается не через произведение или сумму
B
Через произведение или сумму возможно в инфинитарной версии предикатов
Ещё, насколько помню, такое используется для подстановочной интерпретации квантификации (в модельной семантике не она, там объектная), но там всё ломается, и исследователям пришлось для неё менять понятие логического вывода, чтобы не ломалось.
Ещё, насколько помню, такое используется для подстановочной интерпретации квантификации (в модельной семантике не она, там объектная), но там всё ломается, и исследователям пришлось для неё менять понятие логического вывода, чтобы не ломалось.
B
Если мы уж берём инфинитарную версию логики, то нам нужно следить за её компактностью (в ней расходятся понятия полноты и компактности)
B
А если в ней допускаются доказательства бесконечной длины, то начинаются также проблемы с конструктивными особенностями такой логики, поскольку там сразу расходятся понятия доказуемости и вычислимости, так как могут существовать доказательства, выполнение которых никогда не закончится (в том числе циклические, т.е. инфинитарные логики с бесконечными доказательствами могут исследовать логические круги)
B
А между бесконечными формулами и бесконечными доказательствами есть очевидная односторонняя связь, так как бесконечное доказательство описывается бесконечной формулой
Oℕ
изоморфизм достаточно достаточно диаграммен?
B
В общем, даже такая техническая мелочь может влиять на математические свойства логической системы
ЕО
Ну а как без равенства определить изоморфизм? Кажется, что равенство это зло, от которого никак не избавиться
B
Зависит от равенства
B
Например, можно записать вариант правила Лейбница в теории категорий
Oℕ
так тут человека равенство не смущает
Oℕ
ну в инфинити категориях можно без внешнего равенства, наверное
2021 August 14
ЕО
Но нет синтаксического языка для квазикатегорий (кроме HoTT, где равенства есть)
ЕО
А я бы с удовольствием посмотрел на такое
2021 August 16
2021 August 20
SK
"Из этого следует существование объекта X и стрелки h: С -> X.
Но не доказать существование стелок p: X -> A и q: X -> B и тем более коммутативности диаграм: f = h∘p, g = h∘q"
Вопрос закрыт с определением product - можно определить его через adjoint. Спасибо всем большое за ссылки на многие статьи. Я поставил их себе в план изучения.
Но не доказать существование стелок p: X -> A и q: X -> B и тем более коммутативности диаграм: f = h∘p, g = h∘q"
Вопрос закрыт с определением product - можно определить его через adjoint. Спасибо всем большое за ссылки на многие статьи. Я поставил их себе в план изучения.
