前束范式 Prenex normal form ——贾林杰.

Presentation on theme: "前束范式 Prenex normal form ——贾林杰."— Presentation transcript:

1 前束范式 Prenex normal form ——贾林杰

2 CONTENT 1 2 3 定义——DEFINITION 转化——CONVERSION 应用——USE PRENEX NORMAL FORM
前束范式 1 定义——DEFINITION 2 CONTENT 转化——CONVERSION 3 应用——USE 前束范式 ——维基百科

3 PART I 前束范式的定义

4 对于一个谓词逻辑公式，如果被写做量词和约束变量在前，无量词的部分在后的话，那么这个式子就被叫做前束范式。
(1) 对于一个谓词逻辑公式，如果被写做量词和约束变量在前，无量词的部分在后的话，那么这个式子就被叫做前束范式。 (1)Prenex normal form ——维基百科

5 前束范式的定义 一个简单的例子： ∀𝑥 𝑥 2 ≥0 ∧∀𝑦 𝑦 2 ≥0 不是前束范式 ∀𝑥∀𝑦 𝑥 2 ≥0∧ 𝑦 2 ≥0 是前束范式

6 PART II 前束范式的转化 每个一阶逻辑算式都可以被转化为一个与之等价的前束范式。 Every first-order formula is logically equivalent (in classical logic) to some formula in prenex normal form.

7 (∀𝑥 𝑃)∧𝑄 ⇔ ∀𝑥(𝑃∧𝑄) (∀𝑥 𝑃)∨𝑄 ⇔ ∀𝑥(𝑃∨𝑄) (∃𝑥 𝑃)∧𝑄 ⇔ ∃𝑥(𝑃∧𝑄)
前束范式的转换 “和”(conjunction)与“或”(disjunction) (∀𝑥 𝑃)∧𝑄 ⇔ ∀𝑥(𝑃∧𝑄) (∀𝑥 𝑃)∨𝑄 ⇔ ∀𝑥(𝑃∨𝑄) (∃𝑥 𝑃)∧𝑄 ⇔ ∃𝑥(𝑃∧𝑄) (∃𝑥 𝑃)∨𝑄 ⇔ ∃𝑥(𝑃∨𝑄) Q：这些公式的运用是否有要求呢？

8 前提：对于已经在P出现的变量x不能出现在Q中， 其他的未被约束的自由变元则不做要求。
前束范式的转换 前提：对于已经在P出现的变量x不能出现在Q中， 其他的未被约束的自由变元则不做要求。 一个例子：

9 ¬∀𝑥𝑃⇔∃𝑥¬𝑃 ¬∃𝑥𝑃⇔∀𝑥¬𝑃 非（negation）： (∀𝑥𝑃)→𝑄 ⇔ ¬(∀𝑥𝑃)∨𝑄 ⇔ ∃𝑥¬𝑃 ∨𝑄⇔ ∃𝑥 ¬𝑃∨𝑄
前束范式的转换 利用 P → Q ⇔ ¬P ∨ Q; 非（negation）： ¬∀𝑥𝑃⇔∃𝑥¬𝑃 ¬∃𝑥𝑃⇔∀𝑥¬𝑃 思考在已知关于“和”,“或” ,“非”的转换方式的情况下怎么推导关于蕴含的转换方式： 举例：将 （∀x P) → Q 转换为它的前束范式 Answer: (∀𝑥𝑃)→𝑄 ⇔ ¬(∀𝑥𝑃)∨𝑄 ⇔ ∃𝑥¬𝑃 ∨𝑄⇔ ∃𝑥 ¬𝑃∨𝑄 ⇔ ∃𝑥 (𝑃→ 𝑄) 𝑃→𝑄 ⇔ ¬𝑃∨𝑄 (1) ¬∃𝑥𝑃⇔∀𝑥¬𝑃 (2) ∃𝑥 𝑃 ∨𝑄 ⇔ ∃𝑥 𝑃∨𝑄 (3) 用到的公式：

10 𝑃→ ∃𝑥𝑄 ⇔ ∃𝑥 𝑃→𝑄 𝑃→ ∀𝑥𝑄 ⇔ ∀𝑥 𝑃→𝑄 ∃𝑥𝑃 →𝑄 ⇔ ∀𝑥 𝑃→𝑄 (∀𝑥𝑃)→𝑄 ⇔ ∀𝑥(𝑃→𝑄)
前束范式的转换 运用同样的方法我们可以得到： 蕴含(Implication): 𝑃→ ∃𝑥𝑄 ⇔ ∃𝑥 𝑃→𝑄 𝑃→ ∀𝑥𝑄 ⇔ ∀𝑥 𝑃→𝑄 ∃𝑥𝑃 →𝑄 ⇔ ∀𝑥 𝑃→𝑄 (∀𝑥𝑃)→𝑄 ⇔ ∀𝑥(𝑃→𝑄) 同样地，需要满足x仅在P（Q）中出现，Q（P）中不含有x!!

11 前束范式的转换 简单的练习 (1)(𝑃∨∃𝑥𝑄 𝑥 )→ ∀𝑧 𝑅(𝑧) (2)∀𝑥𝑃(𝑥)→∃𝑥𝑄(𝑥)

12 ⇔ ∀𝑧 ∃𝑥 𝑃∨𝑄 𝑥 →𝑅 𝑧 ⇔ ∀𝑧(𝑃∨∃𝑥𝑄 𝑥 )→𝑅(𝑧))
Answer： (1)(𝑃∨∃𝑥𝑄 𝑥 )→∀𝑧 𝑅(𝑧) ⇔ ∀𝑧 ∃𝑥 𝑃∨𝑄 𝑥 →𝑅 𝑧 ⇔ ∀𝑧(𝑃∨∃𝑥𝑄 𝑥 )→𝑅(𝑧)) ⇔ ∀𝑧∀𝑥(𝑃∨𝑄(𝑥)→𝑅(𝑧)) 用到的公式： P→ ∀𝑥𝑄 ⇔ ∀𝑥 𝑃→𝑄 (1) 𝑃∨∃𝑥𝑄 𝑥 ⇔∃𝑥 𝑃∨𝑄 𝑥 (2) ∃𝑥𝑃 →𝑄 ⇔ ∀𝑥 𝑃→𝑄 3 𝑃→𝑄 ⇔ ¬𝑃∨𝑄(4) ¬∃𝑥𝑃⇔∀𝑥¬𝑃 (5) 2 ∀𝑥𝑃 𝑥 →∃𝑥 𝑄 𝑥 ⇔ ¬∀𝑥𝑃(𝑥)∨∃𝑥𝑄(𝑥)⇔ ∃𝑥¬𝑃 𝑥 ∨∃𝑥𝑄 𝑥 ⇔∃𝑥(𝑃(𝑥)→𝑄(𝑥))⇔ ∃𝑥(¬𝑃(𝑥)∨𝑄(𝑥))

13 回顾对“和”与“或”转化时讨论的一个例子：
前束范式的转换 回顾对“和”与“或”转化时讨论的一个例子： Q:那么怎么将其转换为前束范式呢？？

14 前束范式的转换 自由变元和约束变元 给定一个谓词公式如∀x P(x) ∨ Q(y), 把量词后边所跟的x叫做量词的指导变元。在量词的作用域P(x)中，x都被量词的指导变元所约束，称为约束变元。（简单理解就是量词后边的那个在量词所作用的范围中都叫约束变元）。那么不受约束的y就叫做自由变元 拿我们的问题来举例： ∃x的作用范围是 所以这里的x是约束变元， 而x=0中的x不受约束，所以这个x是自由变元。

15 前束范式的转换 换名规则与代入规则 约束变元的换名规则： 对于约束变元可以换名，其更改的变元名称范围是量词中的指 导变元，以及该量词作用域中所出现的该变元，在公式的其余 部分不变。 换名时一定要更改为作用域中没有出现的变元名称。 自由变元的代入规则： 对于谓词公式的自由变元，可以代入，代入时需对公式中出现 该自由变元的每一处进行。 用以代入的变元与原公式中所有变元的名称不能相同

16 因此对于被约束的变量x，我们可以利用换名规则将其更名为y，于是我们就得到了：
前束范式的转换 因此对于被约束的变量x，我们可以利用换名规则将其更名为y，于是我们就得到了： 同理对于前边的练习题： ∀𝑥 𝑃(𝑥) → ∃𝑥 𝑄(𝑥) 我们也可以有换名后得到：∃𝑥 ∃𝑦(𝑃(𝑥) → 𝑄(𝑦)) 一个公式的前束范式不是唯一的

17 (1)¬[∀𝑥∃𝑦𝐹(𝑢, 𝑥, 𝑦)→∃𝑥(¬∀𝑦𝐺(𝑦, 𝑣)→𝐻(𝑥))]
前束范式的转换 前束范式的转换 换名公式练习 (1)¬[∀𝑥∃𝑦𝐹(𝑢, 𝑥, 𝑦)→∃𝑥(¬∀𝑦𝐺(𝑦, 𝑣)→𝐻(𝑥))] (2)∀𝑥((∃𝑦𝑅 𝑥, 𝑦 ∧∀𝑦¬𝑆 𝑥, 𝑦 )→¬(∃𝑦𝑄(𝑥, 𝑦)∧𝑃))

18 ¬[∀𝑥∃𝑦𝐹(𝑢, 𝑥, 𝑦)→∃𝑥(¬∀𝑦𝐺(𝑦, 𝑣)→𝐻(𝑥))]
前束范式的转换 前束范式的转换 ¬[∀𝑥∃𝑦𝐹(𝑢, 𝑥, 𝑦)→∃𝑥(¬∀𝑦𝐺(𝑦, 𝑣)→𝐻(𝑥))] ¬∃𝑥[∀𝑦¬𝐹(𝑢, 𝑥, 𝑦)∨(∀𝑦𝐺(𝑦, 𝑣)∨𝐻(𝑥))] 𝑧 ¬∃𝑥[∀𝑦¬𝐹(𝑢, 𝑥, 𝑦)∧(∀𝑧𝐺 𝑧, 𝑣 ∧𝐻 𝑥 )] ⇔∀𝑥[∃𝑦𝐹(𝑢, 𝑥, 𝑦)∧∃𝑧¬𝐺(𝑧, 𝑣)∧¬𝐻(𝑥)] ⇔∀𝑥∃𝑦∃𝑧(𝐹(𝑢, 𝑥, 𝑦)∧¬𝐺(𝑧, 𝑣)∧¬𝐻(𝑥)) P→ ∀𝑥𝑄 ⇔ ∀𝑥 𝑃→𝑄 1 𝑃∧∃𝑥𝑄 𝑥 ⇔∃𝑥 𝑃∧𝑄 𝑥 2 (∃𝑥 𝑃)∧𝑄 ⇔ ∃𝑥(𝑃∧𝑄)(2) 用到的公式：

19 ∀𝑥((∃𝑦𝑅(𝑥, 𝑦)∧∀𝑦¬𝑆(𝑥, 𝑦))→¬(∃𝑦𝑄(𝑥, 𝑦)∧𝑃))
前束范式的转换 前束范式的转换 ∀𝑥((∃𝑦𝑅(𝑥, 𝑦)∧∀𝑦¬𝑆(𝑥, 𝑦))→¬(∃𝑦𝑄(𝑥, 𝑦)∧𝑃)) w v ∀𝑥((∃𝑦𝑅(𝑥, 𝑦)∧∀𝑤¬𝑆(𝑥, 𝑤))→¬(∃𝑣𝑄(𝑥, 𝑣)∧𝑃)) ⇔ ∀𝑥(∃𝑦∀𝑤(𝑅(𝑥, 𝑦)∧¬𝑆(𝑥, 𝑤))→∀𝑣(¬𝑄(𝑥, 𝑣)∨¬𝑃)) ⇔ ∀𝑥∀𝑦∃𝑤∀𝑣((𝑅(𝑥, 𝑦)∧¬𝑆(𝑥, 𝑤))→(¬𝑄(𝑥, 𝑣)∨¬𝑃)) ∀𝑥 𝑃 ∧𝑄 ⇔ ∀𝑥 𝑃∧𝑄 1 ∃𝑥 𝑃 ∧𝑄 ⇔ ∃𝑥 𝑃∧𝑄 2 ∃𝑥 𝑃 ∧𝑄 ⇔ ∃𝑥 𝑃∧𝑄 3 ∃𝑥 𝑃 ∨𝑄 ⇔ ∃𝑥 𝑃∨𝑄 4 𝑃→ ∀𝑥𝑄 ⇔ ∀𝑥 𝑃→𝑄 (5) 用到的公式：

20 关于量词的次序 那么(3)(4)呢？ (1)∃𝑥∃𝑦𝐴(𝑥, 𝑦) ⇔ ∃𝑦∃𝑥𝐴(𝑥, 𝑦)
(2)∀𝑥∀𝑦𝐴(𝑥, 𝑦) ⇔ ∀𝑦∀𝑥𝐴(𝑥, 𝑦) (3)∃𝑥∀𝑦𝐴(𝑥, 𝑦) ⇔ ∀𝑦∃𝑥𝐴(𝑥, 𝑦) (4)∀𝑥∃𝑦𝐴(𝑥, 𝑦) ⇔ ∃𝑦∀𝑥𝐴(𝑥, 𝑦) (1)(2)是正确的 那么(3)(4)呢？

21 假设A(x,y)表示x和y同姓，论域x为甲村的人，论域y为乙村的人
∃𝑥∀𝑦𝐴(𝑥, 𝑦) ：甲村所有人，乙村都有人和他同姓 ∀𝑦∃𝑥𝐴(𝑥, 𝑦)：乙村有一个人，甲村所有人都和他同姓 显然(3)是不成立的,而(4)也同理

22 ∀𝑥∀𝑦𝐴 𝑥,𝑦 →∃𝑦∀𝑥𝐴 𝑥,𝑦 ∃𝑥∀𝑦𝐴 𝑥,𝑦 →∃𝑦∃𝑥𝐴 𝑥,𝑦 ∃𝑦∀𝑥𝐴 𝑥,𝑦 →∀𝑥∃𝑦𝐴 𝜆,𝑦
多个量词存在时一些永真的蕴含式 ∀𝑥∀𝑦𝐴 𝑥,𝑦 →∃𝑦∀𝑥𝐴 𝑥,𝑦 ∃𝑥∀𝑦𝐴 𝑥,𝑦 →∃𝑦∃𝑥𝐴 𝑥,𝑦 ∃𝑦∀𝑥𝐴 𝑥,𝑦 →∀𝑥∃𝑦𝐴 𝜆,𝑦

23 ∀𝑥∀𝑦𝐴 𝑥,𝑦 →∃𝑦∀𝑥𝐴 𝑥,𝑦 ∀𝑥∀𝑦𝐴(𝑥, 𝑦) ⇔ ∀𝑦∀𝑥𝐴(𝑥, 𝑦) 将∀𝑥𝐴(𝑥, 𝑦)看作关于𝑦的谓词𝑃 𝑦
proof ∀𝑥∀𝑦𝐴(𝑥, 𝑦) ⇔ ∀𝑦∀𝑥𝐴(𝑥, 𝑦) 将∀𝑥𝐴(𝑥, 𝑦)看作关于𝑦的谓词𝑃 𝑦 即表示为∀𝑦𝑃 𝑦 ，若成立 则∃𝑦𝑃 𝑦 肯定也成立 即该蕴含式永真 ∃𝑥∀𝑦𝐴 𝑥,𝑦 →∃𝑦∃𝑥𝐴 𝑥,𝑦 同理

24 那么假设这个𝑦为 𝑦 0 , ∀𝑥𝐴 𝑥,𝑦 。则∀𝑥∃𝑦𝐴 𝜆,𝑦 式子中 对于∀𝑥,肯定存在这个 𝑦 0 , 使得∀𝑥𝐴 𝑥,𝑦 成立。
∃𝑦∀𝑥𝐴 𝑥,𝑦 →∀𝑥∃𝑦𝐴 𝜆,𝑦 𝒑𝒓𝒐𝒐𝒇 ∃𝑦∀𝑥𝐴 𝑥,𝑦 成立， 那么假设这个𝑦为 𝑦 0 , ∀𝑥𝐴 𝑥,𝑦 。则∀𝑥∃𝑦𝐴 𝜆,𝑦 式子中 对于∀𝑥,肯定存在这个 𝑦 0 , 使得∀𝑥𝐴 𝑥,𝑦 成立。 则蕴含式正确。

25 ∃𝑥(𝑃(𝑥)∧𝑄(𝑥))≢∃𝑥𝑃(𝑥)∧∃𝑥𝑄(𝑥) ∀𝑥 𝑃 𝑥 ∨𝑄 𝑥 ≢∀𝑥𝑃 𝑥 ∨∀𝑥𝑄 𝑥
简单的了解一些其他的式子 Distributing the Existential Quantifier（量词的分配） ∀𝑥 𝑃 𝑥 ∧𝑄 𝑥 ≡∀𝑥𝑃 𝑥 ∧∀𝑥𝑄 𝑥 ∃𝑥 𝑆 𝑥 ∨𝑅 𝑥 ≡∃𝑥𝑆 𝑥 ∨∃𝑥𝑅 𝑥 ∃𝑥(𝑃(𝑥)∧𝑄(𝑥))≢∃𝑥𝑃(𝑥)∧∃𝑥𝑄(𝑥) ∀𝑥 𝑃 𝑥 ∨𝑄 𝑥 ≢∀𝑥𝑃 𝑥 ∨∀𝑥𝑄 𝑥 ∃𝑥(𝑃(𝑥)→𝑄(𝑥))≢∃𝑥𝑃(𝑥)→∃𝑥𝑄(𝑥) ∀𝑥(𝑃(𝑥)→𝑄(𝑥))≢∀𝑥𝑃(𝑥)→∃𝑥𝑄(𝑥)

26 PART III 前束范式的应用

27 一些证明系统只能处理用前束范式写成的原理。这种概念对于发展算术阶层和分析阶层非常重要。
前束范式的应用 一些证明系统只能处理用前束范式写成的原理。这种概念对于发展算术阶层和分析阶层非常重要。 哥德尔(1)证明他的一阶逻辑完备性的前提是，所有的公式都已经被改写为前束范式。 塔斯基定理。 与几何有关的塔斯基公理(2)(Tarski’s axioms)是一个逻辑系统。该逻辑系统中所有的语言都可以写为全称量词在前，存在量词在后的前束范式。这一事实帮助塔斯基证明了欧几里得几何是可判定的。 (1)哥德尔完备性定理——Gödel's completeness theorem (2)塔斯基公理——Tarski's axioms

28 Come from Wikipedia prenex normal form

29 THANK YOU