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

第30行：

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

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

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

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

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

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