# Highlighted Resources

1. Teach Yourself Logic 2017: A Study Guide
2. Logic in Computer Science, Modelling and Reasoning about Systems

# 数理逻辑

## 数理逻辑

• 数学的一个分支，研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统
• 与数学基础和理论计算机科学紧密相关。

## 形式系统

formal system

• 用于以公理根据规则集（被称作logical calculus)推断定理的系统。
• 命题演算、一阶逻辑、lambda演算等都是形式系统。
• 数理逻辑中，核心概念都是由形式逻辑系统（formal logical system）表示的。这些系统尽管各不相同，但是他们都有一个共性：表达式仅在某一个特定的形式语言中有效。

model theory

• 数理逻辑主要分支之一。

• 数理逻辑主要分支之一。

proof theory

• 数理逻辑主要分支之一。

• 数理逻辑主要分支之一。

## 命题逻辑

• 以逻辑运算符结合原子命题来构成代表“命题”的公式，以及允许某些公式建构成“定理”的一套形式“证明规则”。
• 命题逻辑是最简单的形式系统。

## 一阶逻辑

• 命题逻辑的扩展，额外包含了断言和量化。

## 二阶逻辑

second-order logic

• 一阶逻辑和二阶逻辑都使用了论域（有时叫做“域”或“全集”）的想法。论域是可以在其上量化的个体元素的集合。一阶逻辑只包括取值为论域的个体元素的变量和量词。
• 一阶逻辑的扩展，又被扩展为高阶逻辑和类型论。

## 高阶逻辑

higher-order logic

• In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more expressive, but their model-theoretic properties are less well-behaved than those of first-order logic.
• The term “higher-order logic”, abbreviated as HOL, is commonly used to mean higher-order simple predicate logic. Here “simple” indicates that the underlying type theory is simple, not polymorphic or dependent.

## 类型论

type theory

• A type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every “term” has a “type” and operations are restricted to terms of a certain type.
• Type theory is closely related to (and in some cases overlaps with) type systems, which are a programming language feature used to reduce bugs. Type theory was created to avoid paradoxes in a variety of formal logics and rewrite systems.
• Two well-known type theories that can serve as mathematical foundations are Alonzo Church’s typed λ-calculus and Per Martin-Löf’s intuitionistic type theory.

# 形式逻辑

## 形式逻辑

formal logic

• 研究纯形式内容的推论的一门学科，这种内容是很明确的。若一个推论可以被表达成一个完全抽象的规则（即不只是和任一特定事物或性质有关的规则）的一个特定应用，则这个推论拥有纯形式内容。形式逻辑的规则由亚里斯多德最先写成。在许多逻辑的定义中，逻辑推论与带有纯形式内容的推论会是同一种概念。但这不表示非形式逻辑的概念是空洞的，因为没有任何一种形式语言可以捕捉到自然语言语义间所有的微细差别。

## 形式语言

formal language

• 形式语言是用精确的数学或机器可处理的公式定义的语言。一般有两个方面：语法和语义。
• 专门研究语言的语法的数学和计算机科学分支叫做形式语言理论，它只研究语言的语法不致力于它的语义。在形式语言理论中，形式语言是一个字母表上的某些有限长字符串的集合。一个形式语言可以包含无限多个字符串。
• 某字符串是否属于某一形式语言，需要明确的标准表示此标准的方法有：枚举法，形式文法，正则表达式，自动机，decision procedure。

## 自动机

automata

• 自动机是形式语言的一个有限表示
• 与形式语言紧密相关：自动机消耗输入符号，并在自身的不同状态间转移，可以通过状态机消耗完整个字符串之后是否达到某些特定状态来定义一个字符串是否属于某一个语言。语言可以通过某种自动机来识别，比如图灵机、有限状态自动机

turing machine

## 有限状态自动机

finite state automata

# 解释

## 计算机科学和逻辑之间的关系

1. 程序语言学、语义学的研究和程序验证中的模型检测从模型论中衍生而来。
2. 哥德尔不完备性定理证明了：任何有能力表达皮亚诺算术的逻辑系统中，都存在既无法证明、也无法证伪的语句。
3. 当使用一阶逻辑表示人工智能Agent中的目标和状态时，frame problem是必须解决的基础问题之一。
4. Curry-Howard correspondence是逻辑系统和计算机软件之间的关系（换言之，“证明”和“程序”的等价性）。此理论在证明和程序之间建立了精确的关联。尤其是，此理论指出了简单类型lambda演算和直觉命题逻辑的证明之间的关联对应。这一结果与证明论有关，直觉主义逻辑和线性逻辑在此起了很大作用。
5. λ演算和组合子逻辑这样的演算现在属于理想程序语言。
7. 计算机科学在自动验证和自动寻找证明等技巧方面的成果对逻辑研究做出了贡献，比如说自动定理证明逻辑编程
8. 时序逻辑（temporal logic）用于并发系统的论证推导。

### 计算机逻辑年刊

IEEE Symposium on Logic in Computer Science（LICS）。

## Mathematical Logic - 数理逻辑

### 数理逻辑中的基本结果

• 一阶公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说，证明集合是原始递归的。实质上，这就是哥德尔完全性定理，虽然那个定理的通常陈述使它与算法之间的关系不明显。
• 有效的一阶公式的集合是无限不可数（Uncountable Infinite）的。这一集合是“递归枚举的”，即不存在一图灵机（从而不存在任何现有计算机和算法）可以对某个非一阶公式的输入告诉你“这个输入一定不是一阶公式”——它可能一直运算下去。
• 普遍有效的二阶公式的集合甚至不是递归可枚举的。这是哥德尔不完全性定理的一个结果。
• 勒文海姆-斯科伦定理。

• 相继式演算中的切消定理。
• 保罗·约瑟夫·科恩（Paul Cohen）在1963年证明的连续统假设的独立性。

## Formal System - 形式系统

A formal system is used to infer theorems from axioms according to a set of rules. These rules used to carry out the inference of theorems from axioms are known as the logical calculus of the formal system. A formal system is essentially an “axiomatic system”. In 1921, David Hilbert proposed to use such system as the foundation for the knowledge in mathematics. A formal system may represent a well-defined system of abstract thought. Spinoza’s Ethics imitates the form of Euclid’s Elements. Spinoza employed Euclidean elements such as “axioms” or “primitive truths”, rules of inferences, etc., so that a calculus can be built using these.

A formal system can be expressed as the following:

1. A finite set of symbols, that can be used for constructing formulas (i.e. finite strings of symbols).
2. A grammar, which tells how well-formed formulas (abbreviated wff) are constructed out of the symbols in the alphabet. It is usually required that there be a decision procedure for deciding whether a formula is well formed or not.
3. A set of axioms or axiom schemata: each axiom must be a wff.
4. A set of inference rules.

### 数学中的形式系统列表

• Domain relational calculus, a calculus for the relational data model
• Functional calculus, a way to apply various types of functions to operators
• Join calculus, a theoretical model for distributed programming Lambda calculus, a formulation of the theory of reflexive functions that has deep connections to computational theory
• Matrix calculus, a specialized notation for multivariable calculus over spaces of matrices
• Modal μ-calculus, a common temporal logic used by formal verification methods such as model checking
• Pi-calculus, a formulation of the theory of concurrent, communicating processes that was invented by Robin Milner
• Predicate calculus, specifies the rules of inference governing the logic of predicates
• Propositional calculus, specifies the rules of inference governing the logic of propositions
• Refinement calculus, a way of refining models of programs into efficient programs
• Rho calculus, introduced as a general means to uniformly integrate rewriting and lambda calculus
• Tuple calculus, a calculus for the relational data model, inspired the SQL language
• Umbral calculus, the combinatorics of certain operations on polynomials
• Vector calculus (also called vector analysis), comprising specialized notations for multivariable analysis of vectors in an inner-product space

## First Order Logic - 一阶逻辑

As a Formal System:

1. Symbols:

Quantifier symbols: ∀ and ∃. Logical connectives: ∧ for conjunction, ∨ for disjunction, → for implication, ↔ for biconditional, ¬ for negation. Predicate symbols: n-ary, n >= 0. Function symbols.

1. Formation rules: Terms: variables, functions.
Formulas:
• The set of formulas (also called well-formed formulas[9] or WFFs) is inductively defined by the following rules:
• Predicate symbols. If P is an n-ary predicate symbol and t1, …, tn are terms then P(t1,…,tn) is a formula.
• Equality. If the equality symbol is considered part of logic, and t1 and t2 are terms, then t1 = t2 is a formula.
• Negation. If φ is a formula, then {\displaystyle \lnot } \lnot φ is a formula.
• Binary connectives. If φ and ψ are formulas, then (φ {\displaystyle \rightarrow } \rightarrow ψ) is a formula. Similar rules apply to other binary logical connectives.
• Quantifiers. If {\displaystyle \varphi } \varphi is a formula and x is a variable, then {\displaystyle \forall x\varphi } \forall x\varphi (for all x, {\displaystyle \varphi } \varphi holds) and {\displaystyle \exists x\varphi } \exists x\varphi (there exists x such that {\displaystyle \varphi } \varphi ) are formulas.
2. 简介 不像命题逻辑只处理简单的陈述命题，一阶逻辑还额外包含了断言和量化。

1.

# Content of Mathematical Logic in Wikipedia

Mathematical logic

# Relationships - 关系

(logic
(mathematical-logic
(model-theory
(programming-language-theory)
(semantics)
(model-theory))
(proof-theory
(formal-system))
(recursive-theory)
(axiomatic-set-theory)
(formal-logic)))

(formal-verification
())

(formal-systems
(propositional-logic)
(first-order-logic)
(second-order-logic)
(higher-order-logic)
(type-theory)



# References

1. Levesque, Hector; Ronald Brachman (1985). “A Fundamental Tradeoff in Knowledge Representation and Reasoning”. In Ronald Brachman and Hector J. Levesque. Reading in Knowledge Representation. Morgan Kaufmann. p. 49. ISBN 0-934613-01-X.