从名义集绑定到函数与 lambda 抽象：置换模型逻辑与函数逻辑的联系
计算机科学中的逻辑
2013-05-28 v1
摘要
Permissive-Nominal Logic (PNL) 通过可以在其参数中绑定名字的项构造器扩展了一阶谓词逻辑。它在（许可）名义集中取语义。在 PNL 中，全称量词或 lambda 绑定器只是满足公理的项构造器，其指代是名义原子抽象上的函数。然后我们有高阶逻辑（HOL）及其在普通（即 Zermelo-Fraenkel）集合中的模型；全称量词或 lambda 的指代是完全或部分函数空间上的函数。这引出了以下问题：这两个绑定模型之间是如何联系的？在 PNL 和 HOL 之间，以及在名义集和函数之间，可能存在怎样的翻译？我们展示了从 PNL 到 HOL，以及从 PNL 模型到某些 HOL 模型的翻译。它是自然的，但也是部分的：我们将完整 PNL 的一个受限子系统翻译为 HOL。无法翻译的额外部分是名义集关于置换的对称性质。用一点名义集术语来说：我们可以翻译名字和绑定，但不能翻译它们的名义等变性性质。这似乎是合理的，因为 HOL——以及普通集合——不是等变的。因此，通过这种翻译来看，PNL 和 HOL 及其模型做着不同的事情，但它们享有同构的非平凡且丰富的子系统。
引用
@article{arxiv.1111.4611,
title = {From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions},
author = {Gilles Dowek and Murdoch Gabbay},
journal= {arXiv preprint arXiv:1111.4611},
year = {2013}
}