数理逻辑

2022年12月7日 (三) 09:03的版本

您可以在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
• 《可计算性与数理逻辑》第四版，布勒斯
• 《作为哲学的数理逻辑》杨睿之

图集

• 

  命题逻辑的符号

• 

  基本符号

链接

• From Type Theory to Haskell in 10 Minutes