Search code examples
coqproof

Coq: Proving proposition f (x y) -> f y

Is it possible to prove

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

either w/ or (preferably) w/out axioms?

Solution

  • The answer is "no" to proving w/out axioms (and I'm afraid it may be difficult to find meaningful axioms for proving it either). For suppose

    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 has type True -> False, which is unprovable