I met and spoke with:
Keith Devlin, who happens to be working in intelligence analysis. I told him about Bringsjord's reasoning assistant Slate, and he said he would look it up. Intelligence analysis seems to be all about "debiasing" expert opinions.
John McCarthy, whose goals are very close to mine. We hold on to the Leibnizian ideal. (I would actually like to debate someone who is "against" logical AI). I asked him if he knew of an interface / language / system for supporting the process of formalizing arbitrary texts, a sort of semi-structured language to support the process of gradual formalization, along with revisions, ontology changes, etc. I told him about the people doing Mathematical Knowledge Management, and said I would like to create a system to help formalize general arguments. He said he was interested and told me to contact him if I did anything in this direction. He then gave me his business card, with cell phone and all.
Happy that I got the interest of the bigshot, I started joking around with my colleagues. I saw a man who seemed to be having an interesting argument about Occam's razor: why should the universe be simple? I jumped in with Schmidhuber's argument that "by the anthropic principle, we are more likely to be living in a quickly-computable universe".
He was amused, so he introduced himself.
- Hi, I'm Kevin Kelly
- You are Kevin Kelly???
We walked to Oorlam to have a few drinks, where I sat next to Henrik, who picked things up faster than me, partly due to his knowledge of recursion theory. Kevin Kelly blew our minds with:
* Bayesianism as a meta-method is wrong/bad.
* The application of Kolmogorov Complexity to the problem of induction is philosophically bad (citing the arbitrary choice of universal machine). There are many paths to the truth. People tend to like Solomonoff induction because it's too tempting. He also said that he got one of the KC bigshots to admit that MDL is not about finding the true theory (thus putting all disagreement off the table).
* The problem of induction is the problem of the undecidability of the halting problem.
* Topology and recursion theory are the right tools for thinking about induction. Verifiable propositions are to be interpreted as open sets.
* The cases where induction is needed are the boundary points (i.e. they can't be logically verified, since any open set around them will intersect with the outside... the semantics isn't very clear to me)
* Topological structures are invariant under "Goodman's grue" automorphisms, whereas Bayesian structures aren't. (I remarked that it's well-known that the uniform prior is sensitive to the representation one uses)
That day I also ran into a few other people, one of whom was Breanndán, the expert Lisper who I've been meaning to talk to.