English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Permissive-Nominal Logic (PNL) extends first-order predicate logic withterm-formers that can bind names in their arguments. It takes a semantics in(permissive-)nominal sets. In PNL, the forall-quantifier or lambda-binder arejust term-formers satisfying axioms, and their denotation is functions onnominal 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 fullor partial function spaces.  This raises the following question: how are these two models of bindingconnected? What translation is possible between PNL and HOL, and betweennominal sets and functions?  We exhibit a translation of PNL into HOL, and from models of PNL to certainmodels of HOL. It is natural, but also partial: we translate a restrictedsubsystem of full PNL to HOL. The extra part which does not translate is thesymmetry properties of nominal sets with respect to permutations. To use alittle nominal jargon: we can translate names and binding, but not theirnominal equivariance properties. This seems reasonable since HOL---and ordinarysets---are not equivariant.  Thus viewed through this translation, PNL and HOL and their models dodifferent things, but they enjoy non-trivial and rich subsystems which areisomorphic.

From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions