8

在https://www.cs.umd.edu/~rrand/vqc/Real.html#lab1可以阅读：

Coq 的标准库对实数采用了一种非常不同的方法：公理方法。

并且可以找到以下公理：

Axiom
  completeness :
    ∀E:R → Prop,
      bound E → (∃x : R, E x) → { m:R | is_lub E m }.

图书馆没有提到，但在为什么 Coq 中的实数公理化？可以找到相同的描述：

我想知道 Coq 是否将实数定义为 Cauchy 序列或 Dedekind 切割，所以我检查了 Coq.Reals.Raxioms 和......这两个都没有。实数及其运算（作为参数和公理）被公理化。为什么会这样？

此外，实数紧密依赖于子集的概念，因为它们的定义属性之一是每个上界子集都有一个最小上界。Axiom 完整性将这些子集编码为 Props。”

尽管如此，每当我查看https://coq.inria.fr/library/Coq.Reals.Raxioms.html时，我都看不到任何公理化方法，特别是我们有以下引理：

Lemma completeness :
    forall E:R -> Prop,
      bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.

我在哪里可以找到 Coq 中实数的这种公理化方法？

4

2 回答 2

8

你提到的描述确实已经过时了，因为我问了你链接的问题，我以更标准的方式重写了定义 Coq 标准库实数的公理。实数现在分为 2 层

  • 建设性实数，根据柯西序列定义，根本不使用公理；
  • 经典实数，它是一组构造实数的商，并且确实使用 3 个公理来证明您提到的最小上界定理。

Print AssumptionsCoq 通过以下命令轻松地为您提供任何术语的公理：

Require Import Raxioms.
Print Assumptions completeness.

Axioms:
ClassicalDedekindReals.sig_not_dec : forall P : Prop, {~ ~ P} + {~ P}
ClassicalDedekindReals.sig_forall_dec
  : forall P : nat -> Prop,
    (forall n : nat, {P n} + {~ P n}) -> {n : nat | ~ P n} + {forall n : nat, P n}
FunctionalExtensionality.functional_extensionality_dep
  : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
    (forall x : A, f x = g x) -> f = g

正如你所看到的，这 3 个公理是纯逻辑的，它们根本不涉及实数。他们只是假设了经典逻辑的一个片段。

如果你想要 Coq 中实数的公理化定义，我为构造实数提供了一个

Require Import Coq.Reals.Abstract.ConstructiveReals.

如果您假设上述 3 个公理，这将成为经典实数的接口。

于 2021-10-23T09:06:26.613 回答
1

这些描述已经过时。过去实数的类型及其R基本性质是公理化的。但是现在（自2019 年以来？）它是根据更基本的公理来定义的，或多或少就像在传统数学中所做的那样。

于 2021-10-23T03:33:59.413 回答