Is there a category of logical propositions and deductions?

Question

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?

Answer 1

For intuitionistic logic, cartesian closed categories are equivalent to what you‘re asking for. Look up the Curry-Howard-Lambek correspondence.