# C logical consequence of S iff S union {-C} UNSAT

I'm trying to do the following demonstration:

(C and S are CNF) C is a logical consequence of S iff. S u {-C} UNSAT

And I did the following:

C is a logical consequence of S iff. S u {-C} UNSAT iff.

for all interpretation I that SAT S -> I SAT C iff.

for all I, eval_I(S) = 1 -> eval_I(C) = 1 iff.

for all I, -eval_I(S) = 1 or eval_I(C) = 1 iff.

for all I, eval_I(S) = 0 or eval_I(C) = 1 iff...

And I got stuck right there. Any clues? Thaks!

You need to apply De Morgan at some point. Trying to stick with your notation:

for all interpretations I, I SAT S -> I SAT C
iff
for all interpretations I, not(not(I SAT S -> I SAT C))
iff
for all interpretations I, not(I SAT S and not I SAT C)
iff
for all interpretations I, not(I SAT S and I SAT -C)
iff
not exists interpretation I, (I SAT S and I SAT -C)
iff
not exists interpretation I, I SAT (S u {-C})
iff
not SAT (S u {-C})
iff
UNSAT (S u {-C})