s
Теорема о полноте позволяет так делать.
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 24
AC
Когда сказали "населена" я подумал про термы, естественно. Тут слишком вольно пользуются терминологией и смешивают аксиоматическую теорию и её модели. 😊
AC
Она позволяет переходить от одного понятия к другому, но это всё равно разные понятия из "разных миров". Кроме того, редкая теория обладает полнотой. 🤷♀️
[
Теории худые, так и запишем
AC
Так без добавления самой CH в ZFC в качестве аксиомы доказать отсутствие такого множества тоже нельзя. 🤷♀️
AC
Радуйтесь, если они хотя бы издают звук.
s
Ну и при этом могут существовать модели, в которых никаких промежуточных множеств нет, ведь так?
AC
Видимо. Как и такие, в которых есть. 🤷♀️
s
Ну собственно про это и шла речь.
s
Где «аксиомы допускают существование» означает «существует модель», а выводимость означает таки выводимость.
AB
На бесконечностях может быть много странных штук. В конечных случаях этих странностей обычно не бывает.
АП
Читал обсуждение выше и подумал:
Можно ли сформулировать (существует ли) соответствие между теориями и типами?
Можно ли сформулировать (существует ли) соответствие между теориями и типами?
NR
Не знаю что имеется ввиду под теориями но возможно Rosetta paper это то что вы ищете
AC
Да. Соответствие Карри-Говарда(-Ламбека и других).
K
Типы можно считать логическими утверждениями. Если тип населён - то он правда, иначе - ложь. А код - это доказательство
ПС
только надо осторожнее язык выбирать, а то любой тип будет населён