# What is the definition of computational content?

I am interested in type theory and proof theory. I have read a lot of papers and books that use the term "computational content" (For example: https://scholar.google.com/scholar?hl=en&q=%22computational+content+of%22&btnG=&as_sdt=1%2C33&as_sdtp=) and I have developed an intuitive sense of the meaning, but I have never seen the term formally defined.

Is anyone aware of a paper or book which defines this term?

Let's say I have a sentence of the form $\forall x\exists y\theta(x, y)$, where "$\theta(x, y)$" is "simple" (say, only bounded quantifiers) - I'm not interested in how hard it is to evaluate $\theta(a, b)$ for a given $a, b$. Then a computational interpretation begins with Skolemization: we look at the sentence $$\exists F\forall x(\theta(x, F(x))).$$ We're interested in what sorts of $F$ work here.

One reasonable question to ask is, Can such an $F$ be given by an algorithm? This yields a distinction between "computably true" sentences and "not computably true" sentences.

But as you correctly observe, this is a very coarse distinction in many cases. We often care about the runtime of an algorithm, or its complexity in some other sense (e.g. space used). So we may ask: "Is there an $F$ which works which is in $\mathcal{C}$?" for some nice complexity class $\mathcal{C}$.

We may also be interested in provable correctness. Maybe there's a polynomial-time computable $F$, but proving that this $F$ works requires large cardinals :P. It would be quite reasonable to say that this is pretty bonkers. So now we're interested in the theories within which statements like "There is a polytime-computable solution" are proved.

And, finally, we may also run into the opposite problem: given two non-computably true sentences, we may want to argue that one is "more computably true" than the other. To do this we now need to compare noncomputable functions, e.g. via Turing reducibility. So we can also go to a "larger" context, and work there. (See e.g. this paper, and also reverse mathematics.)

All of these concerns - the complexity of Skolem functions, and the difficulty of proving such complexity results - are broadly part of one intuition: that our desire to prove a theorem does not stop only at determining its correctness. I would call all the nuances of a theorem, in this sense, its "computational content" - and since this is so broad, I would not hope for a formal definition of this term. (You could create one, but I think it would necessarily lose some of the aspects of the term. Not everything has to be formalized, and I say this as a formalist!)

• I did not realize that the term was used so broadly. Can you clarify what you mean by "nuances of a theorem"? – user2377 Oct 24 '16 at 22:14
• @user2377 The phrase I used was "nuances . . . in this sense" - I was specifically talking about exactly the computability-, complexity-, and proof-theoretic details I and the other answers discuss. – Noah Schweber Oct 24 '16 at 23:08
• I find it very frustrating that the term is used so often, and authors rarely give it even an informal definition. But since your answer provides insight into why this is the case, I am accepting it. – user2377 Oct 26 '16 at 14:24

For all the titles on the first page of that link, "the computational content of $x$" means "the extraction of algorithms from $x$".

For instance, from an intuitionist proof of $\forall a \ \exists b$ you can extract an algorithm from $a$ to get $b$. Even from a classical proof of $\forall a \ \exists b$, some of this papers show how to extract an algorithm from $a'$ to get $b'$, at least in the right contexts.

A key early proponent of this concept was Georg Kreisel, who gave this statement of the goal and a proposed definition in 1958: “to determine the constructive (recursive) content or the constructive equivalent of the non-constructive concepts and theorems used in mathematics, particularly arithmetic and analysis....The concept of recursive interpretation is intended to give a precise formulation of the notion of constructive content (equivalent)." Solomon Feferman's 1996 commentary offers context.

• Perhaps my "intuitive understanding" is incorrect. You are saying that "computational content" means the extraction of an algorithm, not the algorithm that is extracted? – user2377 Oct 24 '16 at 14:33
• I have clarified that I was explaining what the phrase means in the titles. For any particular theorem, the computational content is an algorithm (e.g. from reals to reals) rather than the extractive process (from proofs to such algorithms). And when a constructive mathematician talks about the constructive content of a particular theorem, they may mean a particular algorithm. But when type-theorists and proof-theorists talk about computational content, they are usually interested in an extractive process and how it applies to a variety of theorems. – Matt F. Oct 24 '16 at 20:09

I don't think it's supposed to be a formal notion. But for instance for a statement like $\forall a\exists b$, the computational content could be: how hard is it to find that $b$. Is $b$ a computable function of $a$, for example.

• I agree. Just a remark: In (one of the flavours of) realizability theory, a realizer for a formula like $\forall a \exists b$ is precisely a Turing machine which calculates a suitable $b$ when given an arbitrary $a$ as input. – Ingo Blechschmidt Oct 24 '16 at 13:19
• Perhaps my "intuitive understanding" is incorrect. You are saying that the computational content of $\forall a \exists b$ is the difficulty in finding a $b$, not the method by which a $b$ is found? – user2377 Oct 24 '16 at 14:30
• @user2377 I think "content" is more in the sense of the content of a speech. Like "Let's discuss the left-wing content of Cruz's speech". – Bjørn Kjos-Hanssen Oct 24 '16 at 20:31