How to get an “indirect implicant” in propositional logic

Question

I am trying to solve a problem in propositional logic, which I do not think I have ever seen, anywhere described. I post it here to find out if it seems to have a standard solution for it.

Problem: Considering the propositional executable logical formula F and the sentence p found in F , it is determined whether there exists an executable propositional formula phi that does not contain p such that

 phi => (F => p) 

and if so, specify such phi.

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

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

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

Then the solution is phi paris or lyon , as it follows from this (F => france)

(Update: actually the exact solution (paris or lyon) and not berlin , because we did not indicate anything that these sentences are mutually exclusive, therefore paris and berlin (or lyon and berlin ) can be true at the same time and implies contradiction.In the present, from the corresponding background knowledge, the solution would be simplified to paris or lyon ).

This is similar to the problem of finding the implicant for the formula (F => p) , but it is not the same as a simple implicant may contain p (and in fact a simple implicant is just p ).

Again, I post it here in the hope that someone with a lot of experience will look at it and say, “ah, but this is just a variant of the problem.” That would be ideal, as it would allow me to use existing algorithms (in particular, feasibility) and concepts.

Also, just for additional information, I'm actually trying to solve this for equality logic, i.e. propositional logic, where sentences are equalities. This, of course, is more complicated, but a propositional case can be a good step.

Thank you 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 operators:

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

F can be expanded by simplifying the values => :

 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 push forward through F consequences, we will make 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)) 

Further 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 for 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 is my own decision. I posted a question about finding out about a standard solution, but maybe it is not.

• Convert F to the equivalent formula DNF (Disjunctive Normal Form), i.e. the conjunction conjunction F1 or ... or Fn , where each Fi is a conjunctive sentence. A conjunctive sentence is a conjuncture of literals, where a literal is either a sentence or its negation. Converting a formula to DNF is a standard procedure.

• For each clause 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 was the only clause in DNF F , then if inputs(Fi) , we need p so that the truth value output(Fi) ( neutral means that it can in any case) for F to be stored.

• The trick, of course, is that Fi , as a rule, will not be the only disjoint. For a given disjunct Fi without output true , there may exist a disjunction Fj with a separate output such that ìnputs(Fj) and inputs(Fi) are feasible, i.e. There is an assignment to the inputs Fi that satisfy Fj , and therefore suppose that p is false, while preserving F Therefore, we call the clauses the output true G1, ..., Gk and disjuncts with the output false or neutral H1, ..., Hl and define phi as

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

Then phi is a solution because it does not contain p and implies F => p . It does not contain p , because it is formed from inputs , which does not 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 clauses in DNF F only Gi have a chance to hold true (all their literals, but p already known). Since they all contain p , if F true, then it must be such that p also holds.

Let's see how this controls the given example.

DNF

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

is an

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

Therefore, we have

• G1 equal to not berlin and france
• H1 equals 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

 (lyon or paris) and not berlin 

The presence of not berlin in a solution is not intuitive. This is because F assumes that more than one of berlin , paris and lyon will be true at the same time. Therefore, requiring that either paris or lyon be true, it also requires not berlin , or else france and not france will be implied. If you have background knowledge that claims that no more than one variable will be true at a time, the solution will be just lyon or paris , since this automatically means not berlin .