Proof of second incompleteness theorem for Set theory without Arithmetization of Syntax

Question

Is there a proof of the second incompleteness theorem of Godel for set theory which doesn't use Arithmetization of Syntax (Godel numbering)?

I came across a short proof by Thomas Jech (here), but I think he uses Godel numbering for defining "k" in his proof. Nevertheless Bagaria in his article (here) in referencing Jech, mentioned there is no need of arithmetizing the syntax.

My question is, does his proof crucially depend on Godel numbering? If the answer is yes, is there a proof of second incompleteness theorem for Set theory(ZFC) which doesn't need some fixed coding of formulas by proving there is no model of ZFC, in ZFC itself?, or the use of such coding is unavoidable?

Answer 1

I understand the question to be about how to represent syntax internally in a theory. The traditional approach in logic is to use natural numbers and Gödel encodings.

Computer science, and in particular programming language theory, have a very rich theory of syntax. The abstract view of syntactic expressions is that they are finite trees, and that is how syntax is actually represented internally in compilers and other programs that process syntactic expressions. Of course, trees can easily be dealt with in a set theory, so you could use them to present syntax.

(A word of warning: if you speak to a computer scientit and state that syntax is about sequences of symbols they'll think you ignorant, or that you teleported from 1950's. Concrete syntax that humans use is indeed made of sequences of symbols, but these are viewed as convenience for humans, and are prompty parsed into abstract syntax trees. Nobody ever writes code that processes syntax by working directly with sequences of symbols.)

Category theorists have something to say about syntax as well. Joyal's arithmetic universes were designed to give an abstract account of Gödel's incompleteness proofs. Joyal never managed to publish this work, but Emilia Maietti kindly wrote it up in Joyal's arithmetic universes via type theory.

This is not the end of the story however. (Some) computer scientists are obsessed with finding the best way to deal with bound variables and binding operators (such as $\forall$, $\exists$, $\int$, etc.). There are abstract mathematical accounts of syntax with binding, for example higher-order abstract syntax. Perhaps the most interesting to this audience is nominal syntax which uses permutation models of ZF. Murdoch Gabbay's publications page has a wealth or resources, perhaps one can start with Foundations of nominal techniques: logic and semantics of variables in abstract syntax (published as https://doi.org/10.2178/bsl/1305810911 in the Bulletin of Symbolic Logic).

Answer 2

As mentioned in the comments, there are semantic proofs in set theory (thus non constructive, i.e they do not provide a recipe for constructing an undecidable sentence). However, Goedel himself first proved his celebrated result without arithmetization - and constructively. He showed the result to von Neumann, who asked him if he could produce an arithmetic undecidable sentence. Goedel then revised his proof for publication using his famous coding, beta-function, etc. The original proof without arithmetization as far as I know is lost. I don't know of a logician who has constructed this simpler proof, but it is possible. You don't need polynomials to talk about undecidability - that is an roundabout device that Goedel introduced simply in order to make the undecidable sentence an arithmetic (diophantine) one. The sentence can also be in ZF set theory for example, which states that a certain sequence does not belong in a certain set - the sequence could be of ordinal numbers, with the coding of each number represents a symbol in the language. 0 = (, 1 = ), 2 = universal quantifier, etc. etc. And then you don't use polynomials at all. Your sentence is just about sequences of ordinals.