量词的辖域

Section 6.6 量词的辖域

一个量词的指导变元是紧跟在这个量词后面的那个个体变项
在\(\forall x ( {\color{green}{ \cdots}} )\quad \)中\({\color{Blue}{x}}\)是\(\forall \)的指导变元。
在\(\exists y ( {\color{green}{ \cdots}} ) \quad\)中\({\color{Blue}{y}}\)是\(\exists\)的指导变元。
括号里的绿色\(\quad {\color{green}{ \cdots}} \quad \)部分是该量词的辖域，例子如下

紧跟在某个量词和其指导变元后面的括号里的部分称为这个量词的辖域
\(\forall x ( {\color{Blue}{F(x,y) \imp G(x,x)}} ) \quad \) 蓝色的部分就是 \(\forall\)的辖域
\(\forall x ( {\color{Blue}{F(x,y) \imp G(x,x)}} ) \imp \exists y ({\color{green}{H(x) \wedge L(x,y,z)}}) \) 蓝色的部分就是 \(\forall\)的辖域，绿色的部分是\(\exists\)辖域

当量词和指导变元后面的括号里只包含一个谓词而没有任何逻辑运算符时，括号可以省略。此时，量词的辖域就是这个谓词。

例如:\(\forall x ({\color{blue}{F(x)}}) \quad \)可以省略括号写成 \(\quad \forall {\color{blue}{F(x)}} \) \(\quad \forall \quad \)的辖域就是\({\color{blue}{F(x)}}\)。

出现在两个不同辖域的变项，即使它们的字母相同，也是两个相互独立的变项。

\(\forall {\color{Blue}{x}} ( {\color{Blue}{F(x,y) \imp G(x,x)}} ) \imp \exists {\color{green}{y}} ({\color{green}{H(x) \wedge L(x,y,z)}}) \)

在上面的例子中蓝色的x和绿色的x是两个不同的变项，蓝色的y和绿色的y也是不同的变项

把一个一阶逻辑公式中各个辖域里所有的约束出现变项连同其相应的指导变元都换成在整个公式中从来没出现过的字母称为换名规则
换名前后的两个公式等值
例如\(\quad \forall x F(x,y) \quad\) x是指导变元，同时在\(\forall\)的辖域里约束出现一次，可以把这两处x换成除y以外的任何字母。
\(\displaystyle \quad \forall x F(x,y) \Iff \forall t F(t,y) \Iff \forall k F(k,y) \)

请利用换名规则使下面公式中不存在同名的指导变元

\begin{equation*} \forall x F(x) \wedge \neg \exists x G(x) \end{equation*}

\begin{equation*} \forall x F(x) \wedge \neg \exists y G(y) \end{equation*}

利用换名规则使下面的一阶逻辑公式里同名变项不能既约束出现又自由出现

\(\forall x F(x,y,z) \imp \exists y G(x,y,z) \)

识别出蓝色和绿色两个辖域

\(\forall {\color{Blue}{x}} {\color{Blue}{F(x,y,z)}} \imp \exists {\color{green}{y}} \color{green}{G(x,y,z)} \)

x在第一个辖域里约束出现，在第二个辖域里自由出现，因此需要用换名规则把约束出现的x换成整个公式里从未出现的字母t

y在第一个辖域里自由出现，在第二个辖域里约束出现，因此需要用换名规则把约束出现的y换成整个公式里从未出现的字母w

z在两个辖域里都自由出现，不需要换

\(\forall t F(t,y,z) \imp \exists w G(x,w,z) \)