# 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?

• Are you presuming that humans brains run algorithms? Commented Nov 13, 2017 at 11:48
• @AndrejBauer Are you presuming that human solve problems by magic? Commented Nov 13, 2017 at 12:02
• The first sentence is a bit misleading, especially in that context. I'd ignore it.
– chi
Commented Nov 13, 2017 at 12:07
• Well, if some predicate logic sentences can be decided in bounded time, it does not mean that all of them can. Commented Nov 13, 2017 at 12:15
• This seems like a philosophical question, since it's not clear what "discovered to be valid" means. If it means "proved formally", then the statement is false. Commented Nov 13, 2017 at 12:59

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.

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.

• I do not see how this answers the question. Moreover, I can say the same about the machines: they are good at finding heuristics but cannot prove unprovable. Commented Nov 13, 2017 at 18:05
• @ValentinaTihhomirova The book says (I paraphrase) "If you work hard enough you can always, in principle, find a proof." The answer says, "That's not true -- there are statements that are true but have no proof." How is that not an answer? Commented Nov 13, 2017 at 18:35
• Sorry, I did read "author is correct" in the first reading. Thanks for highlighting where I fail. Commented Nov 14, 2017 at 20:05