How to obtain an "indirect implicant" in propositional logic

Question

I am trying to solve a problem in propositional logic that I don't think I have ever seen described anywhere. I am posting it here to see if someone has a hopefully standard solution for it.

Problem: given a propositional satisfiable logic formula F and a proposition p occurring in F, determine whether there is a satisfiable propositional formula phi not containing p such that

phi => (F => p)

and if so, provide such a phi.

For intuition, I would call phi an "indirect implicant of p wrt F", because it needs to imply p without mentioning p. Instead, it mentions other propositions that affect p through F.

Here's an example, where 'france', 'lyon', 'paris' and 'berlin' are all propositions:

F is "paris => france and lyon => france and berlin => not france"

p is "france"

Then a solution phi is paris or lyon, since that implies (F => france)

(Update: actually the precise solution is (paris or lyon) and not berlin because we did not state anywhere that these propositions are mutually exclusive, so paris and berlin (or lyon and berlin) could both be true at the same time and imply a contradiction. In the present of appropriate background knowledge the solution would be simplified to paris or lyon).

It resembles the problem of finding an implicant for the formula (F => p), but it is not the same since a simple implicant can contain p (and in fact the prime implicant is simply p).

Again, I am posting it here in the hope that someone with more experience looks at it and says: "ah, but that's just a variant of problem such and such". That would be ideal as it would allow me to leverage existing algorithms (particularly satisfiability) and concepts.

Also, just for extra information, I am actually trying to solve this for equality logic, that is, propositional logic where propositions are equalities. That's of course more complex, but the propositional case may be a good stepping stone.

Thanks for your time.

Answer 1

Given your example

F is "paris => france and lyon => france and berlin => not france"

p is "france"

Where F has 4 statements:

F1 = paris
F2 = france and lyon
F3 = france and berlin
F4 = not france

F can be decomposed, through simplifying implications =>:

F1-2: "paris => france and lyon" = "(not paris) or (france and lyon)"

F2-3: "france and lyon => france and berlin" = "(not france or not lyon) or (france and berlin)"

F3-4: "france and berlin => not france" = "(not france or not berlin) and (not france)"

And if we forward-chain through F implications, we will be doing reasoning:

Reason(F): not (not (not F1 or F2) or F3) or F4

not (not (not paris or (france and lyon)) or (france and berlin)) or (not france)

So, we have the following solutions:

S1: not france

S2: not (not (not F1 or F2) or F3):
     not (not (not paris or (france and lyon)) or (france and berlin))

Next we can evaluate p where:

p: france => france = TRUE

S1 = not france = not TRUE = FALSE ~ not applicable

S2 = not (not (not paris or (france and lyon)) or (france and berlin))

   = not (not (not paris or (TRUE and lyon)) or (TRUE and berlin))

   = not (not (not paris or lyon) or berlin)

   = not ((paris AND not lyon) or berlin)

   = not (paris AND not lyon) AND not berlin

   = not (paris AND not lyon) AND not berlin

   = (not paris OR lyon) AND not berlin

So, for p to be TRUE in F you need these conditions to be TRUE:

pF1 AND pF2:

pF1 = (not paris OR lyon) = (paris,lyon) in { (F,F), (F,T), (T,T) }

pF2 = not berlin => berlin = FALSE

Answer 2

Here's my own solution. I had posted the question hoping to learn of a standard solution, but perhaps there is not one.

1. Convert F to an equivalent DNF formula (Disjunctive Normal Form), that is, a disjunction of conjunctions F1 or ... or Fn, where each Fi is a conjunctive clause. A conjunctive clause is a conjunction of literals, where a literal is either a proposition or its negation. Conversion of a formula to DNF is a standard procedure.

2. For each disjunct Fi. It is in one of three forms:

   • L1 and ... and Lmi and p
   • L1 and ... and Lmi and not p
   • L1 and ... and Lmi (p does not occur in it).

   Let inputs(Fi) be the conjunction L1 and ... and Lmi, and output(Fi) be true, false, and neutral respectively.

   The intuition is that, if Fi were the only disjunct in the DNF of F, then if inputs(Fi) holds we need p to have the truth value output(Fi) (neutral meaning it could go either way) for F to hold.

3. The catch is, of course, that Fi will typically not be the only disjunct. For a given disjunct Fi without output true, there may be a disjunct Fj with a distinct output such that ìnputs(Fj) and inputs(Fi) is satisfiable, that is, there is an assignment to the inputs of Fi that satisfy Fj as well, and therefore admit p to be false while still satisfying F. We therefore name the disjuncts with output true G1, ..., Gk and disjuncts with output false or neutral H1, ..., Hl, and define phi to be

   (inputs(G1) or ... or inputs(Gk)) and not (inputs(H1) or ... or inputs(Hl))
   

Then phi is the solution because it does not contain p and implies F => p. It does not contain p because it is formed out of inputs, defined not to contain p. It implies F => p because it satisfies at least one of the inputs(G_) and does not satisfy any of the inputs(H_). This means that, of all the disjuncts in the DNF of F, only the Gi's have a chance of holding true (all their literals but p are already known to be satisfied). Because they all contain p, if F is true then it must be the case that p holds as well.

Let's see how this manages the example given.

The DNF of

paris => france and lyon => france and berlin => not france

is

(not berlin and france) or
(not lyon and not paris and not france)

We therefore have

• G1 equal to not berlin and france
• H1equals to not lyon and not paris and not france

so

• inputs(G1) = not berlin
• inputs(H1) = not lyon and not paris

and therefore phi is

not berlin and not (not lyon and not paris)

which is equivalent to

(lyon or paris) and not berlin

The presence of not berlin in the solution is not intuitive. It is there because F admits that more than one of berlin, paris and lyon be true at the same time. So, while requiring that either paris or lyon be true, it also requires not berlin, or otherwise both france and not france would be implied. In the presence of background knowledge stating that at most one variable be true at the same time, the solution would be simply lyon or paris since that would automatically imply not berlin.