How to transform a sequent notation to rule form?

74 Views Asked by At

I can write this proposition in sequent notation:

$$(P\rightarrow Q)\rightarrow (\neg P \lor Q)$$

as this one in rule form (see here):

$$\frac{(P\rightarrow Q)}{(\neg P \lor Q)}$$

But how can I transform, for example, these into rule form?

$$(P\rightarrow Q)\leftrightarrow(\neg(P\land\neg Q))$$ $$((P\land Q)\rightarrow R)\rightarrow((P\land\neg R)\rightarrow\neg Q)$$ $$((P\lor Q)\rightarrow (P\land S))\rightarrow(\neg P\lor\neg Q)$$

Are there any specific rules to follow? I saw a similar example on wikipedia but I cannot follow it.

1

There are 1 best solutions below

9
On BEST ANSWER

First, in sequent notation it would be:

$$(P \to Q) \vdash (\neg P \lor Q)$$

rather than

$$(P \to Q) \to (\neg P \lor Q)$$

The latter is a tautology and as such can be used as an axiom in an axiom system, but the latter is not a sequent.

Second, for

$$(P\rightarrow Q)\leftrightarrow(\neg(P\land\neg Q))$$

you would need two rules:

$$\frac{P\rightarrow Q}{\neg (P \land \neg Q)}$$

and

$$\frac{\neg (P \land \neg Q)}{P\rightarrow Q}$$

The

$$((P\land Q)\rightarrow R)\rightarrow((P\land\neg R)\rightarrow\neg Q)$$

is easy, as that just becomes:

$$\frac{(P\land Q)\rightarrow R}{(P\land\neg R)\rightarrow\neg Q}$$

The

$$((P\lor Q)\rightarrow (P\land S))\rightarrow(\neg P\lor\neg Q)$$

can be written as a rule

$$\frac{(P\lor Q)\rightarrow (P\land S)}{\neg P\lor\neg Q}$$

but please note that this is not a valid inference, and indeed

$$((P\lor Q)\rightarrow (P\land S))\rightarrow(\neg P\lor\neg Q)$$

is not a tautology!