4
$\begingroup$

Let $\Sigma$ be a signature and $\phi$ be a formula over $\Sigma$ and $\vec{y}$ be a context suitable for it. How do I show that the following sequent is derivable? namely

$$\phi\!\left[\vec{x}\!\left/\vec{y}\right.\right]\vdash_{\vec{x}}\left(\exists \vec{y}\right)\left(\phi\land\left(\vec{y} = \vec{x}\right)\right)$$

It feels trivial but I don't find any suitable rules to derive it. For reference by rules I mean the following (I just don't find anything that allows me to deduct a sequent containing $\exists y$ that appears on the right of $\vdash$):

enter image description here enter image description here

$\endgroup$
  • $\begingroup$ What book and author are you quoting from? Not all authors give the same notation and inference rules for first-order logic. $\endgroup$ – hardmath Jan 4 '17 at 1:35
  • $\begingroup$ @hardmath This is part D of Elephant by Peter Johnstone. ncatlab.org/nlab/show/Elephant $\endgroup$ – h__ Jan 4 '17 at 2:28
1
$\begingroup$

Rewritten after h__'s comment

1) $(∃y)(\phi \land (y=x)) ⊢_x (∃y)(\phi \land (y=x))$ --- identity axiom

2) $\phi \land (y=x) ⊢_{x,y} (∃y)(\phi \land (y=x))$ --- rule for existential quantification

3) $\phi[x/y] \land (x=x) ⊢_x (∃y)(\phi \land (y=x))$ --- with substitution $[x/y]$.

4) $\phi[x/y] \vdash_x \phi[x/y]$ --- identity axiom

5) $\phi[x/y] \vdash_x \top$ --- rule for (finite) conjunction

6) $\top \vdash_x (x=x)$ --- equality rule

7) $\phi[x/y] \vdash_x (x=x)$ --- from 5) and 6) by cut rule

8) $\phi[x/y] \vdash \phi[x/y] \land (x=x)$ --- from 4) and 7) by rule for (finite) conjunction

$\phi[x/y] \vdash_x (∃y)(\phi \land (y=x))$ --- from 3) and 8) by cut rule.

$\endgroup$
  • $\begingroup$ And if Mauro cannot derive it, it is likely that it is underivable. =) $\endgroup$ – user21820 Jan 5 '17 at 11:21
  • $\begingroup$ @user21820 - Thanks a lot ! But I think you are wrong... the formula is "easily" derivable with Natural Deduction and I'm not prone to think that the system of the book (also if - according to me - uselessly complicated) is "incomplete. $\endgroup$ – Mauro ALLEGRANZA Jan 5 '17 at 12:23
  • $\begingroup$ Haha I estimate the likelihood of error in a randomly selected deductive system in a textbook to be non-negligible, because it's so easy to make mistakes, and I'm no exception; I can perform sound reasoning with no problem at all, but when I attempted to translate my system to using a sequent-style calculus at math.stackexchange.com/a/1822074 I made a few mistakes that were pointed out by Henning and DanielV). Anyway I'm too lazy to try out the system mentioned in the question. It is tiring for me to follow other people's deductive systems. =) $\endgroup$ – user21820 Jan 5 '17 at 15:15
  • 1
    $\begingroup$ Thanks for the response. Someone helped me on another place. So if we write $\psi(\vec{y})$ for $(\phi\land\left(\vec{y} = \vec{x}\right))$ then we can go from $(\exists\vec{y})\psi\vdash_{\vec{x}}(\exists\vec{y})\psi$ to $\psi\vdash_{\vec{x}, \vec{y}}(\exists\vec{y})\psi$ by (f), and then make a subsitution $[\vec{y}/\vec{x}]$, to get $\psi[\vec{y}/\vec{x}]\vdash_{\vec{x}, \vec{y}}(\exists\vec{y})\psi$, which is just $\phi\left[\vec{x}\left/\vec{y}\right.\right]\land\top\vdash_{\vec{x}}\left(\exists \vec{y}\right)\left(\phi\land\left(\vec{y} = \vec{x}\right)\right)$. Q.E.D. $\endgroup$ – h__ Jan 5 '17 at 18:51
  • $\begingroup$ @MauroALLEGRANZA for conjunction, isn't that included in (c)? $\endgroup$ – h__ Jan 6 '17 at 1:16

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.