The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Le 3 nov. 2011 à 17:33, Guillaume Yziquel a écrit :

> Le Thursday 03 Nov 2011 à 14:16:01 (+0100), Matthieu Sozeau a écrit :
>> 
>> 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.
> 
> Maybe I missed something, but his PhD seems to refer to the first
> incompleteness theorem and not the completeness theorem. At first
> glance, it doesn't seem really related to model theory.

Still, there is some model theory involved (e.g. p57) and there might
be good references in it.
-- Matthieu