In computer programming, many tasks can be done more efficiently using appropriate data structures. If we’re going to maintain a bunch of items which we’ll need to frequently do searches on by name, then an alphabetically sorted binary tree might save time, for example. The “paradox” is that none of these structures actually exist in the compiled machine code. Our RAM has no special slots for nodes of binary trees. Our CPU machine code has no special opcodes for any of these structures. No, the machine code is nothing but low-level conditional jumps. Whether the program was written with sophisticated data structures or whether it was brute-forced with giant unwieldy arrays, the compiled machine code looks the same: the jumps move around a bit but they’re still just low-level conditional jumps.
The same phenomenon happens with mathematical proofs. If I prove a theorem from ZFC, then, in principle, the proof can be “unwrapped” until it’s nothing but a giant list of steps, each of which is either an axiom of ZFC, a tautology, or an appeal to Modus Ponens. If I prove the theorem in a very dumb, brute force way, or if I use some brilliant strategy to make it more followable, the unwrapped version will still just be axioms, tautologies, and Modus Ponens. The fancy strategy– and any definition which it happens to use for the sake of human readability– only “exists” informally.
If a programmer wanted to troll you, he could implement binary trees without ever mentioning them, just purely manipulating pointers in a way which is equivalent but with no user-friendly explanation (and no names like “root”, “parent”, “left” or “right”). This corresponds to the first paragraph above. If you asked him why his bizarre code works, he could give you an extremely opaque but nevertheless legitimate proof using nothing but axioms, tautologies, and Modus Ponens. This corresponds to the second paragraph above.
Of course, this isn’t really a paradox at all; there’s nothing contradictory about it. It’s just something interesting to think about.
FURTHER READING
Obscure Numbers
The Illogician
Newcomb’s Paradox