Перевод с двойным отрицанием включает три логические системы. Есть классическая логика c и интуиция c логика c, но перевод не является частью ни одной из этих логик. В конце концов, перевод - это отношения между двумя разными вселенными логики; как это может принадлежать одному из них? Вместо этого эти логики должны быть построены как объекты внутри некоторых других логик c (вероятно, в те, в которые вы "верите" или "реальны"), и тогда перевод с двойным отрицанием является теоремой этого ambient logi c, который описывает две внутренние логики. TL; DR: перевод с двойным отрицанием - это процесс / теорема о logi c, а не в logi c.
По этой причине вы не можете написать перевод с двойным отрицанием как лемму в логике c из 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, вам придется сделать это доказательство в какой-то «высшей» системе логик c, которая обычно является либо неформальной логикой естественного языка c, которую я сейчас использую, или язык Lta c, язык tacti c. Программы Lta c - это программы, которые Coq запускает для генерации доказательств. В частности, вы могли бы написать две тактики. Один из них, если вы дадите ему термин excluded_middle -> P (он же классическое доказательство P), по существу попытается root исключить все варианты использования этой классики, чтобы получить новое, интуитивное c доказательство двойного перевод отрицания P. Другой, учитывая (интуитивно c) доказательство перевода двойного отрицания P, превращает его в классическое доказательство P (иначе оно доказывает excluded_middle -> P). (Обратите внимание на мой осторожный язык: я говорю P, но не NN P, только «перевод двойного отрицания P». Это потому, что вне Coq, на естественном языке или Lta c, мы можем определить, что такое «перевод двойного отрицания 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 _).
Оглядываясь назад, я думаю, что вы могли бы реализовать это направление с Class es и Instance s (тип направленный поиск неявных значений - это еще один процесс Coq, который находится за пределами логики c из 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.