# Thread: valid sequent

1. ## valid sequent

Hi,

I have used the semantic tableau procedure to check if the following sequent is valid. I get the answer that it is valid, however I am not sure if it is indeed valid and I havent made an error while writing the tableau. I havent included the tableau in this post as I don't know how to include it but the sequent is the following:

$
(\exists x A(x)) \rightarrow B \vdash \forall x (A(x) \rightarrow B)
$

Is this sequent indeed valid?

Another sequent:

$
(\forall x A(x)) \rightarrow B \vdash \exists x (A(x) \rightarrow B)
$

Also for this 2nd sequent I get the result that it is valid.

Am I correct for both sequents?

Thanks for any help.

2. Originally Posted by sanv
$
(\exists x A(x)) \rightarrow B \vdash \forall x (A(x) \rightarrow B)
$
Assume x does not occur free in B.

By the deduction and generalization theorems,

$
\exists x A \rightarrow B \vdash \forall x (A \rightarrow B),
$

$
\{(\exists x A \rightarrow B), A\} \vdash B.
$

Since $A \vdash \exists x A$ (using a contraposition and verify this), the above formula is valid.

$
(\forall x A(x)) \rightarrow B \vdash \exists x (A(x) \rightarrow B)
$
1. $
\forall x A \rightarrow B \vdash \exists x (A \rightarrow B),
$

2. $
\neg \exists x \neg A \rightarrow B \vdash \exists x (A \rightarrow B),
$

3. $
\neg \exists x \neg A \rightarrow B \vdash A \rightarrow B,
$

4. $
\{(\neg \exists x \neg A \rightarrow B), A\} \vdash B, (\text{by deduction theorem})
$

Since $A \vdash \neg \exists x \neg A$ (verify this), the above formula is valid.