形式证明

数学上，一个公理系统（英语：Axiomatic system，或称公理化系统，公理体系，公理化体系）是一个公理的集合，从中一些或全部公理可以一并用来逻辑地导出定理。一个数学理论由一个公理系统和所有它导出的定理组成。一个完整描述出来的公理系统是形式系统的一个特例；但是通常完全形式化的努力仅带来在确定性上递减的收益，并让人更加难以阅读。所以，公理系统的讨论通常只是半形式化的。一个形式化理论通常表示一个公理系统，例如在模型论中表述的那样。一个形式化证明是一个证明在形式化系统中的表述。一个公理系统称为自洽（或称相容、一致），如果它没有矛盾，也就是说没有从公理同时导出一个命题及其否定的能力。在一个公理系统中，一个公理被称为独立的，若它不是一个从系统的其它公理可以导出的定理。一个系统称为独立的，若它的每个公理都是独立的。虽然独立性不是一个系统的必要需求，自洽性却是必要的。若一个公理系统中，每个命题及其否定命题中至少有一方可被证明，则称该公理系统为完备 。公理系统的数学模型是一个定义良好的集合，它给系统中出现的未定义术语赋予意义，并且是用一种和系统中所定义的关系一致的方式。具体模型的存在性能证明系统的自洽性。模型也可以用来显示一个公理在系统中的独立性。通过构造除去一个特定公理的子系统的有效模型，我们表明该省去的公理是独立的，若它的正确性不可以从子系统得出。两个模型被称为同构，如果它们的元素可以建立一一对应，并且以一种保持它们之间的关系的方式。一个其每个模型都同构于另一个的公理系统称为范畴式的，而可范畴化的性质保证了系统的完备性。第一个被提出的公理系统是欧氏几何。公理化方法经常被作为一个单一的方法或着一致的过程来讨论。以欧几里得为榜样，它确实在很多世纪中被这样对待：直到19世纪初叶，在欧洲数学和哲学中古希腊数学的遗产代表了智力成就（在几何学家的风格中，更几何的发展）的最高标准这件事被视为理所当然（例如在斯宾诺莎的著作中所述）。这个传统的方法中，公理被假设为不言自明的，所以无可争辩，这在19世纪逐渐被扫除，这是随着非欧几何的发展，实分析的基础，康托的集合论和弗雷格在数学基础方面的工作，以及希尔伯特的公理方法作为研究工具的“新”用途而发生的。例如，群论在该世纪末第一个放到了公理化的基础上。一旦公理被明确地提出（例如，逆元必须存在），该课题就可以自主的进展，无须参考这类研究的起源—变换群。所以，现在在数学以及它所影响的领域中，至少有3种“模式”的公理化方法。调皮地说，可能的态度有：第一种情况是经典的演绎方法。第二种采用了博学点，一般化这个口号；它和概念可以和应该用某种内在的自然的广泛性来表达的假设是一致的。第三种在20世纪数学中有显著的位置，特别是在基于同调代数的课题中。很显然公理化方法在数学之外是有局限性的。例如，在政治哲学中，导致不可接受的结论的公理很可能被彻底拒绝；所以没有人真的认同上面的第一个版本。