The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thursday 19 May 2011 09:09:24 Lauri Alanko wrote:
> On Thu, May 19, 2011 at 11:41:55AM -0400, Adam Chlipala wrote:
> > Georgi Guninski wrote:
> > >what is the formal definition of "empty"
> > 
> > A type [T] is empty if you can prove [T -> False].
> 
> Sorry to nitpick, but the above might be a bit confusing to someone
> unfamiliar with the concept. Surely the formal (intensional)
> definition of "empty" is that a type [T] is empty if there are no
> closed terms [t] such that [t : T]?  Only due to the consistency of
> Coq is this (extensionally) equivalent with your definition above.

I'd formalize your definition as "~ inhabited T".  And it's trivial to prove 
the two definitions are equivalent:

Lemma uninhabited_iff_empty: forall T:Type,
  (~ inhabited T) <-> (T -> False).
Proof.
firstorder.
Qed.
-- 
Daniel Schepler