The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 3 nov. 2011 à 14:10, Guillaume Yziquel a écrit :

> Le Thursday 03 Nov 2011 à 08:57:24 (-0400), Adam Chlipala a écrit :
>> Daniel Schepler wrote:
>>> But it's starting to sound like the theory you're formalizing is
>>> possibly tied tightly enough with ZF-type semantics that using a
>>> ZF system would indeed be appropriate.  I think Adam wasn't
>>> necessarily saying that using a ZF system would automatically be a
>>> bad idea, just that in most of mathematics outside pure set and
>>> model theory (and even in quite a bit of set theory), it's more
>>> natural to formulate it in type theoretic terms.
>> 
>> I'd put it this way: when some development is said to be doable in
>> ZF but not CIC, I immediately doubt whether the development has
>> practical value.  Not that there's anything wrong with impractical
>> mathematics.... ;)
> 
> Talking about impractical mathematics and model theory... Has anyone
> implemented or tried to implement in Coq any kind of model-theoretic
> result? I'm specifically thinking of Gödel's completeness theorem, of
> which I believe some kind of constructive proof exists.

Have a look a Russell O'Connor's thesis.
-- Matthieu