I am tasked to find a proof of $\vdash \exists x (\phi \implies \forall x \phi)$ by using the Hilbert axioms. I've been trying for about 2 hours. I tried using the results from the previous parts of the exercise below. I am also allowed to use substitution instances of tautologies (i.e $\vdash p \implies p$ implies $\vdash \phi \implies \phi$ where $p$ is a propsitional variable and $\phi$ is a first-order formula), that $\exists x$ is defined as $\neg \forall x \neg$, and the standard meta-theorems like proof by contradiction.

enter image description here

enter image description here

Basically I've tried to work backwards:

$$\vdash \exists x (\phi \implies \forall x \phi)$$ $$\vdash \forall x (\phi \implies \forall x \phi)$$ $$\vdash (\phi \implies \forall x \phi)$$

This last step seems impossible to prove, as it would have me show that if a property is true for some x then it is true for all $x$ (obviously not true if $\phi$ is taken to be "is even")

Similarly I tried invoking part (c)

$$\vdash \exists x (\phi \implies \forall x \phi)$$ $$\vdash \forall x (\phi \implies \forall x \phi)$$
$$\vdash (\exists x \phi \implies \forall x \phi) \implies \forall x(\phi \implies \forall x \phi)$$

Again, this would require to show that if a propery is true for some x then it is true for all $x$.

The only other way to introduce an $\exists$ as the "main connective" is by (a). But that seems to go nowhere as well.

  • $\begingroup$ There's no mention of axioms related to ∃ quantifier in above reference, if really so then you have to use your book's definition of ∃ (as most likely related to ∀ defined in most books) to change to a wff with ∀ only, then try to use all above axioms to prove, perhaps you may also need proof by negation... $\endgroup$
    – cinch
    Dec 13, 2021 at 4:01
  • $\begingroup$ @mohottnad I tried that and I got nowhere. $\endgroup$
    – ngc1300
    Dec 13, 2021 at 4:06
  • $\begingroup$ So you can confirm your book defines ∃ = ¬∀¬ and that's it, no any axioms involving ∃? $\endgroup$
    – cinch
    Dec 13, 2021 at 4:07
  • $\begingroup$ @mohottnad Correct $\endgroup$
    – ngc1300
    Dec 13, 2021 at 4:09
  • $\begingroup$ @mohottnad But it doesn't have to be strictly from the axioms. I can used the results from the other part of the Exercise. $\endgroup$
    – ngc1300
    Dec 13, 2021 at 4:12

1 Answer 1


Hilbert system is well known to be very cumbersome to prove some straightforward result compared with natural deduction systems, especially for this non-trivial Drinker Paradox sentence and you don't even have the useful deduction meta-theorem. Since we know it'll be a little hard (as the last exercise in your book) so we may stand upon a known result from prenex normal form in predicate calculus that $\vdash (∀x\phi → \psi) \to ∃x(\phi → \psi)$, where $x$ does not occur free in $\psi$. So with this known theorem we can prove your result based solely on your system in only 7 steps as follows:

  1. $\vdash (\forall x \phi → \forall x \phi) \to ∃x(\phi → \forall x \phi)~~~~~$ ...known theorem

  2. $\vdash (\forall x \phi→((\psi→\forall x \phi) → \forall x \phi))→((\forall x \phi→(\psi→\forall x \phi))→(\forall x \phi→ \forall x \phi))~~~~~$ ...Ax 2

  3. $\vdash \forall x \phi→((\psi→\forall x \phi)→\forall x \phi)~~~~~$ ...Ax 1

  4. $\vdash (\forall x \phi→(\psi→\forall x \phi))→(\forall x \phi→\forall x \phi)~~~~~$ ...MP from 2, 3

  5. $\vdash \forall x \phi→(\psi→\forall x \phi)~~~~~$ ...Ax 1

  6. $\vdash \forall x \phi→\forall x \phi~~~~~$ ...MP from 4, 5

  7. $\vdash \exists x (\phi \to \forall x \phi)~~~~~$ ...MP from 1, 6. Done!

Now sketch a proof of this known theorem in your specific formal system. As discussed in comments we only have one way to prove any result including $\exists$ quantifier in your system, so after plugin $\lnot \forall \lnot$ we 'd better use proof by negation technique to initally assume $\forall x \lnot (ϕ→ψ)$ where $x$ does not occur free in $ψ$, given the assumption $(∀xϕ→ψ)$. Now perhaps it's clear how to formally proceed with the given assumption and use your Axiom 4 (universal instantiation) to derive at $\bot$, thus our known theorem is proved...

  • $\begingroup$ Step 2 seems incorrect: $x$ is free in $\phi$, so Axiom 5 does not apply. $\endgroup$ Dec 13, 2021 at 8:38
  • $\begingroup$ I found the proof that I need math.stackexchange.com/a/807558/455950. I just have to change the y's to x's. $\endgroup$
    – ngc1300
    Dec 13, 2021 at 15:04
  • $\begingroup$ Although I just realized his ⊢(∀𝑥𝛽→𝛼)↔∃𝑥(𝛽→𝛼) step is not quite the one I'm given in (c), and the derivation of this is 10 steps math.stackexchange.com/a/782290/455950. It seems to me that this should have been added as a hint or a previous exercise. $\endgroup$
    – ngc1300
    Dec 13, 2021 at 15:43
  • $\begingroup$ @VladimirSotirov thx for checking and spot issue in my original proof, now corrected. $\endgroup$
    – cinch
    Dec 15, 2021 at 4:34

Not the answer you're looking for? Browse other questions tagged .