B
Это не в BHK, так как там несколько сложнее
Ну, в той же топологии, очень много рассматривается, скажем, бесконечное объединение и пересечение.
Какие при этом возникают формулы бесконечной длины?
Size: a a a
2021 August 13
B
Например, на домене натуральных чисел
NI
Всё просто - есть проиндексированные (например) натуральными числами стрелки, есть их произведение по всем натуральным числам, есть проекции -
для любого натурального числа, получаем такую-то стрелку-проекцию.
для любого натурального числа, получаем такую-то стрелку-проекцию.
B
Например, Пхi:P(x) на бесконечном домене будет P(x1) ^ ... ^ Р(х inf)
B
Это бесконечная формула
B
Формулы бесконечной длины разрешены только в инфинитарной логике
B
(как и доказательства бесконечной длины)
B
И там нужно смотреть за таким свойством логической системы как компактность
NI
А зачем эта запись нужна прям обязательно?
Ну так много случаев, когда можно что-то бесконечной записью обозначить.
Иногда, это даже удобно, например, всякие проективные/прямые пределы.
Или вон начальные алгебры или терминальные коалгебры по теореме Адамека тоже записываются, как (ко)предел бесконечной последовательности стрелок.
Ну так много случаев, когда можно что-то бесконечной записью обозначить.
Иногда, это даже удобно, например, всякие проективные/прямые пределы.
Или вон начальные алгебры или терминальные коалгебры по теореме Адамека тоже записываются, как (ко)предел бесконечной последовательности стрелок.
NI
Но в целом, и в этих примерах, без бесконечной записи можно обойтись.
Просто так удобнее бывает нарисовать.
Просто так удобнее бывает нарисовать.
B
Эта бесконечная запись дефиниционально доступна из произведения такого рода
В финитарной логике не должны быть доступны формулы бесконечной длины (ещё с Гильберта)
В финитарной логике не должны быть доступны формулы бесконечной длины (ещё с Гильберта)
NI
Ну недоступны они, хорошо, пусть.
И не надо.
И не надо.
NI
Для записи произведения по бесконечному индексу, это и не надо.
B
Поэтому там используют семантики не в виде логического индексированного произведения или суммы
B
Не очень многие инфинитарные логики в итоге имеют хорошие математические свойства
NI
@stask
Кванторы, это правый (forall) и левый (exists) сопряжённые к соответствующему pullback-функтору, порождённому морфизмом между контекстами.
Левый сопряжённый, при этом, выглядит очень просто (тупо композицией).
Кратко можно прочитать тут -
https://ncatlab.org/nlab/show/quantification
Кванторы, это правый (forall) и левый (exists) сопряжённые к соответствующему pullback-функтору, порождённому морфизмом между контекстами.
Левый сопряжённый, при этом, выглядит очень просто (тупо композицией).
Кратко можно прочитать тут -
https://ncatlab.org/nlab/show/quantification
NI
Охмлин. Да причём тут инфинитарные логики?
С бесконечностями как-то и так справляются.
И даже именно представление в виде бесконечного произведения не требует формул бесконечной длины.
Но некоторые "навороты" требует.
С бесконечностями как-то и так справляются.
И даже именно представление в виде бесконечного произведения не требует формул бесконечной длины.
Но некоторые "навороты" требует.
B
Бесконечности имеются здесь только в форме формул / термов бесконечной длины и доказательств бесконечной длины.
B
Если хотя бы одна формула синтаксически допустимо переводится в формулу бесконечной длины, то это уже нестандартный вид логик, который и называется инфинитарным