Coq中实数的“小于”是如何定义的？
我只是想知道实数的“小于”关系是如何定义的。
我理解对于自然数(nat)，<可以递归地定义为一个数字是另一个数的(1+)继承者S。我听说很多关于实数的东西在Coq中都是公理的，不计算。
但我想知道，对于Coq中的实数是否有一组最小公理，根据这些公理可以导出其他性质/关系。(例如，Coq.Reals.RIneq认为Rplus_0_r : forall r, r + 0 = r.是一条公理，除其他外)
特别是，我感兴趣的是，是否可以在平等关系的基础上定义诸如<或<=之类的关系。例如，我可以想象在传统的数学中，给定两个数字r1 r2
r1 < r2 <=> exists s, s > 0 /\ r1 + s = r2.但这是否符合Coq的建设性逻辑？我能用它至少对不等式进行一些推理(而不是一直重写公理)吗？
回答 2
Stack Overflow用户
发布于 2015-12-21 19:50:52
Coq.Reals.RIneq认为，Rplus__r : forall r，r +0=R是一个公理，除其他外
吹毛求疵：Rplus_0_r不是公理，但Rplus_0_l是公理。您可以在模块Coq.Reals.Raxioms中获得它们的列表，以及在Coq.Reals.Rdefinitions中使用的参数列表。
正如你所看到的，“大于(或等于)”和“小于或等于”都是用“小于”来定义的，这是假设的，而不是使用你建议的命题。
看起来，Rlt确实可以按照您建议的方式定义:这两个命题可以证明是等价的，如下所示。
Require Import Reals.
Require Import Psatz.
Open Scope R_scope.
Goal forall (r1 r2 : R), r1 < r2 <-> exists s, s > 0 /\ r1 + s = r2.
Proof.
intros r1 r2; split.
- intros H; exists (r2 - r1); split; [lra | ring].
- intros [s [s_pos eq]]; lra.
Qed.但是，对于s > 0位来说，您仍然需要定义它的“严格正”的含义，并且根本不清楚最终是否会有更少的公理(例如，严格正数的概念应该在加法、乘法等项下关闭)。
Stack Overflow用户
发布于 2016-01-28 01:08:20
实际上，Coq.Real库有点弱，因为它完全被指定为公理，而且在过去的一些(简短)点上，它甚至是不一致的。
所以，le的定义有点“特别”，从系统的角度来看，它具有零的计算意义，只是一个常数和几个公理。您可以添加公理"x < x“，Coq无法检测它。
值得指出的是Coq的Reals的一些替代结构：
我最喜欢的经典结构是乔治·冈蒂埃和B·沃纳在“四色定理”中所做的那个：http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/。
它只使用排除的中间公理(主要是比较实数)，因此对其一致性的置信度很高。
reals最著名的无公理特性是C-玉米项目，http://corn.cs.ru.nl/，但我们知道建设性分析与通常的分析有很大不同。
https://stackoverflow.com/questions/34401774
复制相似问题
腾讯云开发者
