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?

  • 1
    $\begingroup$ Are you presuming that humans brains run algorithms? $\endgroup$ – Andrej Bauer Nov 13 '17 at 11:48
  • 2
    $\begingroup$ @AndrejBauer Are you presuming that human solve problems by magic? $\endgroup$ – Valentina Tihhomirova Nov 13 '17 at 12:02
  • 1
    $\begingroup$ The first sentence is a bit misleading, especially in that context. I'd ignore it. $\endgroup$ – chi Nov 13 '17 at 12:07
  • 1
    $\begingroup$ Well, if some predicate logic sentences can be decided in bounded time, it does not mean that all of them can. $\endgroup$ – rus9384 Nov 13 '17 at 12:15
  • 3
    $\begingroup$ 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. $\endgroup$ – Yuval Filmus Nov 13 '17 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.

  • 1
    $\begingroup$ 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. $\endgroup$ – Valentina Tihhomirova Nov 13 '17 at 18:05
  • 4
    $\begingroup$ @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? $\endgroup$ – David Richerby Nov 13 '17 at 18:35
  • 1
    $\begingroup$ Sorry, I did read "author is correct" in the first reading. Thanks for highlighting where I fail. $\endgroup$ – Valentina Tihhomirova Nov 14 '17 at 20:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.