CODEWITHSUNDEEP
coqproof
jaam
jaam

Reputation: 970

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?

Upvotes: 1

Views: 64

Answers (1)

jaam
jaam

Reputation: 970

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

Upvotes: 2

Related Questions