logic - 仅用基本策略在 coq 中证明 ~~(~~S -> S)

Question

可以~~(~~S -> S)用coq解决吗？我知道你不能在直觉逻辑中执行双重否定消除，但这是否可能，因为你只是证明了双重否定(~~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.