Schmidhuber: >>It's the simplest thing, given this use of mathematical >>language we have agreed upon. But here the power of the >>formal approach ends - unspeakable things remain unspoken.
Marchal: >I disagree. I would even say that it is here that the serious formal >approach begins. Take "unprovable" for "unspeakable", we can >meta-reason (informally or formally) and study the logical structure >of the set of unprovable sentences by sound universal machines. Schmidhuber: Unprovable does not mean unspeakable! You can spell out many unprovable things. Why care for the subset of provable sentences? Aren't we interested in the full set of all describable sentences? We can generate it, without caring for proofs at all. "Unspeakable" means "beyond formal definition." In particular, the way we humans communicate and agree on a common formal language is not formally defined. You write "x" and I say, ok, it's an "x", but that's all based on some sort of informal agreement that involves complex pattern recognition and learning processes. Usually we do not question the validity of outcomes of such cognitive processes, and just go ahead with formal derivations. But there is this major informal step *before* formal reasoning can start, and good textbooks on logic acknowledge this.