 Internal logic of a topos

The subobject classifier supplies intuitionistic truth values. Subobjects interpret predicates, finite limits interpret finite conjunctions and equality, and suitable image and adjoint constructions interpret quantifiers. One must distinguish internal intuitionistic arguments from classical reasoning in the external category of sets.