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.