3

我正在阅读 B.Russell 的《数学哲学导论》一书，并试图将其中描述的所有定理形式化。

一对多关系由以下文本描述（书上的上下文）。

一对多关系可以定义为这样的关系，如果 x 与 y 有关系，则没有其他项 x' 也与 y 有关系。

或者，它们也可以定义如下：给定两个项 x 和 x'，与 x 具有给定关系的项和与 x' 有关系的项没有共同的成员。

或者，再一次，它们可以被定义为这样的关系，使得它们中的一个及其逆的相对乘积意味着同一性，其中两个关系 R 和 S 的“相对乘积”是当存在一个中间项 y，使得 x 具有 R 与 y 的关系，y 具有 S 与 z 的关系。

它提出了三种定义方式。我已经成功地描述了前两个并证明了它们的等价性。当我被困在第三个时，我试图摆脱“相对产品”的概念，直接进入它的内涵，但也失败了。

以下是我的定义，我犯了什么错误吗？

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.

以下是我如何解释第三个的定义，我也未能证明它们的等价性。

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

5

我认为你误译了第三个定义。原文说：

或者，再一次，它们可以被定义为这样的关系，使得它们中的一个的相对乘积和它的逆积暗示同一性

（强调我的）。那将翻译为：

forall x y, relative_product R (converse R) x y -> id x y

也就是说，它应该是一个直接的暗示，而不是你断言的等价。您不能希望从其他任何一个中证明您的第三个陈述，因为它不等价：考虑非空集合上的空关系。这当然是一个一对多的关系，但其逆的相对乘积也是空的，所以不是完整的恒等关系。

于 2014-08-25T08:51:20.027 回答
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，和一个居民y:X。为了证明你的目标，你需要有一个证人z这样R y z和R z y。在没有任何其他信息的情况下，我想你唯一的选择就是必须具有反R身性和.zy

于 2014-08-25T07:29:15.630 回答