CODEWITHSUNDEEP
setcoq
user5876164
user5876164

Reputation: 503

How to define an empty set with axiom of subsets in coq

I have an axiom

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

Axiom AXIOM_OF_SUBSETS :
  forall prop x, exists y, forall u,
    IN u y <-> IN u x /\ (prop u)
.

Now I would like to build an empty set out of this, like

Definition EMPTYSET : set.
  Check (AXIOM_OF_SUBSETS (fun _ : set => False) x).

The result of Check is:

AXIOM_OF_SUBSETS (fun _ : set => False) x
     : exists y : set,
         forall u : set, IN u y <-> IN u x /\ False

Is there a way to define an EMPTYSET in this situation?

I have found a very simple, but dangerous solution for this:

Just change Parameter set : Type. to Parameter set : Prop..

It worked well at least for axioms, lemmas and theorems that I have written so far. Will this be the right way to resolve the issue for the rest of the program?

For the problem right above, refer to the https://github.com/coq/coq/wiki/Prop_or_Set .

Upvotes: 2

Views: 316

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

I take it that you want to formalize Zermelo-Fraenkel set theory in Coq. There are two issues with your code:

  1. In order to apply your axiom, you need to have some set lying around. (Your code mentions a variable x that is not defined anywhere.) One popular option is to combine the axiom of subsets with another axiom that guarantees the existence of some set, such as the axiom of infinity. If you go this way, you need to declare this axiom explicitly.

  2. Coq does not allow the axiom of choice by default. As a result, it is not possible to extract a witness of an existence proof, and to define EMPTYSET based on the proof term you gave. You can solve this issue by either assuming the axiom of choice (check singleton_choice in Coq.Logic.ClassicalChoice (https://coq.github.io/doc/master/stdlib/Coq.Logic.ClassicalChoice.html)), or by slightly changing your formulation of your axiom to avoid the existential quantifier.

    Axiom set : Type.
Axiom In : set -> set -> Prop.
Axiom comprehension : (set -> Prop) -> set -> set.
Axiom comprehension_spec :
  forall prop x u, In u (comprehension prop x) <-> In u x /\ prop u.

Upvotes: 2

Related Questions