0
$\begingroup$

I am trying to find a proof of Gödel's second incompleteness theorem for an axiomatic theory T of finite strings from some fixed alphabet Γ, where Γ is, or is similar to, the set of symbols required to write T-sentences. I'm not fussy about what function and predicate symbols are taken as primitive in T (probably at least concatenation, but whatever it takes to make the proof easier). It is also fine (and preferred, if it simplifies the proof at all) if Γ is not finite (with a function symbol to construct variable names) but the union of a finite set with an infinite set of variables $x_1,x_2,\ldots$ (as is often done in the definition of FOL).

Something similar was mentioned in the following question answer as "the computer scientist's dream formulation", but for "lisp-like data": https://math.stackexchange.com/a/2095088/330299

Paulson wrote a computer checked proof of the incompleteness theorems for a theory of hereditarily finite sets, documented in these two papers:

$\endgroup$
  • $\begingroup$ What exactly is an axiomatic theory of finite strings? What sort of operations on strings are we supposed to be able to perform? $\endgroup$ – Noah Schweber Apr 24 at 2:23
  • $\begingroup$ @NoahSchweber, I added some clarification to one of the sentences: "I'm not fussy about what function and predicate symbols are taken as primitive in T (probably at least concatenation, but whatever it takes to make the proof easier)." An axiomatic theory of finite strings over the alphabet Γ is an axiomatic theory with a standard model whose universe of discourse is the set of finite strings over Γ. Analogously, PA and Primitive Recursive Arithmetic are axiomatic theories of natural numbers. $\endgroup$ – Dustin Wehr Apr 24 at 4:37
  • $\begingroup$ You might look at Raymond Smullyan's "To Mock a Mockingbird". Each bird has a song that it sings to each other bird. The birds are letters in the alphabet. He chooses the characteristics of the birds to have enough text processing to make the Gödel proof go through. $\endgroup$ – Ross Millikan Apr 24 at 4:49
  • $\begingroup$ Church numerals are essentially a way to represent finite strings in lambda calculus, using just two variables. This is similar to the "lisp-like data" idea, because lisp is a specific kind of lambda calculus. The key issue is having enough induction to prove the incompleteness theorems. In arithmetic $I\Delta_0$ induction and the totality of exponentiation is enough. However, I have not seen many detailed presentations of theories of formal strings that include induction axioms. $\endgroup$ – Carl Mummert Apr 24 at 13:22
  • $\begingroup$ Thank you @RossMillikan. I have ordered a copy. $\endgroup$ – Dustin Wehr May 1 at 13:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.