Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In PNL, the forall-quantifier or lambda-binder are just term-formers satisfying axioms, and their denotation is functions on nominal atoms-abstraction. Then we have higher-order logic (HOL) and its models in ordinary (i.e. Zermelo-Fraenkel) sets; the denotation of forall or lambda is functions on full or partial function spaces. This raises the following question: how are these two models of binding connected? What translation is possible between PNL and HOL, and between nominal sets and functions? We exhibit a translation of PNL into HOL, and from models of PNL to certain models of HOL. It is natural, but also partial: we translate a restricted subsystem of full PNL to HOL. The extra part which does not translate is the symmetry properties of nominal sets with respect to permutations. To use a little nominal jargon: we can translate names and binding, but not their nominal equivariance properties. This seems reasonable since HOL -- and ordinary sets -- are not equivariant. Thus viewed through this translation, PNL and HOL and their models do different things, but they enjoy non-trivial and rich subsystems which are isomorphic.

翻译：许可标称逻辑（PNL）通过引入可在参数中绑定名称的项构成算子，扩展了一阶谓词逻辑。该逻辑以（许可）标称集合为其语义。在PNL中，全称量词或lambda绑定器仅是满足公理的项构成算子，其指称是标称原子抽象上的函数。而高阶逻辑（HOL）及其在普通（即策梅洛-弗兰克尔）集合中的模型，其全称量词或lambda的指称是完整或部分函数空间上的函数。由此引发如下问题：这两种绑定模型如何关联？PNL与HOL之间、标称集合与函数之间可能存在何种翻译？我们展示了从PNL到HOL的翻译，以及从PNL模型到特定HOL模型的映射。这一翻译是自然的，但存在局限性：仅将完全PNL的限制性子系统翻译至HOL。未被翻译的额外部分是对称性属性（即标称集合关于置换的对称性质）。用标称术语而言：能够翻译名称与绑定，但无法翻译其标称等变性。这似乎合理，因为HOL（以及普通集合）不具备等变性。因此，通过该翻译审视，PNL与HOL及其模型虽然各有侧重，但共享非平凡且丰富的同构子系统。