Given a system of natural deduction, for example, say $\phi$ is a metavariable, it seems to me that there are only two valid proofs (up to the usual equivalence of proofs, i.e. $\beta \eta$ equivalence) of $\phi \wedge \phi \to \phi \wedge \phi$, (the one which swaps components, and the identity, speaking in terms of the Curry-Howard correspondence) and I expect that in general, any propositional formulae without quantifiers should have finitely many proofs. This leads to several questions:
Given a proposition in some system of natural deduction without quantifiers, are there only finitely many non-equivalent proofs? Is there a simple combinatorial method for determining the number of inequivalent proofs of a given proposition?
Given a proposition in a system of natural deduction with quantifiers, are there ever infinitely many non-equivalent proofs?
Of course, the first question is an extension of the very-non trivial question of consistency: (How many proofs are there of $\bot$? -- exactly $0$) And I suspect it might be feasible to study via similar methods, such as the sub-formula property, but I was wondering whether or not this has been done in the literature, and similarly for the second question.