在Coq中提升存在感

Question

可以在Coq中证明这个引理吗？

Lemma liftExists : forall (P : nat -> nat -> Prop),
  (forall n:nat, exists p:nat, P n p)
  -> exists (f : nat -> nat), forall n:nat, P n (f n).

简单的destruct不编译，因为我们无法在exists p:nat, P n p排序中消除对象Prop，以在f排序中生成函数Set。

如果Coq无法证明这个引理，那么forall n:nat, exists p:nat, P n p的含义是什么？在建设性数学中，它将意味着函数f的存在，但我的印象是我们永远不会在Coq中看到这个函数f，甚至在上面所表达的Prop排序中也是如此。

Answer 1

由于限制将Prop删除到Set中，因此Coq无法证明这一点。至于哲学的“意义”，我不确定是否有人有关于此的非常好的故事。 forall n:nat, exists p:nat, P n p的居民是函数返回一对p和一个证明，但另外它们是一个在编译程序时可以忽略的函数，因为你知道什么都不会看到返回的值。

因此，部分这种Prop与Set系统是一种更有效地编译程序的方法，但实际上它也用于逻辑属性。在Coq中，Prop类型是不可预测的，而Set类型则不是，即使如此，将Props的中间规律作为公理，并证明这是一致的，你可以诉诸于“proof-irrelevant model”，你在通过忽略除了它们是否有人居住之外的所有信息，将道具中的类型解释为集合。从经典逻辑的角度来看（所有你关心的都是真值），这是有道理的，但如果你对建设性的数学感兴趣，那就有点奇怪了！