数理逻辑：修订间差异 - 求闻百科，共笔求闻

第30行：

* [[一阶逻辑|一阶]]公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说，证明集合是原始递归的。实质上，这就是[[哥德尔完全性定理]]，虽然那个定理的通常陈述使它与[[算法]]之间的关系不明显。

* 有效的[[一阶逻辑|一阶]]公式的集合是[[不可判定問題|不可计算]]的，也就是说，不存在算法用作检测一條公式是否普遍成立。不过，儘管一阶邏輯不可判定，仍是“半可判定”的，即存在某个算法，滿足：对此算法输入一个一阶公式，如果这个一阶公式是普遍有效的，那么算法将在某一时刻停机；如果不是普遍有效的，那么算法将会永远不停地计算下去。然而，即使算法已经运行了亿万年，仍无法分辨公式是否有效。换句话说，有效公式的集合是“[[递归可枚举集合]]”。

* 有效的[[一阶逻辑|一阶]]公式的集合是[[不可判定问题|不可计算]]的，也就是说，不存在算法用作检测一条公式是否普遍成立。不过，儘管一阶邏辑不可判定，仍是“半可判定”的，即存在某个算法，满足：对此算法输入一个一阶公式，如果这个一阶公式是普遍有效的，那么算法将在某一时刻停机；如果不是普遍有效的，那么算法将会永远不停地计算下去。然而，即使算法已经运行了亿万年，仍无法分辨公式是否有效。换句话说，有效公式的集合是“[[递归可枚举集合]]”。

* 普遍有效的[[二阶逻辑|二阶]]公式的集合甚至不是递归可枚举的。这是[[哥德尔不完全性定理]]的一个结果。

* [[勒文海姆-斯科伦定理]]。

第54行：

* [[逻辑]]

* [[邏輯的语义]]

* [[邏辑的语义]]

* [[模型论]]

* [[證明论]]

* [[证明论]]

* [[遞歸论]]

* [[递归论]]

* [[一阶逻辑]]

* [[相继式演算]]

* [[直觉主义逻辑]]

* [[完備性]]

* [[完备性]]

第68行：

[[Category:邏輯]]

[[Category:邏辑]]

[[Category:数理邏輯| ]]

[[Category:数理邏辑| ]]

[[Category:规则|科学]]

@@ 第30行： / 第30行： @@
 * [[一阶逻辑|一阶]]公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说，证明集合是原始递归的。实质上，这就是[[哥德尔完全性定理]]，虽然那个定理的通常陈述使它与[[算法]]之间的关系不明显。
-* 有效的[[一阶逻辑|一阶]]公式的集合是[[不可判定問題|不可计算]]的，也就是说，不存在算法用作检测一條公式是否普遍成立。不过，儘管一阶邏輯不可判定，仍是“半可判定”的，即存在某个算法，滿足：对此算法输入一个一阶公式，如果这个一阶公式是普遍有效的，那么算法将在某一时刻停机；如果不是普遍有效的，那么算法将会永远不停地计算下去。然而，即使算法已经运行了亿万年，仍无法分辨公式是否有效。换句话说，有效公式的集合是“[[递归可枚举集合]]”。
+* 有效的[[一阶逻辑|一阶]]公式的集合是[[不可判定问题|不可计算]]的，也就是说，不存在算法用作检测一条公式是否普遍成立。不过，儘管一阶邏辑不可判定，仍是“半可判定”的，即存在某个算法，满足：对此算法输入一个一阶公式，如果这个一阶公式是普遍有效的，那么算法将在某一时刻停机；如果不是普遍有效的，那么算法将会永远不停地计算下去。然而，即使算法已经运行了亿万年，仍无法分辨公式是否有效。换句话说，有效公式的集合是“[[递归可枚举集合]]”。
 * 普遍有效的[[二阶逻辑|二阶]]公式的集合甚至不是递归可枚举的。这是[[哥德尔不完全性定理]]的一个结果。
 * [[勒文海姆-斯科伦定理]]。
@@ 第54行： / 第54行： @@
 {{mathportal}}
 * [[逻辑]]
-* [[邏輯的语义]]
+* [[邏辑的语义]]
 * [[模型论]]
-* [[證明论]]
+* [[证明论]]
-* [[遞歸论]]
+* [[递归论]]
 * [[一阶逻辑]]
 * [[相继式演算]]
 * [[直觉主义逻辑]]
-* [[完備性]]
+* [[完备性]]
 {{-}}
@@ 第68行： / 第68行： @@
 {{Computer Science}}
-[[Category:邏輯]]
+[[Category:邏辑]]
-[[Category:数理邏輯| ]]
+[[Category:数理邏辑| ]]
 [[Category:规则|科学]]