×

zbMATH — the first resource for mathematics

Completeness and Herbrand theorems for nominal logic. (English) Zbl 1100.03016
Summary: Nominal logic [A. M. Pitts, Inf. Comput. 186, 165–193 (2003; Zbl 1056.03014)] is a variant of first-order logic in which abstract syntax with names and binding is formalized in terms of two basic operations: name-swapping and freshness. It relies on two important principles: equivariance (validity is preserved by name-swapping), and fresh name generation (“new” or fresh names can always be chosen). It is inspired by a particular class of models for abstract syntax trees involving names and binding, drawing on ideas from Fraenkel-Mostowski set theory: finite-support models in which each value can depend on only finitely many names.
Although nominal logic is sound with respect to such models, it is not complete. In this paper we review nominal logic and show why finite-support models are insufficient both in theory and practice. We then identify (up to isomorphism) the class of models with respect to which nominal logic is complete: ideal-supported models in which the supports of values are elements of a proper ideal on the set of names. We also investigate an appropriate generalization of Herbrand models to nominal logic. After adjusting the syntax of nominal logic to include constants denoting names, we generalize universal theories to nominal-universal theories and prove that each such theory has an Herbrand model.

MSC:
03B70 Logic in computer science
03B60 Other nonclassical logic
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Foundations of Databases (1995) · Zbl 0842.68022
[2] DOI: 10.1145/359657.359659 · Zbl 0387.68003
[3] Higher Order Operational Techniques in Semantics (1997)
[4] The Definition of Standard ML - Revised (1997)
[5] DOI: 10.1016/0890-5401(92)90008-4 · Zbl 0752.68036
[6] Proceedings of the 18th Symposium on Logic in Computer Science (LICS) pp 118– (2003)
[7] Sheaves in Geometry and Logic: A First Introduction to Topos Theory (1992)
[8] DOI: 10.1016/0020-0190(95)00144-2 · Zbl 0875.94114
[9] DOI: 10.1016/S0304-3975(96)00171-5 · Zbl 0903.68105
[10] DOI: 10.2178/bsl/1182353871
[11] Handbook of Mathematical Logic pp 345– (1977)
[12] Introduction to Automata Theory, Languages, and Computation (1979) · Zbl 0426.68001
[13] The completeness of the first-order functional calculus 14 pp 159– (1949)
[14] DOI: 10.1145/138027.138060 · Zbl 0778.03004
[15] Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (1994) · Zbl 0828.68036
[16] DOI: 10.1007/s001650200016 · Zbl 1001.68083
[17] Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS) pp 139– (2004)
[18] Workshop on Thirty Five Years of Automath (2002)
[19] Labelled Non-Classical Logics (2000)
[20] From Frege to Gödel pp 1– (1967)
[21] DOI: 10.1016/S0890-5401(03)00023-3 · Zbl 1054.68028
[22] From Frege to Gödel pp 284– (1967)
[23] Automorphisms of First-Order Structures pp 131– (1994)
[24] Models of ZF-Set Theory 223 (1970)
[25] Denotational Semantics: The Scott-Strachey Aapproach to Programming Language Ttheory 1 (1981)
[26] Combinatory Logic (1958)
[27] A formulation of the simple theory of types 5 pp 56– (1940)
[28] From Frege to Gödel pp 355– (1967)
[29] An Introduction to Non-Classical Logic (2001) · Zbl 0981.03002
[30] Proceedings of the 20th International Conference on Logic Programming (ICLP) 3132 pp 269– (2004)
[31] Proceedings of the Conference on Foundations of Software Science and Computation Structures (FOSSACS) 3441 pp 379– (2005)
[32] Proceedings of the Conference on Rewriting Techniques and Applications (RTA) 3467 pp 74– (2005)
[33] Natural Deduction: A Proof-Theoretical Study (1965) · Zbl 0173.00205
[34] DOI: 10.1016/S0890-5401(03)00021-X · Zbl 1054.68079
[35] DOI: 10.1007/978-3-540-27836-8_30
[36] Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) pp 199– (1989)
[37] Notre Dame Journal of Formal Logic 31 pp 64– (1990)
[38] DOI: 10.2307/421090 · Zbl 0930.03095
[39] Indagationes Mathematicae 34 pp 381– (1972)
[40] Principles of Program Analysis (2005) · Zbl 1069.68534
[41] The Lambda Calculus (1984)
[42] DOI: 10.1007/978-3-540-30124-0_20
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.