Danko Ilik: Formalising a Completeness theorem in Coq
Source: Mathematics and theoretical computing seminar
Formalising a Completeness theorem in Coq
LIX, Ecole Polytechnique
Povzetek: I will talk about a constructive completeness theorem for 1st order classical logic in respect to a slightly modified notion of classical model, about its formalisation in Coq and about the motivation for using it as a program. A main ingredient of the proof of the theorem is a proof of a more general theorem: that any filter over a complete countable boolean algebra can be extended to an ultrafilter, constructively.