Can anyone comment on the distinction between two different methods of formal proof? Since I'm pretty shaky on the methods and terminology of Proof Theory I a refer to them below as the "implicit" and "explicit" approaches. Apologies for my ignorance - I am a physicist and not a mathematician by trade!
Suppose we have a mathematical system with property $X$. We have two theorems:
I. The system will have property $X$ if and only if it has property $A$;
II. The system will have property $X$ if and only if it has property $B$.
Then without any further work we can say that, for this sytem, $A \iff B$. We don't need to see any details to know this to be true. This is what I am calling "implicit" proof (I suppose you could call it a transitive strategy, or something).
By "explicit" proof I mean that we start with property $A$ (resp. $B$) and, step-by-step, demonstrate how it implies property $B$ (resp. $A$) without reference whatsoever to $X$. We haven't proven anything new - we already knew this should happen from the "implicit" argument - but we have seen explicitly how and why it comes about.
To my mind these methods of proof seem conceptually distinct. Is any such distinction drawn in the literature? Would you have a preference for one method over the other? I hope my question makes sense!