Satisfiability of first-order logic is undecidable?

I struggle with understanding why the satisfiability in the first-order logic is undecidable. Could you explain it with some examples? I've also seen that satisfiability in some first-order formulas are decidable.

Please explain it with as much as many examples.

The fact that first-order logic (with some non-triviality constraints) is undecidable means that no algorithm can decide correctly whether a given first-order formula is true or not. However, for any single statement $\varphi$ it is easy to come up with an algorithm that decides $\varphi$ correctly (just hard-code the answer). So it is impossible to give examples of "undecidable statements", since there is no such thing.

What is possible is to give a restricted set of sentences whose truth value is already undecidable. In effect, this is what the proof of undecidability does. The proof shows that you can encode the statement "the Turing machine $T$ halts on empty input" in first-order logic (again, given some mild non-triviality constraints), so this infinite sequence of statement is already undecidable, that is, no algorithm can correctly decide whether such a formula is true or not.

StackExchange Computer Science Q#30670, answer score: 7