# Predicate Logic Hilbert Proof

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.

• 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). – Andreas Blass Nov 10 '18 at 1:51
• 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 – Ryan Wibberley Nov 10 '18 at 5:38
• See : Elliott Mendelson, Introduction to Mathematical Logic, CRC Press (6th ed 2015), page 79. – Mauro ALLEGRANZA Nov 10 '18 at 8:34
• I'm confused how the example on page 79 of the book is related to this question? Is there something I'm missing here? – Ryan Wibberley Nov 11 '18 at 17:28
• In my copy of the book, at page 79 there is the proof. – Mauro ALLEGRANZA Nov 14 '18 at 11:17