Barbara & the other (categorical) https://en.wikipedia.org/wiki/Syllogism take the "existential viewpoint" (see introduction on https://en.wikipedia.org/wiki/Categorical_proposition) that involves "term": https://en.wikipedia.org/wiki/Term_logic instead of just "sentential": https://en.wikipedia.org/wiki/Propositional_calculus logic. From https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... the universal quantification "all" in Barbara corresponds to the generalized product (conjunction rather than implication) type. B is also known as the composition combinator & (implicational) forms are shown here: https://en.wikipedia.org/wiki/Hypothetical_syllogism#Alterna...