Danko Ilik: Formalising a Completeness theorem in Coq

Formalising a Completeness theorem in Coq

Danko Ilik
Team TYPICAL
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.

Gradivo:  handout.pdf