可自由代入（个体变项）：修订间差异
无编辑摘要 |
无编辑摘要 |
||
| 第1行： | 第1行： | ||
[[分类:谓词逻辑]] | [[分类:谓词逻辑]]{{DEFAULTSORT:ke3zi4you2dai4ru4}} | ||
{{#seo: | |||
|keywords=自由代入 | |||
|description=本文介绍谓词公式进行项之间代换时可自由代换这一性质的定义、性质，包括其定义在变换中的必要性。 | |||
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}} | |||
|published_time=2023-07-24 | |||
}} | |||
{{InfoBox | {{InfoBox | ||
|name=可自由代入 | |name=可自由代入 | ||
| 第5行： | 第11行： | ||
}} | }} | ||
在一个[[谓词公式]]中，一个[[项（谓词逻辑）|项]]对一个[[个体词（谓词逻辑）|个体变项]]'''可自由代入'''，指将公式中这个个体变项全部出现替换为这个项时，不会影响其语义。 | 在一个[[谓词公式]]中，一个[[项（谓词逻辑）|项]]对一个[[个体词（谓词逻辑）|个体变项]]'''可自由代入'''，指将公式中这个个体变项全部出现替换为这个项时，不会影响其语义。 | ||
不可自由代入的情况包括：这个项代入后，其中至少一个个体变项会落在作用在同名个体变项的量词辖域内，导致这个个体变项的量化情况改变。 | |||
== 定义 == | == 定义 == | ||
| 第11行： | 第18行： | ||
对公式 <math>\phi</math> ，个体变项 <math>x</math> 和项 <math>t</math> ，若对 <math>t</math> 中的每一个个体变项 <math>y</math> ， 个体变项 <math>x</math> 在 <math>\phi</math> 中的每一个自由出现都不在 <math>\forall y</math> 或 <math>\exists y</math> 的辖域内，则称项 <math>t</math> 对个体变项 <math>x</math> 在公式 <math>\phi</math> 中可自由代入( <math>t</math> is free for <math>x</math> in <math>\varphi</math> <ref>https://math.stackexchange.com/q/2938727</ref> )。 | 对公式 <math>\phi</math> ，个体变项 <math>x</math> 和项 <math>t</math> ，若对 <math>t</math> 中的每一个个体变项 <math>y</math> ， 个体变项 <math>x</math> 在 <math>\phi</math> 中的每一个自由出现都不在 <math>\forall y</math> 或 <math>\exists y</math> 的辖域内，则称项 <math>t</math> 对个体变项 <math>x</math> 在公式 <math>\phi</math> 中可自由代入( <math>t</math> is free for <math>x</math> in <math>\varphi</math> <ref>https://math.stackexchange.com/q/2938727</ref> )。 | ||
== 含义 == | |||
可自由代入意味着将这个公式中，这一个体变项的全部出现都代换成这个项，不会出现由于命名冲突导致语义改变的情况。 | |||
若不满足可自由代入的条件，意味着存在名称冲突，此时总是可以通过[[易字]]解决对应冲突。 | |||
因此，在其他涉及代入的讨论中，可以限制给定个体变项和给定项之间满足可自由代入关系，若出现不可自由代入的先进行易字以转化为这种情况，以简化讨论中对符号重复情况的限制。 | |||
== 例子 == | |||
显然，以下几种情况一定都可自由代入。 | |||
# <math>x</math> 在 <math>\phi</math> 中没有自由出现。甚至，<math>x</math> 在 <math>\phi</math> 中没有出现。 | # <math>x</math> 在 <math>\phi</math> 中没有自由出现。甚至，<math>x</math> 在 <math>\phi</math> 中没有出现。 | ||
# <math>t</math> 中没有个体变项。 | # <math>t</math> 中没有个体变项。 | ||
2026年1月4日 (日) 14:28的版本
| 可自由代入 | |
|---|---|
| 术语名称 | 可自由代入 |
| 英语名称 | |
在一个谓词公式中，一个项对一个个体变项可自由代入，指将公式中这个个体变项全部出现替换为这个项时，不会影响其语义。
不可自由代入的情况包括：这个项代入后，其中至少一个个体变项会落在作用在同名个体变项的量词辖域内，导致这个个体变项的量化情况改变。
定义
对公式 [math]\displaystyle{ \phi }[/math] ，个体变项 [math]\displaystyle{ x }[/math] 和项 [math]\displaystyle{ t }[/math] ，若对 [math]\displaystyle{ t }[/math] 中的每一个个体变项 [math]\displaystyle{ y }[/math] ， 个体变项 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中的每一个自由出现都不在 [math]\displaystyle{ \forall y }[/math] 或 [math]\displaystyle{ \exists y }[/math] 的辖域内，则称项 [math]\displaystyle{ t }[/math] 对个体变项 [math]\displaystyle{ x }[/math] 在公式 [math]\displaystyle{ \phi }[/math] 中可自由代入( [math]\displaystyle{ t }[/math] is free for [math]\displaystyle{ x }[/math] in [math]\displaystyle{ \varphi }[/math] [1] )。
含义
可自由代入意味着将这个公式中，这一个体变项的全部出现都代换成这个项，不会出现由于命名冲突导致语义改变的情况。 若不满足可自由代入的条件，意味着存在名称冲突，此时总是可以通过易字解决对应冲突。
因此，在其他涉及代入的讨论中，可以限制给定个体变项和给定项之间满足可自由代入关系，若出现不可自由代入的先进行易字以转化为这种情况，以简化讨论中对符号重复情况的限制。
例子
显然，以下几种情况一定都可自由代入。
- [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中没有自由出现。甚至，[math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中没有出现。
- [math]\displaystyle{ t }[/math] 中没有个体变项。
- [math]\displaystyle{ t }[/math] 中个体变项在 [math]\displaystyle{ \phi }[/math] 中没有对应的量化表达式。
- [math]\displaystyle{ t }[/math] 中的个体变项只有 [math]\displaystyle{ x }[/math] 。