Other stuff about yesterday: Dan Licata gave an interesting talk at the ConCert group meeting, about engaging in all sorts of shenanigans at the constructor and kind levels of a lambda-cubist sort of dependent type theory. Went to hot dogs, went through a proof of the Friedberg-Muchnik theorem with tom7, which states that there exist recursively enumerable sets A and B such that A is not turing-reducible to B (i.e. A is not recursive even given an oracle for membership in B) and B is not turing-reducible to A. This is a really weird thing, since it means, at some level, that there are "problems" that are "easier than" the halting problem, yet still undecidable. In fact there is a very powerful theorem due to Sacks that says for any countable partial order P, there is a collection X of R.E. sets such that P is isomorphic to (X, ≤T) where ≤T is the turing-reducibility relation. This means there is no "easiest impossible problem" nor is there any "hardest still-not-turing-complete" problem, and it means you can find countably many different problems none of which help you solve any of the others.