On page 441, fundamental fact 2 asserts that:
The property of forming a proof-pair is testable in BlooP, and consequently, it is represented in TNT by some formula having two free variables.
Why is this the case? I get the fact that a BlooP program can mechanically test if a certain derivation is correct, but how can you represent that it is with a formula? If i for example say that 10 is not a prime, a program could divide all the numbers up to 10 and return that there do exist whole numbers when multiplied, gives the product 10, and therefore the statement is false. But how can a formal system represent that?
I feel like this has been asked before, but this is one of the key notions behind computability theory — there is a 1:1 primitive recursive mapping (many, in fact) between finite sequences of whole numbers and whole numbers themselves. Perhaps the simplest way — although this version isn't one-to-one, it doesn't have to be — is to repeatedly use what's known as a pairing function $\langle \cdot, \cdot\rangle:\mathbb{N}^2\mapsto\mathbb{N}$ that takes pairs of numbers to a single number, and represent the sequence $\{a_1, a_2, \ldots, a_n\}$ as $\langle n, \langle a_1, \langle a_2, \langle\ldots\langle a_{n-1}, a_n\rangle\ldots\rangle$. Since a program is, ultimately, just a finite sequence of numbers, this gives a unique number for each program. And importantly, given a number we can extract the sequence of numbers corresponding to it by using nothing but bounded loops. This is because it's straightforward to make it such that the pairing function always satisfies the condition that $\langle i,j\rangle$ is greater than both $i$ and $j$ ; this means that to extract the original $i$ and $j$ from $n=\langle i,j\rangle$ we can simply test all $i$ and $j$ between $1$ and $n$ to see what works.
For more information, you might want to learn about the Kleene Recursion Theorem; there's a lot of sometimes dauntingly dense formality, but over time you will build an intuition about these sorts of things.