gpt4 book ai didi

coq - Coq 中实数的更强完备性公理

转载 作者:行者123 更新时间:2023-12-01 10:32:22 30 4
gpt4 key购买 nike

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

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))}.

这是必需的吗? (即它是从其他人那里得到的)一致性会不会有任何问题?另外,为什么这不是标准库中的定义(我猜这部分是主观的)。

最佳答案

你的supremum 公理等价于排中律,换句话说,通过引入这个公理,你将经典逻辑带到了表格中。

完整性 公理已经暗示了 weak form排中律,如 sig_not_dec 引理(Rlogic 模块)所示,它说明了否定公式的可判定性:

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

supremum 公理蕴含 LEM

让我们使用sig_not_dec 引理的标准证明来证明,利用更强的完备性公理(supremum),我们可以推导出排中律的强形式。

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 隐含supremum公理

现在,让我们证明 LEM 的强版本蕴含了 supremum 公理。为此,我们展示了在建设性设置中,我们可以推导出 supremumnegated 形式,其中 存在 y:R, E y/\y > x 部分被替换为 ~ (forall y, y > x -> ~ E y),然后使用通常的经典事实,我们证明原始陈述成立好吧。

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 - Coq 中实数的更强完备性公理,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/41326216/

30 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com