# Danko Ilik: Formalising a Completeness theorem in Coq

Date: 4. 6. 2008

Source: Mathematics and theoretical computing seminar

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