Undecidable predicate logic is decidable by people?

Logic in computer science (By Michael Huth,Mark Ryan, second edition, page 132) says


Every φ can, in principle, be discovered to be valid or not, if you
are prepared to work arbitrarily hard at it; but there is no uniform
mechanical procedure for determining whether φ is valid which will
work for all φ.

For me, it sounds contradictory because I take your ability to decide any formula as a uniform mechanical procedure. If you can do it, then you have a uniform mechanical procedure. What do I fail to understand?

Just to be clear what validity means here, the discussion happens in the context of validity definition:


Given a logical formula φ in predicate logic, does ⊨ φ hold, yes or
no?

The author is incorrect. A consequence of Godel's incompleteness is that any sufficiently complex logic has statements that are true, but have no proof of truth.

If every statement had a proof or disproof, then we could iterate through all strings, check if it was a proof or disproof, and eventually we'd find one, making logic decidable. We know that this isn't the case, since this could solve the halting problem.

In the context of your question, this means there are valid formulas with no proofs of validity.

Humans have an excellent set of heuristics for proving things. We are good at seeing patterns and incorporating past knowledge. But ultimately we can't find proofs that don't exist.

StackExchange Computer Science Q#83851, answer score: 8