1. 一致性
直觉主义逻辑不承认经典逻辑中的排中律——对于任意命题P，或者P真，或者¬P为真。
但是和经典逻辑一样，接受无矛盾律——任何命题P，P和¬P不能同时为真。
无矛盾的逻辑系统，称为一致的，或者协调的。
一个有用的逻辑系统不能包含矛盾。
2. 完备性
上文关于一致性的讨论中，我们并没有区分逻辑公式的证明和语义，
所谓证明，就是一串符号推导序列，从一些合法的公式经过一步或多步，推导出另一些合法的公式。
而公式的语义则是人为选择的，人们倾向于为公式选择可靠的语义，
即，所有可证的公式，在语义上都为真。
但是可靠性并不意味着完备性，
即，所有语义上为真的命题，并不一定总是可证的。
3. 第一第二不完备性定理
人们在研究逻辑系统的时候，对一致性和完备性有着很强烈的追求，
谁都希望自己发明的逻辑系统中没有矛盾，而且所有为真的命题都可证。
但是1931年，哥德尔发现了两个定理，粉碎了这个幻想，
任何相容的形式系统，只要蕴涵皮亚诺算术公理，就可以在其中构造在体系中不能被证明的真命题，因此通过推演不能得到所有真命题（即体系是不完备的）。
—— 哥德尔第一不完备性定理
哥德尔定理，给出了符号推导方法的局限性，
如果要求系统无矛盾，那么某些事实可能是不可证的。
此外，哥德尔第二不完备性定理指出，
任何逻辑自洽的形式系统，只要蕴涵皮亚诺算术公理，它就不能用于证明它本身的相容性。
好吧，连自身的一致性，也不能在系统之内证明了。
所以，在软件开发过程中，检查一个软件系统是否符合设计要求，所使用的方法就是对它进行测试，在这个软件系统之外进行证明。
4. 排除错误
在使用编程语言的时候，我们都或多或少的接触过类型这个概念。
类型系统的一个重要作用就是，通过类型检查排除可能会发生的错误。
和逻辑系统一样，如果类型系统保证所有良类型的程序都按预期正常表现，
我们就说它是可靠的，
这是一个很好的性质，如果A成立，则B成立，建立了符号和行为之间的联系。
不幸的是，程序即使经过了类型检查，
也保证不了那些不在预期范围之内的特性，
即，如果A成立，则C是否成立，我们是不确定的。
例如，对除法表达式进行简单的类型检查，能保证除法操作数的类型合法，
但无法避免除0错误，
这可能需要更强大的类型系统才行。
另一方面，上面提到良类型的程序，预期会表现正常。
但是，类型不合法的程序，却未必会出错。
如果A不成立，那么B是否成立也是不确定的。
这两件事和停机问题是一脉相承的，
对于图灵完备的编程语言来说，要想判定一段程序的所有运行时特征，唯一的办法运行它，仅依赖静态检查是行不通的。
不存在通用的过程，来判断一段程序是否停机。
5. Believe the type
那么我们还要相信类型吗？
要相信。
我们要相信类型系统，可以帮我们排除那些已被证明的错误。
相信类型系统，能指导我们设计出一致的软件。
Show me your type, and I'll show you your language.
然而，类型信息却不等同于文档，它只能提供一些辅助信息，
它不是用来传递知识的，真是如有雷同，实属巧合，
这恰恰反映了在知识传递方面，所做的工作还不够。
结语
本文从逻辑系统出发，介绍了人们经常提及的一些特性，
包括一致性，完备性，可靠性，进而还介绍了哥德尔不完备性定理。
类型检查可看做是一种逻辑推导，
它可以排除某些已知的错误，但也不是万能的。
要想写出高质量的代码，除了在设计方面多花一些心思之外，
更好的办法就是对它进行测试，不论是静态检查还是运行时检查，
不论是自动化的单元测试，还是人工测试。
完全依赖设计和检查是行不通的，有时候唯一可以发现错误的办法就是运行它。
参考
计算机科学中的现代逻辑学
离散数学教程
数理逻辑
Type Systems
Type-driven Development with Idris
网友评论