ПС
Большая сила доказательств?
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 23
ПС
Чем меньше предположений, тем в большем числе теорий это доказательство можно воспроизвести
ПС
Ну и, плюс, бывают такие аксиомы, из которых следуют парадоксальные для нашего мира вещи (фольклорный пример про Аксиому выбора и Банаха-Тарского)
AC
"Отмену аксиом"?! Это как вообще??? Каких? 😃
AC
В смысле, больше моделей или что?
DK
ну одну оставили для приличия. да и та на аксиому мало похожа))
AC
Мне неловко указывать на очевидное, но в HoTT существенно больше одной аксиомы.
DK
значит самое время копать. куда?
AC
Можно начать с https://ncatlab.org/nlab/show/homotopy+type+theory как обычно.
Сходу понятно, что как расширение MLTT, HoTT "наследует" все аксиомы MLTT, плюс добавляет несколько своих, плюс можно добавить ещё несколько непротиворечивых по желанию.
Сходу понятно, что как расширение MLTT, HoTT "наследует" все аксиомы MLTT, плюс добавляет несколько своих, плюс можно добавить ещё несколько непротиворечивых по желанию.
ПС
Я имел в виду теорию как множество утверждений, но так будет, наверное, точнее, да
AC
С моделями-то широко известно, что так, но с доказательствами это не работает. 😊
AC
А может и работает. У меня был в голове пример, но я его "вывернул на изнанку" — был не прав. 😅
AC
Но всё равно хрен сравнишь "больше-меньше". Если бы был результат типа "доказательство, использующее N аксиом можно воспроизвести в любой теории с N+k аксиом" — тогда да, но я не уверен, что "лишние" аксиомы никогда ничему не мешают... 🤔
AC
"По идеи", если "лишние аксиомы" не делают систему противоречивой, то мешать не должны...
NR
Я бы записывал в аксиомы все теоремы
NR
Хм. Или все не не-теоремы?
NR
Тут придётся задать порядок
AC
Нет, это просто не имеет смысла. 😃
NR
Это правда