On Tue, 3 Jun 2003, Lawrence Paulson wrote:
Isabelle's internal logic comes from Lambek and Scott. It is an instance of Example 1.1 on page 132, where all types are assumed to be non-empty.
But this is the heart of the matter. There is a certain precise sense in which what happens in a topos between the empty set and a singleton set governs the behavior of the rest of the topos. Instead, why not factor out the topos logic and add whatever nonemptiness assumptions that are perceived necessary from a practical standpoint as an additional theory? This factoring shouldn't affect those that rely on the non-emptiness assumptions, but it would make a big difference to those who want to work in the topos logic. -- Todd Wilson A smile is not an individual Computer Science Department product; it is a co-product. California State University, Fresno -- Thich Nhat Hanh