In the Hilbert proof system for predicate logic, prove that the formula:

$\exists x~\big(B(x)\to C(x)\big)\to\big(\forall x~B(x)\to\exists x~C(x)\big)$

I'm awful with Hilbert Proofs and have no idea where to even start with this one. Any help would be greatly appreciated.

  • 3
    $\begingroup$ When I read the first few words of the question, I was going to ask which of the many Hilbert proof systems you're asking about. But then I read the formula you're trying to prove and realized that it's not valid (there are counterexamples with just two elements). $\endgroup$ – Andreas Blass Nov 10 '18 at 1:51
  • 1
    $\begingroup$ Put in the question wrong when I typed this up. Fixed it now, the final predicate identifier was suppose to be \exists not \forall. I believe the formula is valid now $\endgroup$ – Ryan Wibberley Nov 10 '18 at 5:38
  • $\begingroup$ See : Elliott Mendelson, Introduction to Mathematical Logic, CRC Press (6th ed 2015), page 79. $\endgroup$ – Mauro ALLEGRANZA Nov 10 '18 at 8:34
  • $\begingroup$ I'm confused how the example on page 79 of the book is related to this question? Is there something I'm missing here? $\endgroup$ – Ryan Wibberley Nov 11 '18 at 17:28
  • $\begingroup$ In my copy of the book, at page 79 there is the proof. $\endgroup$ – Mauro ALLEGRANZA Nov 14 '18 at 11:17

Your Answer

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

Browse other questions tagged or ask your own question.