prove validity of following sequent

Question

How to prove validity of following sequent using rules of conjunction, disjunction, implication, negation etc. Premises: $ c \wedge n \Rightarrow t$ , $h \wedge \sim s$, $h \wedge \sim(s\vee c) \Rightarrow p $ Conclusion: $ n \wedge \sim t \Rightarrow p $ It should be proceeded as follows:

$ 1- c \wedge n \Rightarrow t$ Premise

$2- h \wedge \sim s$ Premise

$3- h \wedge \sim(s\vee c) \Rightarrow p $ Premise

$4- n \wedge \sim t $ Assumption

$5- n $ Using rule and_elimination1 on line 4

$6- \sim t $ Using rule and_elimination2 on line 4

$7- \sim (c \wedge n) $ Using MT rule on lones 6 and 1

$8- h $ Using rule and_elimination1 on line 2

$9- \sim s $ Using rule and_elimination2 on line 2

$8- p $ By following which rules, we can get this p ?

Answer 1

$ 1- c \wedge n \Rightarrow t$ $$ \equiv \sim (c \wedge n) \vee t \equiv \sim c \vee \sim n \vee t \equiv n \wedge \sim t \Rightarrow \sim c $$

$2- h \wedge \sim s$

$3- h \wedge \sim(s\wedge c) \Rightarrow p $ $$\equiv h \wedge (\sim s\vee \sim c) \Rightarrow p \equiv (h \wedge \sim s) \vee (h \wedge \sim c) \Rightarrow p \equiv \sim(h \wedge \sim s) \wedge \sim(h \wedge \sim c) \vee p $$

$4-\text{(from 2,3) } \sim (h \wedge \sim c) \vee p$ $$\equiv \sim h \vee c \vee p $$

$5-\text{(from 2) } h$

$6-\text{(from4,5) } c \vee p $ $$\sim c \Rightarrow p$$

$7-\text{(from 6,1) } n \wedge \sim t \Rightarrow p $

Answer 2

Note that, up to step 9 in your proof, you have not yet used the 3rd premise :

$h \land \lnot (s \lor c) \Rightarrow p$,

and we need it to complete the proof.

We will start from step 9.

$10 − \lnot c \lor \lnot n$ by De Morgan from 7 : $\lnot (c \land n)$

$11 - \lnot c$ by disjunctive syllogism from 10 and 5 [Note : disjunctive syllogism is a particular case of $\lor$-elimination]

$12 - \lnot c \land \lnot s$ using $\land$-introduction on 11 and 9

$13 - \lnot (c \lor s)$ again by De Morgan

$14 - h \land (s \lor c)$ using $\land$-introduction on 13 and 8

$15 - p$ using MP on 13 and 3 (the 3rd premise)

$16 - (n \land \lnot t) \Rightarrow p$ using $\Rightarrow$-introduction on 4 and 15, "discharging" the "temporary" assumption 4.

Thus, we conclude with :

$c∧n⇒t, h∧ \lnot s, h∧ \lnot (s∨c)⇒p \vdash (n \land \lnot t) \Rightarrow p$.

Answer 3

I'll add my own loose answer here, and point out that we don't know exactly what your negation rule says. The only rule I will use is a resolution rule of inference R which can get described by saying "given two formulas $\phi$ and $\psi$ which only contain disjunction symbols and literals, if there exists a literal $\alpha$ in $\phi$ such that it is the negation of a literal $\alpha$' in $\psi$, then we can infer any formula which consists solely of all of the remaining literals in $\alpha$ and $\psi$ and disjunction symbols." You can verify that this rule holds by showing that disjunction commutes, that it associates, and that {AN$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$.

So, first we need to find equivalent formulas to each of the relevant formulas here. The formulas contain only disjunction symbols and literals (lower case letters or the negations of lower case letters). I use Polish notation.

CKcnt is logically equivalent to ANKcnt, since Cxy is logically equivalent to ANxy. ANKcnt is logically equivalent to "AANcNnt" by the Petrus Hispanus law which says that NKxy is logically equivalent to ANxNy.

KhNs gives us "h" and "Ns".

CKhNAscp is logically equivalent to ANKhNAscp which is logically equivalent to AANhNNAscp by laws previously mentioned by name. By the double negation law which says that NNx is logically equivalent to x, we then have "AANhAscp".

KnNt gives us "n" and "Nt". Thus, I'll precede as follows:

assumption 1 AANcNnt
assumption 2 h
assumption 3 Ns
assumption 4 AANhAscp
assumption 5 n
assumption 6 Nt
R 4, 2     7 AAscp ("Nh" and "h")
R 7, 3     8 Acp (Ns, s... I'll just list one letter hereafter)
R 1, 5     9 ANct  (n)
R 9, 6    10 Nc  (t)
R 8, 10   11 p.  (c)

Here's another proof:

assumption 1 AANcNnt
assumption 2 h
assumption 3 Ns
assumption 4 AANhAscp
assumption 5 n
assumption 6 Nt
R 4, 1     7 AAAANhsNntp (c)
R 7, 2     8 AAAsNntp (h)
R 8, 3     9 AANntp (s)
R 9, 5    10 Atp  (n)
R 10, 6   11 p.  (t)

There does exist a more general resolution rule S here, which would give us a shorter proof:

assumption 1 AANcNnt
assumption 2 h
assumption 3 Ns
assumption 4 AANhAscp
assumption 5 n
assumption 6 Nt
S 4, 2, 3  7 Acp (h, s)
S 1, 5, 6  8 Nc (n, t)
S 7, 8     9 p.  (c)