匹配道具？或任何其他定义“双重否定翻译”的方式

Question

我正在尝试为Coq中的所有命题定义Double-negation translation，因此我可以证明“直觉逻辑”中无法证明（或具有非常严格的证明）的经典事实，但是我认为这不可能通过使用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).

关于如何定义这样的定义的任何想法？

Answer 1

双重否定转换涉及三个逻辑系统。有经典的逻辑和直觉的逻辑，但是翻译不是这两种逻辑的一部分。毕竟，翻译是两个不同逻辑领域之间的关系。它怎么能属于其中之一？取而代之的是，这些逻辑需要被构造为其他逻辑的对象（可能是您“相信”或“真实”的）逻辑，然后双重否定翻译是描述该逻辑的环境逻辑的一个定理。两种内在逻辑。 TL; DR：双重否定翻译是一种过程/定理about逻辑，而不是within逻辑。因此，您无法在Coq的逻辑内编写双重否定转换，例如引理。我的意思是，您当然可以定义

Inductive sentence : Set := ... . (* E.g. syntax of FOL *)
Definition NN : sentence -> sentence.
Definition classically_provable : NN -> Prop.
Definition intuitionistically_provable : NN -> 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的outside用自然语言或Ltac，我们可以定义“ P的双重否定转换”是什么。内部 Coq，对此没有可定义的NN : Prop -> Prop。）因此，例如，您可以这样定义命题的翻译：

Ltac nn_transl P :=
  match 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 x: ?T, ?Q =>
    let Q' := nn_transl Q in
    uconstr:(forall x: T, Q')
  | exists x: ?T, ?Q =>
    let Q' := nn_transl Q in
    uconstr:(~forall x: T, ~Q')
  | _ => uconstr:(~~P)
  end.

实施证明的实际翻译似乎并不容易，但应该可行。