The halting problem implies that it’s impossible to write a program that correctly deduces whether every other program halts or not. But you can write a program that correctly deduces whether many programs halt, and labels the rest “unknown”.
Likewise, the finite version of FairBot checks whether there’s a proof of cooperation of length less than N (for some large fixed N), cooperates if so, and defects otherwise. There are programs that cooperate with FairBot but have no short proof of that fact—and FairBot defects against those programs. (I.e. it defects against the “unknown” programs.)
The halting problem implies that it’s impossible to write a program that correctly deduces whether every other program halts or not. But you can write a program that correctly deduces whether many programs halt, and labels the rest “unknown”.
Likewise, the finite version of FairBot checks whether there’s a proof of cooperation of length less than N (for some large fixed N), cooperates if so, and defects otherwise. There are programs that cooperate with FairBot but have no short proof of that fact—and FairBot defects against those programs. (I.e. it defects against the “unknown” programs.)
Does that help clarify things?