During some recent traveling, I re-read some sections of Douglas Hofstadter’s Gödel, Escher, Bach. Of particular interest was a step in the proof of Kurt Gödel’s first incompleteness theorem which involved substituting a variable of a formula with the formula itself. Hofstadter calls this peculiar operation “quining” after the logician W. V. Quine, who wrote extensively about self-reference. As with the previous times I read through that part, I noticed that the operation didn’t specify a variable for substitution like substitutions generally do, but instead performed substitution on all free variables, which is something I haven’t encountered anywhere else. This oddity wasn’t even mentioned, much less justified. Unlike after my previous reads, this time I decided to figure out why it was performed that way.

Now, the more interesting parts of Gödel’s Incompleteness Theorem involve what we now call Gödel coding to demonstrate that classes of logical systems can represent quining their own formulas and verifying their own proofs, the latter of which was very surprising at the time. But those parts turn out to be unnecessary for dealing with this small facet of Gödel’s proof, so let’s just deal with the proof’s final proposition, which is comparatively simple and straightforward: given that a logical system supports the operations of quining and proof verification (and logical conjunction and negation, and an existential quantifier), that logical system is incomplete (or inconsistent).

Let’s represent the predicate for whether p is a valid proof of formula f by VALID_PROOF(p, f), and use QUINE(x) to represent the formula x with all occurrences of free variables replaced by x. With this convention, the Gödel string G is “¬∃p: VALID_PROOF(p, QUINE("¬∃p: VALID_PROOF(p, QUINE(t))"))”, which is more readably written as “¬∃p: VALID_PROOF(p, QUINE(u))” where its “uncle” u is “¬∃p: VALID_PROOF(p, QUINE(t))”.

What’s QUINE(u)? That’s u with all occurrences of its only free variable (namely, t) replaced by u. That gives “¬∃p: VALID_PROOF(p, QUINE(u))”, which is G.
Now, “∃p: VALID_PROOF(p, f)” means “f is a theorem”.
So “∃p: VALID_PROOF(p, QUINE(u))” means “QUINE(u) is a theorem”. But QUINE(u) is G, so that’s equivalent to “G is a theorem”.
Hence G, which is “¬∃p: VALID_PROOF(p, QUINE(u))”, means “G is not a theorem”, which naturally is incompatible with the logical system being complete (unless it’s inconsistent). QED.

(Technical note: I use “∃p: VALID_PROOF(p, f)” instead of “THEOREM(f)” to adhere to the convention that relations are primitive recursive. That convention is Hofstadter’s: Gödel himself did use “THEOREM(f)”, which he wrote as “Bew(f)” from beweisbar, meaning provable.)

What goes wrong if we use a more typical substitution operation, that explicitly specifies the variable to substitute, instead? Let’s try it and see! If we define QUINE(x, v) to be the formula x with all occurrences of the variable v replaced by x, then the “uncle” u is “¬∃p: VALID_PROOF(p, QUINE(t, t))” and G is “¬∃p: VALID_PROOF(p, QUINE(u, t))”.

What’s QUINE(u, t)? That’s u with all occurrences of the variable t replaced by u, which is “¬∃p: VALID_PROOF(p, QUINE(u, u))”. Which is a problem because it’s not an exact match for G! That’s why the quining operation in Gödel’s proof is defined as applying to all free variables: it lets Gödel get away with implicitly defining the substitution variable by making it the only variable he fails to bind, rather than having to explicitly state it, thereby making it subject to substitution itself and consequently be defeated by his own trick for indirectly generating self-reference.

Having to deal with little details like this (which I’ve never seen mentioned before) is why Gödel’s Incompleteness Theorem was such a tour de force. Even if one started to get an inkling of what was going on, keeping the different levels of logic straight is itself mentally taxing, much less working out all the tricks needed to bridge between them.

Now, I personally find the standard string-rewriting presentation of formal logic to feel highly artificial, and more naturally performed by thinking of the formulas and their components as expressions instead of strings. An expression with free variables has a value which is dependent on the values of those variables, which is mighty close to saying it’s a function. So … fine, let’s bring in lambda notation to make it a function! We can then treat functions as “complete” entities, manipulable the same way truth values and numbers are. What’s QUINE in this formulation? It’s simply the call of its argument on itself, i.e. λx: x(x). Here, u becomes λt: ¬∃p: VALID_PROOF(p, QUINE(t)) and we get to define G as u(u), which is blatantly obviously QUINE(u). Then the chain goes G is u(u) is ¬∃p: VALID_PROOF(p, QUINE(u)) is ¬∃p: VALID_PROOF(p, G) is “G is not a theorem”. Much cleaner, IMHO!

To do the logic this way, we’d have to change the Gödel coding to work on expression trees, but that should be easier than the string-based coding schemes, as the algebraic manipulations that formal systems perform are more simply represented as operations on expressions than operations on strings. For instance, this way you evade precedence and associativity concerns, as well as all the syntactic well-formedness concerns — subexpressions are always “meaningful” but most substrings will not be. The big problem is handling bound variables (also a PITA with string-rewriting). I find combinatory logic to be particularly elegant for this. The general existential expression ∃x: Φ(x) (with arbitrary predicate Φ) can be written EΦ to eliminate the variable x. Universal quantification can also be written with its own A combinator, but we’d need axioms and/or inference rules for it, and they’d be inelegantly redundant with E’s. Alternately, (at the cost of having less-clear notation) it can be written as (NE)(NΦ) where N is the predicate negating combinator, i.e. NΦ = ¬∘Φ so (NΦ)x = (¬∘Φ)(x) = ¬(Φ(x)) — if you want to keep your combinators “pure” from logical operations so you can reduce them to S and K, you can replace N with (B¬) where B is the (pure) combinator for function composition, or adopt a convention that makes truth values and ¬ combinators as well. And finally, any lambda expression can be reduced to an equivalent “point-free” form that lacks the lambda and its bound variable, and which contains no variable-binding constructs if the body of the original lambda expression contained none itself. Since those three constructs (∃, ∀, and λ) are the only ways we have to bind variables, working from the most deeply nested variable-binding subexpressions outward we can convert any well-formed formula to an equivalent combinator expression with no bound variables. By using combinatory logic for our encoding, we avoid encoding bound variables altogether, and without the requirement to verify that variables are free or don’t collide with others, the encoding task gets much simpler!

Or so my intuition says. Has anyone actually done this kind of thing for combinatory logic? Referencing the above-linked article from Stanford’s online Encyclopedia of Philosophy, it looks like Raymond Smullyan probably has done so in his book To Mock a Mockingbird — so that’s likely to be my next read in metalogic now that I’ve finished GEB again. I have vague memories about combinatory logic being explored in his earlier book The Lady or the Tiger?, but I’m pretty sure it didn’t get into Gödelean incompleteness — perhaps it just stopped at the computational universality of SK combinator calculus. I don’t think it got into logical quantifiers, either. Come to think of it, the SEP article only mentioned quantifiers in its first section, and all the results in the later sections were for systems that lacked quantifier combinators like E, so we never see combinator quantifier inference rules like Φx ⇒ EΦ or AΦ ⇒ Φx. Not even in the part on Gödelean incompleteness, curiously!