Coq中实数的更强完整性公理 [英] Stronger completeness axiom for real numbers in Coq

问题描述

这是Coq标准库中定义的完整性公理。

Here is the completeness axiom defined in the Coq standard library.

Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.

Definition bound (E:R -> Prop) := exists m : R, is_upper_bound E m.

Definition is_lub (E:R -> Prop) (m:R) :=
is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).



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

假设我添加了

Axiom supremum :forall E:R -> Prop,
  (exists l : R,is_upper_bound E l) -> 
  (exists x : R, E x) -> 
  { m:R | is_lub E m /\ (forall x:R, x<m -> exists y:R,(E y /\ y >x))}.

这是必需的吗？ （即是否遵循其他原则）是否存在一致性问题？另外，为什么这不是标准库中的定义（我想这是主观的）。

Is this required? (i.e does it follow from the others) Would there be any issues with consistency? Also, why is this not the definition in the standard library (I guess this part is subjective).

推荐答案

您的至上公理与被排除中间律是等价的，换句话说，通过引入该公理，您可以将经典逻辑引入表中。

Your supremum axiom is equivalent to the law of excluded middle, in other words by introducing this axiom you are bringing classical logic to the table.

完整性公理已经意味着排除中律定律的弱形式，如 sig_not_dec 引理（ Rlogic 模块） ，表示否定公式的可判定性：

The completeness axiom already implies a weak form of the law of excluded middle, as shown by the means of the sig_not_dec lemma (Rlogic module), which states the decidability of negated formulas:

Lemma sig_not_dec : forall P : Prop, {~~ P} + {~ P}.

最高级公理意味着LEM

让我们使用 sig_not_dec 引理的标准证明来显示具有更强完整性的公理（ supremum ）可以得出排除中间律的强形式。

supremum axiom implies LEM

Let's use the standard proof of the sig_not_dec lemma to show that with the stronger completeness axiom (supremum) we can derive the strong form of the law of excluded middle.

Lemma supremum_implies_lem : forall P : Prop, P \/ ~ P.
Proof.
intros P.
set (E := fun x => x = 0 \/ (x = 1 /\ P)).
destruct (supremum E) as (x & H & Hclas).
  exists 1. intros x [->|[-> _]].
  apply Rle_0_1. apply Rle_refl. exists 0; now left.
destruct (Rle_lt_dec 1 x) as [H'|H'].
- left.
  pose proof (Rlt_le_trans 0 1 x Rlt_0_1 H') as Hx0.
  destruct (Hclas 0 Hx0) as (y & [contra | (_ & Hp)] & Hy0).
  + now apply Rgt_not_eq in Hy0.
  + exact Hp.
- right. intros HP.
  apply (Rlt_not_le _ _ H'), H; now right.
Qed.

LEM表示至尊公理

现在，让我们证明LEM的强版本意味着至高公理。我们这样做是为了证明，在构造性设置中，我们可以得出 supremum 的取反形式，其中存在y：R，E y / \ y> x 部分被替换为〜（forall y，y> x->〜E y），然后使用通常的经典事实

LEM implies supremum axiom

Now, let us show that the strong version of LEM implies the supremum axiom. We do this by showing that in constructive setting we can derive a negated form of supremum where the exists y:R, E y /\ y > x part gets replaced with ~ (forall y, y > x -> ~ E y), and then using the usual classical facts we show that the original statement holds as well.

Require Import Classical.

Lemma helper (z : R) (E : R -> Prop) :
    (forall y, y > z -> ~ E y) -> is_upper_bound E z.
Proof.
  intros H x Ex.
  destruct (Rle_dec x z).
  - assumption.
  - specialize (H x (Rnot_le_gt x z n)); contradiction.
Qed.

Lemma supremum :forall E:R -> Prop,
  (exists l : R,is_upper_bound E l) ->
  (exists x : R, E x) ->
  {m:R | is_lub E m /\ (forall x:R, x<m -> exists y:R, E y /\ y > x)}.
Proof.
  intros E Hbound Hnonempty.
  pose proof (completeness E Hbound Hnonempty) as [m Hlub].
  clear Hbound Hnonempty.
  exists m. split; auto.
  intros x Hlt.
  assert (~ (forall y, y > x -> ~ E y)) as Hclass.
    intro Hcontra; apply helper in Hcontra.
    destruct Hlub as [Hup Hle].
    specialize (Hle x Hcontra).
    apply Rle_not_lt in Hle; contradiction.
  (* classical part starts here *)
  apply not_all_ex_not in Hclass as [y Hclass]; exists y.
  apply imply_to_and in Hclass as [Hyx HnotnotEy].
  now apply NNPP in HnotnotEy.
Qed.

这篇关于Coq中实数的更强完整性公理的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！