Undecidable predicate logic is decidable by people?

Question

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?

Answer 1

Keep in mind that the book was written for undergraduate students, and there are aspects of logic that will demand a considerable level of sophistication, which is often omitted at this introductory level.

Importantly, the sentence

Every φ can, in principle, be discovered to be valid or not, if you are prepared to work arbitrarily hard at it.

is not, and cannot be, a sentence about proofs realized within the context of a formal theory, but as performed by people (possibly with the help of machines) in real life. Taken out of context, the sentence is obviously false, from any pragmatic standpoint. Moreover, it philosophically oversimplifies and confuses the subject, in a way that is in fact questionable, even from a didactic point of view.

That said, I wouldn't take these issues too seriously. Apparently, the book has many good qualities, and it is really hard to convey this kind of subject to the intended audience in a way that is both rigorous and inviting.

Answer 2

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.