我正在尝试为Coq 中的所有命题定义双重否定翻译，因此我可以证明在“直觉逻辑”中无法证明（或有非常硬的证明）的经典事实，但我认为这不可能使用Inductive或Fixpoint关键词。有Fixpoint，我需要匹配arbitary命题。（虽然我只需要一阶逻辑，即合取、析取、条件、否定forall和exists量词）我也不能使用Inductive. 这是我失败的方法
Inductive NN (P : Prop) : Prop :=
| nn_cond (P1 P2 : Prop) (Heq : P = P1 /\ P2) (H : NN P1 -> NN P2).
我最后需要证明一个Lemma类似的
Lemma NN__EM (P : Prop) : NN P <-> (excluded_middle -> P).
关于如何定义这样的定义的任何想法？
双否定翻译涉及三个逻辑系统。有经典逻辑和直觉逻辑，但翻译不属于这两种逻辑中的任何一种。毕竟，翻译是两个不同的逻辑世界之间的关系；它怎么可能属于其中之一？相反，需要将这些逻辑构造为其他逻辑（可能是您“相信”或“真实”的逻辑）内的对象，然后双重否定转换是描述两个内部逻辑的环境逻辑的定理。TL;DR：双重否定翻译是一个关于逻辑的过程/定理，而不是在逻辑内。
出于这个原因，您不能在 Coq 的逻辑中编写双重否定翻译，例如引理。我的意思是，你当然可以定义
Inductive sentence : Set := ... . (* E.g. syntax of FOL *)
Definition NN : sentence -> sentence.
Definition classically_provable : sentence -> Prop.
Definition intuitionistically_provable : sentence -> Prop.
Theorem double_negation_translation (p : sentence) :
classically_provable p <-> intuitionistically_provable (NN p).
但这并不能证明Coq 的任何内容。它只证明了Coq内部构造的其他一些逻辑。如果你想证明关于 Coq 的这一点，你必须在一些“更高”的逻辑系统中做这个证明，这通常是我现在使用的非正式的自然语言逻辑，或者语言 Ltac，战术语言。Ltac 程序是 Coq 运行以生成证明的程序。特别是，您可以编写两种策略。一个，如果你给它一个术语excluded_middle -> P（又名 的经典证明P），本质上将试图根除该经典的所有用途，以产生 的双重否定翻译的新的、直观的证明P。另一个，给出双重否定翻译的（直觉）证明P，把它变成经典的证明P（又名它证明了excluded_middle -> P）。（注意我的谨慎语言：我说P但不是NN P，只有“”的双重否定翻译P。那是因为，在Coq之外，在自然语言或 Ltac 中，我们可以定义““的双重否定翻译P是什么。在Coq 中，对此没有定义NN : Prop -> Prop。）
因此，例如，您可以像这样定义命题的翻译：
Ltac nn_transl P :=
lazymatch P with
| ?L /\ ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
uconstr:(L' /\ R')
| ?L \/ ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
uconstr:(~(~L' /\ ~R'))
| not ?Q =>
let Q' := nn_transl Q in
uconstr:(~Q')
| ?L -> ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
uconstr:(L' -> R')
| forall t: ?T, @?Q t =>
constr:(
forall t: T,
ltac:(
let Qt := eval hnf in (Q t) in
let Qt' := nn_transl Qt in
exact Qt'))
| exists t: ?T, @?Q t =>
constr:(
~forall t: T,
~ltac:(
let Qt := eval hnf in (Q t) in
let Qt' := nn_transl Qt in
exact Qt'))
| _ => uconstr:(~~P)
end.
实现证明的实际翻译似乎并不容易，但应该是可行的。我已经实现了更简单的方向（对经典的双重否定）：
Definition excluded_middle : Prop := forall x, x \/ ~x.
Tactic Notation "assert" "double" "negative" constr(P) "as" ident(H) :=
let P' := nn_transl P in
assert (H : P').
Ltac int_to_nn_class_gen' nn_int_to_class_gen P :=
let x := fresh "x" in
let excl := fresh "excl" in
lazymatch P with
| ?L /\ ?R =>
let xl := fresh x "_l" in
let xr := fresh x "_r" in
let rec_L := int_to_nn_class_gen' nn_int_to_class_gen L in
let rec_R := int_to_nn_class_gen' nn_int_to_class_gen R in
uconstr:(
fun (x : P) (excl : excluded_middle) =>
let (xl, xr) := x in
conj (rec_L xl excl) (rec_R xr excl))
| ?L \/ ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
let arg := fresh x "_arg" in
let arg_l := fresh arg "_l" in
let arg_r := fresh arg "_r" in
let rec_L := int_to_nn_class_gen' nn_int_to_class_gen L in
let rec_R := int_to_nn_class_gen' nn_int_to_class_gen R in
uconstr:(
fun (x : P) (excl : excluded_middle) (arg : ~L' /\ ~R') =>
let (arg_l, arg_r) := arg in
match x with
| or_introl x => arg (rec_L x excl)
| or_intror x => arg (rec_R x excl)
end)
| not ?Q =>
let Q' := nn_transl Q in
let arg := fresh x "_arg" in
let rec_Q := nn_int_to_class_gen Q in
uconstr:(
fun (x : P) (excl : excluded_middle) (arg : Q') => x (rec_Q arg excl))
| ?L -> ?R =>
let L' := nn_transl L in
let arg := fresh x "_arg" in
let rec_L := nn_int_to_class_gen L in
let rec_R := int_to_nn_class_gen' nn_int_to_class_gen R in
uconstr:(
fun (x : P) (excl : excluded_middle) (arg : L') =>
rec_R (x (rec_L arg excl)) excl)
| forall t: ?T, @?Q t =>
constr:(
fun (x : P) (excl : excluded_middle) (t : T) =>
ltac:(
let Qt := eval hnf in (Q t) in
let rec_Qt := int_to_nn_class_gen' nn_int_to_class_gen Qt in
exact (rec_Qt (x t) excl)))
| exists t: ?T, @?Q t =>
let arg := fresh x "_arg" in
let wit := fresh x "_wit" in
constr:(
fun
(x : P) (excl : excluded_middle)
(arg :
forall t: T,
ltac:(
let Qt := eval hnf in (Q t) in
let Qt' := nn_transl Qt in
exact (~Qt'))) =>
match x with ex_intro _ t wit =>
ltac:(
let Qt := eval hnf in (Q t) in
let rec_Qt := int_to_nn_class_gen' nn_int_to_class_gen Qt in
exact (arg t (rec_Qt wit excl)))
end)
| _ =>
let arg := fresh x "_arg" in
uconstr:(fun (x : P) (excl : excluded_middle) (arg : ~P) => arg x)
end.
Ltac nn_int_to_class_gen' int_to_nn_class_gen P :=
let NNP := nn_transl P in
let nnx := fresh "nnx" in
let excl := fresh "excl" in
lazymatch P with
| ?L /\ ?R =>
let nnl := fresh nnx "_l" in
let nnr := fresh nnx "_r" in
let rec_L := nn_int_to_class_gen' int_to_nn_class_gen L in
let rec_R := nn_int_to_class_gen' int_to_nn_class_gen R in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) =>
let (nnl, nnr) := nnx in
conj (rec_L nnl excl) (rec_R nnr excl))
| ?L \/ ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
let prf := fresh nnx "_prf" in
let arg := fresh nnx "_arg" in
let arg_l := fresh arg "_l" in
let arg_r := fresh arg "_r" in
let rec_L := nn_int_to_class_gen' int_to_nn_class_gen L in
let rec_R := nn_int_to_class_gen' int_to_nn_class_gen R in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) =>
match excl P with
| or_introl prf => prf
| or_intror prf =>
nnx (conj
(fun arg : L' => prf (or_introl (rec_L arg)))
(fun arg : R' => prf (or_intror (rec_R arg))))
end)
| not ?Q =>
let arg := fresh nnx "_arg" in
let rec_Q := int_to_nn_class_gen Q in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) (arg : Q) =>
nnx (rec_Q arg excl))
| ?L -> ?R =>
let arg := fresh nnx "_arg" in
let rec_L := int_to_nn_class_gen L in
let rec_R := nn_int_to_class_gen' int_to_nn_class_gen R in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) (arg : L) =>
rec_R (nnx (rec_L arg excl)) excl)
| forall t: ?T, @?Q t =>
constr:(
fun (nnx : NNP) (excl : excluded_middle) (t : T) =>
ltac:(
let Qt := eval hnf in (Q t) in
let rec_Qt := nn_int_to_class_gen' int_to_nn_class_gen Qt in
exact (rec_Qt (nnx t) excl)))
| exists t: ?T, @?Q t =>
let prf := fresh nnx "_prf" in
let wit := fresh nnx "_wit" in
constr:(
fun (nnx : NNP) (excl : excluded_middle) =>
match excl P with
| or_introl prf => prf
| or_intror prf =>
False_ind P
( nnx
( fun
(t : T)
(wit :
ltac:(
let Qt := eval hnf in (Q t) in
let Q' := nn_transl Qt in
exact Q')) =>
ltac:(
let Qt := eval hnf in (Q t) in
let rec_Qt := nn_int_to_class_gen' int_to_nn_class_gen Qt in
exact (prf (ex_intro _ t (rec_Qt wit excl))))))
end)
| _ =>
let prf := fresh nnx "_prf" in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) =>
match excl P with
| or_introl prf => prf
| or_intror prf => False_ind P (nnx prf)
end)
end.
Ltac int_to_nn_class_gen :=
let rec
int_to_nn_class_gen :=
fun P => int_to_nn_class_gen' nn_int_to_class_gen P
with
nn_int_to_class_gen :=
fun P => nn_int_to_class_gen' int_to_nn_class_gen P
in
int_to_nn_class_gen.
Ltac nn_int_to_class_gen :=
let rec
int_to_nn_class_gen :=
fun P => int_to_nn_class_gen' nn_int_to_class_gen P
with
nn_int_to_class_gen :=
fun P => nn_int_to_class_gen' int_to_nn_class_gen P
in
nn_int_to_class_gen.
Tactic Notation "nn_int_to_class" constr(P) hyp(H) :=
let new := fresh "class_" H in
let transl := nn_int_to_class_gen P in
refine (let new : excluded_middle -> P := transl H in _).
回过头来看，我认为你可能可以用Classes 和Instances来实现这个方向（隐式值的类型导向查找是另一个 Coq 过程，它在 Coq 的逻辑之外），因为翻译完全是由一个自我完成的包含名词，但我不知道其他方向（这将是分析实际的举证期限fun (excl : excluded_middle) => ...为用途excl）可以做到这样。以下是饮酒者悖论的证明：
Theorem nn_excluded_middle X : ~~(X \/ ~X).
Proof. tauto. Defined.
Theorem drinker's (P : Set) (x : P) (D : P -> Prop)
: excluded_middle -> exists y, D y -> forall z, D z.
Proof.
assert double negative (exists y, D y -> forall z, D z) as prf.
{
intros no.
apply (nn_excluded_middle (forall y, D y)).
intros [everyone | someone].
- apply no with x.
intros prf_x y prf_y.
apply prf_y, everyone.
- apply (nn_excluded_middle (exists y, ~D y)).
intros [[y sober] | drunk].
+ apply no with y.
intros drunk.
contradiction (drunk sober).
+ contradict someone.
intros y.
specialize (no y).
contradict no.
intros drunk_y z sober_z.
apply drunk.
exists z.
exact sober_z.
}
nn_int_to_class (exists y, D y -> forall z, D z) prf.
exact class_prf.
Defined.