公理系统：修订间差异

删除的内容添加的内容

行内

2008年1月6日 (日) 08:46的版本

数学上，一个公理系统（或称公理化系统，公理体系，公理化体系）是一个公理的集合，从中一些或全部公理可以用来一起逻辑的导出定理。一个数学理论由一个公理系统和所有它导出的定理组成。一个完整描述出来的公理系统是形式系统的一个特例；但是通常完全形式化的努力带来在确定性上递减的收益，并让人更加无法阅读。所以，公理系统的讨论通常只是半形式化的。一个形式化理论通常表示一个公理系统，例如在模型论中表述的那样。一个形式化证明是一个证明在形式化系统中的表述。

性质

一个公理系统称为自洽（或称相容），如果它没有矛盾，也就是说没有从公理导出一个命题机器逆命题的能力。

在一个公理系统中，一个公理被称为独立的，若它不是一个从系统的其它公理可以导出的定理。一个系统称为独立的，若它的每个定理都是独立的。

虽然独立性不是一个系统的必要需求，自洽性却是必要的。一个公理系统称为完备的，若每个命题都可以导出或其逆可以导出。

模型

公理系统的数学模型是一个定义严谨的集合，它给系统中出现的未定义术语赋予意义，并且是用一种和系统中所定义的关系一致的方式。具体模型^[1]的存在性能证明系统的自洽。

模型也可以用来显示一个公理在系统中的独立性。通过构造除去一个特定公理的子系统的正确模型，我们表明该省去的公理是独立的，若它的正确性不可以从子系统得出。

两个模型被称为同构，如果它们的元素可以建立一一对应，并且以一种保持它们之间的关系的方式。一个其每个模型都同构于另一个的公理系统称为范畴式的，而可范畴化的性质保证了系统的完备性。

第一个公理系统是欧氏几何。

公理化方法

公理化方法经常被作为一个单一的方法或着一致的过程来讨论。以欧几里德为榜样，它确实在很多世纪中被这样对待：直到19世纪初叶，在欧洲数学和哲学中希腊数学的遗产代表了智力成就（在几何学家的风格中，更几何的发展）的最高标准这件事被视为理所当然（例如在斯宾诺莎的著作中所述）。

这个传统的方法中，公理被设定为不言自明的，所以无可争辩，这在19世纪逐渐被扫除，这是随着非欧几何的发展，实分析的基础，康托的集合论和弗雷格在数学基础方面的工作，以及希尔伯特的公理方法作为研究工具的“新”用途而发生的。例如，群论在该世纪末第一个放到了公理化的基础上。一旦公理理清了（例如，逆元必须存在），该课题可以自主的进展，无须参考这类研究的起源—变换群。

所以，现在在数学以及它所影响的领域中至少有3种“模式”的公理化方法。用讽刺描述法，可能的态度有：

接受我的公理，你就必须承担它们的后果。
我拒绝你的公理之一并且采纳更多的模型（I reject one of your axioms and accept extra models）。
我的公理集定义了一个研究领域。

第一种情况定义了经典的演绎方法。第二种采用了博学点，一般化这个口号;它和概念可以和应该用某种内在的自然的广泛性来表达的假设是一致的。第三种在20世纪数学中有显著的位置，特别是在基于同调代数的课题中。

很显然公理化方法在数学之外是有局限性的。例如，在政治哲学中，导致不可接受的结论的公理很可能被大量拒绝；所以没有人真的统一上面的第一个版本。

参看

註釋

^ 一个模型称为是具体的，如果所赋予的意义是现实世界中的对象和关系，而不是像抽象模型那样基于另外的公理系统。

[1] 一个模型称为是具体的，如果所赋予的意义是现实世界中的对象和关系，而不是像抽象模型那样基于另外的公理系统。

[1]

@@ 第1行： / 第1行： @@
-[[数学]]上，一个'''公理系统'''（'''axiomatic system'''，或称'''公理化系统'''，'''公理体系'''，'''公理化体系'''）是一个[[公理]]的[[集合]]，从中一些或全部公理可以用来一起逻辑的导出[[定理]]。一个[[数学理论]]由一个公理系统和所有它导出的定理组成。一个完整描述出来的公理系统是[[形式化系统]]的一个特例；但是通常完全形式化的努力带来在确定性上递减的收益，并让人更加无法阅读。所以，公理系统的讨论通常只是半形式化的。一个'''形式化理论'''（'''formal theory'''）通常表示一个公理系统，例如在[[模型论]]中表述的那样。一个'''形式化证明'''是一个证明在形式化系统中的表述。
+[[数学]]上，一个'''公理系统'''（或称'''公理化系统'''，'''公理体系'''，'''公理化体系'''）是一个[[公理]]的[[集合]]，从中一些或全部公理可以用来一起逻辑的导出[[定理]]。一个[[数学理论]]由一个公理系统和所有它导出的定理组成。一个完整描述出来的公理系统是[[形式系统]]的一个特例；但是通常完全形式化的努力带来在确定性上递减的收益，并让人更加无法阅读。所以，公理系统的讨论通常只是半形式化的。一个'''形式化理论'''通常表示一个公理系统，例如在[[模型论]]中表述的那样。一个'''形式化证明'''是一个证明在形式化系统中的表述。
 ==性质==
-一个公理系统称为'''自洽'''（'''consistent'''，或称'''相容'''），如果它没有'''矛盾'''（'''contradiction'''）， 也就是说没有从公理导出一个命题机器逆命题的能力。
+一个公理系统称为'''自洽'''（或称'''相容'''），如果它没有'''矛盾'''，也就是说没有从公理导出一个命题机器逆命题的能力。
 在一个公理系统中，一个公理被称为'''独立'''的，若它不是一个从系统的其它公理可以导出的定理。一个系统称为'''独立'''的，若它的每个定理都是独立的。
@@ 第15行： / 第15行： @@
 模型也可以用来显示一个公理在系统中的'''独立性'''。通过构造除去一个特定公理的子系统的正确模型，我们表明该省去的公理是'''独立'''的，若它的正确性不可以从子系统得出。
-两个模型被称为'''[[同构]]'''，如果它们的元素可以建立一一对应，并且以一种保持它们之间的关系的方式。一个其每个模型都同构于另一个的公理系统称为'''范畴式'''的（'''categorial'''），而'''可范畴化'''的性质保证了系统的'''完备性'''。
+两个模型被称为'''[[同构]]'''，如果它们的元素可以建立一一对应，并且以一种保持它们之间的关系的方式。一个其每个模型都同构于另一个的公理系统称为'''范畴式'''的，而'''可范畴化'''的性质保证了系统的'''完备性'''。
 第一个公理系统是[[欧氏几何]]。
@@ 第21行： / 第21行： @@
 ==公理化方法==
-'''公理化方法'''（'''axiomatic method'''）经常被作为一个单一的方法或着一致的过程来讨论。以[[欧几里德]]为榜样，它确实在很多世纪中被这样对待：直到[[19世纪]]初叶，在欧洲数学和哲学中[[希腊数学]]的遗产代表了智力成就（在几何学家的风格中，'''更几何'''的发展）的最高标准这件事被视为理所当然（例如在[[斯宾诺莎]]的著作中所述）。
+'''公理化方法'''经常被作为一个单一的方法或着一致的过程来讨论。以[[欧几里德]]为榜样，它确实在很多世纪中被这样对待：直到[[19世纪]]初叶，在欧洲数学和哲学中[[希腊数学]]的遗产代表了智力成就（在几何学家的风格中，'''更几何'''的发展）的最高标准这件事被视为理所当然（例如在[[斯宾诺莎]]的著作中所述）。
 这个传统的方法中，公理被设定为'''不言自明'''的，所以无可争辩，这在19世纪逐渐被扫除，这是随着[[非欧几何]]的发展，[[实分析]]的基础，[[康托]]的[[集合论]]和[[弗雷格]]在数学基础方面的工作，以及[[希尔伯特]]的公理方法作为研究工具的“新”用途而发生的。例如，[[群论]]在该世纪末第一个放到了公理化的基础上。一旦公理理清了（例如，[[逆元]]必须存在），该课题可以自主的进展，无须参考这类研究的起源—[[变换群]]。