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)

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 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)

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)

日本、中国、韓国はそれぞれの伝統に依拠しつつ西洋哲学を受容することで近代哲学を形成してきた。哲学や思想における特徴や制限は、他の思想を鏡として、そこに映し出すことで明らかになる。なぜ違いが生まれたのか 。互いの違いをどう克服するのか。西田幾多郎、吉田松陰、九鬼周造、西周、和辻哲郎、土田杏村、大西克礼、戸坂潤...。受容から対話へと続く道から、いま、東アジアにおける哲学的創造の新たな意義と可能性が拓か れる。.

Safeguarding GenAI models against threats and aligning them with security requirements is imperative yet challenging. This chapter provides an overview of the security landscape for generative models. It begins by elucidating common vulnerabilities and attack vectors, including adversarial attacks, model inversion, backdoors, data extraction, and algorithmic bias. The practical implications of these threats are discussed, spanning domains like finance, healthcare, and content creation. The narrative then shifts to exploring mitigation strategies and innovative security paradigms. Differential privacy, blockchain-based provenance, quantum-resistant algorithms, (...) and human-guided reinforcement learning are analyzed as potential techniques to harden generative models. Broader ethical concerns surrounding transparency, accountability, deepfakes, and model interpretability are also addressed. The chapter aims to establish a conceptual foundation encompassing both the technical and ethical dimensions of security for generative AI. It highlights open challenges and lays the groundwork for developing robust, trustworthy, and human-centric solutions. The multifaceted perspective spanning vulnerabilities, implications, and solutions is intended to further discourse on securing society’s growing reliance on generative models. Frontier model security is discussed using Anthropic proposed approach. (shrink)

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 ...

I argue that Descartes' Second Causal Proof of God in the Third Meditation evidences, and commits him to, the belief that time is "strongly discontinuous" -- that is, that there is actually a gap between each consecutive moment of time. Much of my article attempts to reconcile this interpretation, the "received view," with Descartes' statements about time, space, and matter in his other writings, including his correspondence with various philosophers.

" L'argent est l'envers de toutes les images que le cinéma montre et monte à l'endroit " écrit Gilles Deleuze dans le deuxième volet de Cinéma. Le capital est toujours derrière le cinéma. Le Capital hante Cinéma du début à la fin. C'est donc une lecture marxiste du diptyque composé de L'Image-mouvement et L'Image-temps que propose Jun Fujita dans Ciné-capital. Comment fonctionne le mode de production ciné-capitaliste? Comment celui-ci fait-il produire de la plus-value aux images? Pourquoi et comment s'approprie-t-il (...) le travail même du spectateur? En quel sens peut-on soutenir qu'Eisenstein et Hitchcock ont anticipé l'arrivée de la New Economy des années 1990 (dématérialisation du travail et financiarisation de l'économie)? Quand et comment les images s'insurgent-elles contre l'exploitation ciné-capitaliste? Comment se mettent-elles à valoir pour elles-mêmes? Pourquoi le cinéma politique, depuis Straub et Huillet, a-t-il cessé de privilégier le tournage au bord de la mer? Qu'est-ce qui permet à Deleuze d'affirmer qu'Ozu est un cinéaste de gauche? Telles sont quelques-unes des questions abordées dans Ciné-capital. (shrink)

A provocative examination of how the great religious traditions can remain relevant in modern times by incorporating scientific truths learned about human nature over the last century A single purpose lies at the heart of all the great religious traditions: awakening to the astonishing reality of the true nature of ourselves and the universe. At the same time, through centuries of cultural accretion and focus on myth and ritual as ends in themselves, this core insight has become obscured. Here, Ken (...) Wilber provides a path for re-envisioning a religion of the future that acknowledges the evolution of humanity in every realm while remaining faithful to that original spiritual vision. For the traditions to attract modern men and women, Wilber asserts, they must incorporate the extraordinary number of scientific truths learned about human nature in just the past hundred years—for example, about the mind and brain, emotions, and the growth of consciousness—that the ancients were simply unaware of and thus were unable to include in their meditative systems. Taking Buddhism as an example, Wilber demonstrates how his comprehensive Integral Approach—which is already being applied to several world religions by some of their adherents—can avert a “cultural disaster of unparalleled proportions”: the utter neglect of the glorious upper reaches of human potential by the materialistic postmodern worldview. Moreover, he shows how we can apply this approach to our own spiritual practice. This, his most sweeping work since Sex, Ecology, Spirituality, is a thrilling call for wholeness, inclusiveness, and unity in the religions of tomorrow. (shrink)

東洋の思想的な伝統を踏まえ、広い視野で哲学の新しい眺望を切り開いた『善の研究』。難解で知られるこの名著を丁寧に、深く掘り下げて読み解く西田哲学入門。 『善の研究』は西田の最初の著作ながら、晩年に至るまでの思索全体を貫く考え方が示されている主著。その魅力は、西洋の哲学と格闘しながら、その不十分性を乗り越えて物事の真相に迫ろうとする西田の思いがそのまま 表現されている点にある。仏教や儒教など、東洋の思想的な伝統をも踏まえた広い視野で哲学の世界に新しい眺望を切り開いた本書の面白さや意義を分かりやすく解説。西田の思考を丁寧に読み解き、西田が何を語ろうとし たのかを深く掘り下げて明らかにする、格好の西田哲学入門。.

Nietzsche never presented a worked-out normative ethical theory and appeared to regard any attempt to do so as woefully misguided. He poured scorn on the main contenders for such a theory in his day, and in ours – Kantian ethics and utilitarianism. Moreover, he repeatedly referred to himself as an 'immoralist' and gave one of his books the title Beyond Good and Evil, thus seeming only to confirm the impression that he was more interested in demolishing, and even abolishing morality (...) altogether than in making any constructive contribution to the subject. While the topic of morality appears as a central and almost obsessive interest in his works – especially in the sequence of books from Daybreak: Thoughts on the Prejudices of Morality (1881) to On the Genealogy of Morality (1887) – it generally does so as the target of relentless criticism. Many have concluded, not surprisingly, that Nietzsche, rather than being interested in replacing an existing conception of morality with a better one of his own, was in the business of advising us to abandon morality altogether – to live, in some sense, without morality. (shrink)

This important book features collected essays on the distinguished psychoanalyst Dr. Michael Eigen, who has emerged as an influential innovator within and beyond psychoanalysis. Drawing on the ideas of W. R. Bion, Winnicott, the Kabbalah, artists and scientists, Eigen's work is noted for its creativity which combines spirituality with psychoanalysis. The book begins with a series of articles on Eigen's perspective on time, before covering topics such as the evolution of the psyche, mystery and metaphor, and breakdown and recovery. These (...) papers feature a rich array of subjects and reflections, with many clinical examples and applications to domains beyond psychotherapy, including politics, societal contexts and creativity. Dr. Eigen is one of the most influential psychoanalysts of the current era and this collection of essays provides insightful discussion on his ideas. This celebration of Michael Eigen will fascinate any psychoanalyst interested in his work. (shrink)

「西欧」と「近代」を相対化し、今、エスニックの次元から『日本哲学』を創始すること=「われわれの問題に発して思索する」スタイルを提唱。.

膨大な資料をもとに魅力あふれる西田の素顔を描きだし、彼の言葉に豊かな広がりを与える決定的評伝。.

The concept of meaning, since Frege initiated the linguistic turn in 1884, has been the subject of numerous theories, hypotheses, methodologies and distinctions. One distinction of considerable strategic value relates to the location of meaning: some aspects of meaning can be found in language and are modelled with semantic values of various kinds; some aspects of meaning can be found in communicative processes and are modelled with pragmatic inferences of one sort or another. One hypothesis of great heuristic utility concerns (...) the relationship that is assumed between the semantic and the pragmatic. This collection of especially commissioned papers examines current thinking on the plausible nature of the semantic, the possible character of the pragmatic and the mechanics of their intersection. (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)

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)

I explicate the conditions required for criminal responsibility, provide an overview of criminal defenses, distinguish criminal responsibility from both tort liability and moral responsibility, and explicate the current state of the insanity defense.

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.

In this unique work, Ken Gale and Jonathan Wyatt bring together three areas of scholarship: collaborative writing as method of inquiry, the philosophical approaches of the French philosopher, Gilles Deleuze, and the performativity of both writing and the "self". The book is a reflexive exploration into the theory and practice of collaborative writing, with their between-the-twos sequences of exchanged writings using a variety of forms and genres at the book's heart. Their collaboration offers an experimental, transgressive and nomadic inquiry into (...) subjectivity. Based upon the authors' joint doctoral dissertation, the book draws for its theoretical base primarily from the work of Deleuze, from both his philosophical "figures" and the insights that he offers into his collaborations with others. It also tells a story, conveying a sense of a relationship developing over time. This book will interest both academics and postgraduate students in the field of qualitative inquiry, including those involved in narrative inquiry, cultural, communication and performance studies, and autoethnography. (shrink)