## Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free.(English)Zbl 1251.03035

Summary: By operations on models we show how to relate completeness with respect to permissive-nominal models to completeness with respect to nominal models with finite support. Models with finite support are a special case of permissive-nominal models, so the construction hinges on generating from an instance of the latter, some instance of the former in which sufficiently many inequalities are preserved between elements. We do this using an infinite generalisation of nominal atoms-abstraction.
The results are of interest in their own right, but also, we factor the mathematics so as to maximise the chances that it could be used off-the-shelf for other nominal reasoning systems too. Models with infinite support can be easier to work with, so it is useful to have a semi-automatic theorem to transfer results from classes of infinitely-supported nominal models to the more restricted class of models with finite support.
In conclusion, we consider different permissive-nominal syntaxes and nominal models and discuss how they relate to the results proved here.

### MSC:

 03B70 Logic in computer science 03C98 Applications of model theory 03G25 Other algebras related to logic
Full Text:

### References:

 [1] James Cheney Completeness and Herbrand theorems for nominal logic , Journal of Symbolic Logic, vol. 71(2006), pp. 299-320. · Zbl 1100.03016 · doi:10.2178/jsl/1140641176 [2] Nicolaas G. de Bruijn Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem , Indagationes Mathematicae , vol. 34(1972), no. 5, pp. 381-392. · Zbl 0253.68007 [3] Gilles Dowek and Murdoch J. Gabbay Permissive nominal logic , Proceedings of the 12th international ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming $$($$PPDP 2010$$)$$,2010, pp. 165-176. [4] —- Permissive nominal logic , Transactions on Computational Logic ,(2012), · Zbl 1352.03042 [5] Gilles Dowek, Murdoch J. Gabbay, and Dominic P. Mulligan Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques , Logic Journal of the IGPL , vol. 18(2010), no. 6, pp. 769-822, (journal version). · Zbl 1215.03048 · doi:10.1093/jigpal/jzq006 [6] Murdoch J. Gabbay FM-HOL a higher-order theory of names, 35 years of Automath (F. Kamareddine, editor),2002. [7] —- A general mathematics of names , Information and Computation , vol. 205(2007), no. 7, pp. 982-1011. · Zbl 1123.03047 · doi:10.1016/j.ic.2006.10.010 [8] —- Nominal algebra and the HSP theorem, Journal of Logic and Computation , vol. 19(2009), no. 2, pp. 341-367. · Zbl 1163.03017 · doi:10.1093/logcom/exn055 [9] —- Foundations of nominal techniques: logic and semantics of variables in abstract syntax , Bulletin of Symbolic Logic, vol. 17(2011), no. 2, pp. 161-229. · Zbl 1253.03059 · doi:10.2178/bsl/1305810911 [10] —- Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables , Mathematical Structures in Computer Science , vol. 21(2011), pp. 997-1033. · Zbl 1228.68022 · doi:10.1017/S0960129511000272 [11] —- Meta-variables as infinite lists in nominal terms unification and rewriting , Logic Journal of the IGPL ,(2012), · Zbl 1278.68119 [12] —- Nominal terms and nominal logics: from foundations to meta-mathematics , Handbook of philosophical logic , vol. 17, Kluwer,2012. [13] Murdoch J. Gabbay and Aad Mathijssen A formal calculus for informal equality with binding , WoLLIC ’07: 14th Workshop on Logic, Language, Information and Computation, Lecture Notes in Computer Science, vol. 4576, Springer,2007, pp. 162-176. · Zbl 1213.03038 · doi:10.1007/978-3-540-73445-1_12 [14] —- Nominal universal algebra: equational logic with names and binding , Journal of Logic and Computation , vol. 19(2009), no. 6, pp. 1455-1508. · Zbl 1191.08003 · doi:10.1093/logcom/exp033 [15] Murdoch J. Gabbay and Andrew M. Pitts A new approach to abstract syntax with variable binding , Formal Aspects of Computing , vol. 13(2001), no. 3-5, pp. 341-363. · Zbl 1001.68083 · doi:10.1007/s001650200016 [16] Wilfrid Hodges Model theory , Cambridge University Press,1993. [17] Dominic P. Mulligan Online nominal bibliography ,2010, family http://www.citeulike.org/ group/11951/. [18] M. H. A. Newman On theories with a combinatorial definition of equivalence , Annals of Mathematics , vol. 43(1942), no. 2, pp. 223-243. · Zbl 0060.12501 · doi:10.2307/1968867 [19] Andrew M. Pitts Nominal logic, a first order theory of names and binding , Information and Computation , vol. 186(2003), no. 2, pp. 165-193. · Zbl 1056.03014 · doi:10.1016/S0890-5401(03)00138-X [20] Christian Urban, Andrew M. Pitts, and Murdoch J. Gabbay Nominal unification , Theoretical Computer Science , vol. 323(2004), no. 1-3, pp. 473-497. · Zbl 1078.68140 · doi:10.1016/j.tcs.2004.06.016
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.