欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
数理逻辑
来自开放百科 - 灰狐
您可以在Wikipedia上了解到此条目的英文信息 数理逻辑 Thanks, Wikipedia. |
数理逻辑
目录 |
简介
数理逻辑(Mathematical logic)是数学的一个分支,其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。
在逻辑和数学里,命题演算(或称句子演算)是一个形式系统,有着可以由以逻辑运算符结合原子命题来构成代表“命题”的公式,以及允许某些公式建构成“定理”的一套形式“证明规则”。
归纳和演绎,是人类认识世界活动中广泛应用的两套思维方法。
归纳用于发现,演绎用于推理。这是相当普遍的看法。
归纳与演绎是对立的统一。它们相互支持,相互补充,使我们越来越接近于真理。
观点
理论逻辑也称为数理逻辑或符号逻辑,是数学的形式方法在逻辑领域的推广。它把类似于长期用来表达数学关系的某种语言和语法应用于逻辑。——希尔伯特和阿克曼,1928 《数学指南 —— 实用数学手册》p.895
莱布尼兹认为,要认识一个普遍的真理,例子再多也没有用。事实的真理要靠归纳经验得来,是偶然的、个别的。推理的真理靠演绎得来,靠逻辑的必然性得来,才是必然的,普遍的。斯宾诺莎更推崇演绎法,用几何学的体例写出他的《伦理学》。他确信哲学上的一切问题,都可以用几何的方法加以证明。《数学与哲学》张景中 p.162
历史
体系
数理逻辑的主要分支包括:模型论、证明论、递归论和公理化集合论。
Pure and Applied Logic (PAL) 领域包括:
- automated theorem proving
- category theory and categorical logic
- constructive mathematics
- formal verification
- foundations of decision theory
- foundations of programming languages
- homotopy type theory
- logics of programs
- logic in linguistics
- lambda calculus
- learning theory
- model theory
- proof theory
- set theory
- temporal and modal logics
- theory of computing
- type theory
项目
- Prolog logic programming language
- Proof assistant
- 定理证明/公式推导
课程
- Formal Reasoning course notes
- Pure and Applied Logic (PAL) program at Carnegie Mellon University
- Propositional logic and First-order logic 有完整的幻灯片资料供下载
文档
书籍
- 《Simply Logical Intelligent Reasoning by Example》 (Fully Interactive Online Edition)
- 《Homotopy Type Theory: Univalent Foundations of Mathematics》 The Univalent Foundations Program
- 《Practical Foundations For Programming Languages》 Robert Harper, 2016
- 《Type Theory and Functional Programming》 Simon Thompson
- 《An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof》 Peter B. Andrews
- 《可计算性与数理逻辑》第四版,布勒斯
- 《作为哲学的数理逻辑》杨睿之
图集
链接
分享您的观点