# ⊢∃𝑥(𝜙⟹∀𝑥𝜙) using Hilbert-style proof [duplicate]

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.

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.

• 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... Dec 13, 2021 at 4:01
• @mohottnad I tried that and I got nowhere. Dec 13, 2021 at 4:06
• So you can confirm your book defines ∃ = ¬∀¬ and that's it, no any axioms involving ∃? Dec 13, 2021 at 4:07
• @mohottnad Correct Dec 13, 2021 at 4:09
• @mohottnad But it doesn't have to be strictly from the axioms. I can used the results from the other part of the Exercise. Dec 13, 2021 at 4:12

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...

• Step 2 seems incorrect: $x$ is free in $\phi$, so Axiom 5 does not apply. Dec 13, 2021 at 8:38
• I found the proof that I need math.stackexchange.com/a/807558/455950. I just have to change the y's to x's. Dec 13, 2021 at 15:04
• 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. Dec 13, 2021 at 15:43
• @VladimirSotirov thx for checking and spot issue in my original proof, now corrected. Dec 15, 2021 at 4:34