Category Theory
(CT) is a branch of mathematics regarded by its
proponents either as an alternative to or as a
profoundly revised and generalized version of the Set
theory in its role of unifying conceptual framework for
mathematics.
Relationships between CT and logic are twofold. On the
one hand, CT may be used as a powerful algebraic tool
for combining logical systems and studying relations
between logical systems. From this point of view
applications of CT in Universal Logic are natural and
straightforward. On
the other hand, CT allows for an "internal"
reconstruction of basic logical
notions (truth-values, connectives, quantifiers) through
a
category-theoretic construction of topos. Since topos
may be regarded as a generalised domain of discourse as
well as a generalised geometrical space, this latter
approach reveals new deep links between logic and
geometry (topology).
The two approaches in the categorical logic are not
formally incompatible
but prima facie they assume different attitudes toward
the followingphilosophical dilemma: Whether any
mathematical theory needs certain logical foundations
(to be made explicit through some formal logical system)
or the formal logic itself is nothing but a particular
application of mathematics, so one should build logic on
a mathematical background rather than the other way
round? CT sheds a new light on this old controversy, and
allows for a substantial revision of its terms.
In this introductory tutorial we will give the basic
notions of CT, briefly sketch both approaches in
categorical logic, and consider the issue of Universal
Logic from a category-theoretic point of view.