I am trying to understand how to prove if a rule is derivable or not using sequent calculus.
A practice problem in my book I am learning from has the following question:
Consider the rule:
$$\frac{}{\Gamma \hspace{10pt} \exists x\phi \hspace{10pt} \forall x\phi }$$
Determine whether this rule is derivable or not.
I think you need to start from the assumption rule to state $\Gamma \phi \models \phi$ and then make inferences from there. My intuition wants to say that this is not a derivable rule since the existential quantifier is less strict than the universal quantifier, but I'm not sure how to prove it or if my intuition is even correct...
Thank you in advance for helping me work through this problem.
Edit: I am working with the calculus defined in the book Mathematical Logic by H.-D. Ebbinghaus, J. Flum, and W. Thomas in chapter IV.
To prove that an inference rule is invalid, you just need provide a model in which the rule fails. In your case, you need to provide a language, a formula $φ$ in that language and a structure over that language where $\exists x\ ( φ(x) )$ is true but $\forall x\ ( φ(x) )$ is false.