Follow 语言的基本语法规则

Follow 语言根据 Metamath 语言的启发而设计， 它是一个专门为计算机设计的数学证明语言。 Follow 语言基于计算机最擅长的字符串的 替换 和 比较 两个操作而设计，语法上非常简单。 也正是因为它语法上的简洁性，Follow 语言也成为了一个非常好的一阶数理逻辑的入门工具。

关键词一 type

type prop

prop 的全称是 proposition ，它的中文含义是 提议。 它属于一阶逻辑的核心类型。 提议可能是对的也可能是错的，所以 proposition 可能是对的也可能是错的。

关键词二 term

term prop imp(prop p0, prop p1) {
  (p0 -> p1) // 人类便于理解的表达式
}

imp 的全称是 imply，它的中文含义是 因此。 它属于一阶逻辑的核心连接符。 它隐含的真值表达式是:

• imp(False, False) = True;
• imp(False, True ) = True;
• imp(True, False) = False;
• imp(True, True ) = True;

需要注意的是，这种隐含的真值表达式应该只在我们的脑子里， Follow 语言的编译器并不知道 imp 需要满足这样一张真值表达式。

关键词三 axiom

公理是一系列我们人类可以接受的 term 组合。 公理由（条件 + 结论）组成。 条件由关键词 -|(条件) 开头，结论由 -|(结论) 开头。 在 Follow 语言中，公理可以是多个条件和多个结论。 这里建议将结论写在开头，条件写在末尾。这条建议和 Follow 语言的证明语法有关。

这是三条一阶逻辑的基本公理， 逻辑学家发现只需要从这三条公理出发就可以推导出所有其他imp的结论。 因为这三条公理隐含地等价于上面的四条imp的真值表达式。 Follow语言的编译器能够看到的是这三条公理代码块，而我们的脑子里能看到真值表达式。

// 一阶逻辑第一条公理
axiom a1(prop p0, prop p1) {
  |- imp(p0,imp(p1,p0)) // (p0 -> (p1 -> p0))
}

// 一阶逻辑第二条公理
axiom a2(prop p0, prop p1, prop p2) {
  |- imp(imp(p0,imp(p1,p2)), imp(imp(p0,p1),imp(p0,p2)))
  // ((p0->(p1->p2))->((p0->p1)->(p0->p2)))
}

// 一阶逻辑第三条公理
axiom mp(prop p0, prop p1) {
  |- p0
  -| p1
  -| imp(p1, p0) // (p1 -> p0)
}

关键词四 thm

thm a1i(prop p0, prop p1) {
  |- imp(p0, p1) // (p0 -> p1)
  -| p1
} = {
  mp(imp(p0,p1), p1) // |- imp(p0, p1) -| imp(p1, imp(p0, p1)) -| p1
  a1(p1, p0) // |- imp(p1, imp(p0, p1))
}

thm 的全称是 theorem ，它的中文含义是 定理。 定理是一系列需要证明的 term 组合。

Follow 的证明语法是一个逆向的过程。 我们从剖析上面这个定理 a1i 的证明过程，来介绍 Follow 的证明语法。

• 第一步是起始阶段，我们需要证明 imp(p0,p1)。
• 第二步是输入 mp(imp(p0,p1),p1)。经过对字符串的替换操作， 它会产生这样一个 term 组合 |- imp(p0,p1) -| imp(p1,imp(p0,p1)) -| p1； 编译器通过对字符串的比较发现，组合中的imp(p0,p1)正是第一步中我们要证明的结论， 所以它就会知道，我们不需要再证明 imp(p0,p1)， 而是要证明另外两个 term：imp(p1,imp(p0,p1)) 和 p1。 接着，编译器比较发现 p1 已经在 a1i 的条件中，不需要再证明。 所以它会知道，经过第二步后，我们只需要再证明 imp(p1,imp(p0,p1))。
• 第三步是输入 a1(p1,p0)。经过对字符串的替换操作， 它会产生这样一个 term |- imp(p1,imp(p0,p1))。 编译器通过对字符串的比较操作，发现这正是我们需要证明的结论。 因为第三步并没有条件，也就没有新的需要证明的 term。
• 由于没有新的需要证明的term，因此编译器也就判定定理 a1i 被证明。

我们回顾一下这个证明过程，我们不断地输入前面的公理或者定理，将需要证明的目标转化为新的目标。 整个证明语法就像一条字符水流，而我们沿着水流成功到达源点，得知了真相 —— a1i 是正确的。 这正是我为什么将这个语言起名叫做 Follow 的原因。让我们跟着证明流一起进入数理逻辑的世界吧。