मैं वर्तमान में उलझन में हूं कि निम्नलिखित प्रमेय को कैसे सिद्ध किया जाए:

Theorem excluded_middle2 : 
 (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P).

मैं यहाँ फंस गया हूँ:

Theorem excluded_middle2 : 
  (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P).
Proof.
  intros.
  evar (Q : Prop).
  specialize H with (P : Prop) (Q : Prop).

मुझे पता है कि कोक में बहिष्कृत मध्य के कानून को साबित करना असंभव है, लेकिन मैं वास्तव में जानना चाहता हूं कि इस दिए गए प्रमेय के साथ बहिष्कृत मध्य के कानून को साबित करना संभव है?

0
Jeff Li 25 पद 2021, 13:17

1 उत्तर

सबसे बढ़िया उत्तर

हाँ तुम कर सकते हो। एक तरीका, ssreflect का उपयोग करना, इस प्रकार है (शायद छोटे तरीके हैं):

Lemma orC P Q : P \/ Q -> Q \/ P.
Proof. by case; [right | left]. Qed.

Theorem excluded_middle2 : 
 (forall P Q : Prop, (P -> Q) -> (~ P \/ Q)) -> (forall P, P \/ ~ P).
Proof.
move=> orasimply P.
have pp : P -> P by [].
move: (orasimply P P pp).
exact: orC.
Qed.
0
Pierre Jouvelot 25 पद 2021, 14:23