3

私は、B.Russell 著の本 Introduction to Mathematical Philosophy を読んでいて、そこに記述されているすべての定理を形式化しようとしていました。

一対多の関係は、次のテキストで説明されています ( contexts on book )。

1 対多の関係は、x が y に対して問題の関係を持っている場合、y に対しても関係を持っている項 x' が他に存在しないような関係として定義できます。

または、再び、次のように定義することもできます: 2 つの項 x と x' が与えられた場合、x が与えられた関係を持つ項と x' が持つ項には、共通の要素はありません。

または、再び、それらの 1 つとその逆の相対積が同一性を意味するような関係として定義することができます。ここで、2 つの関係 R と S の「相対積」は、あるときに x と z の間に成立する関係です。 x が y に対して R の関係をもち、y が z に対して S の関係をもつような中間項 y。

3 つの定義方法があります。最初の 2 つの記述に成功し、それらが同等であることを証明しました。3番目に行き詰っている間、「相対的な製品」の概念を取り除き、その意味合いに直接到達しようとしましたが、失敗しました.

以下は私の定義です。間違いはありましたか?

Definition one_many {X} (R : relation X) : Prop :=
  forall x y, R x y -> forall x', x <> x' -> ~(R x' y).

Definition one_many' {X} (R : relation X) : Prop :=
  forall x x' y, R x y -> R x' y -> x = x'.

Inductive relative_product
          {X} (R: relation X) (S: relation X) : relation X :=
  | rp0 : forall x y, forall z, R x y -> S y z -> relative_product R S x z.
Inductive converse {X} (R : relation X) : relation X :=
  | cv0 : forall x y, R x y -> converse R y x.
Inductive id {X} : relation X :=
  | id0 : forall x, id x x.

Definition one_many'' {X} (R : relation X) : Prop :=
  forall x y, relative_product R (converse R) x y <-> id x y.

以下は、3番目の定義をどのように解釈するかであり、それらの同等性を証明することもできませんでした.

Goal forall {X} (R : relation X),
    one_many'' R <-> (forall x y, R x y -> forall x', converse R y x' -> x = x').
Proof.
  intros. unfold one_many''. split.

  intros.
  assert (relative_product R (converse R) x x' <-> id x x'). apply H.
  inversion H2. apply id_eqv. apply H3.
  apply rp0 with y. assumption. assumption.

  intros.
  split. intro.
  inversion H0. subst.
  apply id_eqv. apply H with y0.
  assumption. assumption.

   (* I'm stuck here. This subgoal is obviously not provable. *)

どの証明が であるかid_eqvはLemma id_eqv : forall {X} (x:X) (y:X), x = y <-> id x y、前もって簡単に証明できます。

誰かが私がどこで間違ったのかを理解するのを手伝ったり、ヒントをくれたりできますか? 前もって感謝します。

4

2 に答える 2

0

勝手な推測ですが、R再帰的にする必要があるか、空ではない必要があるかもしれません。あなたのスクリプトを使用すると、証明する必要があります

1 subgoal
X : Type
R : relation X
H : forall x y : X, R x y -> forall x' : X, converse R y x' -> x = x'
y : X
______________________________________(1/1)
relative_product R (converse R) y y

したがって、関係Rがあり、住民が 1 人いy:Xます。あなたの目標を証明するには、 と のようzな証人が必要です。他の情報がなければ、あなたの唯一のショットは反射的である必要があると思います.R y zR z yRzy

于 2014-08-25T07:29:15.630 に答える