Regarding question 1: 

Formalizing the idea of richness of structure is very difficult. This is not because the question is inherently impossible to answer, but because many of the relevant questions are open problems in logic which do not yet have satisfactory explanations. As just one example, we don't have entirely satisfactory explanations of what the complexity of a proof is, which seems necessary to make the idea of rich structure a fruitful one. 

Concretely, let's restrict our attention to set equipped with structure, and then further restrict our attention to purely algebraic structures on a set -- that is, we posit that our set has a collection of operations whose equations are universally quantified equalities on the operations. Now, notice that for any such algebraic structure, the one-element set provides a trivial model. 

Of course, it's utterly absurd to say that the one-element set has rich structure because it's a model of all algebraic theories. The reason it's absurd to say such a thing, is because it's a model of all algebraic theories for trivial reasons -- in other words, there's a trivial, generic, proof that the one-element set satisfies all those equalities (namely, all functions into a one-element set are equal, by the extensionality of equality of functions). 

In order to rule out these boring counterexamples, we need a concept of the complexity of proofs, so that we have some formal way of saying that an equation is satisfied for an interesting reason. For example, we may wish to say that the natural numbers have nontrivial commutative monoid structure $(\mathbb{N}, 0, +)$, because the proofs of the associativity and commutativity of addition are not trivial (though of course they are very easy -- which is itself another idea that calls for formalization!). 

However, even the equality theory of proofs is very difficult, let alone being able to measure their relative complexities. The basic technology here is Gentzen's sequent calculus, and the basic question here is how to deal with lemmas (i.e., the "cuts" of his cut-elimination theorem). Namely, if we take a proof, and factor it into a series of lemmas, is it still the same proof? If we answer the question with a "yes", then we have a theory of proof which says we should compare the normal forms of proofs -- but it's easy to show that even in the propositional case, the presence of lemmas can make proofs doubly-exponentially smaller. It seems extremely weird to say that such a dramatic change makes no difference! If we answer the question with a "no", then some trivial rearrangements can cause us to declare two proofs not the same, which is also strange. 

One way of squaring this circle is to suggest that perhaps we should look at the *complexity* of proof-normalization, and equate two proofs when it only takes a small amount of work to go to a common normal form. However, this suggestion has the problem that we don't know how to do this. Perhaps the closest we can presently come to this is with Jean-Yves Girard's Geometry of Interaction, which gives a fixed point semantics to proof normalization, which can be used to get numerical estimates of the complexity of normalizing individual proofs. However, this is very much current research, and many basic questions about GoI remain open.