Not explicitly specifying instances of a type in coq

Question

I'm interested in trying my hand at constructing set theory using Coq. I would like to define a type sets without specifying what its members are, and a function mapping two sets to a Prop

Definition elem (s1 s1 : sets) : Prop.

I would then make the axioms of set theory hypotheses, and express theorems as (for example)

Theorem : ZFC -> (forall s : sets, ~ elem s s).

However, the syntax above doesn't work. Is this idea something that can be done in Coq? Is there a better way to accomplish this goal in Coq? I am very new to Coq, so I apologize if there is an obvious way of doing this that I don't know.

Answer 1

You need to give names to theorems. And for postulating things, use Parameter and Axiom (which technically mean the same thing but you can use to informally distinguish between concepts and facts).

Parameter set : Type.
Parameter elem : set -> set -> Prop.

Axiom set_extensionality : forall x y, (forall z, elem z x <-> elem z y) -> x = y.
(* etc. *)

In comparison, Definition and Theorem are used for defining and proving things. Having postulated the ZFC axioms, you can prove that a set is not an element of itself. The Theorem command takes a theorem name first (used to refer to it in the future):

Theorem no_self_elem : forall x, ~ elem x x.
Proof.
  (* tactics here. *)
Qed.