A sketch of a proof of a version of Goedel's incompleteness theorem

Consider a first order language (FOL) L that, in addition to the standard ingredients of FOL, including equality and a store of names and predicates, has the following:

• A binary function +.
• A names for every symbol of the language. I will suppose that the name for the symbol "s" is "'s'". (Double quote marks are meta-language quotation; single quote marks are L-quotation.)
• A binary predicate Quotes.

The intended interpretation of L will have as its domain the collection of all strings of finite length, including the empty string, of symbols from L. In the intended interpretation, "+" is string concatenation, so that if "a" denotes the string "xx" and "b" denotes the string "yy", then "a+b" denotes the string "xxyy". Finally, in the intended interpretation, a and b satisfy Quotes if and only if a is of the form "'a'+'b'+...+'m'" and b is of the form "'ab...m'".

Introduce the abbreviation Substring(u,v) for the expression: ∃x∃y(v=x+u+y).

Introduce the abbreviation Begins(u,v) for the expression: ∃x(v=u+x).

Introduce the abbreviation FirstQuotes(u,v) for the expression: ∃x∃y∃w (~SubString(''', x) & u=x+w+y & Quotes(w,v) & ~Begins('+',y)).  Informally, this says that v is the first expression that is quoted in u.

Introduce the abbreviation FirstQuoteSubstituted(u, v) for the expression: ∃x∃y∃z∃w(FirstQuotes(u,y) & Quotes(w,y) & u=x+w+z & v=x+'()'+y.  Informally, this says that v is what you get if you replace the first quoted expression in u with "()".

Introduce the abbreviation SelfSubstitutes(u) for the expression: ∃x(FirstQuotes(u,x) & FirstQuoteSubstituted(u,x)).  This says that the first thing quoted by u is u itself with the first quoted expression replaced by "()".

Now, enriching the language as needed (I think we need one enrichment: we need a "Balanced" predicate which checks if parentheses are balanced), define the predicate or abbreviation Provable(u). Finally, form the sentence:

1. ∀x(∀z(z='*' → (SelfSubstitutes(x) & FirstQuoteSubstituted(x,z)))→~Provable(x)),

where we expand out all abbreviations, fixing up variables over which we quantify to avoid conflicts, and where "*" abbreviates:

• ∀x(∀z(z=() → (SelfSubstitutes(x) & FirstQuoteSubstituted(x,z)))→~Provable(x)).

We can then check that (1) is the one and only value of x that satisfies the antecedent of the conditional in (1) whose consequent is ~Provable(x).

Consequently, (1) is true if and only if it is not Provable. If all Provable sentences are true, then (1) must be true and not Provable. (For if (1) were false, it would be Provable, and hence true. If (1) were true and Provable, (1) would be false.)

If this works mathematically, I think it could work very nicely didactically, with some refinement.

Of course, I probably got some details wrong.  Maybe I made a bigger mistake, too.

If morbid curiosity leads you to ask what my Goedel-like sentence looks like when expanded, it looks like the following if we take "Provable" to be a primitive in L: ∀g(∀h(h='∀'+'g'+'('+'∀'+'h'+'('+'h'+'='+'('+')'+'→'+'('+'∃'+'t'+'('+'∃'+'q'+'∃'+'r'+'∃'+'s'+'('+'~'+'∃'+'m'+'∃'+'n'+'('+'q'+'='+'m'+'+'+'''+'''+'''+'+'+'n'+')'+'&'+'g'+'='+'q'+'+'+'s'+'+'+'r'+'&'+'Q'+'u'+'o'+'t'+'e'+'s'+'('+'s'+','+'t'+')'+'&'+'~'+'∃'+'p'+'('+'r'+'='+'''+'+'+'''+'+'+'p'+')'+')'+'&'+'∃'+'x'+'∃'+'y'+'∃'+'z'+'∃'+'w'+'('+'∃'+'q'+'∃'+'r'+'∃'+'s'+'('+'~'+'∃'+'m'+'∃'+'n'+'('+'q'+'='+'m'+'+'+'''+'''+'''+'+'+'n'+')'+'&'+'g'+'='+'q'+'+'+'s'+'+'+'r'+'&'+'Q'+'u'+'o'+'t'+'e'+'s'+'('+'s'+','+'y'+')'+'&'+'~'+'∃'+'p'+'('+'r'+'='+'''+'+'+'''+'+'+'p'+')'+')'+'&'+'Q'+'u'+'o'+'t'+'e'+'s'+'('+'w'+','+'y'+')'+'&'+'g'+'='+'x'+'+'+'w'+'+'+'z'+'&'+'t'+'='+'x'+'+'+'''+'('+')'+'''+'+'+'y'+')'+'&'+'∃'+'x'+'∃'+'y'+'∃'+'z'+'∃'+'w'+'('+'∃'+'q'+'∃'+'r'+'∃'+'s'+'('+'~'+'∃'+'m'+'∃'+'n'+'('+'q'+'='+'m'+'+'+'''+'''+'''+'+'+'n'+')'+'&'+'g'+'='+'q'+'+'+'s'+'+'+'r'+'&'+'Q'+'u'+'o'+'t'+'e'+'s'+'('+'s'+','+'y'+')'+'&'+'~'+'∃'+'p'+'('+'r'+'='+'''+'+'+'''+'+'+'p'+')'+')'+'&'+'Q'+'u'+'o'+'t'+'e'+'s'+'('+'w'+','+'y'+')'+'&'+'g'+'='+'x'+'+'+'w'+'+'+'z'+'&'+'h'+'='+'x'+'+'+'''+'('+')'+'''+'+'+'y'+')'+')'+'→'+'~'+'P'+'r'+'o'+'v'+'a'+'b'+'l'+'e'+'('+'g'+')'+')'→(∃t(∃q∃r∃s(~∃m∃n(q=m+'''+n)&g=q+s+r&Quotes(s,t)&~∃p(r='+'+p))&∃x∃y∃z∃w(∃q∃r∃s(~∃m∃n(q=m+'''+n)&g=q+s+r&Quotes(s,y)&~∃p(r='+'+p))&Quotes(w,y)&g=x+w+z&t=x+'()'+y)&∃x∃y∃z∃w(∃q∃r∃s(~∃m∃n(q=m+'''+n)&g=q+s+r&Quotes(s,y)&~∃p(r='+'+p))&Quotes(w,y)&g=x+w+z&h=x+'()'+y))→~Provable(g)).

If we have an explicit formula for Provable(x), we need to fix up the "'P'+'r'+'o'+'v'+'a'+'b'+'l'+'e'+'('+'g'+')'" and "Provable(g)" parts.