Вы пробовали спрашивать в списках рассылки Coq или Isabelle?
Дейв Кларк
2
Я не уверен, подходит ли это для теории, но посмотрите на это . Полнота есть, а компактность недалеко.
Каве
См. Также запись AFP для версии в Изабель / HOL (с 2004 года).
Макарий
Ответы:
17
Теорема компактности для классической логики первого порядка является прямым следствием теоремы полноты, и, фактически, можно непосредственно доказать компактность с помощью аргумента стиля Хенкина, используемого для полноты, даже не упоминая деривацию.
Теорема полноты для классического FOL относительно стандартных моделей Тарского была формализована в Mizar. Смотрите серию статей в http://fm.mizar.org/2005-13/fm13-1.html
Я говорю «почти», потому что есть один технический момент, доказывающий правильность алгоритма сортировки, который я еще не успел закончить, однако основной компонент (конструктивная теорема ультрафильтра для счетных языков) формализован.
Можно также рассмотреть полноту и, следовательно, компактность, для нестандартного понятия действительности, и получить полное и формализованное конструктивное доказательство.
Ответы:
Теорема компактности для классической логики первого порядка является прямым следствием теоремы полноты, и, фактически, можно непосредственно доказать компактность с помощью аргумента стиля Хенкина, используемого для полноты, даже не упоминая деривацию.
Теорема полноты для классического FOL относительно стандартных моделей Тарского была формализована в Mizar. Смотрите серию статей в http://fm.mizar.org/2005-13/fm13-1.html
Та же самая теорема о полноте, но с конструктивным доказательством, была почти формализована мной в помощнике по доказательству Coq, см. Почтовый файл по адресу https://sites.google.com/site/dankoilik/publications/phd-thesis.
Я говорю «почти», потому что есть один технический момент, доказывающий правильность алгоритма сортировки, который я еще не успел закончить, однако основной компонент (конструктивная теорема ультрафильтра для счетных языков) формализован.
Можно также рассмотреть полноту и, следовательно, компактность, для нестандартного понятия действительности, и получить полное и формализованное конструктивное доказательство.
источник
Компактность для FOL была сделана в HOL Джоном Харрисоном и сообщена на TPHOLs 1998. См. Формализация базовой теории моделей первого порядка .
источник