Mathematica If-then vs. Implies

Question

I am new to Mathematica(v8) and am using it to program propositional logic.

I'm wondering what the difference is between the If and the Implies operators. For example,
both If[p,q] and Implies[p,q] return q for p=True (as expected).

But when I try to obtain SatisfiabilityInstances, I get the following:

SatisfiabilityInstances[If[p, q], {p, q}]
(*
  {{True, True}}
*)  

unless I ask it for more instances:

SatisfiabilityInstances[If[p, q], {p, q}, All]

SatisfiabilityInstances::boolv: "If[p,q] is not Boolean valued at {False,True}.

However:

SatisfiabilityInstances[Implies[p, q], {p, q}, All]   

returns the expected out of:

(* {{True, True}, {False, True}, {False, False}} *)

What is causing this difference in the outputs?

Answer 1

It is what it said -- If is not Boolean, i.e. it returns not only true or false. Try If[False,True] and you'll see no result. If[a,b,c,d] can return any b, c and d, not only Boolean, for example If[True,2] returns 2. So, If is for branching (even being functional) while Implies is a normal Boolean function.

P.S. Ah, Implies also can return 2. So the difference is that If[False,True] returns nothing, so SatisfiabilityInstances function can't find true area.

P.P.S. More precisely, if the first argument of If[] is False then it returns it's third argument. When it is absent, it returns nothing.

Answer 2

You may try:

SatisfiabilityInstances[If[p, q, Not[q]], {p, q}, All]