双否定翻译涉及三个逻辑系统。有经典逻辑和直觉逻辑，但翻译不是这两种逻辑的一部分。毕竟，翻译是两个不同的逻辑世界之间的关系；它怎么可能属于其中一个呢？相反，这些逻辑需要被构造为其他逻辑(可能是你"相信"或"真实"的逻辑(内部的对象，然后双重否定翻译是描述两个内部逻辑的环境逻辑的定理。TL；DR：双重否定翻译是一个关于逻辑的过程/定理，而不是中的。
我试图定义Coq中所有命题的双否定翻译，这样我就可以证明"直觉逻辑"中不可证明的(或有很难证明的(经典事实，但我认为使用Inductive或Fixpoint关键字是不可能的。对于Fixpoint，我需要匹配一个任意命题。(虽然我只需要一阶逻辑，即合取、析取、条件、否定和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).
我该如何定义这样的定义？
出于这个原因，你不能把双重否定翻译写成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(是否可以这样做。以下是Drinker悖论的证明：
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.