Formal languages are widely regarded as being above all mathematical objects and as producing a greater level of precision and technical complexity in logical investigations because of this. Yet defining formal languages exclusively in this way offers only a partial and limited explanation of the impact which their use actually has. In this book, Catarina Dutilh Novaes adopts a much wider conception of formal languages so as to investigate more broadly what exactly is (...) going on when theorists put these tools to use. She looks at the history and philosophy of formal languages and focuses on the cognitive impact of formal languages on human reasoning, drawing on their historical development, psychology, cognitive science and philosophy. Her wide-ranging study will be valuable for both students and researchers in philosophy, logic, psychology and cognitive and computer science. (shrink)

Revised version of chapter in J. N. Mohanty and W. McKenna (eds.), Husserl’s Phenomenology: A Textbook, Lanham: University Press of America, 1989, 29–67. -/- Logic for Husserl is a science of science, a science of what all sciences have in common in their modes of validation. Thus logic deals with universal laws relating to truth, to deduction, to verification and falsification, and with laws relating to theory as such, and to what makes for theoretical unity, both on the (...) side of the propositions of a theory and on the side of the domain of objects to which these propositions refer. This essay presents a systematic overview of Husserl’s views on these matters as put forward in his Logical Investigations. It shows how Husserl’s theory of linguistic meanings as species of mental acts, his formal ontology of part, whole and dependence, his theory of meaning categories, and his theory of categorial intuition combine with his theory of science to form a single whole. Finally, it explores the ways in which Husserl’s ideas on these matters can be put to use in solving problems in the philosophy of language, logic and mathematics in a way which does justice to the role of mental activity in each of these domains while at the same time avoiding the pitfalls of psychologism. (shrink)

Every branch of mathematics has its subject matter, and one of the distinguishing features of logic is that so many of its fundamental objects of study are rooted in language. The subject deals with terms, expressions, formulas, theorems, and proofs. When we speak about these notions informally, we are talking about things that can be written down and communicated with symbols. One of the goals of mathematical logic is to introduce formal definitions that capture our intuitions (...) about such objects and enable us to reason about them precisely. At the most basic level, syntactic objects can be viewed as strings of symbols. For concreteness, we can identify symbols with particular set-theoretic objects, but for most purposes, it doesn't matter what they are; all that is needed is that they are distinct from one another. (shrink)

This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal (...) language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification. (shrink)

Mathematical logic is a branch of mathematics that takes axiom systems and mathematical proofs as its objects of study. This book shows how it can also provide a foundation for the development of information science and technology. The first five chapters systematically present the core topics of classical mathematical logic, including the syntax and models of first-order languages, formal inference systems, computability and representability, and Gödel’s theorems. The last five chapters present extensions and (...) developments of classical mathematical logic, particularly the concepts of version sequences of formal theories and their limits, the system of revision calculus, proschemes (formal descriptions of proof methods and strategies) and their properties, and the theory of inductive inference. All of these themes contribute to a formal theory of axiomatization and its application to the process of developing information technology and scientific theories. The book also describes the paradigm of three kinds of language environments for theories and it presents the basic properties required of a meta-language environment. Finally, the book brings these themes together by describing a workflow for scientific research in the information era in which formal methods, interactive software and human invention are all used to their advantage. The second edition of the book includes major revisions on the proof of the completeness theorem of the Gentzen system and new contents on the logic of scientific discovery, R-calculus without cut, and the operational semantics of program debugging. This book represents a valuable reference for graduate and undergraduate students and researchers in mathematics, information science and technology, and other relevant areas of natural sciences. Its first five chapters serve as an undergraduate text in mathematical logic and the last five chapters are addressed to graduate students in relevant disciplines. (shrink)

Logicians have always found inspiration for new research in the ordinary language that is used on a daily basis and acquired naturally in childhood. Whereas the logical issues in the foundations of mathematics motivated the development of mathematical logic with its emphasis on notions of proof, validity, axiomatization, decidability, consistency, and completeness, the logical analysis of natural language motivated the development of philosophical logic with its emphasis on semantic notions of presupposition, entailment, modality, conditionals, and intensionality. The (...) relation between research programs in both mathematical and philosophical logic and natural language syntax and semantics as branches of theoretical linguistics has increased in importance throughout the last fifty years. This chapter reviews the development of one particularly interesting and lively area of interaction between formal logic and linguistics—the semantics of natural language. Research in this emergent field has proved fruitful for the development of empirically, cognitively adequate models of reasoning with partial information, sharing or exchanging information, dynamic interpretation in context, belief revision and other cognitive processes. (shrink)

Duality in Logic and Language [draft--do not cite this article] Duality phenomena occur in nearly all mathematically formalized disciplines, such as algebra, geometry, logic and natural language semantics. However, many of these disciplines use the term ‘duality’ in vastly different senses, and while some of these senses are intimately connected to each other, others seem to be entirely … Continue reading Duality in Logic and Language →.

Having studied mathematics, in particular foundations and philosophy of mathematics, it happened that I was asked to teach logic to the students in the Faculty of Philosophy of the Radboud University Nijmegen. It was there that I discovered that logic is much more than just a mathematical discipline consisting of definitions, theorems and proofs, and that logic can and should be embedded in a philosophical context. After ten years of teaching logic at the Faculty of (...) Philosophy at the Radboud University Nijmegen, thirty years at the Faculty of Philosophy of Tilburg University and nine years at the Faculty of Philosophy of the Erasmus University Rotterdam, I got many ideas how to improve my LOGIC book which was published twenty five years ago in 1993 by Verlag Peter Lang. Although the amount of work was enormous, I felt I should do it. It is like working on a large painting where you put some extra color in one corner, add a little detail at another place, shed some more light on a particular face, etc. (shrink)

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency (...) program. Similar efforts continue, but have been expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages. (shrink)

We discuss the differences between first-order set theory and second-order logic as a foundation for mathematics. We analyse these languages in terms of two levels of formalization. The analysis shows that if second-order logic is understood in its full semantics capable of characterizing categorically central mathematical concepts, it relies entirely on informal reasoning. On the other hand, if it is given a weak semantics, it loses its power in expressing concepts categorically. First-order set theory and second-order (...) logic are not radically different: the latter is a major fragment of the former. (shrink)

The two volumes in this advanced textbook present results, proof methods, and translations of motivational and philosophical considerations to formal constructions. In this Vol. I the author explains preferential structures and abstract size. In the associated Vol. II he presents chapters on theory revision and sums, defeasible inheritance theory, interpolation, neighbourhood semantics and deontic logic, abstract independence, and various aspects of nonmonotonic and other logics. In both volumes the text contains many exercises and some solutions, and the author (...) limits the discussion of motivation and general context throughout, offering this only when it aids understanding of the formal material, in particular to illustrate the path from intuition to formalisation. Together these books are a suitable compendium for graduate students and researchers in the area of computer science and mathematical logic. (shrink)

"Foundations of the Formal Sciences" is a series of interdisciplinary conferences in mathematics, philosophy, computer science and linguistics. The main goal is to reestablish the traditionally strong links between these areas of research that have been lost in the past decades. The second conference in the series had the subtitle "Applications of Mathematical Logic in Philosophy and Linguistics" and brought speakers from all parts of the Formal Sciences together to give a holistic view of how (...) class='Hi'>mathematical methods can improve our philosophical and technical understanding of language and scientific discourse, ranging from the theoretical level up to applications in language recognition software. Audience: This volume is of interest to all formal philosophers and theoretical linguists. In addition to that, logicians interested in the applications of their field and logic students in mathematics, computer science, philosophy and linguistics can use the volume to broaden their knowledge of applications of logic. (shrink)

We provide a syntax and a derivation system fora formal language of mathematics called Weak Type Theory (WTT). We give the metatheory of WTT and a number of illustrative examples.WTT is a refinement of de Bruijn''s Mathematical Vernacular (MV) and hence:– WTT is faithful to the mathematician''s language yet isformal and avoids ambiguities.

Mathematical Logic: An Introduction is a textbook that uses mathematical tools to investigate mathematics itself. In particular, the concepts of proof and truth are examined. The book presents the fundamental topics in mathematical logic and presents clear and complete proofs throughout the text. Such proofs are used to develop the language of propositional logic and the language of first-order logic, including the notion of a formal deduction. The text also covers Tarski’s definition (...) of truth and the computability concept. It also provides coherent proofs of Godel’s completeness and incompleteness theorems. Moreover, the text was written with the student in mind and thus, it provides an accessible introduction to mathematical logic. In particular, the text explicitly shows the reader how to prove the basic theorems and presents detailed proofs throughout the book. Most undergraduate books on mathematical logic are written for a reader who is well-versed in logical notation and mathematical proof. This textbook is written to attract a wider audience, including students who are not yet experts in the art of mathematical proof. (shrink)

This books states, as clearly and concisely as possible, the most fundamental principles of set-theory and mathematical logic. Included is an original proof of the incompleteness of formal logic. Also included are clear and rigorous definitions of the primary arithmetical operations, as well as clear expositions of the arithmetic of transfinite cardinals.

Assuming no previous study in logic, this informal yet rigorous text covers the material of a standard undergraduate first course in mathematical logic, using natural deduction and leading up to the completeness theorem for first-order logic. At each stage of the text, the reader is given an intuition based on standard mathematical practice, which is subsequently developed with clean formal mathematics. Alongside the practical examples, readers learn what can and can't be calculated; for example (...) the correctness of a derivation proving a given sequent can be tested mechanically, but there is no general mechanical test for the existence of a derivation proving the given sequent. The undecidability results are proved rigorously in an optional final chapter, assuming Matiyasevich's theorem characterising the computably enumerable relations. Rigorous proofs of the adequacy and completeness proofs of the relevant logics are provided, with careful attention to the languages involved. Optinal sections discuss the classification of mathematical structures by first-order theories; the required theory of cardinality is developed from scratch. Throughout the book there are notes on historical aspects of the material, and connections with linguistics and computer science, and the discussion of syntax and semantics is influenced by modern linguistic approaches. Two basic themes in recent cognitive science studies of actual human reasoning are also introduced. Including extensive exercises and selected solutions, this text is ideal for students in logic, mathematics, philosophy, and computer science. (shrink)

An excellent introduction to mathematical logic, this book provides readers with a sound knowledge of the most important approaches to the subject, stressing the use of logical methods in attacking nontrivial problems. It covers the logic of classes, of propositions, of propositional functions, and the general syntax of language, with a brief introduction that also illustrates applications to so-called undecidability and incompleteness theorems. Other topics include the simple proof of the completeness of the theory of combinations, Church's (...) theorem on the recursive unsolvability of the decision problem for the restricted function calculus, and the demonstrable properties of a formal system as a criterion for its acceptability. 1950 ed. (shrink)

"Foundations of the Formal Sciences" is a series of interdisciplinary conferences in mathematics, philosophy, computer science and linguistics. The main goal is to reestablish the traditionally strong links between these areas of research that have been lost in the past decades. The second conference in the series had the subtitle "Applications of Mathematical Logic in Philosophy and Linguistics" and brought speakers from all parts of the Formal Sciences together to give a holistic view of how (...) class='Hi'>mathematical methods can improve our philosophical and technical understanding of language and scientific discourse, ranging from the theoretical level up to applications in language recognition software. Audience: This volume is of interest to all formal philosophers and theoretical linguists. In addition to that, logicians interested in the applications of their field and logic students in mathematics, computer science, philosophy and linguistics can use the volume to broaden their knowledge of applications of logic. (shrink)

Depending on what one means by the main connective of logic, the -if..., then... -, several systems of logic result: classic and modal logics, intuitionistic logic or relevance logic. This book presents the underlying ideas, the syntax and the semantics of these logics. Soundness and completeness are shown constructively and in a uniform way. Attention is paid to the interdisciplinary role of logic: its embedding in the foundations of mathematics and its intimate connection with philosophy, (...) in particular the philosophy of language. Set theory is presented both as a conditio sine qua non for logic and as a interesting exact ontology. The study of infinite sets yields perplexing results. Formalization of informal number theory results in formal number theory; Godel's incompleteness is treated. At appropriate places attention is paid to paradoxes, intuitionism, conditionals, the historical development of logic, to logic programming and automated theorem proving for classical logic.". (shrink)

This thesis is on the history and philosophy of logic and semantics. Logic can be described as the ‘science of reasoning’, as it deals primarily with correct patterns of reasoning. However, logic as a discipline has undergone dramatic changes in the last two centuries: while for ancient and medieval philosophers it belonged essentially to the realm of language studies, it has currently become a sub-branch of mathematics. This thesis attempts to establish a dialogue between the modern and (...) the medieval traditions in logic, by means of ‘translations’ of the medieval logical theories into the modern framework of symbolic logic, i.e. formalizations. One of its conclusions is that, when properly understood within their own framework, the interest of medieval logical theories for modern investigations go beyond mere historical interest, but that a thorough conceptual analysis of such theories must be undertaken in order to avoid conceptual misprojections. While such translations of medieval into modern logic have been attempted before, the approach presented here is innovative in that attention is paid to the similarities as well as to the dissimilarities between the two traditions, and to what can be learned from the medieval masters for modern investigations in logic and semantics. (shrink)

A comprehensive introduction to formal logic, Logic and Philosophy: A Modern Introduction is a rigorous yet accessible text, appropriate for students encountering the subject for the first time. Abundant, carefully crafted exercise sets accompanied by a clear, engaging exposition build to an exploration of sentential logic, first-order predicate logic, the theory of descriptions, identity, relations, set theory, modal logic, and Aristotelian logic. And as its title suggests, Logic and Philosophy is devoted not (...) only to logic but also to the philosophical debates that led to the development of the field. Much new material has been added for the 13th edition. An introduction to set theory and its relationship to logic and mathematics, including philosophical issues, is now part of Chapter 13. Chapter 15 is an introduction to modal logic and Kripke semantics, concluding with a discussion of philosophical problems with any logical accommodation of modalities. Instructors who do not wish to present proof methods will find chapters on truth trees for both sentential and first-order logic, and a presentation of trees for modal logic. Special features of this text include presentations of the history of logic, alternatives to traditional methods of conditional and indirect proof, and a discussion of semantic problems with universal and existential instantiations. Throughout, the authors are sensitive to philosophical issues that arise from the relationship between ordinary language, symbolic logic, and justifications for the syntax and semantics of the various symbolic languages. Discussions range from the justification of the truth table for the sentential rendering of if... then statements to semantic and syntactic paradoxes, including some troubling paradoxes that arise in ordinary language (e.g., the so-called hangman or surprise quiz paradox). Logic and Philosophy includes ample material for a one-semester or two-semester course and provides a thorough preparation for more advanced logic courses. (shrink)

Logic and philosophy of logic have increasingly become areas of research and great interest in Latin America and Spain, where significant work has been done and continues to be done in both of these fields. The goal of this volume is to draw attention to this work through a collection of original and unpublished papers by specialists from Latin America and Spain. Some of the papers are of importance for set-theory and model theory. They cover topics such as (...) the foundations of paraconsistency, the use of paraconsistent logic as a basis for set-theory, and the methodological aspects in both the justification of new axioms in set theory and the formalization of pre-theoretic notions. Other papers are related to epistemic logic. They deal with the issues of abduction and the choice of the simplest hypothesis, the definition of group probability, and the nature of explanation and understanding in such logic. There are also papers on logical paradoxes, the semantics of names, and the nature of relations. Max A. Freund is Professor of Logic and Philosophy at the University of Costa Rica and the National University of Costa Rica. He is co-author of the book Modal Logic its syntax and semantics, as well as the author of Judicial Logic, and of a forthcoming book The Logic of Sortals. Max Fernandez de Castro is Professor of Logic and Philosophy at the Autonomous Metropolitan University of Mexico. He is the author of the book Quine y la Ontologíaa and co-author of the books Lógica Matemática I: lógica proposicional, intuicionista y modal, Lógica Matemática II: clásica, intuicionista y modal, Teoría de Conjuntos, Lógica y Temas Afines I. Marco Ruffino is Professor of Philosophy at the University of Campinas and the editor of Manuscrito, the Brazilian international journal for Analytic Philosophy. He has many publications, in important philosophical journals, in the philosophy of language, of logic, and of mathematics; in the history of analytic philosophy, and on Frege and Wittgenstein. (shrink)

Reasoning with quantifier expressions in natural language combines logical and arithmetical features, transcending strict divides between qualitative and quantitative. Our topic is this cooperation of styles as it occurs in common linguistic usage and its extension into the broader practice of natural language plus ‘grassroots mathematics’.We begin with a brief review of by changing the semantics of counting in natural ways. A first approach replaces cardinalities by abstract but well-motivated values of ‘mass’ or other mereological aggregating notions. A second approach (...) keeps the cardinalities but generalizes the meaning of counting to work in models that allow dependencies between variables.Finally, we return to our starting point in natural language, confronting the architecture of our formal systems with linguistic quantifier vocabulary and syntax, as well as with natural reasoning modules such as the monotonicity calculus. In addition to these encounters with formal semantics, we discuss the role of counting in semantic evaluation procedures for quantifier expressions and determine, for instance, which binary quantifiers are computable by finite ‘semantic automata’. We conclude with some general thoughts on yet further entanglements of logic and counting in formal systems, on rethinking the qualitative/quantitative divide, and on connecting our analysis to empirical findings in cognitive science. (shrink)

This is a short survey on the development of the formal specification and verification language H with emphasis on the scientific part. H is a modern highly expressive language solidly based upon advanced mathematical theories such as the internalisation of Kripke semantics within institution theory.

Logic and Computation is concerned with techniques for formal theorem-proving, with particular reference to Cambridge LCF (Logic for Computable Functions). Cambridge LCF is a computer program for reasoning about computation. It combines methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of statements in a programming language. This book consists of two parts. Part I outlines the mathematical preliminaries: elementary logic and domain theory. They are (...) explained at an intuitive level, giving references to more advanced reading. Part II provides enough detail to serve as a reference manual for Cambridge LCF. It will also be a useful guide for implementors of other programs based on the LCF approach. (shrink)

Language in Action demonstrates the viability of mathematical research into the foundations of categorial grammar, a topic at the border between logic and linguistics. Since its initial publication it has become the classic work in the foundations of categorial grammar. A new introduction to this paperback edition updates the open research problems and records relevant results through pointers to the literature. Van Benthem presents the categorial processing of syntax and semantics as a central component in a more general (...) dynamic logic of information flow, in tune with computational developments in artificial intelligence and cognitive science. Using the paradigm of categorial grammar, he describes the substructural logics driving the dynamics of natural language syntax and semantics. This is a general type-theoretic approach that lends itself easily to proof-theoretic and semantic studies in tandem with standard logic. The emphasis is on a broad landscape of substructural categorial logics and their proof-theoretical and semantic peculiarities. This provides a systematic theory for natural language understanding, admitting of significant mathematical results. Moreover, the theory makes possible dynamic interpretations that view natural languages as programming formalisms for various cognitive activities. (shrink)

In this article I deal with the notion of observation, from a phenomenologically motivated point of view, and its representation mainly by means of the formal language of quantum mechanics. In doing so, I have taken the notion of observation in two diverse contexts. In one context as a notion related with objects of a logical-mathematical theory taken as registered facts of phenomenological perception ( Wahrnehmung ) inasmuch as this phenomenological idea can also be linked with a process (...) of measurement on the quantum-mechanical level. In another context I have taken it as connected with a notion of temporal constitution basically as it is described in E. Husserl’s texts on the phenomenology of temporal consciousness. Given that mathematical objects as formal-ontological objects can be thought of as abstractions of perceptual objects by means of categorial intuition, the question is whether and under what theoretical assumptions we can, in principle, include quantum objects in abstraction in the class of formal-ontological objects and thus inquire on the limits of their description within a formal-axiomatical theory. On the one hand, I derive an irreducibility on the level of individuals taken in formal representation as syntactical atoms-substrates without any further content and on the other hand a transcendental subjectivity of consciousness objectified as a self-constituted temporal unity upon which it is ultimately grounded the possibility of generation of an abstract predicative universe of discourse. (shrink)

In dealing with the problem of the interrelations between mathematical logic and formal logic, we must first of all make clear just what mathematical logic is. In our opinion, the concept "mathematical logic" is employed in two different senses in mathematical and logical literature. A successful approach to our problem necessitates a clear differentiation between these two senses. Therefore we shall speak hereafter not of mathematical logic in general, but (...) of mathematical logic in the narrow meaning and in the broad meaning of the term. (shrink)

This book bridges the gaps between logic, mathematics and computer science by delving into the theory of well-quasi orders, also known as wqos. This highly active branch of combinatorics is deeply rooted in and between many fields of mathematics and logic, including proof theory, commutative algebra, braid groups, graph theory, analytic combinatorics, theory of relations, reverse mathematics and subrecursive hierarchies. As a unifying concept for slick finiteness or termination proofs, wqos have been rediscovered in diverse contexts, and proven (...) to be extremely useful in computer science. The book introduces readers to the many facets of, and recent developments in, wqos through chapters contributed by scholars from various fields. As such, it offers a valuable asset for logicians, mathematicians and computer scientists, as well as scholars and students. (shrink)

Meaning and Argument shifts introductory logic from the traditional emphasis on proofs to the symbolization of arguments. It is an ideal introduction to formal logic, philosophical logic, and philosophy of language. Distinctive approach in that this text is a philosophical, rather than mathematical introduction to logic Concentrates on symbolization and does all the technical logic simply with truth tables and no derivations at all Contains numerous exercises and a corresponding answer key Extensive Appendix (...) which allows the reader to explore subjects that go beyond what is usually covered in an introductory logic course. (shrink)

Meaning and Argument shifts introductory logic from the traditional emphasis on proofs to the symbolization of arguments. Another distinctive feature of this book is that it shows how the need for expressive power and for drawing distinctions forces formal language development. This revised edition includes expanded sections, additional exercises, and an updated bibliography. Updated and revised edition includes extended sections, additional exercises, and an updated bibliography. Distinctive approach in that this text is a philosophical, rather than mathematical (...) introduction to logic. Concentrates on symbolization and does all the technical logic simply with truth tables and no derivations at all. Contains numerous exercises and a corresponding answer key. Extensive appendix which allows the reader to explore subjects that go beyond what is usually covered in an introductory logic course. Features accompanying website at www.meaningargument.com. (shrink)

Investigating meta-programming within the logic programming paradigm, Meta-Logics and Logic Programming presents original research on an important extension of logic programming that makes it more amenable for knowledge representation and programming in general. The 12 contributions, many written especially for this book, explore the foundations, language design issues, and applications of meta-programming in logic programming. Meta-programming—the process of writing computer programs that can manipulate representations of other programs—has been key both in the foundations of computer science (...) and in its practical developments. Examples of meta-programs include compilers, interpreters, program analyzers, and partial evaluators. The choice of logic programming as a basis for meta-programming offers several practical and theoretical advantages: among them, the possibility of tackling critical foundational problems of meta-programming within a strong theoretical framework, and the surprising ease of programming. The usual framework of logic programming (and more generally first-order logic), however, has to be modified and extended to formally deal with meta-programs, extensions the editors call "meta-logics." Along with an exploration of meta-programming in logic programming, the definitions, formal properties, and use of these extensions constitute one of the book's main themes. The first part of the book, Foundations, focuses on the representation problem—how object programs are represented within meta-programs. The second part, Language Support for Meta-Logics, is concerned with language extensions that make meta-programming easier and more elegant. The third part, Meta-Logics for Knowledge Management, deals with the use of meta-logic for advanced knowledge representation purposes. Logic Programming series. (shrink)

Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought (1879), by G. Frege.--Some metamathematical results on completeness and consistency; On formally undecidable propositions of Principia mathematica and related systems I; and On completeness and consistency (1930b, 1931, and 1931a), by K. Gödel.--Bibliography (p. [111]-116).

This volume honours the life and work of Solomon Feferman, one of the most prominent mathematical logicians of the latter half of the 20th century. In the collection of essays presented here, researchers examine Feferman’s work on mathematical as well as specific methodological and philosophical issues that tie into mathematics. Feferman’s work was largely based in mathematical logic, but also branched out into methodological and philosophical issues, making it well known beyond the borders of the mathematics (...) community. With regard to methodological issues, Feferman supported concrete projects. On the one hand, these projects calibrate the proof theoretic strength of subsystems of analysis and set theory and provide ways of overcoming the limitations imposed by Gödel’s incompleteness theorems through appropriate conceptual expansions. On the other, they seek to identify novel axiomatic foundations for mathematical practice, truth theories, and category theory. In his philosophical research, Feferman explored questions such as “What is logic?” and proposed particular positions regarding the foundations of mathematics including, for example, his “conceptual structuralism.” The contributing authors of the volume examine all of the above issues. Their papers are accompanied by an autobiography presented by Feferman that reflects on the evolution and intellectual contexts of his work. The contributing authors critically examine Feferman’s work and, in part, actively expand on his concrete mathematical projects. The volume illuminates Feferman’s distinctive work and, in the process, provides an enlightening perspective on the foundations of mathematics and logic. (shrink)

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. (shrink)

Recent historical studies have investigated the first proponents of methodological structuralism in late nineteenth-century mathematics. In this paper, I shall attempt to answer the question of whether Peano can be counted amongst the early structuralists. I shall focus on Peano’s understanding of the primitive notions and axioms of geometry and arithmetic. First, I shall argue that the undefinability of the primitive notions of geometry and arithmetic led Peano to the study of the relational features of the systems of objects that (...) compose these theories. Second, I shall claim that, in the context of independence arguments, Peano developed a schematic understanding of the axioms which, despite diverging in some respects from Dedekind’s construction of arithmetic, should be considered structuralist. From this stance I shall argue that this schematic understanding of the axioms anticipates the basic components of a formal language. (shrink)

Many books explain what is known about the universe. This book investigates what cannot be known. Rather than exploring the amazing facts that science, mathematics, and reason have revealed to us, this work studies what science, mathematics, and reason tell us cannot be revealed. In The Outer Limits of Reason, Noson Yanofsky considers what cannot be predicted, described, or known, and what will never be understood. He discusses the limitations of computers, physics, logic, and our own thought processes. Yanofsky (...) describes simple tasks that would take computers trillions of centuries to complete and other problems that computers can never solve; perfectly formed English sentences that make no sense; different levels of infinity; the bizarre world of the quantum; the relevance of relativity theory; the causes of chaos theory; math problems that cannot be solved by normal means; and statements that are true but cannot be proven. He explains the limitations of our intuitions about the world -- our ideas about space, time, and motion, and the complex relationship between the knower and the known. Moving from the concrete to the abstract, from problems of everyday language to straightforward philosophical questions to the formalities of physics and mathematics, Yanofsky demonstrates a myriad of unsolvable problems and paradoxes. Exploring the various limitations of our knowledge, he shows that many of these limitations have a similar pattern and that by investigating these patterns, we can better understand the structure and limitations of reason itself. Yanofsky even attempts to look beyond the borders of reason to see what, if anything, is out there. (shrink)

This volume contains the proceedings of DEON2020/2021, the 15th International Conference on Deontic Logic and Normative Systems that was organized by the Munich Center for Mathematical Philosophy at LMU Munich (Germany) on 21st-24th July, 2021. The biennial DEON conferences are designed to promote interdisciplinary cooperation amongst scholars interested in linking the formal-logical study of normative concepts, normative language and normative systems with computer science, artificial intelligence, linguistics, philosophy, organization theory, and law.

Theory of Computation -- Mathematical Logic and Formal Languages.

Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as Alternating-time Temporal Logic (...) (ATL). The key insight in ATL is that the path quantifiers of CTL could be replaced by cooperation modalities, of the form , where is a set of agents. The intended interpretation of an ATL formula is that the agents can cooperate to ensure that holds (equivalently, that have a winning strategy for ). In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as group can cooperate to bring about iff it is common knowledge in that . The resulting logic — Alternating-time Temporal Epistemic Logic (ATEL) — shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems. (shrink)