形式系统和数学
形式系统是躲在数学背后的神秘百年老字号。看过多层大楼建造的人都知道，工人是先架起一个钢架，然后砌筑墙壁，安装窗户，到大楼造好的时候已经看不见原先那钢架了。打个比喻，把数学看作这个大楼，形式系统便是隐藏在大楼里的钢架。这个钢架出现问题，大楼便会倒塌。钢架的毛病是大楼的隐忧。同样若是支撑着你正在使用的数学的支架——“形式系统”出现矛盾，那当然会给用户带来严重的破坏！因为这个危机，一些数学家、计算机专家以至国防科学家都关心数学背后的形式系统。近年以机器计算作为研究人工智能的工具，我们已开始直接用上了形式系统。形式系统发动了一场革命，结构变为数学的主题。因此我们更有必要了解一点形式系统与数学的故事。