>>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.
>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.
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