Visser's rules form a basis for the admissible rules of . Here we show that this result can be generalized to arbitrary intermediate logics: Visser's rules form a basis for the admissible rules of any intermediate logic for which they are admissible. This implies that if Visser's rules are derivable for then has no nonderivable admissible rules. We also provide a necessary and sufficient condition for the admissibility of Visser's rules. We apply these results to some specific intermediate logics and (...) obtain that Visser's rules form a basis for the admissible rules of, for example, De Morgan logic, and that Dummett's logic and the propositional Gödel logics do not have nonderivable admissible rules. (shrink)

We present a basis for the admissible rules of intuitionistic propositional logic. Thereby a conjecture by de Jongh and Visser is proved. We also present a proof system for the admissible rules, and give semantic criteria for admissibility.

This paper contains a detailed account of the notion of admissibility in the setting of consequence relations. It is proved that the two notions of admissibility used in the literature coincide, and it provides an extension to multi–conclusion consequence relations that is more general than the one usually encountered in the literature on admissibility. The notion of a rule scheme is introduced to capture rules with side conditions, and it is shown that what is generally understood under the extension of (...) a consequence relation by a rule can be extended naturally to rule schemes, and that such extensions capture the intuitive idea of extending a logic by a rule. (shrink)

Admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In this paper, a Gentzen-style framework is introduced for analytic proof systems that derive admissible rules of non-classical logics. While Gentzen systems for derivability treat sequents as basic objects, for admissibility, the basic objects are sequent rules. Proof systems are defined here for admissible rules of classes of modal logics, including K4, S4, and GL, and also Intuitionistic Logic IPC. With minor (...) restrictions, proof search in these systems terminates, giving decision procedures for admissibility in the logics. (shrink)

In this paper we study the admissible rules of intermediate logics. We establish some general results on extensions of models and sets of formulas. These general results are then employed to provide a basis for the admissible rules of the Gabbay–de Jongh logics and to show that these logics have finitary unification type.

We investigate the logical structure of intuitionistic Kripke-Platek set theory , and show that the first-order logic of is intuitionistic first-order logic IQC.

This paper contains a brief overview of the area of admissible rules with an emphasis on results about intermediate and modal propositional logics. No proofs are given but many references to the literature are provided.

In recent years, the logic of questions and dependencies has been investigated in the closely related frameworks of inquisitive logic and dependence logic. These investigations have assumed classical logic as the background logic of statements, and added formulas expressing questions and dependencies to this classical core. In this paper, we broaden the scope of these investigations by studying questions and dependency in the context of intuitionistic logic. We propose an intuitionistic team semantics, where teams are embedded within intuitionistic Kripke models. (...) The associated logic is a conservative extension of intuitionistic logic with questions and dependence formulas. We establish a number of results about this logic, including a normal form result, a completeness result, and translations to classical inquisitive logic and modal dependence logic. (shrink)

This paper contains a proof-theoretic account of unification in transitive reflexive modal logics, which means that the reasoning is syntactic and uses as little semantics as possible. New proofs of theorems on unification types are presented and these results are extended to negationless fragments. In particular, a syntactic proof of Ghilardi’s result that $\mathsf {S4}$ has finitary unification is provided. In this approach the relation between classical valuations, projective unifiers, and admissible rules is clarified.

In this paper, a proof-theoretic method to prove uniform Lyndon interpolation for non-normal modal logics is introduced and applied to show that the logics E\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {E}$$\end{document}, M\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {M}$$\end{document}, MC\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {MC}$$\end{document}, EN\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {EN}$$\end{document}, MN\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {MN}$$\end{document} have that (...) property. In particular, these logics have uniform interpolation. Although for some of them the latter is known, the fact that they have uniform Lyndon interpolation is new. Also, the proof-theoretic proofs of these facts are new, as well as the constructive way to explicitly compute the interpolants that they provide. It is also shown that the non-normal modal logics EC\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {EC}$$\end{document} and ECN\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ECN}$$\end{document} do not have Craig interpolation, and whence no uniform interpolation. (shrink)

We present a basis for the admissible rules of intuitionistic propositional logic. Thereby a conjecture by de Jongh and Visser is proved. We also present a proof system for the admissible rules, and give semantic criteria for admissibility.

In this paper we prove that three of the main propositional logics of dependence, none of which is structural, are structurally complete with respect to a class of substitutions under which the logics are closed. We obtain an analogous result with respect to stable substitutions, for the negative variants of some well-known intermediate logics, which are intermediate theories that are closely related to inquisitive logic.

In Iemhoff we gave a countable basis for the admissible rules of . Here, we show that there is no proper superintuitionistic logic with the disjunction property for which all rules in are admissible. This shows that, relative to the disjunction property, is maximal with respect to its set of admissible rules. This characterization of is optimal in the sense that no finite subset of suffices. In fact, it is shown that for any finite subset X of , for (...) one of the proper superintuitionistic logics Dn constructed by De Jongh and Gabbay ), all the rules in X are admissible. Moreover, the logic Dn in question is even characterized by X: it is the maximal superintuitionistic logic containing Dn with the disjunction property for which all rules in X are admissible. Finally, the characterization of is proved to be effective by showing that it is effectively reducible to an effective characterization of in terms of the Kleene slash by De Jongh. (shrink)

If the Visser rules are admissible for an intermediate logic, they form a basis for the admissible rules of the logic. How to characterize the admissible rules of intermediate logics for which not all of the Visser rules are admissible is not known. In this paper we give a brief overview of results on admissible rules in the context of intermediate logics. We apply these results to some well-known intermediate logics. We provide natural examples of logics for which the Visser (...) rule are derivable, admissible but nonderivable, or not admissible. (shrink)

A method is presented that connects the existence of uniform interpolants to the existence of certain sequent calculi. This method is applied to several modal logics and is shown to cover known results from the literature, such as the existence of uniform interpolants for the modal logic \. New is the result that \ has uniform interpolation. The results imply that for modal logics \ and \, which are known not to have uniform interpolation, certain sequent calculi cannot exist.

The language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.

In this paper we study the modal behavior of Σ-preservativity, an extension of provability which is equivalent to interpretability for classical superarithmetical theories. We explain the connection between the principles of this logic and some well-known properties of HA, like the disjunction property and its admissible rules. We show that the intuitionistic modal logic given by the preservativity principles of HA known so far, is complete with respect to a certain class of frames.

We introduce Gentzen calculi for intuitionistic logic extended with an existence predicate. Such a logic was first introduced by Dana Scott, who provided a proof system for it in Hilbert style. We prove that the Gentzen calculus has cut elimination in so far that all cuts can be restricted to very simple ones. Applications of this logic to Skolemization, truth value logics and linear frames are also discussed.

In this paper an alternative Skolemization method is introduced that, for a large class of formulas, is sound and complete with respect to intuitionistic logic. This class extends the class of formulas for which standard Skolemization is sound and complete and includes all formulas in which all strong quantifiers are existential. The method makes use of an existence predicate first introduced by Dana Scott.

We study the modal properties of intuitionistic modal logics that belong to the provability logic or the preservativity logic of Heyting Arithmetic. We describe the □-fragment of some preservativity logics and we present fixed point theorems for the logics iL and iPL, and show that they imply the Beth property. These results imply that the fixed point theorem and the Beth property hold for both the provability and preservativity logic of Heyting Arithmetic. We present a frame correspondence result for the (...) preservativity principle Wp that is related to an extension of Löb's principle. (shrink)

In this paper a method to construct Kripke models for subtheories of constructive set theory is introduced that uses constructions from classical model theory such as constructible sets and generic extensions. Under the main construction all axioms except the collection axioms can be shown to hold in the constructed Kripke model. It is shown that by carefully choosing the classical models various instances of the collection axioms, such as exponentiation, can be forced to hold as well. The paper does not (...) contain any deep results. It consists of first observations on the subject, and is meant to introduce some notions that could serve as a foundation for further research. (shrink)

In this paper a method for the replacement, in formulas, of strong quantifiers by functions is introduced that can be considered as an alternative to Skolemization in the setting of constructive theories. A constructive extension of intuitionistic predicate logic that captures the notions of preorder and existence is introduced and the method, orderization, is shown to be sound and complete with respect to this logic. This implies an analogue of Herbrand's theorem for intuitionistic logic. The orderization method is applied to (...) the constructive theories of equality and groups. (shrink)

In this paper we study the modal behavior of Σ‐preservativity, an extension of provability which is equivalent to interpretability for classical superarithmetical theories. We explain the connection between the principles of this logic and some well‐known properties of HA, like the disjunction property and its admissible rules. We show that the intuitionistic modal logic given by the preservativity principles of HA known so far, is complete with respect to a certain class of frames.

This paper is a sequel to the papers Baaz and Iemhoff [4] and [6] in which an alternative skolemization method called eskolemization was introduced that, when restricted to strong existential quantifiers, is sound and complete for constructive theories. In this paper we extend the method to universal quantifiers and show that for theories satisfying the witness property it is sound and complete for all formulas. We obtain a Herbrand theorem from this, and apply the method to the intuitionistic theory (...) of equality and the intuitionistic theory of monadic predicates. (shrink)

Axiom 1 of K is the same as Axiom 1 in L, thus we have nothing to prove. Axiom 2 of K is 2(φ → ψ) → (2φ → 2ψ). We give a derivation of this formula in L: (φ → ψ) ∧ φ → ψ 2((φ → ψ) ∧ φ) → 2ψ (the rule from L) 2(φ → ψ) ∧ 2φ → 2ψ (axiom 3 of L and propositional logic) 2(φ → ψ) → (2φ → 2ψ) (propositional logic) Remain (...) the rules of K. Modus ponens is a rule of both so there is nothing to prove. We show that L proves the Necessitation rule. That is, we have to show that if L φ, then L 2φ. The following derivation in L from assumption φ shows this: φ → φ (propositional logic) 2 → 2φ (the rule from L) 2φ (modus ponens using axiom 2 ) This completes the direction of the proof form left to right. (shrink)

This text contains some basic facts about modal logic. For motivation, intuition and examples the reader should consult one of the standard textbooks in the field.

This paper provides a method to obtain terminating analytic calculi for a large class of intuitionistic modal logics. For a given logic L with a cut-free calculus G that is an extension of G3ip the method produces a terminating analytic calculus that is an extension of G4ip and equivalent to G. G4ip was introduced by Roy Dyckhoff in 1992 as a terminating analogue of the calculus G3ip for intuitionistic propositional logic. Thus this paper can be viewed as an extension of (...) Dyckhoff’s work to intuitionistic modal logic. (shrink)

AI systems have often been found to contain gender biases. As a result of these gender biases, AI routinely fails to adequately recognize the needs, rights, and accomplishments of women. In this article, we use Axel Honneth’s theory of recognition to argue that AI’s gender biases are not only an ethical problem because they can lead to discrimination, but also because they resemble forms of misrecognition that can hurt women’s self-development and self-worth. Furthermore, we argue that Honneth’s theory of recognition (...) offers a fruitful framework for improving our understanding of the psychological and normative implications of gender bias in modern technologies. Moreover, our Honnethian analysis of gender bias in AI shows that the goal of responsible AI requires us to address these issues not only through technical interventions, but also through a change in how we grant and deny recognition to each other. (shrink)

The introduction of contraceptive technologies hasresulted in the separation of sex and procreation. Theintroduction of new reproductive technologies (mainlyIVF and embryo transfer) has led not only to theseparation of procreation and sex, but also to there-definition of the terms mother and family.For the purpose of this essay, I will distinguishbetween:1. the genetic mother – the donor of the egg;2. the gestational mother – she who bears and gives birth to the baby;3. the social mother – the woman who raises the (...) child.This essay will deal only with the form of gestationalsurrogacy in which the genetic parents intend to bethe social parents, and the surrogate mother has nogenetic relationship to the child she bears anddelivers. I will raise questions regarding medicalethical aspects of surrogacy and the obligation(s) ofthe physician(s) to the parties involved. I will arguethat the gestational surrogate is a womb to rent,that there is great similarity between gestationalcommercial surrogacy and organ transplant marketing.Furthermore, despite claims to freedom of choice andfree marketing, I will claim that gestationalsurrogacy is a form of prostitution and slavery,exploitation of the poor and needy by those who arebetter off. The right to be a parent, although notconstitutional, is intuitive and deeply rooted.However, the issue remains whether this rightoverrules all other rights, and at what price to theparties involved. I will finally raise the followingprovocative question to society: In the interim periodbetween today''s limited technology and tomorrow''sextra-corporeal gestation technology (ectogenesis),should utilizing females in PVS (persistent vehetativestate) for gestational surrogacy be sociallyacceptable/permissible – provided they have leftpermission in writing? (shrink)

This article offers a structural analysis of Cicero's Orator, sections 140–8. Situating Cicero's defence of a form of educational activity in relation to his earlier denials that he is teaching anything, the article proposes an explanation for Cicero's apparent reversal of position rooted in status theory, the conceptual framework developed by Greek and Roman rhetorical theorists for schematizing the points at issue in a case and the corresponding lines of approach that a defender should take. Understanding the status-inspired organization of (...) Cicero's self-defence affords readers smoother passage through a text that is often difficult and obscure. Furthermore, this analysis shows how Cicero deploys rhetorical techniques in defence of his educational endeavours both to support his claim to continued relevance and to exemplify the versatility of the ideal orator whom he portrays in the Orator. (shrink)

Amsterdam University Press is a leading publisher of academic books, journals and textbooks in the Humanities and Social Sciences. Our aim is to make current research available to scholars, students, innovators, and the general public. AUP stands for scholarly excellence, global presence, and engagement with the international academic community.

The ethics of artificial intelligence is an upcoming field of research that deals with the ethical assessment of emerging AI applications and addresses the new kinds of moral questions that the advent of AI raises. The argument presented in this article is that, even though there exist different approaches and subfields within the ethics of AI, the field resembles a critical theory. Just like a critical theory, the ethics of AI aims to diagnose as well as change society and is (...) fundamentally concerned with human emancipation and empowerment. This is shown through a power analysis that defines the most commonly addressed ethical principles and topics within the field of AI ethics as either to do with relational power or with dispositional power. Moreover, it is concluded that recognizing AI ethics as a critical theory and borrowing insights from the tradition of critical theory can help the field forward. (shrink)

I graduated from law school in 1970 and I’ve been proud every day since of being a lawyer. My father was a lawyer, as are our two sons, and I’ve always seen lawyers as democracy’s warriors: the people who protect rights and by protecting rights protect justice. You law students are the future democracy warriors—actually, the future of democracy full stop—so this lecture is dedicated to you and to the hope that you will make justice your transcendent preoccupation, no matter (...) what you decide to do with your law degree. You are, after all, in law school where you have a window on what the law says—guided by your professors—and a window on what the law looks like outside the walls of your classrooms—guided by watching the news. (shrink)

Este trabalho analisa a repercussão social do cartaz do “Salão do Livro da Região Sul e Sudeste do Pará”, evento da Feira Pan-Amazônica do Livro de 2018, para compreender como o processo de resposta social (BRAGA, 2006) impôs uma mudança institucional por parte da Secretaria de Cultura do Estado. O país homenageado foi a Colômbia e a peça de divulgação destacava uma mulher negra carregando livros na cabeça, representação das palenqueras. O fato gerou repercussão nas redes sociais e na mídia (...) local e nacional. Os protestos voltaram-se contra a reiteração de uma imagem que inferioriza as mulheres negras, reproduzindo colonialidades de gênero, poder e saber. O corpuscompõe-se de postagens no Facebooke de matérias jornalísticas veiculadas em abril de 2018. Duas técnicas metodológicas foram usadas: a netnografia (RECUERO, 2012; KOZINETS, 2014) e a aplicação de um questionário online, por meio do Facebook e Whatsapp. (shrink)