Какие аксиомы можно безопасно добавить в Coq? - PullRequest
Новая
       48

Какие аксиомы можно безопасно добавить в Coq?

0 голосов
/ 08 декабря 2018

Этот вопрос является просьбой о предоставлении ссылок или объяснений.Основная идея: что если я добавлю каждую аксиому из стандартной библиотеки Coq?Возникнет ли противоречие или они хорошо приспособлены друг к другу?Каковы другие надежные источники информации о Coq, кроме стандартной библиотеки Coq.(Я видел несколько статей из девяностых, восьмидесятых. Очевидно, что существует множество вариантов теорий типов. Какой из них предназначен для современного Coq? Или я должен подумать: «Все, что известно, можно найти в https://coq.inria.fr/refman/, в https://sympa.inria.fr/sympa/arc/coq-club/1993-12/ и в стандартной библиотеке. ")

(A) Знаете ли вы бумагу или другой источник, где доказано, что некоторые аксиомы могут быть правильно добавлены в Coq?Правильно здесь означает, что расширенная система будет консервативным продолжением предыдущего ИЛИ будет считаться безопасным укреплением.

(B) Лично меня интересуют следующие аксиомы:

0) ex2sig(это согласованно?) 

Axiom ex2sig : forall (A:Type) (P:A->Prop), @ex A P -> @sig A P.

1) LEM

2) Функциональная расширяемость 

Axiom functional_extensionality_dep : forall {A} {B : A -> Type},
  forall (f g : forall x : A, B x),
  (forall x, f x = g x) -> f = g.

3) Выбор 

Theorem choice :
 forall (A B : Type) (R : A->B->Prop),
   (forall x : A, exists y : B, R x y) ->
    exists f : A->B, (forall x : A, R x (f x)).

4) "Условия-как-типы" 

Definition E := Type.
Axiom R : forall x : E, x -> E.  
Axiom R_inj : forall (x : E) (a b : x), R x a = R x b -> a = b.

5) Доказательство-несоответствие 

Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.

6) ... (вы можете порекомендовать свою аксиому в комментариях)

Например, принцип Маркова 

Parameter P:nat -> Prop.
Theorem M:((forall n,(P n \/ ~ (P n)))/\ ~(forall n, ~(P n))  -> exists n,P n).

Но нас не очень интересует принцип Маркова.Потому что нам нужна очень сильная классическая теория с LEM (таким образом, доказан принцип Маркова), с какой-то самой сильной формой выбора (которая подразумевает LEM), экстенсиональностью и т. Д. (Какие аксиомы мы также можем добавить?) (Кстати,Есть много вариантов выбора в Coq: реляционный)

ps. Будет ли широкое использование "некомпьютерных" аксиом в Coq рассматриваться как злоупотребление им?(Думаю, нет, но я не уверен.) Какие свойства Coq я потеряю после добавления аксиом?(вы можете сказать и ссылку, и / или мнение)

pps Вопрос большой и состоит из множества связанных частей, поэтому каждый частичный ответ приветствуется.

...