Theory on the structure of proofs I was wondering if there has been a subset of logic devoted to the theory of proof structure. For example, is there a rigorous way to say that two proofs are "isomorphic," or to find upper or lower bounds on the amount of "information" needed in a particular proof?
 A: There is an area of math called Proof Theory (https://en.wikipedia.org/wiki/Proof_theory). It deals not only with the structure of proofs themselves but also with the metatheory around formal deductive systems, like the provability of some statements, the consistency and completeness of systems, and so on.
I do not know the answer to the first question, but proof theorists and logicians talk about the independency of a statement in a certain system; for example, the Generalized Continuum Hypothesis is independent of ZFC Set Theory, in the sense that it cannot be proved nor disproved using only the ZFC axioms. In a sense, ZFC does not have enough information to prove that the GCH is true or false.
A: You might be interested in intuitionistic type theory (which includes homotopy type theory).
Like all type theories, intuitionistic type theory concerns terms and types. Terms and types are primitive notions in type theory, but they can be thought of, respectively, as elements and sets, or as proofs and propositions.
Thus a type theoretic statement "$a : A$" (which says "$a$ is a term of type $A$") could be interpreted to mean "$a$ is an element of the set $A$" or as "$a$ is a proof of the proposition $A$", or even (in the case of homotopy type theory) as "$a$ is a point in the space $A$".
The reason intuitionistic type theory might be of interest to you is that it deals with identity types: given a type $A$ and terms $a,b : A$, there is a type $\mathrm{Id}_A(a,b)$, which can be thought of as a proposition asserting that $a$ and $b$ are equivalent, and whose terms can be thought of as proofs of this proposition. (Thus $p : \mathrm{Id}_A(a,b)$ means that $p$ is a proof that $a$ and $b$ are equivalent terms of type $A$.)
With the interpretation of types-as-propositions and terms-as-proofs, this is to say that if $a$ and $b$ are two proofs of a proposition $A$, then there is a proposition $\mathrm{Id}_A(a,b)$, whose proofs are themselves assertions that the proofs $a$ and $b$ are equivalent.
A: In addition to the already mentioned field of Proof Theory you might want to have a look at the field of Structural Proof Theory (sadly the wikipedia entry is rather incomplete). In particular, the area of Deep Inference and the study of Proof Nets are dealing with the question when two derivations are equivalent "up to bureaucracy". Upper and lower bounds for the information contained in a proof measured by its size are investigated in the area of Proof Complexity.
