0

我想证明以下定理

Goal (forall x, P x \/ Q x) -> (forall x, P x) \/ (forall x, Q x).

有上下文

1 subgoal
P : nat -> Prop
Q : nat -> Prop
R : nat -> nat -> Prop
H : forall x : nat, P x \/ Q x
______________________________________(1/1)
(forall x : nat, P x) \/ (forall x : nat, Q x)

该陈述在谓词逻辑中似乎是正确的,但我不知道如何证明它。问题本质上是我不能一次消除所有的 forall,但我不能在破坏假设 H 之前既不向左也不向右应用。

有没有一种简单的方法可以做到这一点?

4

1 回答 1

0

P认为是均匀的,是奇怪的,你Q应该看到你的定理是有缺陷的。

于 2013-09-25T22:11:09.113 回答