1

so I can't figure out something when using the resolution proof system.

We are given: {¬a → ¬b, b} on a

what I can't figure out is why: ¬a → ¬b becomes a ∨ ¬b

I understand it becomes an ∨, but why does ¬a get changed it to a?

Thanks.

Javanoob33
  • 29
  • In what sense "$¬a → ¬b$ becomes $a \lor b$" ? In propisitional logic we prove that : $a → b$ is equivalent to : $\lnot a \lor b$. Thus, $\lnot a → b$ becomes : $\lnot \lnot a \lor b$ which, by double negation, is : $a \lor b$. – Mauro ALLEGRANZA Jun 12 '14 at 10:15
  • I'm looking at the answer and the first step (converting into CNF) it changes it from ¬a→¬b into a∨b .

    So basically they've skipped a step?

    So I'm a little unsure, can you explain why ¬a→b becomes : ¬¬a∨b ? Thanks

     – Javanoob33 Jun 12 '14 at 10:17
  • Sorry that's a little bit confusing. Is this what you mean? → is implication, therefore when a is false and b is true.

    Therefore to satisfy this, we add a ¬ onto a, which then becomes ¬¬a and then double negation rules this out?

     – Javanoob33 Jun 12 '14 at 10:22
  • $a→b$ is equivalent to $¬a∨b$ : check with truth table. The cases are : (i) $b$ True; then $a→b$ is True and also $¬a∨b$ is. When (ii) $b$ False and $a$ False, $a→b$ is True and $¬a∨b$ also is ($True \lor False$ is False). Lastly (iii) : $b$ False and $a$ True, in which case $a→b$ is False; but in this case $¬a∨b$ is $False \lor False$ which is is False. Thus, all cases are covered and they are equivalent. – Mauro ALLEGRANZA Jun 12 '14 at 10:23
  • Sorry I'm not really good with this stuff, would you be able to explain it in laymans terms (someone with no idea). lol thanks – Javanoob33 Jun 12 '14 at 10:25
  • yeah I understand the truth table. I'm just still unsure on how ¬a → ¬b becomes a ∨ b – Javanoob33 Jun 12 '14 at 10:29
  • But in order to avoid misunderstanding ... See your first comment : it is not true that you can "convert" $¬a→¬b$ into $a∨b$. Check the statement of the problem, because (all my comment amount to this) : $¬a→¬b$ is $a \lor \lnot b$. – Mauro ALLEGRANZA Jun 12 '14 at 10:30
  • @MauroALLEGRANZA and OP, but why did the $b$ lose its negation? it should've been $a \lor \lnot b$ – tpb261 Jun 12 '14 at 10:30
  • sorry that was a typo. I understand they amount to that, but I'm just not following as to how you attain that. – Javanoob33 Jun 12 '14 at 10:32
  • @tpb261 - thanks for your comment. It is asked in my first comment about OP's : "what I can't figure out is why: ¬a → ¬b becomes a ∨ b". He is right in his doubt : it does not. – Mauro ALLEGRANZA Jun 12 '14 at 10:32
  • The resolution method works with formulas in conjunctive normal form (CNF, or, equivalently, with sets of clauses, where each clause is a disjunction of literals). Such formulas don't contain the implication connective. So, in order to apply resolution in the presence of $\to$ (or anything else that's not in CNF), there must be a preliminary step converting the data to CNF. You should look at your source for resolution to see how this preliminary step is handled; that should include converting $\neg a\to\neg b$ to $a\lor\neg b$. – Andreas Blass Jun 12 '14 at 12:11

2 Answers2

1

You have to check that $\lnot a → \lnot b$ is equivalent to $a \lor \lnot b$ via truth table.

I'll details the four cases entering the truth-value for $a$ and $b$.

(i) : $T-T$

In this case $\lnot a → \lnot b$ is $F \rightarrow F$ which, by truth-functional definition of $\rightarrow$ is $T$.

While $a \lor \lnot b$ is $T \lor F$, which also is $T$.

(ii) : $T-F$

In this case $\lnot a → \lnot b$ is $F \rightarrow T$, which is $T$.

While $a \lor \lnot b$ is $T \lor T$, which again is $T$.

(iii) : $F-T$

In this case $\lnot a → \lnot b$ is $T \rightarrow F$, which is $F$.

But $a \lor \lnot b$ is $F \lor F$, which is $F$ also.

Finally :

(iv) : $F-F$

In this case $\lnot a → \lnot b$ is $T \rightarrow T$, which is $T$.

While $a \lor \lnot b$ is $F \lor T$, which is $T$.

Having covered all possible cases, we can see that in each case the two formulae has the same truth value; thus, they are equivalent.

Comment

The "brief" explanation is that

$a → b$ is equivalent to $\lnot a \lor b$.

Thus, starting from $\lnot a → \lnot b$ we get : $\lnot \lnot a \lor \lnot b$.

Then we apply double negation to rewrite it as :

$a \lor \lnot b$.

See Conjunctive normal form for the explanation of the method, which amounts to :

Every propositional formula can be converted into an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: the double negative law, De Morgan's laws, and the distributive law.

See example regarding : Convert to negation normal form.

Mauro ALLEGRANZA
  • 94,169
1

Given a formal language and being $\alpha$ and $\beta$ two formulas, the notation $\alpha \vee \beta$ is normally presented as a convention for writting $¬\alpha \rightarrow \beta $. If you define $\alpha \equiv a$ and $\beta \equiv ¬ b$, then $\ ¬a \rightarrow ¬b$ is equivalent to $\ ¬\alpha \rightarrow \beta$ is equivalent to $\alpha \vee \beta$ is equivalent to $a \vee ¬b$.

Also, for convince yourself that $\alpha \vee \beta$ and $¬\alpha \rightarrow \beta$ are equivalent formulas and that I'm not cheating you, you can compare the truth table of the first one with the truth table of the second one and verify that they are the same one.

Daniel Muñoz Parsapoormoghadam
  • 248