如何在命题逻辑中获得"间接含义"

Question

我试图解决命题逻辑中的一个问题,我认为这在任何地方都没有见过.我在这里发帖,看看是否有人有一个希望的标准解决方案.

问题:给定一个命题满足的逻辑式F和命题p中发生F,确定是否有令人满意的命题公式phi不包含 p使得

phi => (F => p)

如果是的话,提供这样的phi.

对于直觉,我会称之为phi"p wrt F的间接含义",因为它需要暗示p而不提p.相反,它提到了影响p through的其他命题F.

这是一个例子,"法国","里昂","巴黎"和"柏林"都是命题:

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

p is "france"

然后解决方案是paris or lyon,因为这意味着(F => france)

(更新:其实准确的解决方案是(paris or lyon) and not berlin因为我们没有在任何地方指出这些主张是相互排斥的,所以paris和berlin(或lyon和berlin)可以都在同一时间真正和暗示的矛盾在本适当的背景知识的解决办法.简化为paris or lyon).

它类似于找到公式的含义的问题(F => p),但它不同,因为一个简单的蕴涵者可以包含p(事实上​​,主要含义是简单的p).

再次,我在这里发帖,希望有经验的人看到它并说:"啊,但这只是问题的变种等等".这将是理想的,因为它将允许我利用现有算法(特别是可满足性)和概念.

另外,仅仅为了获得额外的信息,我实际上是在尝试解决这个问题,即平等逻辑,即命题是等式的命题逻辑.这当然更复杂,但命题案例可能是一个很好的敲门砖.

谢谢你的时间.

Answer 1

鉴于你的例子

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

p is "france"

其中F有4条语句：

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

F可以通过简化含义进行分解=>：

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)"

如果我们通过F影响进行前向链接，我们将进行推理：

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)

所以，我们有以下解决方案：

S1: not france

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

接下来我们可以评估p哪里：

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

因此，要p成为 TRUE，F您需要满足以下条件TRUE：

pF1 AND pF2:

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

pF2 = not berlin => berlin = FALSE