数理逻辑：修订间差异

求闻百科，共笔求闻
交互式浏览历史
添加的内容 删除的内容
可视化wikitext
（修改自此处；原许可：CC BY-SA 3.0［网站升级迁移］）
 
小 （机器人：更改已重定向的分类 逻辑到逻辑学（原分类名经繁简转换））
 

（未显示4个用户的8个中间版本）

第17行： 第17行：
== 数理逻辑论的体系 ==
== 数理逻辑论的体系 ==


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


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


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


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


== 參考資料 ==
== 参考资料 ==
{{Reflist}}
{{Reflist}}


{{Reflist|1}}
{{reflist}}
* {{tsl|en|A. S. Troelstra|}} & {{tsl|en|Helmut Schwichtenberg||H. Schwichtenberg}} (2000). ''Basic Proof Theory'' (Cambridge Tracts in Theoretical Computer Science) (2nd ed.). Cambridge University Press. ISBN 0-521-77911-1.
* {{tsl|en|A. S. Troelstra|}} & {{tsl|en|Helmut Schwichtenberg||H. Schwichtenberg}} (2000). ''Basic Proof Theory'' (Cambridge Tracts in Theoretical Computer Science) (2nd ed.). Cambridge University Press. ISBN 0-521-77911-1.
* {{tsl|en|George Boolos|}} & {{tsl|en|Richard Jeffrey|}} (1989). ''Computability and Logic'' (3rd ed.). Cambridge University Press. ISBN 0-521-00758-5.
* {{tsl|en|George Boolos|}} & {{tsl|en|Richard Jeffrey|}} (1989). ''Computability and Logic'' (3rd ed.). Cambridge University Press. ISBN 0-521-00758-5.
第47行： 第47行：
== 外部链接 ==
== 外部链接 ==


* [https://web.archive.org/web/20050105093147/http://www.uni-bonn.de/logic/world.html Mathematical Logic around the world]
* [http://www.uni-bonn.de/logic/world.html Mathematical Logic around the world]
* [http://home.swipnet.se/~w-33552/logic/home/index.htm Polyvalued logic] {{Wayback|url=http://home.swipnet.se/~w-33552/logic/home/index.htm |date=20090605030110 }}
* [http://home.swipnet.se/~w-33552/logic/home/index.htm Polyvalued logic]
* [https://web.archive.org/web/20110411024825/http://www.cis.upenn.edu/~giorgi/cl.html Computability logic] 数理逻辑的新方向 - 从真理的理论到可计算性的理论。
* [http://www.cis.upenn.edu/~giorgi/cl.html Computability logic] 数理逻辑的新方向 - 从真理的理论到可计算性的理论。


== 参见 ==
== 参见 ==
{{mathportal}}
{{mathportal}}
* [[逻辑]]
* [[逻辑]]
* [[邏輯的語義]]
* [[邏辑的语义]]
* [[模型論]]
* [[模型论]]
* [[證明論]]
* [[证明论]]
* [[遞歸論]]
* [[递归论]]
* [[一階逻辑]]
* [[一阶逻辑]]
* [[相继式演算]]
* [[相继式演算]]
* [[直觉主义逻辑]]
* [[直觉主义逻辑]]
* [[完備性]]
* [[完备性]]


{{-}}
{{-}}
第68行： 第68行：
{{Computer Science}}
{{Computer Science}}


[[Category:邏輯]]
[[Category:逻辑学]]
[[Category:數理邏輯| ]]
[[Category:数理邏辑| ]]
[[Category:规则|科学]]
[[Category:规则|科学]]
取自“https://www.qiuwenbaike.cn/wiki/数理逻辑”