The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Hi,

I guess you think "predicate" under "propositional function".

So, predicate is just term "Q x" but term:

exists x, Q x

is statement in which you assert that exists some x with property "Q x".

But, also you must to declare predicate Q and in declaration you must to
assign in which type of elements with "Q" property belong to (nat, Z,
Real,..., etc or in some type which you define).

Also, is "exists x, Q x" hypothesis or goal which you want to prove?

So, if you think that x is a natural number and "exists x, Q x" is a
hypothesis then your context can be:

Section Your_Section.

Parameter Q : nat -> Prop.

Hypothesis H_Your_Name : exists x, Q x.

and now you can to prove some goal which you want to prove.

If "exists x, Q x" is a goal which you want to prove (under some
hypotheses) then your context can be:

Section Your_Section.

Parameter Q : nat -> Prop.

(*Your Hypotheses*)

Goal exists x, Q x.

But in Coq Tutorial you have very good introduction of using Coq for
proving statements in propositional and predicate logic.

Greetings,

Marko Malikoviæ

>
> Hey,
>
> How can I represent a propositional function in Coq? Something along the
> lines of:
>
> Ex Q(x)
>
> (where E is supposed to be the existential quantifier)
>
> I'm sure this is trivial, but I am totally lost!
>
> Cheers,
>
> Pete
> --
> View this message in context:
> http://www.nabble.com/First-Order-Logic---Propositional-Function-tp23065352p23065352.html
> Sent from the Coq mailing list archive at Nabble.com.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
dr. sc. Marko Malikoviæ
Filozofski fakultet u Rijeci