Wednesday, December 31, 2014

Almost all integers contain the digit 3

This is my last chance to blog this year. However, I did not get back into the proof of Gödel's incompleteness theorem yet. So instead, this post is motivated by this Numberphile video, which explains why almost all integers contain the digit 3. More precisely, the percentage of integers that contain at least one occurrence of the digit '3' in the set $$\mathbb{N}_u = \{0,1,2,3,\cdots,u-1\}$$ goes to 100% as the upper bound $$u$$ goes to infinity.

We are going to attack this problem with two different approaches. First, we'll use a recurrence relation approach. Second, we'll go over the combinatorial proof discussed in the video. Finally, we'll check that the two approaches do give the same answer.

In both approaches, we will use values of $$u$$ that are powers of 10. So if $$u = 10^n$$, for $$n \in \mathbb{N}^+$$, then the set under consideration $$\mathbb{N}_{10^n}$$, which we denote $$A_n$$, is the set of all of the (non-negative) integers containing at most $$n$$ digits.

Recurrence relation approach

In this approach, we use $$S_n$$, for $$n \in \mathbb{N}^+$$, to denote the subset of $$A_n$$ of all of the integers that contain at least one occurrence of the digit '3' and we use $$T_n$$ to denote $$|S_n|$$, the cardinality of $$S_n$$.
• Since $$A_1=\{0,1,2,3,4,5,6,7,8,9\}$$, $$S_1=\{3\}$$ and $$T_1=1$$.
• Since $$A_2=\{0,1,2,3,4,\cdots,98,99\}$$, $$S_2=\{ 3,13,23,30,31,32,33,34,\cdots,39,43,53,63,73,83,93\}$$$$=\{ 3,13,23,43,53,63,73,83,93\}$$$$\cup \{30,31,32,33,34,\cdots,39\}$$. In other words, we can split the set $$S_2$$ into two subsets, one whose elements all start with the digit '3'  (there are exactly 10 such integers), and the other one whose elements do not start with the digit '3' (there are exactly $$9\cdot T_1$$ of those, since if the first digit is not '3' then the least significant digit must belong to $$S_1$$). Thus, $$T_2 = 10 + 9\cdot T_1 = 10 + 9 = 19$$.
• Similarly, since $$A_3=\{0,1,2,3,4,\cdots,998,999\}$$, $$S_3$$ is the union of two sets,  one whose elements all start with the digit '3'  (there are exactly $$10^2$$ such integers), and the other one whose elements do not start with the digit '3' (there are exactly $$9\cdot T_2$$ of those, since if the most significant digit is not '3' then the number formed by the other digits must belong to $$S_2$$). Thus, $$T_3 = 10^2 + 9\cdot T_2= 100 + 9\cdot 19 = 271$$.
• Since this reasoning clearly generalizes to all values of $$n \in \mathbb{N}^+$$, we obtain the following recurrence relation:
$\left\{ \begin{array}{ll} T_1 = 1 & \\ T_n = 10^{n-1} + 9T_{n-1} & \text{if}\ n>1 \end{array} \right.$ Now, let's solve this recurrence relation by iteration to get a closed-form formula for $$T_n$$:

$$\begin{array}{l@{0pt}l} T_1 & = 1\\ T_2 = 10^1 + 9T_1 & = 10+9 \\ T_3 = 10^2 + 9T_2 & = 10^2+9(10+9) \\ & = 10^2 + 9\cdot 10 + 9^2 \\ T_4 = 10^3 + 9T_3 & = 10^3+9(10^2 + 9\cdot 10 + 9^2) \\ & = 10^3+9\cdot 10^2 + 9^2 \cdot 10 + 9^3\\ T_5 = 10^4 + 9T_4 & = 10^4+9(10^3+9\cdot 10^2 + 9^2 \cdot 10 + 9^3)\\ & = 10^4+9\cdot 10^3+9^2\cdot 10^2 + 9^3 \cdot 10 + 9^4\\ \cdots &\\ T_n = 10^{n-1} + 9T_{n-1} & = 10^{n-1}+9\cdot 10^{n-2}+9^2\cdot 10^{n-3} + \cdots + 9^{n-2}\cdot 10^1 + 9^{n-1}\\ \end{array}$$

In conclusion, $$\displaystyle T_n = \sum_{i=0}^{n-1} \left( 9^{n-i-1}\cdot 10^i\right)$$ for $$n \in \mathbb{N}^+$$

Since this formula is rather ugly, let's turn to the combinatorial approach discussed in the Numberphile video.

Combinatorial approach

It is easy to determine the total number of integers with exactly $$n$$ digits without having to enumerate them, namely $$10 \times 10 \times \cdots \times 10 = 10^n$$,  since there are exactly 10 digits to choose from for each position in the $$n$$-digit number. Note that this count actually includes all of the numbers with leading zeros, such as 01 and 00023, which are identical to 1 and 23, respectively. In other words, what we really have is  $$\left|A_n\right|= 10^n$$.

Similarly, we can compute the total number of integers with at most $$n$$ digits that do not contain the digit '3', namely $$9 \times 9 \times \cdots \times 9 = 9^n$$, since there are now only 9 digits to choose from at each position in the integer.

In conclusion, $$T_n = 10^n -9^n$$.

This is both a much nicer and easier-to-derive closed-form formula than the one we obtained with the recurrence relation approach. But are the two formulas equal?

Let's check our work

Let $$P(n)$$, for $$n \in \mathbb{N}^+$$, denote: $$\displaystyle \sum_{i=0}^{n-1} \left( 9^{n-i-1}\cdot 10^i\right) = 10^n - 9^n$$

We now prove by mathematical induction that $$P(n)$$ holds for  $$n \in \mathbb{N}^+.$$

Basis:
•  $$\displaystyle \sum_{i=0}^{1-1} \left( 9^{1-i-1}\cdot 10^i\right) = \sum_{i=0}^{0} \left( 9^{1-i-1}\cdot 10^i\right) = 9^{1-0-1}\cdot 10^0 = 9^0 \cdot 10^0 =1$$
• $$10^1 - 9^1 = 10 - 9 = 1$$
• Therefore $$P(1)$$ holds
Inductive step:
• Assume that $$P(n)$$ holds for any $$n \in \mathbb{N}^+$$, that is: $\sum_{i=0}^{n-1} \left( 9^{n-i-1}\cdot 10^i\right) = 10^n - 9^n \quad \text{[inductive hypothesis]}$
• Let's compute the left-hand side of $$P(n+1)$$:
$\begin{array}{l@{0pt}l} \sum_{i=0}^{n} \left( 9^{n-i}\cdot 10^i\right) & = 9\left(\frac{1}{9}\sum_{i=0}^{n} \left( 9^{n-i}\cdot 10^i\right)\right)\\ & = 9\left(\sum_{i=0}^{n} \left( 9^{n-i-1}\cdot 10^i\right)\right)\\ & = 9\left(\sum_{i=0}^{n-1} \left( 9^{n-i-1}\cdot 10^i\right) + \sum_{i=n}^{n} \left( 9^{n-i-1}\cdot 10^i\right) \right)\\ & = 9\left(\sum_{i=0}^{n-1} \left( 9^{n-i-1}\cdot 10^i\right) + \left( 9^{n-n-1}\cdot 10^n\right) \right)\\ & = 9\left(\sum_{i=0}^{n-1} \left( 9^{n-i-1}\cdot 10^i\right) + \frac{10^n}{9} \right)\\ & = 9\left( \left(10^n - 9^n\right) + \frac{10^n}{9} \right) \quad \text{by the inductive hypothesis} \\ & = 9\cdot 10^n - 9\cdot 9^n + 10^n\\ & = 10\cdot 10^n - 9\cdot 9^n\\ & = 10^{n+1} - 9^{n+1}\\ \end{array}$
• Therefore $$P(n+1)$$ holds.

Main result

We are now in a position to prove our main result, namely that the percentage of integers that contain the digit '3' in the set $$A_n$$  goes to 100% as $$n$$ goes to infinity. This percentage is equal to
$$100\times\frac{T_n}{\left|A_n\right|}=100\times\left(\frac{10^n-9^n}{10^n}\right)=100\times\left(1-\frac{9^n}{10^n}\right)= 100 - 100\left(\frac{9}{10}\right)^n$$.
And this percentage goes to 100% as $$n$$ goes to infinity, since $$\displaystyle \lim_{n \to \infty}\left( \frac{9}{10}\right)^n = 0$$.

Discussion

Of course, all of the proofs above still hold if we had picked the digit '8' (say) instead of the digit '3'. In other words, it is also true that almost all integers contain the digit '8'. So, if we use $$E_n$$ to denote the cardinality of the subset of $$A_n$$ of all of the integers that contain at least one occurrence of the digit '8', $$E_n = 10^n-9^n$$. Similarly for the digit '5' (say): $$F_n = 10^n-9^n$$.

But, if both $$100\times\frac{T_n}{\left|A_n\right|}$$ and  $$100\times\frac{E_n}{\left|A_n\right|}$$ go to 100% as $$n$$ goes to infinity, the sum of these two percentages will eventually exceed 100%! That is true. However, this sum double counts all of the integers that contain both the digit '3' and the digit '8'. The correct percentage of such integers is $$100\times\frac{10^n-8^n}{10^n}$$, which also goes to 100% as $$n$$ goes to infinity.

So there is no paradox here. When $$n$$ gets large enough, almost all of the integers will contain all of the digits 0 through 9. Note that all of these results are asymptotic. Indeed, it takes relatively large values of $$n$$ for these percentages to get anywhere close to 100%. For example, for the percentage of integers that contain the digit '3' to reach 90%, 95%, 99% and 99.99%, the number $$n$$ of digits in the integer must be larger than 21, 28, 43 and 87, respectively.

Tuesday, July 9, 2013

Robinson Arithmetic is Σ1-complete

Recall that Q (i.e., Robinson Arithmetic) is an axiomatized formal theory (AFT) of arithmetic couched in the interpreted formal language LA. Let L be a subset of LA and let T be some AFT of arithmetic.

We say that T is L-sound iff, for any sentence φ in L, if T ⊢ φ, then φ is true.

We say that T is L-complete iff, for any sentence φ in L, if φ is true, then T ⊢ φ.

In chapter 9, Peter Smith defines a subset of LA, called Σ1. Then, using the fact that Q is order-adequate, he proves that Q is Σ1-complete. This is important because the well-formed formulas (wff's) of Σcan express the decidable numerical properties and relations, and therefore Q will be sufficiently strong. Now to the details...

First, let's define a few interesting subsets of LA:

Sunday, July 7, 2013

In chapter 9, Peter Smith defines the following concept: A theory T that captures the relation ≤ is order-adequate if it satisfies the following nine properties:
• O1: T ⊢ ∀x (0 ≤ x)
• O2: For any n, T ⊢ ∀x ((x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n) → x ≤ n)
• O3: For any n, T ⊢ ∀x (x ≤ n → (x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n))
• O4: For any n, if T ⊢ φ(0) and T ⊢ φ(1) and ... and T ⊢ φ(n) then T ⊢ (∀x ≤ n)φ(x)
• O5: For any n, if T ⊢ φ(0) or T ⊢ φ(1) or ... or T ⊢ φ(n) then T ⊢ (∃x ≤ n)φ(x)
• O6: For any n, T ⊢ ∀x (x ≤ n → x ≤ Sn)
• O7: For any n, T ⊢ ∀x (n ≤ x  → (n = x  ∨ Sn ≤ x))
• O8: For any n, T ⊢ ∀x (x ≤ n ∨ n ≤ x)
• O9: For any n>0, T ⊢ (∀x ≤ n-1)φ(x) → (∀x ≤ n)(x ≠ n → φ(x))
Then, we have the following theorem:

Wednesday, July 3, 2013

Robinson Arithmetic captures the "less-than-or-equal-to" relation

In this post, we'll start discussing the material in Chapter 9 of Peter Smith's book, namely up to section 9.3.

Before proceeding, review the definition of Robinson Arithmetic (denoted Q) as well as what it means for a theory to capture a numerical relation.

Now, we'll show that Robinson Arithmetic captures the ≤ numerical relation with the open well-formed formula: ∃x (x + m = n).

In other words, we are going to prove the following two-part theorem:
Theorem: If m and n are natural numbers, then:
1. If m ≤ n, then Q ⊢ ∃x (x + m = n)
2. If m > n, then Q ⊢ ¬ ∃x (x + m = n)
Recall that if m and n are natural numbers, then m and n are the numerical terms representing m and n, respectively, in the formal theory.

Proof sketch of part 1:

Sunday, June 30, 2013

Q - Robinson Arithmetic

Now that we are familiar with Baby Arithmetic (BA), we can make its language more expressive by allowing variables and quantifiers back into its logical vocabulary. When we do this, we simply obtain the interpreted language LA, that was described earlier.

Since we now have variables and quantifiers, we can replace the schemata of BA with regular axioms (see below). The resulting formal system of arithmetic is called Robinson Arithmetic and is often denoted by the letter Q, as described in Chapter 8 of Peter Smith's book. Here is his definition of Q:

Friday, June 28, 2013

Baby arithmetic

Since chapter 7 in Peter Smith's book is so short, I'll summarize it quickly and then start discussing chapter 8.

Chapter 7 starts by comparing the two incompleteness theorems discussed in previous chapters (let's call these "Smith's theorems") to Gödel's first incompleteness theorem as follows:

Thursday, June 27, 2013

Consistent, sufficiently strong formal systems of arithmetic are incomplete

In Chapter 6, Peter Smith proves another incompleteness theorem. To place this theorem in context, let's review some definitions about axiomatized formal theories (or AFTs) from earlier posts.

Let T be some AFT.
• T is consistent iff (if and only if) there is no sentence φ such that T proves both φ and ¬ φ.
• T is sound iff every theorem that T proves is true according to the interpretation that is built into T's language.
• T is (negation-)complete iff for every sentence φ in T's language, T proves either φ or ¬ φ.
• T is decidable iff there is an algorithm that, given any sentence φ in T's language, determines whether or not T proves φ.
• If needed, go here to review what it means for T's language to express a numerical property P or a numerical relation R.
• If needed, go here to review what it means for T to capture a numerical property P or a numerical relation R.
• If needed, go here to review what it means for T's language to be sufficiently expressive.

We'll use the following abbreviations:

Monday, June 24, 2013

Sound formal systems with sufficiently expressive languages are incomplete

In chapter 5, Peter Smith uses a counting argument to prove that sound axiomatized formal theories (AFTs) that can express a good amount of arithmetic are incomplete. In short: since their set of theorems is effectively enumerable but their set of true sentences is not, the two sets must be different. In a sound theory, the theorems are all true. Therefore, some truths must remained unproved in such theories.

Let's start with a definition. The language of an AFT of arithmetic is sufficiently expressive if and only if:
1. It can express quantification over numbers, and
2. It can express every effectively decidable two-place numerical relation.
Now, to the pivotal theorem of this chapter:

Sunday, June 23, 2013

An enumerable but not effectively enumerable set

Let's focus on the first half of chapter 5 in Peter Smith's book. First, Smith describes a new characterization of effectively enumerable sets. Second, Smith gives an example of a set of integers that is not effectively enumerable.

Let's define the numerical domain of an algorithm as the set of natural numbers with the following property: when the algorithm takes one of these numbers as input, it terminates and returns a result. Every algorithm has a numerical domain. If the input to some algorithm is not a single natural number, then the numerical domain of this algorithm is the empty set. Otherwise, the numerical domain is the set of those natural numbers on which the algorithm does not crash and does not go into an infinite loop.

It turns out that each numerical domain is effectively enumerable. In fact, the converse is also true, according to the following theorem:

Saturday, June 22, 2013

Capturing numerical properties in a formal language of arithmetic

Peter Smith starts Chapter 4 by describing LA, a formal language that is at the core of several AFTs (axiomatized formal theories) of arithmetic. Then Smith explains what it means for a formal language of arithmetic to "express" a numerical property and the stronger notion of "capturing" a numerical property.

Here is the definition of LA:

Friday, June 21, 2013

Formal systems or axiomatized formal theories

In chapter 3, Peter Smith defines formal systems or, as he calls them, axiomatized formal theories (I will use AFT as an abbreviation for this phrase).

A theory T is an AFT if...

Wednesday, June 19, 2013

Effective computability, decidability and enumerability

In Chapter 2, Smith covers familiar ground. So this post will be short. Here is a quick summary, section by section.

Section 1 reviews terminology pertaining to functions, namely the notions of domain and range, as well as special cases of functions, namely injective (or one-to-one) functions, surjective (or onto) functions and bijective functions (or one-to-one correspondences).

Tuesday, June 18, 2013

Peter Smith's overview of Gödel's incompleteness theorems

Finally! As was my initial goal, I now turn my attention to Peter Smith's book on the proof of Gödel's incompleteness theorems (by the way, I own the first edition of his book; so that is the one I will be referring to). I did not expect to spend that much time on Nagel and Newman's book. But it was worthwhile in getting the big picture.

Chapter 1 is an introductory and user-friendly discussion of topics that were mentioned in earlier posts, such as basic arithmetic, formal systems, (in)completeness, consistency, the statement of Gödel's incompleteness theorems and some of their implications. Therefore, in this post, I will just highlight the points where Smith provides new information or has a different perspective.

Monday, June 17, 2013

Proof sketch of Gödel's incompleteness theorems

In this post, I will follow the outline of the proof given in Section VII of Nagel and Newman's book. Recall that:
• a formal system F is consistent if there is no well-formed formula (wff) w such that F proves both w and ¬ w, and
• a formal system is (semantically) complete if it can prove all of the true wff's that it can express.
Now, Gödel's first incompleteness theorem can be paraphrased as:
Any consistent formal system that is expressive enough to model arithmetic is both incomplete and "incompletable."
and Gödel's second incompleteness theorem can be paraphrased as:
Any consistent formal system that is expressive enough to model arithmetic cannot prove its own consistency.
According to Nagel and Newman, a proof of the first theorem can be sketched in 4 steps:

Friday, June 7, 2013

Mappings and the arithmetization of meta-mathematics

In an earlier post, we discussed mappings in general and then described Gödel numbering, which is a mapping between the set of well-formed formulas (wff's) in a formal system and the set of positive integers.

In part B of section VII, Nagel and Newman describe a more interesting mapping used in Gödel's proof. In this mapping, the domain is the set of meta-mathematical statements about structural properties of wff's, while the co-domain is the set of wff's. This post describes how this mapping enabled Gödel to arithmetize meta-mathematics.

Thursday, June 6, 2013

Mappings and Gödel numbering

Section VI of Nagel and Newman's book describes mappings. A mapping is an operation that applies to two sets called the domain and the co-domain. More specifically, a mapping associates to each element of the domain one or more elements of the co-domain.

Tuesday, May 28, 2013

Absolute proof of consistency of FSN

In section IV of their great little book, Nagel and Newman discuss efforts by Gottlob Frege and then Bertrand Russell to reduce arithmetic to logic. This is clearly another attempt at a relative proof of consistency: if this reduction were successful, then arithmetic would be consistent provided logic is consistent.

Whether this latter statement is true or not, Whitehead and Russell's Principia Mathematica was a landmark achievement: it almost completed the first step in an absolute proof of consistency of arithmetic, since it led to the formalization of an axiomatic system for arithmetic.

In section V, Nagel and Newman describe a formalization of propositional (or sentential) logic, that is, a subset of the logic system in Principia Mathematica (but not a large enough subset to represent arithmetic). The bulk of this section first describes the formalization process, which yields the standard syntax and inference rules of propositional logic (including modus ponens) and then outlines an absolute proof of consistency of this formalized axiomatic system.

This absolute proof of consistency is a proof by contrapositive, which relies on the following true conditional statement:

Sunday, May 26, 2013

Absolute proofs of consistency and meta-mathematics

In earlier posts, we explained why consistency is an important property of axiomatic systems and discussed relative proofs of consistency, in which the proof of consistency of a system is based on the assumption that another axiomatic system is consistent. In this post, we introduce absolute proofs of consistency that do not make any assumptions about any other axiomatic system. Apparently, David Hilbert was the first to study and propose such proofs, according to Nagel and Newman's book (Section III, page 26).

Recall that an axiomatic system is consistent if it cannot derive both a theorem and its negation. What do we mean by the negation of a theorem? Let's take, as a simple example, the theorem: "6 is divisible by 3." Its negation is simply the following statement: "6 is not divisible by 3" or equivalently "It is not the case that 6 is divisible by 3." This second formulation of the negation, although less elegant in English, is preferable because the negation is added to the front of the original theorem. In a formal system, negation is handled by simply adding a symbol for the phrase "it is not the case that." Several symbols have been used for negation, such as ~ and ¬ . We'll use the latter here. So, if T is any theorem in some formal system, then the formula  ¬T is the negation of T.

Remember that our formal system FS did not have a symbol for negation. So we will extend FS into a new formal system called FSN (for FS with Negation), whose alphabet is { E, 0, 1, ¬ }. FSN has exactly one axiom, namely the same as A1 in FSFSN also has the same inference rules as FS, namely IR1 and IR2. But it has one additional inference rule that uses negation. Here is the full description of FSN:

Wednesday, May 22, 2013

Relative proofs of consistency

In the last post, we defined and explained the importance of the property of consistency for an axiomatic system. The second half of Section II in Nagel and Newman's book describes ways of proving that an axiomatic system is consistent.

But first, note that the question of consistency of Euclidean geometry did not arise. Its axioms were supposed to describe the real world; and something that actually exists cannot be self-contradictory. In other words, existence (or truth) implies internal consistency.

The need for consistency proofs arose much later, with non-Euclidean geometries, which do not obviously model space as we experience it. Non-existence does not imply inconsistency. But any interesting abstract construct had better be internally consistent.

Second, checking the internal consistency of all of the theorems produced so far is typically not a valid proof of consistency, because (interesting) axiomatic systems generate an infinite number of theorems. The proof of consistency must guarantee that not a single theorem, including some that we have not yet produced and that we might never produce, contradicts any other theorem in the system.

One possible way to prove the consistency of an axiomatic system is model-based, where a model is a kind of interpretation.

Monday, May 20, 2013

Consistency of axiomatic systems

The "problem of consistency" is the topic of Section II of Nagel and Newman's book.  This section defines "consistency" and explains when and why it became an important property of axiomatic systems.

The oldest and most famous axiomatic system is that of Euclid, in which he systematized all of the knowledge of geometry (and more) available to him over two thousand years ago. Based on five axioms, Euclid was able to rigorously prove a very large number of known and new theorems (called "propositions" in his Elements). His axioms were supposed to be intuitively true. The first four axioms dealt with line segments, lines, circles and angles (see this Wikipedia entry) and have been viewed as self-evident. In contrast, the fifth axiom, which was equivalent to the following statement: "Through a point outside a given line, only one parallel to the line can be drawn" (page 9), was not intuitively true (apparently because the two lines involved extend to infinity in two directions, similarly to asymptotes).

Since this proposed axiom was not obviously true, many mathematicians tried to prove that it logically follows from the first four axioms. Only in the nineteenth century was it demonstrated that it is NOT possible to prove the parallel axiom from the first four axioms.

This proof that it is impossible to prove a given statement is a great precursor of Gödel's incompleteness theorems.

Friday, May 17, 2013

Formal systems, axioms, inference rules, formal proofs

I'll start this post by describing a simple formal system that I made up.

formal system is comprised of axioms and inference rules. Each axiom and inference rule is defined syntactically, that is, by ordered sequences of symbols that follow strict syntactic rules but do not (necessarily) have any meaning. The set of all symbols allowed in a formal system are explicitly listed in its alphabet, simply, a finite, non-empty set of symbols.

My formal system, let's call it FS,  uses the alphabet {E,0,1} and has only one axiom and two inference rules. Here is the axiom (in the box below):

Wednesday, May 15, 2013

Let's get started with Nagel and Newman (Section I)

Let's ease our way into this. I haven't read the Nagel and Newman book in a few years. But I remember it as a short and highly readable overview of the proof. I have a 1986 softcover edition by NYP Press. Today, I want to write about Section I - Introduction. It's really short: under 5 pages.

First, a short quote that makes me feel better about my past failures at REALLY understanding the proof of GIT:

Tuesday, May 14, 2013

I just want to understand the proof of Gödel's incompleteness theorems

So this is it! Summer 2013... This is when I get to master the proof of Gödel's incompleteness theorems (thereafter: GIT).

I discovered GIT as an undergraduate student in one of my Artificial Intelligence courses. My instructor was reading Gödel, Escher, Bach and was raving about the book. He even took some of our exam problems from it. But what I remember most is the outline of the proof of GIT, more precisely the first theorem. To be honest, the only part of it that stuck with me was the idea of numbering the formulas. Of course, at the time, I bought a copy of the book. I liked many parts of it but I never finished it.

Years later, while I was teaching computability theory and other computer science topics, I encountered GIT several times. At some point, I decided I wanted to understand the proof of GIT.

First, I read the classic "Gödel's Proof" by Nagel and Newman. That is a concise and user-friendly overview of the proof. But it was only a proof sketch. So I looked at some textbooks on formal logic, which were neither concise nor user-friendly. I still did not understand the proof.

Finally, a couple of years ago, I came across a promising volume: "Introduction to Gödel’s Theorems" by Peter Smith. I read the first few chapters but then ran out of time (and motivation) to finish it. The following year, I made another attempt: I had to start from scratch and did not get any farther into it the second time around...