證明~~（~~ S - > S）coq只有基本策略

Question

有沒有可能在coq中解決~~(~~S -> S)？我知道你不能在直覺主義邏輯中執行雙重否定消除，但這是可能的，因爲你只需在(~~S -> S)上證明雙重否定，而不是~~S -> S本身？

這只是利用從前奏或標準庫等

Answer 1

基本戰術，而不是引理這是可證明的。一步一步，你做這樣的：

Goal forall S : Prop, ~ ~ (~ ~ S -> S). 
Proof. 
unfold not. 
intros S H1. 
apply H1. 
intro H2. 
apply False_rect. 
apply H2. 
intro H3. 
apply H1. 
intro H4. 
apply H3. 
Defined. 

或者你可以使用tauto，這是直觀的命題演算的決定過程。

Goal forall S : Prop, ~ ~ (~ ~ S -> S). Proof. tauto. Defined.