This question already has an answer here:
I'm looking for a rigorous definition of the category defined (by handwaving) as such:
- objects are "logical propositions" (first order formulas?),
- morphisms are "logical deductions" between them (inference rules?),
- composition is just concatenation of deductions (so I would say in general a morphism is a proof?).
Is it there some issue regarding the size of the objects collection? Can we speak of the "class" of all formulas about e.g. sets?