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

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

Since you expressly asked for links to La Wik, start with Extension by definitions

The article does not seem to address computational complexity directly, so I'm leaving that issue for other users.