Можете ли вы доказать, что исключенное среднее неверно в Coq, если я не импортирую классическую логику

Question

Я знаю, что исключенная середина невозможна в логике построения. Тем не менее, я застрял, когда я пытаюсь показать это в Coq.

Theorem em: forall P : Prop, ~P \/ P -> False.

Мой подход:

intros P H.
unfold not in H.
intuition.

Система говорит следующее:

2 subgoals
P : Prop
H0 : P -> False
______________________________________(1/2)
False
______________________________________(2/2)
False

Как мне поступить? Спасибо

Answer 1

То, что вы пытаетесь построить, - это не отрицание LEM, которое скажет, что «существует некоторый P, такой, что EM не имеет места», а утверждение, которое говорит, что ни одно предложение не является разрешимым, что, конечно, приводит к тривиальное несоответствие:

Axiom not_lem : forall (P : Prop), ~ (P \/ ~ P).

Goal False.
now apply (not_lem True); left.

Нет необходимости использовать причудливую лемму о двойном отрицании; поскольку это явно противоречиво [представьте, что это будет так!]

«Классическое» отрицание LEM действительно:

Axiom not_lem : exists (P : Prop), ~ (P \/ ~ P).

и это не доказуемо [в противном случае EM не было бы приемлемым], но вы можете предположить, что это безопасно; однако это не принесет вам особой пользы.

Answer 2

Нельзя опровергнуть закон исключенного среднего (LEM) в Coq. Предположим, вы доказали свое опровержение LEM. Мы моделируем такую ​​ситуацию, постулируя ее как аксиому:

Axiom not_lem : forall (P : Prop), ~ (P \/ ~ P).

Но тогда у нас также есть более слабая версия (с двойным отрицанием) LEM:

Lemma not_not_lem (P : Prop) :
  ~ ~ (P \/ ~ P).
Proof.
  intros nlem. apply nlem.
  right. intros p. apply nlem.
  left. exact p.
Qed.

Эти два факта вместе сделали бы логику Кока непоследовательной:

Lemma Coq_would_be_inconsistent :
  False.
Proof.
  apply (not_not_lem True).
  apply not_lem.
Qed.