How does one prove the decidability of intuitionistic propositional logic, given the subformula property if a formula $A \rightarrow B$ is a subformula of itself?
Two of the texts I'm reading say that this proof is immediate, but what prevents one from repeatedly applying a rule like:
$\Gamma \vdash A \rightarrow B \\ ----- \\ \Gamma \vdash A \rightarrow B$
Is it that decidability is not actually immediate from the subformula property alone and these authors are implicitly appealing to the specific rules of the logic in question, or am I missing something?
In other words, does decidability only follow from a slightly stronger property like the proper subformula property, or some other strictly decreasing order on sequents?
I am looking specifically at Girard's Proofs and Types, in which he says decidability is an "immediate corollary" of the weak normalization theorem on page 24.
Proofs in sequent calculi can be represented as directed acyclic graphs instead of lists. In this case, there are no repetitions, and so there is a finite number of proofs that contain only subformulas of the derived sequent. Decidability follows from this finite search space.