The Ubiquity of Diagonal Argument Beyond Cantor, Turing, Church, and G?del

While the diagonal argument is most famously associated with pioneering works by Cantor, Turing, Church, and G?del, its utility extends far beyond these seminal contributions. A core aspect of the diagonal argument can be seen in a surprising variety of contexts, including key proofs in real analysis and even in the verification of complex computational behaviors. This article explores the application of diagonalization in real analysis, particularly in the proof of the Arzela-Ascoli theorem, and in a novel approach to the study of machine behavior in concurrency theory.

Diagonalization in Real Analysis: The Proof of the Arzela-Ascoli Theorem

Diagonalization plays a crucial role in proving several fundamental results in mathematical analysis, and the proof of the Arzela-Ascoli Theorem is a prime example. The theorem concerns the compactness of equicontinuous and uniformly bounded families of real-valued functions defined on a compact metric space.

Statement of the Lemma

Given a sequence of functions ( f_n: X rightarrow mathbb{R} ) on a metric space ( X ) that is pointwise bounded, meaning for every ( x in X ) the set ( { f_n(x) : n in mathbb{N} } ) is bounded, and a countable subset ( E subseteq X ), there exists a subsequence ( g_n ) of ( f_n ) that converges pointwise on ( E ).

Proof

Using the Bolzano-Weierstrass Theorem, which states that every bounded sequence of real numbers has a convergent subsequence, we can start by considering each point ( x_1 ) in ( E ). We find a subsequence ( f_{1k} ) of ( f_n ) that converges at ( x_1 ). For the next point ( x_2 ), we can extract a subsequence ( f_{2k} ) of ( f_{1k} ) that converges at ( x_2 ) and ( x_1 ). We continue this process for any finite collection of points ( x_1, x_2, dots, x_m ) in ( E ). However, to ensure convergence for all points in ( E ) simultaneously, we utilize diagonalization.

We count the elements of ( E ) as ( x_1, x_2, dots ) and define a new sequence ( g_n f_{nn} ). By construction, for any ( x_m ), the subsequence ( g_{nn} ) must converge on ( x_m ) because for ( n geq m ), ( g_n ) is part of the subsequence ( f_{mk} ) that converges at ( x_m ). Therefore, ( g_n ) converges pointwise on all of ( E ), proving the lemma.

Diagonalization in the Context of Machine Behavior

The diagonal argument also finds application in verifying the consistency of computational models, particularly in the study of machine behavior in concurrent systems. In my Ph.D. thesis, the diagonal argument was instrumental in demonstrating that certain machines with store buffers can be made to behave like machines without store buffers when threads are properly stepped.

Context and Application

The infinite sequences in my work correspond to different orders of steps taken by threads in a concurrent system. Each sequence, denoted as ( mathbf{s}_n ), represents a possible execution order of the threads until a certain point ( n ), after which a growing prefix remains unchanged. For instance, ( mathbf{s}_n ) maintains the same initial steps as ( mathbf{s}_{n-1} ) for all ( k leq n ).

To achieve a sequence that guarantees the desired property across all possible thread orders, I defined a new sequence ( mathbf{s}_infty ) by diagonalizing over the original sequences. Specifically, ( mathbf{s}_infty_k s_{k1}^k ), where ( s_{k1}^k ) is the first step of the ( k )-th sequence when stepping to the ( k )-th position.

Ensuring the Property

The central property ( P ) in my Ph.D. context is that a machine with store buffers behaves like a machine without store buffers when threads are stepped in the given order. By diagonalizing the sequences, I ensured that the diagonal sequence ( mathbf{s}_infty ) satisfies ( P ) for all possible prefixes. This is because for any finite prefix of ( mathbf{s}_infty ), there exists a corresponding prefix in one of the original sequences that holds the same property.

Mathematically, for all ( n ), ( P(mathbf{s}_infty[0:n-1]) ) holds, where ( mathbf{s}_infty[0:n-1] ) is the prefix of ( mathbf{s}_infty ) up to the ( n )-th step. This is because ( mathbf{s}_infty[0:n-1] mathbf{s}_{nn}[0:n-1] ), and by construction, ( mathbf{s}_{nn} ) satisfies ( P ) up to the ( (n-1) )-th step.

This approach ensures that the resulting sequence ( mathbf{s}_infty ) guarantees consistent machine behavior across all possible thread stepping orders, which is a significant result in the field of concurrent systems and verification.

Conclusion

The diagonal argument, a versatile and powerful technique, finds applications in a wide range of fields, from mathematical analysis to computer science. Its ability to handle simultaneous convergence in real analysis, as seen in the Arzela-Ascoli Theorem, and its role in ensuring consistency in machine behaviors in concurrent systems, as demonstrated in my Ph.D. research, highlight the profound impact of this technique beyond its initial formulations by Cantor, Turing, Church, and G?del.