First-Order Arithmetic

The quest to build a perfect, logical foundation for mathematics led to the development of first-order arithmetic, a formal system designed to capture the essence of the natural numbers. This endeavor sought to answer a fundamental question: can the infinite world of numbers be fully described by a finite set of rules? While incredibly successful, this formalization also uncovered profound and unexpected limitations, revealing a gap between what is true and what is provable. This article explores the dual nature of this powerful system. The first chapter, "Principles and Mechanisms," delves into the axiomatic construction of Peano Arithmetic, explaining how numbers are built from basic symbols and how the principle of induction works, while also revealing the existence of bizarre non-standard models. The subsequent chapter, "Applications and Interdisciplinary Connections," examines how this formal language becomes a universal tool for describing computation and explores its deep connections to computer science, set theory, and the very philosophy of mathematical knowledge.

How do you capture the infinite, intricate dance of numbers with a finite set of rules? This was the grand ambition of mathematicians at the turn of the 20th century: to build a perfect, logical foundation for all of mathematics, starting with the simple counting numbers—the natural numbers $0, 1, 2, 3, \ldots$. The result of this quest, at least for arithmetic, is a formal system known as ​​Peano Arithmetic​​, or ​​PA​​. To understand its principles is to go on a journey to the very edge of reason, to discover not only the immense power of formal logic but also its stunning and beautiful limitations.

Imagine you are given a handful of symbolic Lego bricks and asked to build the entire universe of numbers. What is the absolute minimum you would need? First-order arithmetic gives us a surprisingly sparse toolkit. Our language, let's call it $\mathcal{L}_{PA}$, has just a few symbols: a constant for zero ($0$), a function for "what comes next" called the successor ($S$), and functions for addition ($+$) and multiplication ($\cdot$).

With this language, we lay down the rules of the game—the ​​axioms​​. They are not arbitrary; they are meticulously crafted to capture the essence of what we intuitively know about numbers.

1. ​​The Starting Point​​: We posit that there is a number $0$. But more importantly, $0$ is not the successor of any number. In our line of numbers, it's the absolute beginning; you can't take a step forward from somewhere else and land on it. This is formalized as $\forall x (S(x) \neq 0)$.

2. ​​The Unbroken Chain​​: The successor function, $S$, is our engine of creation. We define the numbers themselves as terms in this language: $1$ is just a shorthand for $S(0)$, $2$ for $S(S(0))$, and so on. We call these terms ​​numerals​​. To ensure this process creates a clean, infinite line of distinct numbers, we need another rule: if two numbers have the same successor, they must be the same number. Formally, $\forall x \forall y (S(x) = S(y) \rightarrow x=y)$. This prevents the number line from looping back on itself or having different branches merge.

3. ​​The Logic of Operations​​: How do we teach our system to add and multiply? We do it recursively, just like a child learns. For addition, we state two simple rules: adding zero to a number doesn't change it ($\forall x (x+0 = x)$), and adding the successor of a number $y$ is the same as taking the successor of the sum with $y$ ($\forall x \forall y (x+S(y) = S(x+y))$). Multiplication is defined similarly, using addition: multiplying by zero gives zero ($\forall x (x \cdot 0 = 0)$), and multiplying by a successor builds upon the previous product ($\forall x \forall y (x \cdot S(y) = (x \cdot y) + x)$). These simple rules are a cascade of logic, allowing us to compute any sum or product.

From these axioms, the familiar world of arithmetic begins to emerge. We can, for instance, define what it means for one number to be less than or equal to another. We can say that $x \le y$ is simply an abbreviation for "there exists some number $z$ such that $x+z=y$". From this single definition, we can use the axioms to prove all the basic properties of order, like reflexivity ($x \le x$) and antisymmetry (if $x \le y$ and $y \le x$, then $x=y$). We can even prove that the order is discrete; there is no number between $x$ and $x+1$. Our blueprint is starting to look like the real thing.

Our axioms are powerful for specific calculations, but mathematics isn't just about calculation; it's about proving properties that hold for all numbers. How can we make a claim about an infinite set of objects?

The answer is the famous principle of mathematical induction, which we can formalize as an axiom. Think of it like a line of dominoes. If you can prove two things—that you can knock over the first domino (a property holds for $0$), and that any falling domino will knock over the next one (if the property holds for a number $x$, it must also hold for its successor $S(x)$)—then you have proven that all the dominoes will fall (the property holds for all numbers).

Here we come to a crucial subtlety, the very thing that makes our system "first-order." What constitutes a "row of dominoes"? In first-order PA, a property is anything that can be described by a formula $\varphi(x)$ in our language $\mathcal{L}_{PA}$. We cannot just say "for all properties...". That would require a more powerful logic (second-order logic). Instead, we have an ​​axiom schema of induction​​: a recipe that generates a new axiom for every single formula we can write down.

$\big(\varphi(0) \wedge \forall x (\varphi(x) \rightarrow \varphi(S(x)))\big) \rightarrow \forall x \varphi(x)$

This is an infinite list of axioms, one for each formula $\varphi$. This might seem like a minor technicality, but it is a fissure in our foundation with monumental consequences. Our language, though infinite in its expressions, is still only countably infinite. The set of all possible properties of numbers (which corresponds to the set of all subsets of natural numbers) is uncountably vast. This means our induction schema, powerful as it is, applies only to a vanishingly small fraction of all the properties of numbers we could imagine. We have built a powerful engine of proof, but it can only run on certain approved tracks.

With our axioms in hand, we have a formal theory, PA. Does it do the job? Does it uniquely capture the natural numbers $\mathbb{N}=\{0, 1, 2, \ldots\}$ that we know and love?

Certainly, the structure of our everyday numbers, where $0$ means zero, $S(n)$ means $n+1$, and $+$ and $\cdot$ mean normal addition and multiplication, is a ​​model​​ for the axioms of PA. Every axiom of PA is a true statement about this structure, which we call the ​​standard model​​.

But is it the only model? Because our induction schema is restricted to properties definable in our language, it is not strong enough to rule out some very strange possibilities. It turns out there are other "number systems" that obey all the rules of PA but look nothing like the natural numbers. These are called ​​non-standard models​​.

A non-standard model can be thought of as containing the entire line of standard numbers $\{0, 1, 2, \ldots\}$ as an initial segment, but then, "beyond infinity," it contains other numbers. These "non-standard" numbers might come in clusters that look like the integers ($\mathbb{Z}$), with numbers like $c$, $c+1$, $c-1$, and so on, where $c$ is an element larger than any standard number. The existence of these bizarre structures can be proven using a powerful tool of first-order logic called the ​​Compactness Theorem​​.

This means PA is not ​​categorical​​—it doesn't pin down a single, unique structure up to isomorphism. We set out to write the blueprint for one specific building, and we found that other, fantastical structures could be built from the very same plan.

This has a profound consequence. If we can find a statement that is true in our standard model but false in some non-standard model, then PA can never prove that statement. A proof in PA is a universal argument that must hold true in every model that satisfies its axioms, standard or not. This creates a fundamental gap between the notion of "truth" (what is true in our intended world of $\mathbb{N}$) and "provability" (what we can demonstrate using the axioms of PA).

Despite this limitation, the power of PA is breathtaking. In one of the most brilliant intellectual achievements of the 20th century, logicians discovered that the language of simple arithmetic is rich enough to describe any process that can be carried out by a computer.

This is formalized through the concept of ​​representability​​. A function, say $f(n_1, \ldots, n_k)=m$, is said to be representable in PA if we can write a formula $\varphi(x_1, \ldots, x_k, y)$ that acts as a perfect definition for it. This means two things: first, PA must be able to prove that for any set of inputs, there exists a unique output. Second, for any concrete calculation, like $f(2,3)=5$, PA must be able to prove the corresponding formula $\varphi(\bar{2}, \bar{3}, \bar{5})$ is true.

The astonishing result is that every computable function—that is, any function for which we could write a computer program—is representable in PA. Whether it's calculating prime numbers, rendering a video, or simulating the weather, if an algorithm can do it, PA can describe it. This discovery created a Rosetta Stone connecting the abstract world of number theory with the concrete world of computation. It meant that statements about numbers could be reinterpreted as statements about the behavior of computer programs, and vice-versa.

This very power to represent computation is what leads to PA's ultimate downfall. By being able to talk about algorithms, PA can, in a way, talk about its own process of proof. This self-reference is the key to unlocking its deepest secrets and limitations.

​​Gödel's Incompleteness​​: Using a clever numbering scheme (Gödel numbering), every formula and proof in PA can be encoded as a unique natural number. Since PA can talk about all computable relations between numbers, it can talk about the syntax of its own language. We can construct a formula, $\mathrm{Pr}_{\mathsf{PA}}(x)$, that represents the property "$x$ is the Gödel number of a sentence provable in PA".

Kurt Gödel used this to construct a sentence, often called $G$, which is equivalent to the statement "The sentence with my own Gödel number is not provable in PA". In essence, $G$ says, "I am unprovable.".

This leads to a paradox. If PA proves $G$, then $G$ must be true, which means $G$ is unprovable—a contradiction. So, if PA is consistent, it cannot prove $G$. But if $G$ is unprovable, then what it says is true! So we have found a true statement about numbers that PA cannot prove. This is ​​Gödel's First Incompleteness Theorem​​.

The rabbit hole goes deeper. The statement "PA is consistent," which can be written as $\mathsf{Con}(\mathsf{PA})$, is itself just a sentence of arithmetic. Gödel then showed that the entire reasoning of his first theorem can be formalized within PA to prove the implication $\mathsf{Con}(\mathsf{PA}) \rightarrow G$. Now, if PA could prove its own consistency, it could use that proof and this implication to prove $G$. But we just saw this is impossible. The conclusion is inescapable: ​​any consistent formal system like PA strong enough to do basic arithmetic cannot prove its own consistency​​. This is ​​Gödel's Second Incompleteness Theorem​​. The dream of a self-verifying, complete foundation for mathematics was shattered.

​​Undecidability and Undefinability​​: The story doesn't end there. These limitations also mean that PA is ​​undecidable​​. There is no algorithm, no master computer program, that can take an arbitrary arithmetic sentence and decide in a finite amount of time whether it is provable in PA or not. If there were, we could use it to solve the Halting Problem—the unsolvable problem of determining whether an arbitrary computer program will finish running or loop forever.

Furthermore, the very notion of "truth" in the standard model of arithmetic is itself beyond the grasp of the language. ​​Tarski's Undefinability Theorem​​ shows that there is no formula True(x) in the language of arithmetic that can correctly identify all the true sentences of arithmetic. Any attempt to create such a formula inevitably creates a "Liar's Paradox" sentence that leads to a contradiction.

In the end, first-order arithmetic presents us with a fascinating duality. It is a system of breathtaking power, capable of encoding the entirety of computation within its simple rules. Yet, this very power forces it to be forever incomplete, unable to prove its own foundations or even to fully define the truth it seeks to capture. It shows us that the world of numbers is far richer and more mysterious than any finite set of axioms can ever fully describe.

After our journey through the principles and mechanisms of first-order arithmetic, one might be left with the impression that we have been playing a very intricate and abstract game. We have meticulously defined a language of symbols, established axioms, and explored the rules of deduction. But what is the point of it all? Is this merely a logician’s pastime, a self-contained world of formal rigor with no bearing on anything outside of it?

The answer, which is as profound as it is surprising, is a resounding no. First-order arithmetic, particularly systems like Peano Arithmetic (PA), is not just a formalization of the natural numbers; it is a crucible in which the very concepts of computation, proof, truth, and the limits of knowledge are tested and revealed. In this chapter, we will see how the simple axioms governing numbers become a powerful lens, allowing us to explore the foundations of computer science, the philosophy of mathematics, and the intricate structure of mathematical theories themselves. It turns out that this formal game holds a mirror to the deepest questions about what can be known and what can be computed.

At first glance, the language of arithmetic—with its symbols for zero, successor, addition, and multiplication—seems rather sparse. How could such a simple tool possibly describe the complex, dynamic processes we see in the world, or even the operations of a modern computer? The first step is to see how we can capture even the most basic intuitive ideas about numbers within this formal language. For instance, the simple fact that zero is not the successor of any number is not a logical truth in itself; it's a specific property of our familiar number system. To build a theory of arithmetic, we must assert it as an axiom, typically written as $\forall x (S(x) \neq 0)$. This is our first "line of code," a foundational statement that begins to shape our formal world to resemble the one we intuitively understand.

From these humble beginnings, we can build up an astonishingly rich descriptive power. We can define complex number-theoretic relationships. For example, the statement "$x$ divides $y$" seems to require a search through all possible factors. Yet, within our formal language, it can be expressed with remarkable elegance. We can state that there exists some number $z$ such that $x \cdot z = y$. Furthermore, we know that if such a $z$ exists (and $x,y$ are positive), it cannot be larger than $y$. This allows us to write the relationship using a bounded formula: $\exists z \le y (x \cdot z = y)$. The ability to express such predicates with bounded quantifiers is the first clue that arithmetic can pin down computational processes that are guaranteed to terminate.

This leads to a monumental insight, one that forms the bedrock of theoretical computer science. It turns out that every computable process—any algorithm that can be executed by a Turing machine—can be described within the language of first-order arithmetic. This process is known as ​​arithmetization​​. The key idea is to use numbers to encode every aspect of a computation: the state of the machine, the contents of its tape, and the sequence of steps it takes. A finite computation, even a very long one, can be encoded as a single, very large natural number.

The truly magical part is that the rules governing a valid computation—the transition from one state to the next—can be expressed as a primitive recursive relation. As we've seen, these relations are representable in PA. This means there exists a universal formula, let's call it $\mathbf{T}(e, i, c)$, which is true if and only if '$c$' is the numerical code for a terminating computation of the program with index '$e$' on input '$i$'.

The statement "program $e$ on input $i$ produces output $o$" then becomes equivalent to the arithmetical sentence: "There exists a number $c$ such that $\mathbf{T}(e, i, c)$ is true and the output extracted from $c$ is $o$." This is a $\Sigma_1$ formula—an existential statement asserting the existence of a computation code. This provides an effective, uniform map from any algorithm to a specific formula in the language of arithmetic. In essence, Peano Arithmetic is not just a theory about numbers; it is a ​​Turing-complete programming language​​. We have discovered a universal computer hidden within the rules of elementary school arithmetic.

Having discovered the immense power of first-order arithmetic, we might be tempted to think we have found what David Hilbert and his followers were looking for at the beginning of the 20th century: a single, consistent, and complete formal system for all of mathematics. A complete system would be one that could, in principle, decide the truth or falsity of any mathematical statement. If arithmetic is a universal language of computation, surely it can "compute" all mathematical truths?

Here, we run into a wall—a beautiful and profound boundary that defines the limits of formal reasoning. The very power of arithmetic to describe computation is what makes it incomplete.

Our first hint of this limitation comes from considering which functions PA can prove are total (i.e., defined for all inputs). PA is powerful enough to prove the totality of every primitive recursive function, a vast class of algorithms that includes most of the functions one encounters in everyday mathematics. We can use the induction schema of PA to mirror the recursive definition of the function, proving step-by-step that it must terminate for any given input.

However, there exist total computable functions that grow so fantastically fast that PA lacks the inductive strength to prove they always halt. We can define a total computable function $g(x)$ that, by its very construction, diagonalizes out of the set of functions provably total in PA. The result is a function that we, standing outside the system, can recognize as total, but that the system itself cannot prove to be so. This reveals a stunning gap between truth and provability.

This gap becomes a chasm when we consider the distinction between what is ​​definable​​ (can be stated) and what is ​​representable​​ (can be decided by proof). A key theorem states that any set representable in PA must be computable (decidable). Why? Because to decide if a number $n$ is in the set, we can just start enumerating all possible proofs in PA. Since the set is representable, we are guaranteed to eventually find either a proof that $n$ is in the set or a proof that it is not. But what about sets that are known to be non-computable? The most famous is the ​​halting set​​, the set of all programs that halt on a given input. This set is certainly definable by a $\Sigma_1$ formula—the very formula $\exists c \, \mathbf{T}(e, i, c)$ we discussed earlier. But Alan Turing proved that this set is not computable. Therefore, it cannot be representable in PA. There are true facts about whether certain programs halt that PA can never prove.

This is the heart of ​​Gödel's First Incompleteness Theorem​​. By arithmetizing the notion of proof itself, we can define a predicate $\mathrm{Pr}_T(x)$ that is true if "$x$ is the Gödel number of a sentence provable in theory $T$." This predicate, it turns out, is also $\Sigma_1$. Gödel used this to construct a sentence, often denoted $G$, which effectively asserts "I am not provable in PA."

• If PA could prove $G$, then $G$ would be true. But $G$ says it is not provable, a contradiction.
• If PA could prove $\neg G$, this would mean it's false that $G$ is unprovable, so $G$ must be provable. But we just showed that if PA proves $G$, the system is inconsistent. So a consistent PA cannot prove $\neg G$ either.

Thus, $G$ is an undecidable sentence. It is true in the standard model of arithmetic (because it is, in fact, unprovable), but it is not provable within the system. This shatters the dream of a complete theory for arithmetic. The very richness that allows arithmetic to talk about its own proofs is the source of its incompleteness.

Gödel's work delivered a second, even more devastating blow to Hilbert's program. ​​Gödel's Second Incompleteness Theorem​​ states that no consistent, recursively axiomatized theory strong enough to formalize arithmetic can prove its own consistency. If PA could produce a proof of the sentence "PA is consistent," it would in fact be inconsistent!

Does this mean the foundations of mathematics are built on sand? Not at all. It simply reveals that the structure of mathematical certainty is not a single, self-supporting tower, but a magnificent web of interconnected theories. We cannot achieve absolute certainty from within, but we can establish powerful ​​relative consistency proofs​​.

A beautiful example of this is the relationship between arithmetic and ​​set theory​​. Zermelo-Fraenkel set theory with the Axiom of Choice ($ZFC$) is the standard foundation for most of modern mathematics. Within $ZFC$, we can construct a set that behaves exactly like the natural numbers—the set of finite von Neumann ordinals, $\omega$. We can define successor, addition, and multiplication on this set and formally prove, within $ZFC$, that this structure satisfies all the axioms of $PA$. In other words, $ZFC$ can prove that a model for $PA$ exists. By the Soundness Theorem (which can also be formalized in $ZFC$), if a theory has a model, it must be consistent. Therefore, $ZFC$ can prove the statement $\mathsf{Con}(\mathsf{PA})$ ("PA is consistent"). This does not provide an absolute proof, but it gives us a strong guarantee: if you believe in the consistency of set theory, you must also believe in the consistency of Peano Arithmetic.

Another fascinating connection exists between classical mathematics and ​​intuitionistic (or constructive) mathematics​​. Intuitionism, founded by L. E. J. Brouwer, is a philosophy that rejects certain principles of classical logic, most famously the Law of the Excluded Middle ($A \vee \neg A$). Proofs by contradiction are generally not allowed. Heyting Arithmetic ($HA$) is the intuitionistic counterpart to $PA$. One might think that classical arithmetic, with its powerful non-constructive proof methods, would be logically "riskier" than its constructive cousin. However, the ​​Gödel-Gentzen negative translation​​ provides a remarkable bridge. It gives an effective procedure for translating any proof in classical PA into a proof in intuitionistic $HA$. The upshot is a relative consistency proof: if $HA$ is consistent, then $PA$ must also be consistent. This stunning result shows that the use of classical logic in arithmetic introduces no new inconsistencies. From a consistency standpoint, classical arithmetic is just as "safe" as constructive arithmetic, a deep result that connects two rival philosophical foundations of mathematics.

Our exploration of first-order arithmetic has been a journey of expanding horizons. We began with a simple set of rules for numbers. We discovered this system was a universal language, capable of describing any conceivable algorithm. This very power led us to its inherent limits—the unprovable truths and the inability to vouch for its own consistency. Yet, even these limitations were not a dead end. They revealed a deeper, interconnected structure within mathematics, linking arithmetic to the grand edifices of set theory and the subtle world of constructive logic.

The study of first-order arithmetic, therefore, is not a niche subfield of logic. It is a central pillar of the modern intellectual landscape, providing the theoretical underpinnings for computer science and forcing us to confront the fundamental nature of proof and truth. The simple act of reasoning about numbers, when pursued with relentless precision, unveils the very architecture of logical thought itself.