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”.
[ul]
[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]