The provability problem in intuitionistic propositional second-order logic with existential quantifier and implication (∃,→) is proved to be undecidable in presence of free type variables (constants). This contrasts with the result that inutitionistic propositional second-order logic with existential quantifier, conjunction and negation is decidable.

There is an intimate connection between proofs of the natural deduction systems and typed lambda calculus. It is well-known that in simply typed lambda calculus, the notion of formulae-as-types makes it possible to find fine structure of the implicational fragment of intuitionistic logic, i.e., relevant logic, BCK-logic and linear logic. In this paper, we investigate three classical substructural logics (GL, GLc, GLw) of Gentzen's sequent calculus consisting of implication and negation, which contain some of the right structural rules. In terms (...) of Parigot's -calculus with proper restrictions, we introduce a proof term assignment to these classical substructural logics. According to these notions, we can classify the -terms into four categories. It is proved that well-typed GLx--terms correspond to GLx proofs, and that a GLx--term has a principal type if stratified where x is nil, c, w or cw. Moreover, we investigate embeddings of classical substructural logics into the corresponding intuitionistic substructural logics. It is proved that the Gödel-style translations of GLx--terms are embeddings preserving substructural logics. As by-products, it is obtained that an inhabitation problem is decidable and well-typed GLx--terms are strongly normalizable. (shrink)

The third author gave a natural deduction style proof system called the \-calculus for implicational fragment of classical logic in. In -calculus, 2015, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear), the fourth author gave a natural subsystem “intuitionistic \-calculus” of the \-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus, but is complicated. In this paper, we introduce some reduction rules for the \-calculus, and give (...) a simple and purely syntactical proof to the theorem by use of the reduction. In addition, we show that we can give a computation model with rich expressive power with our system. (shrink)

This paper shows that the inhabitation problem in the lambda calculus with negation, product, polymorphic, and existential types is decidable, where the inhabitation problem asks whether there exists some term that belongs to a given type. In order to do that, this paper proves the decidability of the provability in the logical system defined from the second-order natural deduction by removing implication and disjunction. This is proved by showing the quantifier elimination theorem and reducing the problem to the provability in (...) propositional logic. The magic formulas are used for quantifier elimination such that they replace quantifiers. As a byproduct, this paper also shows the second-order witness theorem which states that a quantifier followed by negation can be replaced by a witness obtained only from the formula. As a corollary of the main results, this paper also shows Glivenko’s theorem, Double Negation Shift, and conservativity for antecedent-empty sequents between the logical system and its classical version. (shrink)

In this paper we describe the Curry-Howard-De Bruijn isomorphism between Higher Order Many Sorted Intuitionistic Predicate Logic PREDω and the type system λPREDω, which can be considered a subsystem of the Calculus of Constructions. The type system is presented using the concept of a Pure Type System, which is a very elegant framework for describing type systems. We show in great detail how formulae and proof trees of the logic relate to types and terms of the type system, respectively. Finally, (...) we discuss some consequences of the isomorphism with respect to the relation between the systems discussed in this paper. (shrink)

This paper gives new confluence proofs for several lambda calculi with permutation-like reduction, including lambda calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions, and a lambda calculus with explicit substitutions. For lambda calculi with permutative conversion, naïve parallel reduction technique does not work, and traditional notion of residuals is required as Ando pointed out. This paper shows that the difficulties can be avoided by extending the technique proposed by Dehornoy and van Oostrom, called the Z (...) theorem: existence of a mapping on terms with the Z property concludes the confluence. Since it is still hard to directly define a mapping with the Z property for the lambda calculi with permutative conversions, this paper extends the Z theorem to compositional functions, called compositional Z, and shows that we can adopt it to the calculi. (shrink)

This paper applies Dehornoy et al.’s Z theorem and its variant, called the compositional Z theorem, to prove confluence of Parigot’s \-calculi extended by the simplification rules. First, it is proved that Baba et al.’s modified complete developments for the call-by-name and the call-by-value variants of the \-calculus with the renaming rule, which is one of the simplification rules, satisfy the Z property. It gives new confluence proofs for them by the Z theorem. Secondly, it is shown that the compositional (...) Z theorem can be applied to prove confluence of the call-by-name and the call-by-value \-calculi with both simplification rules, the renaming and the \-rules, whereas it is hard to apply the ordinary parallel reduction technique or the original Z theorem by one-pass definition of mappings for these variants. (shrink)

This paper analyses and compares some of the automated reasoners that have been used in recent research for compliance checking. Although the list of the considered reasoners is not exhaustive, we believe that our analysis is representative enough to take stock of the current state of the art in the topic. We are interested here in formalizations at the _first-order_ level. Past literature on normative reasoning mostly focuses on the _propositional_ level. However, the propositional level is of little usefulness for (...) concrete LegalTech applications, in which compliance checking must be enforced on (large) sets of individuals. Furthermore, we are interested in technologies that are _freely available_ and that can be further investigated and compared by the scientific community. In other words, this paper does not consider technologies only employed in industry and/or whose source code is non-accessible. This paper formalizes a selected use case in the considered reasoners and compares the implementations, also in terms of simulations with respect to shared synthetic datasets. The comparison will highlight that lot of further research still needs to be done to integrate the benefits featured by the different reasoners into a single standardized first-order framework, suitable for LegalTech applications. All source codes are freely available at https://github.com/liviorobaldo/compliancecheckers, together with instructions to locally reproduce the simulations. (shrink)

Wilber's most timely, accessible, and practical work to date. Here is a concise, comprehensive overview of Wilber's revolutionary thought and its application in today's world. Wilber has long been hailed as one of the most important thinkers of our time, but--until now--his work has seemed inaccessible to the general reader who lacks a background in consciousness studies or evolutionary theory. Integral Vision will allow a general audience to fully understand what all the excitement has been about. In clear, non-technical language, (...) Wilber presents complex, cutting-edge theories and models that integrate the realms of body, mind, soul, and spirit. He then demonstrates how these theories and models can be applied to real world problems. Finally, Wilber discusses daily practices that readers take up in order to apply this integrative vision to their own, everyday lives. Wilber begins by presenting a leading model of human evolution, a model called "spiral dynamics." He then goes on to summarize his ground-breaking "all-level, all-quadrant" model for integrating the seemingly contradictory realms of science and religion--the "all-level, all-quadrant" model has already been adopted by leading thinkers in a variety of fields. In a chapter entitle "The Real World," Wilber shows how these rather abstract theories and models are being applied to real-world issues such as politics, medicine, business, education, and the environment. Wilber goes on to present a collection of maps of the Kosmos. These are broader models that can integrate the various worldviews that have been developed around the world throughout the ages. The final chapter of the book, "One Taste," proposes that readers take up an "integral transformative practice" such as meditation to help them to apply and develop this integral vision in their personal, everyday lives. (shrink)

Part I -- Scientific Composition and the New Mechanism. - 1. Laura Franklin-Hall: New Mechanistic Explanation and the Need for Explanatory Constraints. - 2. Kenneth Aizawa: Compositional Explanation: Dimensioned Realization, New Mechanism, and Ground. - 3. Jens Harbecke: Is Mechanistic Constitution a Version of Material Constitution?. - 4. Derk Pereboom: Anti-Reductionism, Anti-Rationalism, and the Material Constitution of the Mental. Part II -- Grounding, Science, and Verticality in Nature. - 5. Jonathan Schaffer: Ground Rules: Lessons from Wilson. - 6. Jessica Wilson: (...) The Unity and Priority Arguments for Grounding. - 7. Carl Gillett: The Metaphysics of Nature, Science, and the Rules of Engagement. - 8. Andrew Melnyk: Grounding and the Formulation of Physicalism. - 9. Alyssa Ney: Grounding in the Philosophy of Mind: A Defense. (shrink)

Ever since the publication of his first book, The Spectrum of Consciousness, written when he was twenty-three, Ken Wilber has been identified as the most comprehensive philosophical thinker of our times. This introductory sampler, designed to acquaint newcomers with his work, contains brief passages from his most popular books, ranging over a variety of topics, including levels of consciousness, mystical experience, meditation practice, death, the perennial philosophy, and Wilber's integral approach to reality, integrating matter, body, mind, soul, and spirit. Here (...) is Wilber's writing at its most reader-friendly, discussing essential ideas of the world's great psychological, philosophical, and spiritual traditions in language that is lucid, engaging, and inspirational. (shrink)

It is widely held that Bayesian decision theory is the final word on how a rational person should make decisions. However, Leonard Savage--the inventor of Bayesian decision theory--argued that it would be ridiculous to use his theory outside the kind of small world in which it is always possible to "look before you leap." If taken seriously, this view makes Bayesian decision theory inappropriate for the large worlds of scientific discovery and macroeconomic enterprise. When is it correct to use Bayesian (...) decision theory--and when does it need to be modified? Using a minimum of mathematics, Rational Decisions clearly explains the foundations of Bayesian decision theory and shows why Savage restricted the theory's application to small worlds. The book is a wide-ranging exploration of standard theories of choice and belief under risk and uncertainty. Ken Binmore discusses the various philosophical attitudes related to the nature of probability and offers resolutions to paradoxes believed to hinder further progress. In arguing that the Bayesian approach to knowledge is inadequate in a large world, Binmore proposes an extension to Bayesian decision theory--allowing the idea of a mixed strategy in game theory to be expanded to a larger set of what Binmore refers to as "muddled" strategies. Written by one of the world's leading game theorists, Rational Decisions is the touchstone for anyone needing a concise, accessible, and expert view on Bayesian decision making. (shrink)

The Spectrum of Consciousness (1977)--one of the founding texts of transpersonal psychology--introduces the full-spectrum model, showing how the psychological systems of the West can be integrated with the contemplative traditions of the East. No Boundary: Eastern and Western Approaches to Personal Growth (1979) is a simple yet comprehensive guide to psychologies and therapies available from both Western and Eastern sources. Several important early articles: "The Psychologia Perennis," "Are the Chakras Real?" and "Where It Was, I Shall Become.".

Natural Justice is a bold attempt to lay the foundations for a genuine science of morals using the theory of games. Since human morality is no less a product of evolution than any other human characteristic, the book takes the view that we need to explore its origins in the food-sharing social contracts of our prehuman ancestors. It is argued that the deep structure of our current fairness norms continues to reflect the logic of these primeval social contracts, but the (...) particular fairness norm a society operates is largely a product of cultural evolution. In pursuing this point, the book proposes a naturalistic reinterpretation of John Rawls' original position that reconciles his egalitarian theory of justice with John Harsanyi's utilitarian theory by identifying the environment appropriate to each. (shrink)

Binmore argues that game theory provides a systematic tool for investigating ethical matters.

It is widely held that Bayesian decision theory is the final word on how a rational person should make decisions. However, Leonard Savage--the inventor of Bayesian decision theory--argued that it would be ridiculous to use his theory outside the kind of small world in which it is always possible to "look before you leap." If taken seriously, this view makes Bayesian decision theory inappropriate for the large worlds of scientific discovery and macroeconomic enterprise. When is it correct to use Bayesian (...) decision theory--and when does it need to be modified? Using a minimum of mathematics, Rational Decisions clearly explains the foundations of Bayesian decision theory and shows why Savage restricted the theory's application to small worlds. The book is a wide-ranging exploration of standard theories of choice and belief under risk and uncertainty. Ken Binmore discusses the various philosophical attitudes related to the nature of probability and offers resolutions to paradoxes believed to hinder further progress. In arguing that the Bayesian approach to knowledge is inadequate in a large world, Binmore proposes an extension to Bayesian decision theory--allowing the idea of a mixed strategy in game theory to be expanded to a larger set of what Binmore refers to as "muddled" strategies. Written by one of the world's leading game theorists, Rational Decisions is the touchstone for anyone needing a concise, accessible, and expert view on Bayesian decision making. (shrink)

Wilber's groundbreaking synthesis of religion, philosophy, physics, and psychology started a revolution in transpersonal psychology.

The principal aim of this volume is to elucidate what freedom, sovereignty, and autonomy mean for Nietzsche and what philosophical resources he gives us to re ...

Do conventions need to be common knowledge in order to work? David Lewis builds this requirement into his definition of a convention. This paper explores the extent to which his approach finds support in the game theory literature. The knowledge formalism developed by Robert Aumann and others militates against Lewis’s approach, because it shows that it is almost impossible for something to become common knowledge in a large society. On the other hand, Ariel Rubinstein’s Email Game suggests that coordinated action (...) is no less hard for rational players without a common knowledge requirement. But an unnecessary simplifying assumption in the Email Game turns out to be doing all the work, and the current paper concludes that common knowledge is better excluded from a definition of the conventions that we use to regulate our daily lives. (shrink)

Game theory has proved a useful tool in the study of simple economic models. However, numerous foundational issues remain unresolved. The situation is particularly confusing in respect of the non-cooperative analysis of games with some dynamic structure in which the choice of one move or another during the play of the game may convey valuable information to the other players. Without pausing for breath, it is easy to name at least 10 rival equilibrium notions for which a serious case can (...) be made that here is the “right” solution concept for such games. (shrink)

Sometimes neuroscientists discover distinct realizations for a single psychological property. In considering such cases, some philosophers have maintained that scientists will abandon the single multiply realized psychological property in favor of one or more uniquely realized psychological properties. In this paper, we build on the Dimensioned theory of realization and a companion theory of multiple realization to argue that this is not the case. Whether scientists postulate unique realizations or multiple realizations is not determined by the neuroscience alone, but by (...) the psychological theory under examination. Thus, one might say that, in the splitting or non-splitting of properties, psychology enjoys a kind of autonomy from neuroscience. (shrink)

Drawing on social exchange theory, we argue that family-supportive supervisor behavior (FSSB) inhibits employees’ unethical pro-family behavior (UPFB) via the mediation of felt obligation. We further propose that employees’ positive reciprocity beliefs strengthen the hypothesized relationships. Using a sample consisting of 345 full-time employees from an Internet service company located in China, we found that felt obligation partially mediated the negative relationship between FSSB and UPFB and that the FSSB-felt obligation relationship and the mediation relationship were stronger for employees with (...) higher positive reciprocity beliefs. Theoretical and practical implications, limitations, and future directions are discussed. (shrink)

Many have argued that human enhancement, in particular bioenhancement via genetic engineering, brain-interventions or preimplantation embryo selection, is problematic even if it can be safely implemented. Various arguments have been put forward focusing on issues such as the undermining of autonomy, uneven distribution and unfairness, and the alteration of one’s identity, amongst others. Nevertheless, few, if any, of these thinkers oppose vaccines. -/- In what follows, I argue for the permissibility of a limited set of cognitive enhancements – in particular, (...) the enhancement of evaluative judgment and self-control – by analogy with the permissibility of vaccines. As a result, it follows that if one accepts the permissibility of vaccines one will also, other things being equal, be committed to the permissibility of these enhancements. I then consider and respond to a number of possible objections in order to defend and clarify my position. (shrink)

Ken Binmore's previous game theory textbook, Fun and Games, carved out a significant niche in the advanced undergraduate market; it was intellectually serious and more up-to-date than its competitors, but also accessibly written. Its central thesis was that game theory allows us to understand many kinds of interactions between people, a point that Binmore amply demonstrated through a rich range of examples and applications. This replacement for the now out-of-date 1991 textbook retains the entertaining examples, but changes the organization to (...) match how game theory courses are actually taught, making Playing for Real a more versatile text that almost all possible course designs will find easier to use, with less jumping about than before. In addition, the problem sections, already used as a reference by many teachers, have become even more clever and varied, without becoming too technical. Playing for Real will sell into advanced undergraduate courses in game theory, primarily those in economics, but also courses in the social sciences, and serve as a reference for economists. (shrink)

An increasing amount of data is now available from public and private sources. Furthermore, the types, formats, and number of sources of data are also increasing. Techniques for extracting, storing, processing, and analyzing such data have been developed in the last few years for managing this bewildering variety based on a structure called a knowledge graph. Industry has devoted a great deal of effort to the development of knowledge graphs, and knowledge graphs are now critical to the functions of intelligent (...) virtual assistants such as Siri, Alexa, and Google Assistant. The goal of the Ontology Summit 2020 was to understand not only what knowledge graphs are but also where they originated, why they are so popular, the current issues, and their future prospects. The summit sessions examined many examples of knowledge graphs and surveyed the relevant standards that exist and are in development for knowledge graphs. The purpose of this Communiqué is to summarize our understanding from the Summit in order to foster research and development of knowledge graphs. (shrink)

Humans have long been fascinated by the idea of visiting the past and of seeing what the future will bring. Time travel has been one of the most popular themes of science fiction. Most people have seen the TV series ‘Dr Who’ or ‘Quantum Leap’ or ‘Star Trek’. You’ve probably seen one of the ‘Back to the Future’ or ‘Terminator’ movies, or ‘Twelve Monkeys’. Time travel narratives provide fascinating plots, which exercise our imaginations in ever so many ways. But is (...) the idea of travelling forward and backward in time pure fantasy—or can it be done? To be sure, not all time travel scenarios are coherent. But we hope to persuade you that the most common objections to the very idea of time travel have no real force. (shrink)

Molinism promises the strongest account of God's providence consistent with our freedom. But is it a coherent view, and does it provide a satisfying account of divine providence? The essays in this volume examine the status, defensibility, and application of this recently revived doctrine, and anticipate the future direction of the debate.

Some behavioral economists argue that the honoring of social norms can be adequately modeled as the optimization of social utility functions in which the welfare of others appears as an explicit argument. This paper suggests that the large experimental claims made for social utility functions are premature at best, and that social norms are better studied as equilibrium selection devices that evolved for use in games that are seldom studied in economics laboratories.

I argue that the three strongest arguments against metaphysical libertarianism—the randomness objection, the constitutive luck objection, and the physicalist objection—are actually unsuccessful and therefore that metaphysical libertarianism is more plausible than the common philosophical wisdom allows. My more positive thesis, what I will refer to as “Agent Exceptionalism,” is that, when making decisions and performing actions, human beings can indeed satisfy the four conditions of metaphysical libertarianism: the control condition, the rationality condition, the ultimacy condition, and the physicalism condition.