How to prove in sequent calculus

116 Views Asked by At

build output

$$(\forall x)(\exists y) y \approxeq g(x,y), (\forall x)R(x,x) \vdash (\forall x)(\exists y)R(y,g(x,y))$$

I got to this step and I don’t understand what to do next:

$$ y \approxeq g(x,y), (\forall x)R(x,x) \vdash (\exists y)R(y,g(x,y)) $$

I think i need to use this rule at the end:

$$ \frac{\Gamma \vdash t_1 \approxeq s_1 \quad \cdots \quad \Gamma \vdash t_n \approxeq s_n \quad \Gamma \vdash \left ( \varphi \right )_{t_1, \ldots, t_n}^{x_1, \ldots, x_n}}{\Gamma \vdash \left ( \varphi \right )_{s_1, \ldots, s_n}^{x_1, \ldots, x_n}} $$

but i don't know what steps i need to take to do it

1

There are 1 best solutions below

0
On

Call $\Gamma$ the set of premises.

Using rules for quantifiers we have: $\Gamma \vdash a=g(x,a)$ and $\Gamma \vdash R(a,a)$.

Then you are right; you need the following instance of the above rule:

$\dfrac { \Gamma \vdash t_1=s_1 \ \ \Gamma \vdash \varphi^{x_1}_{t_1} }{\Gamma \vdash \varphi^{x_1}_{s_1} }$

where $\varphi$ is $R(a,x_1)$.

Thus, we have: $\Gamma \vdash R(a, g(x,a))$.

The conclusion follows by $(\exists \text I)$ followed by $(\forall \text I)$.


If you want to prove it in Sequent Calculus, you have to start from the equality axiom and re-introduce the quantifiers.