Home > News > Danko Ilik: Formalising a Completeness theorem in Coq

Danko Ilik: Formalising a Completeness theorem in Coq

Date: 4. 6. 2008
Source: Mathematics and theoretical computing seminar
ńĆetrtek, 5.7.2008, od 14h do 16h, soba 3.07 na Jadranski 21

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