Section 6.14 前束范式
Objectives: 前束范式的定义
- 量词都在括号的前面，括号里面不含量词的一阶逻辑公式叫前束范式
- \(\displaystyle \forall x \exists y \forall z \cdots \forall t ( {\color{Blue}{\cdots}} ) \)
- 任何一阶逻辑公式都有和它等值的前束范式
Objectives: 求前束范式的步骤
- 应用换名规则把能换的变量名字都换掉
- 利用量词否定等值式把否定号移到量词的后面
- 利用量词辖域扩张等值式把所有量词都提到括号外面
Exercises Exercises
1.
求下面公式的前束范式:
\begin{equation*}
\forall x F(x) \wedge \neg \exists x G(x)
\end{equation*}
Hint 1 换名规则
Hint 2 量词否定等值式
Hint 3 x辖域的扩张
Hint 4 y辖域的扩张
Solution
\begin{equation*}
\forall x F(x) \wedge \neg \exists y G(y)
\end{equation*}
\begin{equation*}
\forall x F(x) \wedge \forall y \neg G(y)
\end{equation*}
\begin{equation*}
\forall x (F(x) \wedge \forall y \neg G(y))
\end{equation*}
\begin{equation*}
\forall x \forall y(F(x) \wedge \neg G(y))
\end{equation*}
\begin{equation*}
\forall x \forall y(F(x) \wedge \neg G(y))
\end{equation*}
2.
求下面公式的前束范式:
\begin{equation*}
\forall x F(x) \vee \neg \exists x G(x)
\end{equation*}
Hint 1 应用量词否定的等值式
Hint 2 应用换名规则
Hint 3 x辖域扩张
Hint 4 y辖域扩张
Solution
\(\forall x F(x) \vee \forall x \neg G(x)\)
\(\forall x F(x) \vee \forall y \neg G(y)\)
\(\forall x (F(x) \vee \forall y \neg G(y))\)
\(\forall x \forall y(F(x) \vee \neg G(y))\)
\(\forall x \forall y(F(x) \vee \neg G(y))\)
3.
求下面公式的前束范式:
\begin{equation*}
\forall x F(x) \imp \exists x G(x)
\end{equation*}
Hint 1 换名规则
Hint 2 去箭头
Hint 3 量词否定等值式
量词辖域扩张
\(\forall y F(y) \imp \exists x G(x)\)
\(\neg \forall y F(y) \vee \exists x G(x)\)
\(\exists y \neg F(y) \vee \exists x G(x)\)
\(\exists y \exists x ( \neg F(y) \vee G(x))\)