Szukałem formalizacji twierdzenia o zwartości dla FOL, ale nie znalazłem żadnego. Czy ktoś jest świadomy takiego rozwoju lub powiązanej pracy?
Odpowiedzi:
Twierdzenie o zwartości dla klasycznej logiki pierwszego rzędu jest bezpośrednią konsekwencją twierdzenia o kompletności, i w rzeczywistości można bezpośrednio udowodnić Zwartość za pomocą argumentu w stylu Henkina używanego do Kompletności bez wspominania o wyprowadzeniu.
Twierdzenie o kompletności dla klasycznego FOL w stosunku do standardowych modeli Tarskiego sformalizowano w Mizar. Zobacz serię artykułów pod http://fm.mizar.org/2005-13/fm13-1.html
To samo twierdzenie o kompletności, ale z konstruktywnym dowodem, zostało prawie sformalizowane przez asystenta Coq proof, patrz plik zip pod https://sites.google.com/site/dankoilik/publications/phd-thesis
Mówię „prawie”, ponieważ jest jeden punkt techniczny, który potwierdza poprawność algorytmu sortowania, którego jeszcze nie miałem czasu do ukończenia, jednak główny składnik (konstruktywne twierdzenie o ultrafiltrach dla języków zliczalnych) jest sformalizowany.
Można również rozważyć Kompletność, a tym samym Zwartość, dla niestandardowego pojęcia ważności i uzyskać kompletny i sformalizowany konstruktywny dowód.
Kompaktowość dla FOL została wykonana w HOL przez Johna Harrisona i podana na TPHOLs 1998. Patrz Formalizowanie podstawowej teorii modelu pierwszego rzędu .