Bulletin of Symbolic Logic 17 (2):161-229 (2011)
|Abstract||We are used to the idea that computers operate on numbers, yet another kind of data is equally important: the syntax of formal languages, with variables, binding, and alpha-equivalence. The original application of nominal techniques, and the one with greatest prominence in this paper, is to reasoning on formal syntax with variables and binding. Variables can be modelled in many ways: for instance as numbers (since we usually take countably many of them); as links (since they may `point' to a binding site in the term, where they are bound); or as functions (since they often, though not always, represent `an unknown'). None of these models is perfect. In every case for the models above, problems arise when trying to use them as a basis for a fully formal mechanical treatment of formal language. The problems are practical—but their underlying cause may be mathematical. The issue is not whether formal syntax exists, since clearly it does, so much as what kind of mathematical structure it is. To illustrate this point by a parody, logical derivations can be modelled using a Gödel encoding (i.e., injected into the natural numbers). It would be false to conclude from this that proof-theory is a branch of number theory and can be understood in terms of, say, Peano's axioms. Similarly, as it turns out, it is false to conclude from the fact that variables can be encoded e.g., as numbers, that the theory of syntax-with-binding can be understood in terms of the theory of syntax-without-binding, plus the theory of numbers (or, taking this to a logical extreme, purely in terms of the theory of numbers). It cannot; something else is going on. What that something else is, has not yet been fully understood. In nominal techniques, variables are an instance of names, and names are data. We model names using urelemente with properties that, pleasingly enough, turn out to have been investigated by Fraenkel and Mostowski in the first half of the 20th century for a completely different purpose than modelling formal language. What makes this model really interesting is that it gives names distinctive properties which can be related to useful logic and programming principles for formal syntax. Since the initial publications, advances in the mathematics and presentation have been introduced piecemeal in the literature. This paper provides in a single accessible document an updated development of the foundations of nominal techniques. This gives the reader easy access to updated results and new proofs which they would otherwise have to search across two or more papers to find, and full proofs that in other publications may have been elided. We also include some new material not appearing elsewhere|
|Keywords||Nominal techniques logic and set theory nominal abstract syntax atoms-abstraction names variable binding inductive syntax up to binding alpha-equivalence|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
James Cheney (2006). Completeness and Herbrand Theorems for Nominal Logic. Journal of Symbolic Logic 71 (1):299 - 320.
Kerstin Anna Kunz (2010). Variation in English and German Nominal Coreference: A Study of Political Essays. Peter Lang.
Jan Woleński (2012). Logic as Calculus Versus Logic as Language, Language as Calculus Versus Language as Universal Medium, and Syntax Versus Semantics. Logica Universalis 6 (3-4):587-596.
Tom Sgouros (2005). What is Context For? Syntax in a Non-Abstract World. Journal of Logic, Language and Information 14 (2):235-251.
Don Pigozzi & Antonino Salibra (1995). The Abstract Variable-Binding Calculus. Studia Logica 55 (1):129 - 179.
Robin Hirsch, Ian Hodkinson & Roger D. Maddux (2002). Provability with Finitely Many Variables. Bulletin of Symbolic Logic 8 (3):348-379.
C. F. M. Vermeulen (2000). Variables as Stacks. Journal of Logic, Language and Information 9 (2):143-167.
Sarah Moss (2012). The Role of Linguistics in the Philosophy of Language. In Delia Graff Fara & Gillian Russell (eds.), Routledge Companion to the Philosophy of Language.
Newton C. A. da Costa & Chris Mortensen (1983). Notes on the Theory of Variable Binding Term Operators. History and Philosophy of Logic 4 (1-2):63-72.
Michał Walicki (2012). Introduction to Mathematical Logic. World Scientific.
V. Frederick Rickey (1972). Axiomatic Inscriptional Syntax. I. General Syntax. Notre Dame Journal of Formal Logic 13 (1):1-33.
Frederick Rickey (1973). Axiomatic Inscriptional Syntax. Part II: The Syntax of Protothetic. Notre Dame Journal of Formal Logic 14 (1):1-52.
Added to index2011-05-20
Total downloads4 ( #188,845 of 722,783 )
Recent downloads (6 months)0
How can I increase my downloads?