Re: Topos logic arises naturally

[Todd Wilson <twilson@csufresno.edu>]

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