The Coq mailing list

[Guillaume Yziquel <guillaume.yziquel AT citycable.ch>]

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.

-- 
     Guillaume Yziquel