Assume x does not occur free in B.
By the deduction and generalization theorems,
Since (using a contraposition and verify this), the above formula is valid.
1.
2.
3.
4.
Since (verify this), the above formula is valid.
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:
Is this sequent indeed valid?
Another sequent:
Also for this 2nd sequent I get the result that it is valid.
Am I correct for both sequents?
Thanks for any help.
Assume x does not occur free in B.
By the deduction and generalization theorems,
Since (using a contraposition and verify this), the above formula is valid.
1.
2.
3.
4.
Since (verify this), the above formula is valid.