**Proofs**

chalst: Thanks for your highly relevant comments. Let me see if I can answer.

"You don't need to encode first-order terms as singleton second-order variables..." Right. Actually, thanks for reminding me about the need to quantify over things like total functions. I was pretty much only thinking about building them up as terms, for which the proof that the function is total follows directly from the structure. For quantifiers, probably the easiest technique is to put this predicate into an assumption.

"...you may not be respecting the distinction between the set of total functions and the set of function that SOA can prove total." This is entirely possible. Presumably, the important difference is that you you quantify over the total functions, but when you build up from terms, you're restricted to the provably total. I'm not sure yet how this might bite me.

"Finally, you need to check your translation actually captures the
properties you are after." Actually, I may take the heretical position
that this is *not* necessary. You may want to allow the
translation to have essentially arbitrary properties. Of course, in
many cases there will be a meaningful translation back from target
language to source language, and it may be worth capturing that
formally.

Your point about a rich set of datatypes is well taken. Basically, what I'm trying to figure out is whether such a set of datatypes can be mapped to a simple Z_2 axiomatization using a straightforward definitional scheme. I'm not even sure that growth in the size of propositions matters much: as I said, in most cases, you won't be doing the translation explicitly.

What's the best source to read about these things, especially the polymorphic lambda calculus systems with the same provability strength as Z_2?

**Google**

I poked around at Google Answers a bit. It seems like a useful service, but I don't see any reason to get excited about it. There are two features I might have hoped for.

First, I don't see that the Answers provided help, or even particularly influence, the results of ordinary searches. This is disappointing, because it seems to me that Google's trust metric has the best chance of working when there's high quality manual input, especially regarding the trusted "seed". It's entirely possible that Google has two completely disjoint sets of people manually reviewing Internet sites (one set for Answers, another for deciding the seed), but that they don't talk to each other. I'm not sure.

The second missing feature is a bit harder to define, but it has to do with whether Answers is a true community. There are glimmerings of this. For example, having all the questions and Answers posted, along with comment posting open to all users, is cool. Many of the questions are interesting, and I can see people hanging out there. Another pro-community sign is that ordinary users and Researchers share the same namespace in the account/login system.

Most importantly, a lot of the Researchers seem to know each other, so there is something of a community there. But users don't really get to take part in it, even when (or perhaps because) they buy in monetarily. Part of the problem may be the way identities are concealed

If Google (or somebody else) figured out a way to build a real knowledge-seeking community, with money lubricating the system, I think they'd have something big. As it is, they have a reasonable service with a solid-gold brand behind it.