[FOM] Proof Identity

[Milos Adzic]

Hello everyone,
I have some questions concerning the identity criteria for proofs 
(whether in intuitionistic, classical, BCK or some other logic; 
although  my  focus mainly lies on classical and intuitionistic logic, 
and on sequent calculi and natural deduction calculi systems of 
deduction for these). I am aware that in the literature there have been 
two main (as I find them) proposals. First is the all-well-known 
Normalization Conjecture made by Prawitz which says that two derivations 
denote the same proof iff they are equivalent (where the equivalence in 
question being the reflexive, symmetric and transitive closure of 
immediate reducibility relation). Of course the formal system in 
question is natural deduction system of Prawitz`s /Natural Deduction/. 
Second is the Generality Conjecture, proposed first by Lambek, treated 
by Szabo, and, finally, elaborated  and  characterized  with sufficient 
precision  by Dosen . The conjecture says: Two derivations are 
equivalent iff they have the same generality.Two derivations have the 
same generality when every generalization of one of them leads to a 
generalization of the other, so that in
the two generalizations we have the same assumptions and conclusion.  
Generalizations of derivations are considered that diversify variables 
without changing the rules of inference.(For details, see Dosen: 
"Identity of Proofs based on Normalization and Generality",The Bulletin 
of Symbolic Logic, vol. 9 (2003), pp. 477-503).
I skip the technical details of these two conjectures (although, I 
presume, the details of the former are well known), knowing that it is 
the technical side of the two conjectures that sheds light on the 
questions related to the topic; but, there is no great need for that in 
this point of time. My question is, simply, what are Your views on these 
two conjectures? Do You think they present the important aspects of 
proofs represented by derivations in mentioned formal systems (If we 
think of systems of deduction mentioned, say Gentzen`s LK(J) and NK(J), 
as being the semantics of intuitive mathematical proofs. We can also 
think the other way around, as suggested by Kreisel)? And, if You think 
that this is not the proper setting for discussing identity of proofs, 
what are the main problems that You find with these two conjectures? I 
have some second thoughts concerning the first conjecture, but I would 
really welcome Your opinion on the topic.
Best wishes.
Milos