数理逻辑:修订间差异

求闻百科,共笔求闻
添加的内容 删除的内容
(机器人:删除3个模板:Wayback、​Webarchive、​WebCite)
(我来啦, replaced: 參考 → 参考, 語 → 语 (2), 無 → 无, 義 → 义, 圖 → 图, 數 → 数, 靈 → 灵, 倫 → 伦, 論 → 论 (4), 過 → 过, 個 → 个, 資 → 资, 階 → 阶 (2))
第17行: 第17行:
== 数理逻辑论的体系 ==
== 数理逻辑论的体系 ==


数理逻辑的主要分支包括:[[模型论]]、[[证明论]]、[[递归论]]和[[公理化集合论]]。数理逻辑和[[计算机科学]]有许多重合之处,这是因为许多计算机科学的先驱者既是数学家、又是逻辑学家,如[[艾·圖靈]]、[[邱奇]]等。
数理逻辑的主要分支包括:[[模型论]]、[[证明论]]、[[递归论]]和[[公理化集合论]]。数理逻辑和[[计算机科学]]有许多重合之处,这是因为许多计算机科学的先驱者既是数学家、又是逻辑学家,如[[艾·图灵]]、[[邱奇]]等。


[[程式言理|程序语言学]]、[[语义学]]的研究从[[模型论]]衍生而来,而[[程序验证]]中的[[模型检测]]则从模型论衍生而来。
[[程式言理|程序语言学]]、[[语义学]]的研究从[[模型论]]衍生而来,而[[程序验证]]中的[[模型检测]]则从模型论衍生而来。


[[Curry-Howard同构|柯里-霍华德同构]]给出了“证明”和“程序”的等价性,这一结果与[[证明论]]有关,[[直觉主义逻辑]]和[[线性逻辑]]在此起了很大作用。[[λ演算]]和[[组合子逻辑]]这样的演算现在属于理想[[程序语言]]。
[[Curry-Howard同构|柯里-霍华德同构]]给出了“证明”和“程序”的等价性,这一结果与[[证明论]]有关,[[直觉主义逻辑]]和[[线性逻辑]]在此起了很大作用。[[λ演算]]和[[组合子逻辑]]这样的演算现在属于理想[[程序语言]]。
第30行: 第30行:


* [[一阶逻辑|一阶]]公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说,证明集合是原始递归的。实质上,这就是[[哥德尔完全性定理]],虽然那个定理的通常陈述使它与[[算法]]之间的关系不明显。
* [[一阶逻辑|一阶]]公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说,证明集合是原始递归的。实质上,这就是[[哥德尔完全性定理]],虽然那个定理的通常陈述使它与[[算法]]之间的关系不明显。
* 有效的[[一阶逻辑|一阶]]公式的集合是[[不可判定問題|不可计算]]的,也就是说,不存在算法用作检测一條公式是否普遍成立。不,儘管一邏輯不可判定,仍是“半可判定”的,即存在某算法,滿足:对此算法输入一个一阶公式,如果这个一阶公式是普遍有效的,那么算法将在某一时刻停机;如果不是普遍有效的,那么算法将会永远不停地计算下去。然而,即使算法已经运行了亿万年,仍法分辨公式是否有效。换句话说,有效公式的集合是“[[递归可枚举集合]]”。
* 有效的[[一阶逻辑|一阶]]公式的集合是[[不可判定問題|不可计算]]的,也就是说,不存在算法用作检测一條公式是否普遍成立。不,儘管一邏輯不可判定,仍是“半可判定”的,即存在某算法,滿足:对此算法输入一个一阶公式,如果这个一阶公式是普遍有效的,那么算法将在某一时刻停机;如果不是普遍有效的,那么算法将会永远不停地计算下去。然而,即使算法已经运行了亿万年,仍法分辨公式是否有效。换句话说,有效公式的集合是“[[递归可枚举集合]]”。
* 普遍有效的[[二阶逻辑|二阶]]公式的集合甚至不是递归可枚举的。这是[[哥德尔不完全性定理]]的一个结果。
* 普遍有效的[[二阶逻辑|二阶]]公式的集合甚至不是递归可枚举的。这是[[哥德尔不完全性定理]]的一个结果。
* [[勒文海姆-斯科伦定理]]。
* [[勒文海姆-斯科伦定理]]。
第36行: 第36行:
* [[保罗·约瑟夫·科恩]](Paul Cohen)在1963年证明的[[连续统假设]]的[[逻辑独立性|独立性]]。
* [[保罗·约瑟夫·科恩]](Paul Cohen)在1963年证明的[[连续统假设]]的[[逻辑独立性|独立性]]。


== 料 ==
== 料 ==
{{Reflist}}
{{Reflist}}


第54行: 第54行:
{{mathportal}}
{{mathportal}}
* [[逻辑]]
* [[逻辑]]
* [[邏輯的語義]]
* [[邏輯的语义]]
* [[模型]]
* [[模型]]
* [[證明]]
* [[證明]]
* [[遞歸]]
* [[遞歸]]
* [[一逻辑]]
* [[一逻辑]]
* [[相继式演算]]
* [[相继式演算]]
* [[直觉主义逻辑]]
* [[直觉主义逻辑]]
第69行: 第69行:


[[Category:邏輯]]
[[Category:邏輯]]
[[Category:理邏輯| ]]
[[Category:理邏輯| ]]
[[Category:规则|科学]]
[[Category:规则|科学]]