valid sequent

**sanv** · February 25th 2009, 12:11 PM

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.

**aliceinwonderland** · February 26th 2009, 12:16 AM

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.

Thread: valid sequent

LinkBack

Thread Tools

Display

valid sequent

Similar Math Help Forum Discussions

Is this a valid operation?

is a≡b still valid??

valid,non valid arguments

Is this valid?

Is this valid?

Search Tags