1
$\begingroup$

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?

$\endgroup$

marked as duplicate by mattecapu, Community Oct 21 '18 at 8:14

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.

1
$\begingroup$

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

$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.