Is there a formal notion of what we do when we 'Let X be …'?

This is likely an elementary question to logicians or theoretical computer scientists, but I'm less than adequately informed on either topic and don't know where to find the answer. Please excuse the various vague notions that appear here, without their appropriate formal setting. My question is exactly about what I should have said instead of what follows:

When we make a definition, of either a property, or the explicit value of a symbol, it seems that we are somehow changing the language. Prescribing meaning to a word might be viewed as a kind of transformation of the formal language akin to taking a quotient, where we impose further relations on a set of generators.

I don't know how to describe a 'semantic' object, but am assuming an ad-hoc definition could be as a class of words under an equivalence relation supplied by an underlying logic. If the complexity of such an object is the size of the smallest word in the language that describes it, then making a definition lowers the complexity of some objects (and doesn't change the rest.) The obvious example is that if I add the word group to my language, then saying G is a group is a lot shorter than listing its properties.

It seems that lowering complexity is a main point of making definitions. Further, that one reason mathematical theory-building works, is a compression effect through which I am able to use less resources to describe more complex objects, at the cost of the energy it takes to cram definitions from a textbook.

Likely there is some theory out there that describes this process, but I've not been able to google it. I would appreciate being pointed towards the right source, even if it's a wikipedia link. Specifically:

Where can I find a theory of formal logic or complexity theory that studies the process of adding definitions to a mathematical language, viewed as a transformation that changes complexity?

-
It's unclear to me that there is a definite gain at the complexity level. In order to use a definition, you must decode it, at least in part. For example, even if "G is a group" is known, you need extra information to know that it has an identity element and the decoding process seems to be just as lengthy as the long description of a group. Perhaps there is some gain in partial decoding, if you only need the fact that G is a monoid, but such gains can be had just with appropriate uses of the cut-rule. This is a good question. I wonder if there is a real gain in the end. –  François G. Dorais Apr 5 '10 at 4:58
I changed the tags a bit so that this good question attracts more attention from experts in complexity theory. (I don't think [formal-languages] really applies, but I left it as is.) –  François G. Dorais Apr 5 '10 at 12:50
@FGD: even for just intuitionistic propositional logic there's a doubly-exponential blowup in cut elimination. It seems to me that you need something more subtle than simple cut-elimination to answer this question. This is why I haven't responded to this question, despite the fact that "let x be foo in bar" is exactly the proof term for cut in lambda-calculi. –  Neel Krishnaswami Apr 5 '10 at 13:03
@Neel: I'm thinking the gain with definitions is exactly the same as the gain with allowing cuts, both would give the same amount of "compression." Your observation seems to support this. Does this sound right to you or do you see something else happening here? –  François G. Dorais Apr 5 '10 at 14:39
@Neel: I also think it's a good idea to post the lambda-calculus observation as a partial answer. –  François G. Dorais Apr 5 '10 at 14:48

Kieffer, Avigad, & Frideman, 2008 A language for mathematical knowledge management, which I mentioned in the Proof formalization thread, discusses DZFC, an extension of ZFC with definitions of terms and partial terms. Theorem 1 proves conservativity over ZFC, with respect to which the paper says:

the usual method of eliminating defined function symbols and relation symbols by replacing them by their definiens can result in an exponential increase in length.

Which is roughly in line with some analogous results for other formalisms. Neel mentioned the doubly expontential blow-up for normalisation in the simply typed lambda calculus, and more drastic blowups are possible with higher type systems.

It's unclear to me what notion of complexity is sought, but the expansion in size of terms under expansion will typically be the same as the time complexity of the expansion algorithm.

-
This looks very promising, and close to what I was asking about. I have to read it more carefully to understand whether it answers my question. –  Zavosh Apr 5 '10 at 21:13
Thanks very much. Although the paper only gives some examples of change in complexity, they do establish DZFC as a possible tool for studying this. –  Zavosh Apr 6 '10 at 6:36

I think the question by Zavosh involves a little bit more than extension by definition so let me add a few more words.

Here is what can be done in first order logic. Suppose we start with a theory $T$, and suppose we want to define something provably to exist in every model of $T$, what we do is to add a constant in the language and extend the theory to $T'$ in a proper manner. Confusing? Lets look at an example. Let $T$ be the theory of algebraically closed field with characteristic $0$. Now I know that there is an object $\alpha$ in every model of $T$ satisfying $\alpha^2 +1=0$. We want to have a new theory where there is an object satisfying this property. What we do is to add a constant $a$ to the language and let $T' :=T \cup \{ a^2+1=0 \}$. Any model of $T'$ will be a an algebraically closed field with a special element $\alpha$ satisfying $\alpha^2+1=0$.

I think at the level of first order logic , you can not define something like " Let $x$ be a group", that can only be done in second order logic. There is also a possibility that we can consider the theory where each object is a group, but I am not very sure about this.

About the second part of the question i.e. the purpose of definition is to reduce the complexity. I think there are two things which might interest you.

The first thing is extension by definition as mentioned above by mathy. Essentially, we don't want to say a very long sentence so we want to invent something shorter for it. So what we do is to add in more property and function into the language. By extension of definition we do not change the expressibility of the language. However, as you rightly, point out, the language become simpler, and this is reflected in the fact that some sentence in the old language is expressed with quantifier is expressed in the new language without quantifier. In a very good day, the new language has the ability to express everything with quantifier free statements, and this is what we call the theory admit quantifier elimination. This is very useful when we want to prove our original theory to be complete; we can reduce it to prove the new theory is complete, which is much simpler in various situation.

The second thing is skolemization of the theory which is a very much related process. Essentially what we do is to add in witness for true statements. The difference is that in this case the expressibility of the language changed. So not only you can talk about an object with less energy in the new language but you can talk about object that previously you can not in the original language. This has some use in constructing elementary substructure with small size in model theory. The example that I gave above about algebraically closed field is skolemization and not extension by definition. In the original language we can not talk about $i$ because we can not distinguish $i, -i$. But in the new language we can.

You can wiki the above entries as you see fit.

-
This is very interesting indeed. I had heard of quantifier elimination but didn't realize the connection. I suppose there must be a notion of 'quantifier complexity', say minimum number of quantifiers needed to define a set. Thanks for your thorough answer. I will definitely read up on those topics. –  Zavosh Apr 5 '10 at 2:24
Yes, I believe such notion can be defined. But I am not sure whether it is very useful. Our mind stop working after 2 quantifiers. –  Tran Chieu Minh Apr 5 '10 at 2:32
I meant that for example you could define existential complexity as the least number of existential quantifiers needed to define a set. I imagine it already has a different name. In any case I very much appreciated your answer, but will leave the question open for a day or two in case someone wants to give a complexity theory viewpoint. Thanks again! –  Zavosh Apr 5 '10 at 4:42
Ah, I understood what you said now. –  Tran Chieu Minh Apr 5 '10 at 5:32