Godel: are all undecidable props in consistent math systems subsets of self-referent statements?

Are all undecidable propositions in consistent mathematical systems subsets of self-referent statements? Or are there other types of examples where Godel’s incompleteness theorem applies?

Also: Q2: How commonplace are undecidable propositions in consistent mathematical systems?
And: Q3: Is Hofstadter’s Godel, Escher and Bach still worth reading?

This thread spins off of What do mathematicians do if a proof turns out to be wrong? Rather than continuing the hijack, I’ll take it from part of Indistinguishable’s post:

I don’t see how general this property of incompleteness is. Why do we want our language of propositions to be capable of expressing statements about the behavior of the very proof system itself? I mean sure, if it can’t do that I can see how the system would be incomplete. But are there any mission-critical examples of undecidable statements? (Mission critical: a metaphorical phrase meaning roughly, “Something I should care about.”)

Copy. Paste.
Wikipedia lists examples by Paul Cohen, including the continuum hypothesis and the axiom of choice at least within Zermelo–Fraenkel set theory. There are others. My understanding is highly tenuous. Helpful discussion (especially of Q2 and Q3, above) was provided in the 2004 thread, In simple terms, can someone explain Godel’s Uncertainty Theorem to me?

Check out the Paris-Harrington theorem.

Define “self-referential”. Really, the key problem is not that self-referential statements are problematic: That’s been known since Epimenides. The key to Gödel’s theorem is that any system capable of handling arithmetic is also, through a sort of back door, capable of producing self-referential statements, too. Basically, you can translate statements into numbers, and the rules of your system itself into statements about numbers, and no matter what you do, you end up with statements about numbers that are really statements about statements in disguise, and hence self-referential.

Now, there are some mathematical systems which are not capable of dealing with arithmetic, but which are still capable of doing a limited selection of other interesting things, and some of those systems are in fact complete and consistent. But they’re pretty limited.

The key points to understand about unprovability/incompleteness:

A) There’s no such thing as a statement being absolutely provable/unprovable There’s only provability/unprovability within a particular proof system. (After all, for every statement, some proof system proves it (e.g., you could imagine treating it as an axiom, and then of course it would be trivially provable, within that system))

B) Incompleteness is just a pair of complementary unprovability results.

What is the definition of incompleteness? Well, we say a proof system is incomplete just in case there is some statement X (of the sort considered posable within that system) such that the system neither proves X nor proves the negation of X.

That a particular proof system should fail to prove a particular statement is commonplace; after all, we generally aren’t interested in proof systems in which all statements are provable. Incompleteness is just the special name for when two cases of unprovability happen to “match up”.

C) Not all incompleteness has anything to do with Goedel!

Many sources muddy these waters by bringing up, in the context of Goedel’s incompleteness theorem, the fact that neither the Continuum Hypothesis nor its negation is provable in the popular proof system ZFC [as well as a whole class of similar systems]. But these two results have absolutely nothing to do with each other, beyond the fact that they both take the form “System […] doesn’t prove statement […], nor its negation”. (In fact, the two unprovability results concerning the Continuum Hypothesis don’t really have terribly much to do with each other either…)

Incompleteness is ubiquitous, because unprovability is ubiquitous; unless you had some reason to suppose that a particular proof system was complete, then you have no grounds for being surprised to find that it isn’t. That is, unless you had some reason to suppose that a particular proof system proved at least one among some bunch of statements, then you have no grounds for being surprised to find that it doesn’t.

For example: Consider the following informal sketch of a proof system: you take as axioms that there are things called “numbers”, including a particular number called “1”, and there’s some operation called “+” on them, about which all you assume is that it’s associative and commutative. A perfectly fine proof system. We might ask ourselves if it’s complete.

Well, no; consider a statement like “There exists a number X such that X + X = 1”. This system can’t prove that statement (because everything this system says could be interpreted as about integers, in which case that statement would not be true) nor can it prove the negation of that statement (because everything this system says could be interpreted as about rationals, in which case that statement would be true). Ergo, this system is incomplete. And that’s perfectly unsurprising: was there any reason to have supposed this particular random collection of axioms would prove or disprove all statements of this kind?

Now, we could add more axioms to this system, and thus become able to prove more statements. But, just as well, we could remove axioms, and thus become able to prove less statements. Unprovability is ubiquitous.

[Further parts coming]

Alright, so, remember: incompleteness is the default state of things, so to speak, and there’s no general reason to expect a proof system to be otherwise. And this happens in abundance even without any Goedelian phenomena. [The group axioms are incomplete: it’s undecidable from them whether multiplication is commutative. The field axioms are incomplete: it’s undecidable from them whether 2 has a square root. The axioms for a two-valued, well-pointed Boolean topos with a natural number object in which all epis split are incomplete, just as are the axioms of Zermelo set theory with foundation and choice, and for similar reasons too: in both of these, it’s undecidable whether V[sub]ω+ω[/sub] exists.]. That should answer Q2. As for Q3, of course; why wouldn’t it be?

Hm, part D?
D) Goedel’s first incompleteness theorem (henceforth, GIT1) is about one very specific situation which gives rise to incompleteness in a predictable, mechanical fashion. [There is also the closely related Goedel’s second incompleteness theorem (GIT2) (aka, Loeb’s theorem) which also mechanically constructs, within a certain kind of setup, limits on provability taking a very specific form. If an incompleteness/unprovability/relative provability/whatever result is not equivalent or corollary to one of this form, then it has nothing to do with Goedel’s incompleteness theorems. (E.g., as I said above, neither the continuum hypothesis nor axiom of choice independence results have anything to do with GIT, even though Goedel was also one of the two key figures in proving them. (However, the Paris-Harrington theorem mentioned by ultrafilter is related, and indeed a great example, as it arises as a corollary of GIT2, but concerns a non-self-referential (at least, not manifestly) statement of natural mathematical interest))].

Ok, so what is that specific situation and result dealt with by GIT1? Well, I described it in the thread linked to in the OP, but let me try to present it again, hopefully better, starting from a high level and gradually peeling back the layers:

The first layer:
Suppose, within a particular proof system P, it were possible to pose a statement interpreted as “P disproves (i.e., proves the negation of) this very statement”. (Call this statement H.) Suppose P also has a modicum of self-awareness, in the sense that whenever it proves/disproves X, it also proves that it proves/disproves X (Call this positive introspection). What would happen?

Well, there are various cases. In the following, keep in mind that H basically equals “P disproves H”.
[li]There are cases where P disproves H. In which case, by positive introspection, P also proves “P disproves H”. But the statement “P disproves H” is H itself! So P is inconsistent in the sense that it both disproves and proves H[/li][li]There are cases where P doesn’t disprove H, but it does prove H. In which considering what H says, we have that P proves “P disproves H”, even though P doesn’t actually disprove H. This isn’t actually a straight-up inconsistency, in the sense of both disproving and proving the same statement, but this is a case where P falsely claims to prove/disprove something.[/li][li]Finally, there are cases where P neither proves nor disproves H, and is thus incomplete.[/li][/ul]

So, when such a statement as H is posable within P, and P has the positive introspection property, then either P is inconsistent, incomplete, or claims that it proves a statement even though it doesn’t actually prove that statement [aka, lacks two-way introspection]. Alright, let’s keep that on a corner of our table, and come back to refine it later.

The second layer:
The rest of GIT1 consists of using a now-standard mathematical technique called diagonalization (aka, the Y combinator; essentially due to Cantor, and indeed, in some sense, GIT1 is just the interpretation of Cantor’s theorem in a different environment than its conventional presentation) for how to express H without having to explicitly be given the ability to say things like “this very statement”. The idea is, suppose you had a way of interpreting each object of some kind as a description of some particular subset of [aka, property/predicate on] the objects of the same kind. [For example, certain blocks of text define sets of blocks of text (“the set of three-letter blocks of text”, “the set of palindromic blocks of text”); and those blocks of text which seem to mean other things or nothing at all could at least be interpreted by default to describe the empty set]. And suppose that every definable subset of those objects [definable within the relevant proof system] actually was described, under this interpretation, by some such object. Finally, let’s view a pair of objects (x, y) as representing the statement “y is in the set described by x” [aka, “y has the property described by x”].

Then, from any definable property F([Object[sub]1[/sub]], [Object[sub]2[/sub]]) of pairs of objects, you could define the set “Those objects x such that F(x, x) holds”; being definable, this set is the interpretation of some object c. Now, note that c is in the set it describes if and only if F(c, c) holds. That is to say, the statement represented by (c, c) is true if and only if F(c, c) holds. Accordingly, the statement represented by (c, c) essentially is F(c, c); that is to say, F(c, c) basically is the statement “F holds of this very statement”.

Alright, trick accomplished. Now, we just need to take F to be the property of disprovability within P, and we’ll have constructed the H from layer 1.

Accordingly, the result from layer 1 is now reduced to this: Suppose the P-definable predicates upon objects of a certain kind are construed as represented by particular such objects, and, furthermore, some particular P-definable binary predicate upon such objects can be taken to express that P disproves the application of the predicate represented by the first object to the second object, in such a way as that, under this interpretation, the positive introspection property is validated. Then P is either inconsistent, incomplete, or lacks two-way introspection. (As a corollary, if such a P only proves true things, so that it is consistent and has two-way introspection, then it must be incomplete). This is Goedel’s first incompleteness theorem.

[Coming next: GIT is not about arithmetic!, GIT is Cantor’s theorem (in the guise of Tarski’s indefinability theorem; also essentially the same: the undecidability of halting problems), and of course, GIT2/Loeb’s theorem]

(Well, possibly coming next. I may get lazy, or people may not even be interested. But the “GIT is not about arithmetic (although here’s why people have traditionally connected them (but, please, stop doing that!))!” rant I’ll probably want to do, at least.)

Arithmetic here being “Peano arithmetic”. There’s simpler arithmetics, like Presberger arithmetic, which are complete, consistent and decidable (and also relatively widely used: see the “linear” solver in Isabelle, for instance). Also, of interest, is Robinson arithmetic, which is Peano arithmetic without the induction schema. This is already incomplete, but doesn’t need an appeal to Goedel, or a lengthy proof, to show it (to reinforce Indistinguishable’s point): there’s a short proof of incompleteness in the book I’ll mention below.

If you’re really that interested in Goedelian incompleteness, then you should pick up “An introduction to Goedel’s theorems”, CUP, by Peter Smith. It’s aimed at advanced philosophy undergraduates taking a second logic course, but is rigorous, well written, and very easy to follow. The book also covers topics in undecidability.

Indeed, it is of course the case that whenever you take a consistent system and drop a non-redundant axiom, you’re left with an incomplete system, and conversely. [For when you add an axiom to a complete system, you’re either adding something already provable [in which case it’s redundant], or something already disprovable [in which case adding it as an axiom yields inconsistency]]. Which again shows how ubiquitous, and mundane, mere incompleteness is.

Thus, the incompleteness of Robinson arithmetic is just the consistency of Peano Arithmetic + the fact that the induction schema can’t be derived from the rest of Peano Arithmetic alone. The first of these is trivial by “Well, everything Peano Arithmetic proves is true, so of course it’s consistent” (but see GIT2 and Tarski’s indefinability theorem, to come), and the latter of these, as CRSP rightly points out, is an unprovability result which is easily established without any recourse to Goedelian phenomena (e.g., the induction schema entails that no number is its own successor; however, by considering the naturals augmented with a unique “infinity” element, one readily finds a model of Robinson arithmetic in which some number is its own successor).

That having been said, the Goedelian phenomenon does provide a much more general result: to wit, every computable extension of Robinson arithmetic is likewise incomplete. [Because all computable functions can be defined in Robinson arithmetic (in a “positive introspection”-validating manner). More on this to come in “GIT is not about arithmetic!”…]

Missing word re-instated in bold, though it’s a pedantic fix, and perhaps we should just take completeness to implicitly include consistency from here on.

It would, perhaps, be more accurate to say that GIT is not just about arithmetic. It’s about any system which meets certain conditions, and anything that can model Peano arithmetic happens to be one such system that meets those conditions. The fact that it can be applied to other things as well doesn’t mean that it’s not relevant to arithmetic.

Dude, I just gotta say:WTF?
I think I’ll walk away, leer, and renew my yearly-dues to DENSA.

BTW, y’all know I can tell whether it’s 9/16" or 1/2" with a glance?

Maybe they discussed this my senior year, when we used to go to Dr./Sister Nancy’s Am Lit 406, drunk, at 10am. Ahhh! to argue Puritan/Quaker symbolisms with a buzz going!

Seriously, here are your answers:
Motivation VS Intent. They are not mutually exclusive, nor is one a reactor based soley on result, nor can it be read as: Impetus VS Conditional Reactions.

The incompleteness theorom results from AXIOM being spelled with an “X”, and “X” is a all-to-simplistic assumption.

X is not a given.


Yes, that’s fair. Goedel’s incompleteness theorem is about Peano Arithmetic (or Robinson arithmetic or its Sigma_1 fragment or true arithmetic or the corresponding theories of hereditarily finite sequences or what have you) the way Taylor’s theorem is about hyperbolic trigonometry (or elliptic integrals or the Gamma function or Gaussian distributions). Those are all specific areas yielding instances to which the theorem is applicable, but the theorem is not fundamentally about any of those in particular, and it would be odd to present it in terms of them.

Goedel’s theorem is not even fundamentally about just computable theories [as seen by its alter ego, Tarski’s indefinability theorem]. (For that matter, I daresay the near-universal presentation of GIT1 in terms of incompleteness is an accident of history, setting an odd focus. But I digress). For example, it tells us that an axiomatization of true arithmetic (all the true first-order statements in the language of PA) cannot even be given by a program equipped with an oracle for the halting problem + an oracle for the halting problem for machines equipped with an oracle for the halting problem + an oracle for … .[sup]1[/sup] This, of course, goes well beyond plain computability.

That having been said, computable theories are of course the particular case of most significant interest and clearest foundational importance, so I understand why people would want to present GIT only in terms of the restrictions it places on computably axiomatizable theories. And since interpreting the theory of computable functions within the finitary fragment of set theory or the theory of hereditarily finite sequences or such things is rote and straightforward, even if tedious, I couldn’t mind too much if people continually presented GIT in terms of its implications for extensions of natural systems of finite set theory. [And indeed, at the time of the 1931 paper introducing GIT, still five years before Turing machines or Post machines or the lambda calculus (a lot happened in 1936), those mechanics of defining and dealing with computable functions which are nowadays rote and straightforward were anything but[sup]2[/sup], and a major part of the paper was devoted to explaining these in detail, a fine accomplishment of Goedel’s at the time (given that no one had even set out a definition of the computable functions before). So, again, I can understand why one would continue to connect GIT to such matters of computability, given the seminal historical connection.].

But the final link that now somehow gets emphasized so much, that such systems of finite set theory can furthermore be interpreted within PA (and even Robinson Arithmetic) with devious enough coding, so that whenever one hears GIT1 mentioned, it is always with the refrain “for systems as strong as Peano Arithmetic”, “for systems as strong as Peano Arithmetic”, “for systems as strong as Peano Arithmetic”!. Well, this last part is a parlor trick of vanishing significance, an utter hack, analogous to an amusing programming accomplishment which may deserve an “Ooh, that’s a clever trick”, but doesn’t belong in any kind of code meant to be read and maintained. Even Goedel barely cared about it and only mentions the possibility at the very last minute, tossed-off in a brief digression into number theory near the end of the 1931 paper; in fact, his focus throughout the paper is actually on a system far stronger than PA, and even beyond first-order logic itself (specifically, the typed higher-order logic of Principia Mathematica, though mentions are also given to ZF, NBG, and the Peano axioms for the successor function + direct mechanisms for defining functions via simple recursion). Presenting GIT as tied at a fundamental level to this particular convoluted hack (feeding the establishment of arbitrarily long arithmetic sequences of coprimes into the Chinese Remainder Theorem to observe that finite sequences of naturals can be specified as the residues modulo some constant of some arithmetic sequence) is a little ridiculous, isn’t it? Particularly when this is detour is so often invoked even to illustrate the applicability of GIT1 to theories which can manipulate finite sequences much more directly (e.g., ZF).

Anyway, I forgot what I was going to do in the “GIT is not about arithmetic!” rant I was originally planning, but I’ve probably covered most of it here anyway.

1: In fact, in its original formulation, this is all GIT1 tells us, that this one very particular theory is very complex; it wasn’t till five years later that Rosser generalized GIT1 to the now familiar result concerning arbitrary (possibly consistent but false) extensions of PA
2: As an example of how things which were still being discovered and inobvious at the time are now immediate and mundane, the result of Rosser’s which took five years to see (like I said, a lot happened in 1936) was essentially nothing beyond the realization that computer programs can be computably simulated in parallel (so that if two ), though he did not cast it in these terms and it was also not clear at the time that this was all it amounted to.

Missing words reinstated in bold, though I suspect not too many eyes would persist all the way to that footnote anyway

Incidentally, I might as well give the (presumably, for some people, much clearer) very quick and easy proof of the variant of GIT1 for the “ordinary” case where one’s concern is only with computably enumerable true theories:

Theorem: No theory can be complete, computably enumerable, prove only true things, and set in a language into which statements of the form “Program P eventually halts” can be computably translated under some scheme
Proof: If a theory is complete and proves only true things, then in fact it proves all and only the true statements in its language. If such a theory (of course, by the previous line, there’s basically just one unique such theory for any given language) is furthermore computably enumerable, then it is in fact computably decidable. But the halting problem is famously undecidable, and thus the final condition above is incompatible with the combination of the previous ones.

In case one is particularly keen to relate to this to arithmetic, then, of course, the required lemma is that, as it happens, there is a computable scheme by which statements of the form “Program P eventually halts” can be translated into equivalent statements in the language of natural number addition and multiplication (indeed, even in the very restricted Sigma_1 portion of it), establishing that any true, computably enumerable theory dealing with said language must be incomplete.

Just posting to say that I really appreciate the work you put in here, Indistinguishable.

As for the over-stressed connection of Gödel’s results with arithmetic, it’s probably just a result of over-enthusiastic popularizers: arithmetic and natural numbers are something most people know (or think they do, at any rate), so pointing out the applicability to those concepts may serve to dispel ‘that’s all well and good, but what does it mean for me?’-objections. While a more general presentation is more powerful, it’s also more abstract, and most popular accounts of Gödelian incompleteness aim to get the impact they had on mathematical reasoning in general across, which probably works best when concentrating on some part of mathematics one can assume everybody to have a general familiarity with.

Don’t be so quick. First he has to be correct.

These two statements are at best misleading, and at worst contradictory.
Yes, there is only provable/unprovable within a given system. So… when you remove axioms from the system you reduce the number of statements that can be made.It doesn’t automatically mean that statements that were provable before are unprovable now. Because as you said in the first place provable/unprovable only make sense within the given system. If by removing axioms, you can no longer make the statement, provable/unprovable doesn’t apply.

which is why this statement about incomplete is ludicrous…

The Field axioms do not speak of 2. 2 does not exist until it’s defined by an axiom. The Field axioms by themselves create a complete system consisting of the set S={0,1} and the operators {+,}. And from the axioms alone it is possible to completely fill in the truth table for this system. You can’t ask the question "is there an x in the set S such that xx=2?"

We’ve had this conversation before, (all three of us, actually; me, indistinguishable, and half man half wit,) so I can anticipate where it’s going…
You previously suggested taking a larger system that included 2, and strip it down to the Field axioms while leaving 2 in the language so we could ask the question above… It’s strange that you’ve since forgotten that you needed to do that to be able to ask the question about the square root of 2.

I previously denied that that was allowed. Not going to do that again, since I know the mistake I made previously… I knew three things…
1: You said that holding 2 in the language made the questions about 2 unprovable.
2: Mathematicians do not use the language and axioms like this.
3: Mathematicians believe that Godel’s theorems imply more than you claim they do.

From this I deduced that holding a symbol which you have stripped out of the axioms was not legal. I’m sorry, I was wrong… Guess where I was wrong.
I assumed that [sub]edit/sub was true, that you had actually done the analysis and shown that the system was incomplete. So, when I realized that, the first thing I did was see what was provable when you asked questions about 2 using only the Field axioms, (obviously keeping 2 in the language.) Ok, that wasn’t the first thing I did way back then when we first had this conversation. First, I sulked and said “oh, woe is me. How could I have been so wrong. Is my whole mathematical world view a lie?” Then I did what anyone who comes to believe a new position should do; what anyone who holds that belief should have done in the first place. Guess which I spent more time on: sulking, or the analysis? I spent 2 hours with a knot in my stomach wondering if my whole world view was wrong. 10 minutes into the analysis that went away and I was sure I wasn’t going to have to make the announcement that every mathematician in the world was wrong; and in another 10 I had proved it. Once you put 2 into the language, (or hold it there while stripping every axiom back to the field axioms: [the two are equivalent,]) every question you can ask about 2 from the field axioms is decidable.

e.g. Is there an x in S such that xx=2? No, it’s false. 2 is not in S. xx is. Every question such as “is x+2 an element in S?” is decidable. It’s not an element in S. Neither is x*2. (for all x in S in both cases.)

The fact that you can form a different field where 2 is defined and x*x=2 is true holds absolutely no bearing on the system we’re currently dealing with; as you yourself said:

Yes, mathematicians have always dealt with incompleteness, and it’s often not too difficult to complete a system either. But with anything much more complex than Presburger arithmatic, it always came up inconsistent as well. But it wasn’t until Godel’s theorems that it was known that that would always be the case.

Now, personally I think it would be wonderful to know if there was a set with cardinality between the integers and the reals. That would be really interesting. Inside the system of ZFC it either is or isn’t possible to create that set. And yet, ZFC can never tell us which it is.

I’m no expert, ch4rl3s, but I think the mistake you’re making is a simple, conceptual one – you confuse the axioms of a system with some model that implements them. Take Indistinguishable’s earlier example:

Both the rational and the natural numbers obey the stated axioms; within the rational numbers, it’s easy to find X such that X + X = 1, and within the natural numbers, it’s impossible. So, obviously, the question of whether or not there exists such an X is undecidable from the axioms; else, that X ought to either exist or not exist in both number systems – in both models.

The same now goes for the field axioms and the question of whether or not there’s a square root of 2. Take the rational and real numbers: both, under the usual definitions of addition and multiplication, are fields, and obey the field axioms. Both contain the element ‘2’, and in both it is possible to define the notion of the square root. Yet, only within the reals does that square root exist – so we have two mathematical structures obeying the field axioms that differ on whether or not there is a square root of 2; hence, the question of whether there exists a square root of 2 is not decidable from the field axioms.

Of course, you can construct fields that don’t contain the element ‘2’ at all, which then trivially don’t contain a square root of 2, but that doesn’t mean it’s necessarily an invalid question (as exemplified by the fact that in some models of the field axioms, it’s not only poseable, but even answerable). Besides, you can ask the question in the language the field axioms are in – English (with some formalisation, perhaps), for instance, or the language of first order logic, so why wouldn’t it be valid?

And please, spare us your facetious ‘oh, woe is me!’-adages. They’re really tiresome to read.

So the argument is this, right?

A model satisfies the field axioms when consistently substituting objects from the model for expressions in the field axioms and all statements derivable from the field axioms yields only true statements about the model.

The real numbers are a model satisfying the field axioms.

The rational numbers are a model satisfying the field axioms.

Among the real numbers, 2 has a square root.

Among the rational numbers, 2 doesn’t have a square root.

So there’s a model satisfying the field axioms under which 2 has a square root.

And there’s a model satisfying the field axioms under which 2 doesn’t have a square root.

So the field axioms don’t decide whether 2 has a square root.

If that’s the argument, I do have a question about it. (I’ve had a modal logic course and a set theory course, but my metalogic is very spotty as it was mostly picked up informally here and there rather than through formal coursework.) The thing that’s undecidable is supposed to be a statement in the symbol system it’s undecidable under. But if we’re saying the field axioms don’t decide whether 2 has a square root, and if 2 is just an object in a model that satisfies those axioms, then if 2 is “represented” by different expressions in those axioms (and statements derived from them) under two different models, then is there really a single statement in that axiom system that we’re licensed to call “undecidable”? Is 2 “represented” by different expressions when the two models are applied to the axioms? (In other words, are 2-the-real-number and 2-the-rational-number really the same thing when each is considered as an object in a model satisfying the field axioms?)

It is entirely possible that there’s some specific information (for example, what exactly the field axioms are) that I’m missing that would make the matter clear to me. So feel free to talk to me like an idiot. :wink:

I’d say that 2 is defined within the natural numbers, which are a subset of both the rational and real numbers, so you don’t really have ‘2-the-rational-number’ and ‘2-the-real-number’, but just ‘2-the-natural-number’ embedded within the context of the reals or rationals; or at least, that’s how it seems to me.

Regardless, I think the salient point is the following:

  1. A set of axioms is complete if, for any statement in the axioms’ language, it either proves the statement or its negation;

  2. The field axioms are written in the language of first order logic;

  3. The question of whether or not there is a square root of 2 – or the statement that there is a square root of 2 – is written in the language of first order logic;

  4. The field axioms neither prove nor disprove that statement (as is exemplified by the fact that there are models that satisfy these axioms, yet give different answers to the question);

  5. Hence, the field axioms are incomplete (in a completely ordinary, non-Gödelian way), and the statement ‘2 has a square root’ is undecidable from them.

I’m taking “2” to be an abbreviation for the expression “1 + 1”, which is an expression within the language of the field axioms. In case you’d like to know what the field axioms are, one way of putting them is that they take place in a language with terms “0” and “1”, and binary function symbols “+” and “*”, and assert that:

[li]+ and * are both associative and commutative, with 0 and 1, respectively, as identity elements for them[/li][li]* distributes over + (in the sense that x * (y + z) always equals x * y + x * z)[/li][li]Every object has an inverse with respect to +[/li][li]An object has an inverse with respect to * if and only if it is not equal to 0[/li][/ul]

One first-order statement in this language is the statement “There exists an x such that x * x = 1 + 1”. This statement is neither provable nor disprovable from the above axioms for the reasons above. That is incompleteness.