Logic in a tos

Ryan Shelswell (8/4/98)

In this talk I describe the logic found in a tos. This turns out to be a restricted first-order intuitionistic predicate calculus: all the first-order operations an be constructed in a (mostly) standard topos-theoretic way, except for universal quantification.

I describe an alternative, but well-known, construction of universal quantification and characterise the class of morphisms for which it applies in a tos: this characterisation is based on a simple notion of objects with a finite number of subobjects.

This characterisation turns out to nicely show that in application to information systems modelling, a tos provides a logic effectively equivalent to the full first-order calculus.

Back to titles of seminars.

---

Steve Lack

Last modified: Mon May 18 15:20:38 EST 1998