Как определить пустой набор с аксиомой подмножеств в coq - PullRequest
Новая
       6

Как определить пустой набор с аксиомой подмножеств в coq

2 голосов
/ 07 января 2020

У меня есть аксиома 

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)
.

Теперь я хотел бы построить из этого пустой набор, например 

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

Результат проверки: 

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

Есть ли способ определить EMPTYSET в этой ситуации?

Я нашел очень простое, но опасное решение для этого:

Просто измените Parameter set : Type. на Parameter set : Prop..

Это хорошо работало, по крайней мере, для аксиом, лемм и теорем, которые я написал до сих пор. Будет ли это правильным способом решения проблемы для остальной части программы?

Для решения проблемы выше, обратитесь к https://github.com/coq/coq/wiki/Prop_or_Set.

1 Ответ

2 голосов
/ 07 января 2020

Насколько я понимаю, вы хотите формализовать теорию множеств Цермело-Френкеля в Coq. С вашим кодом есть две проблемы:

  1. Чтобы применить вашу аксиому, вы должны иметь некоторый набор. (В вашем коде упоминается переменная x, которая нигде не определена.) Один из популярных вариантов - объединить аксиому подмножеств с другой аксиомой, которая гарантирует существование некоторого множества, такого как аксиома бесконечности. Если вы go таким образом, вам нужно объявить эту аксиому явно.

  2. Coq не разрешает аксиому выбора по умолчанию. В результате невозможно получить свидетельство доказательства существования и определить EMPTYSET на основании предоставленного вами доказательства. Вы можете решить эту проблему, либо выбрав аксиому выбора (отметьте singleton_choice в Coq.Logic.ClassicalChoice (https://coq.github.io/doc/master/stdlib/Coq.Logic.ClassicalChoice.html)), либо слегка изменив формулировку своей аксиомы, чтобы избежать экзистенциального количественного показателя. 

    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.
...