What you are missing is that in the Post Correspondence Problem you have an unlimited supply of each type of domino. So a finite list of domino types could req

What you are missing is that in the Post Correspondence Problem you have an unlimited supply of each type of domino. So a finite list of domino types could require an unlimited number of dominos to decide. Now we can write programs that attempt some sort of clever reasoning to figure out whether or not there is a solution at all. But given any specific program that does that, there is a finite arrangement of dominos such that either the program produces the wrong answer, or cannot possibly finish. In other words, for any algorithm there is a finite problem that cannot be properly decided by that algorithm. Given an axiom system such as ZFC, we can write a program that searches through all proofs in ZFC for a proof or disproof that a particular case of the Post Correspondence Problem is solvable. This, being an algorithm, has a finite input that it will either produce a wrong answer for (meaning that ZFC contradicts itself) or else will never finish. Whether or not that case has an answer is not decidable within ZFC! Ideally we want the answer to be "there is no solution" in this case. But if we introduce the axiom that there is a solution, we will never find a contradiction and never be aware of any disturbing conclusion beyond, "That solution must be really, really big." It turns out that, no matter how hard we try, first order logic cannot correctly encode the concept of "finite". This is what we mean by "undecidable".