coq - Coq：证明命题 f (xy) -> fy

Question

是否可以证明

Lemma A3 (f x: Prop -> Prop)(y: Prop): f (x y) -> f y.

w/或（最好）w/out公理？

标签： coqproof

Answer 1

答案是“不”证明没有公理（而且恐怕也很难找到有意义的公理来证明它）。假设

Parameter A3: forall (f x:Prop->Prop)(y:Prop), f (x y) -> f y.
Definition f' (x:Prop) := x.
Definition X := fun _:Prop => True.
Check A3 f' X False: True -> False.

A3 f' X False有类型True -> False，这是无法证明的