そりゃそうだっていう

もう向いてないんじゃないかと思いました………。

現実逃避したい。

うん

CoqでClassicalをつかった証明の練習。
ここにあるやつ。
参照：　http://coq.inria.fr/library/Coq.Logic.Classical_Prop.html

Section Classical_Prop.
Require Import Relations_1.
Require Import ClassicalFacts.

Axiom classic : forall P : Prop, P \/ ~P.
Lemma not_and_or_cl : forall P Q : Prop, ~(P /\ Q) -> (~P \/ ~Q).
Proof.
Left as an Exercise for the reader.
Qed.

急になんでこんな話するんだよっってことなんだが、まあ思いの外ZFでやってるローカルな話が構成的に証明できるということに驚いているところでの反例みたいなのが出てきたので。

直接的には半順序の理論での問題です。
ライブラリ探して見つけたやつ -> http://coq.inria.fr/library/Coq.Sets.Relations_1.html

Variable U : Type.
Variable R : U -> U -> Prop.
Hypothesis Preo : Preorder U R.

Definition Comp (x y: U) : Prop := exists z : U, R z x /\ R z y.
Definition Dense (D : (U -> Prop)) : Prop := forall x : U, exists y : U, R y x /\ D y.
Definition Upcl (F : (U -> Prop)) : Prop := forall x y: U, F x -> R x y -> F y.
Definition Dir (F : (U -> Prop)) : Prop := forall x y: U, F x -> F y -> exists z : U, F z /\ R z x /\ R z y.
Definition Fil (F : (U -> Prop)) : Prop := Upcl F /\ Dir F.
Definition Generic (G : (U -> Prop)) : Prop := forall D : (U -> Prop), exists x : U, G x /\ D x.

Hypothesis Atomless : forall x : U, exists y : U, exists z : U,  (R y x) /\ (R z x) /\ ~ (Comp y z).

Theorem generic_fil0 : forall G : U -> Prop, Fil G -> ~ Generic G.

Proof.

intros.
intro.

Definition Complement (I : U -> Prop) (x : U) := ~ I x.

assert (Dense (Complement G)).
  intro x.
  elim (Atomless x).
  intros.
  destruct H1 as [x1 H1].

  assert (~(G x0 /\ G x1)).
    intro.
    destruct H as [Hf0 Hf1].
    destruct H2.
    elim (Hf1 x0 x1).
    intros.
    destruct H1 as [H1 H4].
    destruct H4 as [H4 H5].
    destruct H5.
    exists x2.
    destruct H3.
    trivial.
    apply H.
    apply H2.

  assert (~(G x0) \/ ~(G x1)).
    apply (not_and_or (G x0) (G x1)).  ;; ここでclassic適用
    assumption.

  destruct H3.
    exists x0.
    destruct H1.
    split.
      apply H1.
      apply H3.

    exists x1.
    destruct H1; destruct H4.
    split.
      apply H4.
      apply H3.

elim (H0 (Complement G)).
intros.
destruct H2.
destruct H3.
assumption.

Qed.

End Classical_Prop.

引用ながい（ごめんなさい）
assertionの中にsubのassertionが２つあるし…、こういうのの上手い書き方わかんないですね。
ああ、そういえば、Proof中にDefinitionすんなってある人に怒られたわけだが、代替手段がよくわからないので使ってしまった…＞＜（えろいひと教えて）

えぇと。
引用中の定理generic_fil0の意味合いは、アトムレスな半順序に対してV-ジェネリックフィルターは存在しませんという話。
強制法の言葉で言うと、

へぇclassicいるの、ってまぁそうだよねっていう。
classic使ったのはコメントにある部分です。アトムレスならsplitし続けるのでフィルターで稠密部分を全部捕まえるのは無理だよねっていう。ただ、矛盾を導く際に、splitした２つの強制条件の少なくともどちらか一方はGに入らないということから構成的にその内の入らない一つを選択できそうにないから、classicを使わずにはいられないでしょうなぁ。(たぶん)

強制法だとV-ジェネリックではなくて適当に小さいモデルMを持ってきてM-ジェネリックなものを考えるので、自由にジェネリックフィルターが取れますっていうアレです。この定理は普通の半順序だとジェネリックオブジェクトがM上定義不可能である(Mに入ってこないので)という結果を導くので、結構重要なものです。

…ん？（強制法が何かとか聞かないで…）

らしいです。

にゃんにゃん