CODEWITHSUNDEEP
logiccoq
MayJuneJuly
MayJuneJuly

Reputation: 11

Coq syntax. Predicate Logic

Can anyone help me out with the coq syntax for the following proof:

~ (exists x:D, ~ R x) |- (forall y:D, R y)

Upvotes: 1

Views: 75

Answers (1)

Pedro Abreu
Pedro Abreu

Reputation: 142

First you have to define D and R, either by having it defined beforehand or by having it in scope by a quantifier. And entailment is usually modeled by Coq implication (->).

This would give the following

forall (D : Prop) (R : D -> Prop), ~ (exists x:D, ~ R x) -> (forall y:D, R y).

Upvotes: 1

Related Questions