• Indroduction
• Proofs and Algorithms Part 1
  • Chap1 Predicate Logic
    • 1.1 Inductive Definations
    • 1.2 Languages
    • 1.3 The Languages of Predicate Logic
    • 1.4 Proofs
    • 1.5 Examples of Theories
    • 1.6 Variations on the PRinciple of the Excluded Middle
  • Chap2 Models

Indroduction

引言举\(f(x) = 1 - x^2\)抛物线在\([-1,1]\)围成的面积为例，阿基米德证明其为\(4/3\)。而 17 世纪后，人们可以通过定积分直接计算出该值（而不是证明）。证明与算法在一些问题上殊途同归，如今我们回过头来看有哪些证明的构造可以用应用算法（计算）来解决。

Building a proof and applying an algorithm are two well-known mathematical techniques; they have co-existed for a long time.

本书第一部分（本文），介绍了证明概念的精确定义，并在第二部分给出算法概念的精确定义（就现在而言我对算法的理解为“确定且有限步骤的计算方法”）。精确定义能帮助我们：

• A precise definition of the notion of proof will allow us to understand how to prove independence theorems, which state that there are certain problems for which no proof can provide a solution.

• A precise definition of the notion of an algorithm will allow us to understand how to prove undecidability theorems, which state that certain problems cannot be solved in an algorithm way.

第三部分关注证明与算法的关系，最主要的 Church's theorem，哥德尔不完备定理（negative result counterbalanceed by two positive results）。

Over the next chapters we will explore the deep connections that exist between the concepts of proof and algorithm, and unveil the complexity that hides behind the apparently obvious notion of truth.

Proofs and Algorithms Part 1

Chap1 Predicate Logic

1.1 Inductive Definations

先介绍一些基本工具来定义集合，集合的归纳定义借助不动点定理（The Fixed Point）

1.2 Languages

1.3 The Languages of Predicate Logic

1.4 Proofs

1.5 Examples of Theories

1.6 Variations on the PRinciple of the Excluded Middle

Chap2 Models