We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible.

We study interpolation for elementary fragments of classical linear logic. Unlike in intuitionistic logic (see [Renardel de Lavalette, 1989]) there are fragments in linear logic for which interpolation does not hold. We prove interpolation for a lot of fragments and refute it for the multiplicative fragment (→, +), using proof nets and quantum graphs. We give a separate proof for the fragment with implication and product, but without the structural rule of permutation. This is nearly the Lambek (...) calculus. There is an appendix explaining what quantum graphs are and how they relate to proof nets. (shrink)

The semantic valuations of classical logic, strong Kleene logic, the logic of paradox and the logic of first-degree entailment, all respect the Dunn conditions: we call them Dunn logics. In this paper, we study the interpolation properties of the Dunn logics and extensions of these logics to more expressive languages. We do so by relying on the \ calculus, a signed tableau calculus whose rules mirror the Dunn conditions syntactically and which characterizes the Dunn logics in a uniform (...) way. In terms of the \ calculus, we first introduce two different interpolation methods, each of which uniformly shows that the Dunn logics have the interpolation property. One of the methods is closely related to Maehara’s method but the other method, which we call the pruned tableau method, is novel to this paper. We provide various reasons to prefer the pruned tableau method to the Maehara-style method. We then turn our attention to extensions of Dunn logics with so-called appropriate implication connectives. Although these logics have been considered at various places in the literature, a study of the interpolation properties of these logics is lacking. We use the pruned tableau method to uniformly show that these extended Dunn logics have the interpolation property and explain that the same result cannot be obtained via the Maehara-style method. Finally, we show how the pruned tableau method constructs interpolants for functionally complete extensions of the Dunn logics. (shrink)

This edited volume focuses on the work of Professor Larisa Maksimova, providing a comprehensive account of her outstanding contributions to different branches of non-classical logic. The book covers themes ranging from rigorous implication, relevance and algebraic logic, to interpolation, definability and recognizability in superintuitionistic and modal logics. It features both her scientific autobiography and original contributions from experts in the field of non-classical logics. Professor Larisa Maksimova's influential work involved combining methods of algebraic and relational semantics. Readers will be (...) able to trace both influences on her work, and the ways in which her work has influenced other logicians. In the historical part of this book, it is possible to trace important milestones in Maksimova’s career. Early on, she developed an algebraic semantics for relevance logics and relational semantics for the logic of entailment. Later, Maksimova discovered that among the continuum of superintuitionisitc logics there are exactly three pretabular logics. She went on to obtain results on the decidability of tabularity and local tabularity problems for superintuitionistic logics and for extensions of S4. Further investigations by Maksimova were aimed at the study of fundamental properties of logical systems in big classes of logics, and on decidability and recognizability of such properties. To this end she determined a powerful combination of algebraic and semantic methods, which essentially determine the modern state of investigations in the area, as can be seen in the later chapters of this book authored by leading experts in non-classical logics. These original contributions bring the reader up to date on the very latest work in this field. (shrink)

We give complete sequent-like tableau systems for the modal logics KB, KDB, K5, and KD5. Analytic cut rules are used to obtain the completeness. Our systems have the analytic superformula property and can thus give a decision procedure. Using the systems, we prove the Craig interpolation lemma for the mentioned logics.

We develop a Gentzen-style proof theory for super-Belnap logics, expanding on an approach initiated by Pynko. We show that just like substructural logics may be understood proof-theoretically as logics which relax the structural rules of classical logic but keep its logical rules as well as the rules of Identity and Cut, super-Belnap logics may be seen as logics which relax Identity and Cut but keep the logical rules as well as the structural rules of classical (...) logic. A generalization of the cut elimination theorem for classical propositional logic is then proved and used to establish interpolation for various super-Belnap logics. In particular, we obtain an alternative syntactic proof of a refinement of the Craig interpolation theorem for classical propositional logic discovered recently by Milne. (shrink)

This paper studies a combined system of intuitionistic and classical propositional logic from proof-theoretic viewpoints. Based on the semantic treatment of Humberstone (J Philos Log 8:171–196, 1979) and del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996), a sequent calculus $$\textsf{G}(\textbf{C}+\textbf{J})$$ is proposed. An approximate idea of obtaining $$\textsf{G}(\textbf{C}+\textbf{J})$$ is adding rules for classical implication on top of the intuitionistic multi-succedent sequent calculus by Maehara (Nagoya Math J 7:45–64, 1954). However, in the semantic treatment, some formulas do (...) not satisfy heredity, which leads to the necessity of a restriction on the right rule for intuitionistic implication to keep the soundness of the calculus. The calculus $$\textsf{G}(\textbf{C}+\textbf{J})$$ enjoys cut elimination and Craig interpolation, whose detailed proofs are described in this paper. Cut elimination enables us to show the decidability of this combination both directly and syntactically. This paper also employs a canonical model argument to establish the strong completeness of Hilbert system $$\mathbf {C+J}$$ proposed by del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996). (shrink)

We get cut-free sequent calculi for the interpolable propositional intermediate logics by translating suitable duplication-free tableau calculi developed within a semantical framework. From this point of view, the paper also provides semantical proofs of the admissibility of the cut-rule for appropriate cut-free sequent calculi.

We discuss the methods for providing sequent calculi for Suszko’s basic non-Fregean Logic with sentential identity SCI. After examination of possible strategies and already proposed systems we focus on the new calculus and its modification. It does not satisfy full cut elimination but a slightly generalised form of the subformula property holds for it. It is also standard in the sense of satisfying several conditions on rules formulated by Gentzen and his followers. We examine also the problem of providing (...) a constructive proof of the interpolation theorem in the setting of this sequent calculus. (shrink)

The information explosion and digital modes of learning often combine to inform the quest for the best ways of transforming information in digital form for pedagogical purposes. This quest has become more urgent and pervasive with the ‘turn’ to online learning in the context of COVID-19. This can result in linear, asynchronous, transmission-based modes of teaching and learning which commodify, package and deliver knowledge for individual ‘customers’. The primary concerns in such models are often technical and economic – technology as (...) a cost-effective ‘solution’ to educational challenges. In this paper I argue for the importance of dialogic learning space in teaching and learning by means of Information and Communication Technologies, whether in the form of fully online learning, blended learning or face-to-face encounters using ICT affordances. Although the 20th Century theorists Mikhail Bakhtin (1895–1975) and Hans-Georg Gadamer (1900–2002) produced their seminal works before the advent of ICTs, they were both concerned with the quality and authenticity of human engagement with texts and with other persons and contexts. Besides a shared interest in dialogue as an ontological feature of human life and being, they both used spatiotemporal concepts for understanding and interpreting texts. The article draws on Gadamer’s notions of dialogue and horizon, and Bakhtin’s notions of dialogue and chronotope, to conceptualize dialogic possibilities for online education. Its purpose is to provide a framework, grounded in Bakhtin’s and Gadamer’s ideas, for a dialogic approach to online teaching and learning in higher education. (shrink)

Jesus of Nazareth, like Socrates, left nothing behind written by himself. Yet, the records of his teaching indicate a rich interest in dialogic pedagogy, reflected in his use of the parable, primarily an oral genre, as a dialogic provocation. Working at the interface of pedagogy, theology and philosophy, this article explores the parable of the Good Samaritan from the perspective of dialogic pedagogy. It employs an analytical approach termed diacognition, developed from the notions of dialogue, position and cognition, to analyse (...) the moves within the parable and the teaching situation in which it is located. The article explores how Jesus engages the dialogue of and around the parable to position and reposition his interlocutor, provoking a re-cognition of what it means to love one’s neighbour. It concludes by reflecting on the implications of this analysis for the relation of meaning to knowing and doing. (shrink)

Dialogue is a seminal concept within the work of the Brazilian adult education theorist, Paulo Freire, and the Russian literary critic and philosopher, Mikhail Bakhtin. While there are commonalities in their understanding of dialogue, they differ in their treatment of dialectic. This paper addresses commonalities and dissonances within a Bakhtin-Freire dialogue on the notions of dialogue and dialectic. It then teases out some of the implications for education theory and practice in relation to two South African contexts of learning that (...) facilitate the access to education of disadvantaged groups, one in higher education and the other in early childhood education. (shrink)

This article examines the relationship between online dispute resolution (ODR) and trust. We discuss what trust is, why trust is important, and how trust develops. Our claim is that efforts to implement online dispute resolution on a site or service in a manner that promotes trust need to consider ODR as just one tool in a broader toolbox of trust-building tools and techniques. These techniques are amongst others marketing, education, trust seals, and transparency. By evaluating ODR in its proper context (...) as one component of a larger trust strategy, we can more accurately set expectations for its results and position our projects for success. (shrink)

The article presents proofs of the context freeness of a family of typelogical grammars, namely all grammars that are based on a uni- ormultimodal logic of pure residuation, possibly enriched with thestructural rules of Permutation and Expansion for binary modes.

As an introduction to our work, we emphasize the parallel interpretation of abstract tools and the concepts of undetermined and vague information. Imprecision, uncertainty and their relationships are inspected. Suitable interpretations of the fuzzy sets theory are applied to legal phenomena in an attempt to clearly circumscribe the possible applications of the theory. The fundamental notion of reference sets is examined in detail, hence highlighting their importance. A systematic and combinatorial classification of the relevant subsets of the legal field is (...) supplied for practical application. Although the use of the fuzzy sets theory is sometimes suggested as a palliative measure (no competition exists), it can also be complementary (serve as a building block to improve modelisation). An Appendix gives a brief recall of the key-concepts of the axiomatic theory of fuzziness and its developments: fuzzy sets, fuzzy logic, fuzzy control and theory of possibility. (shrink)

This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates the (...) semantics of the associated logic, and such systems typically violate the subformula property to a high degree. By contrast, nested sequent calculi employ a simpler syntax and adhere to a strict reading of the subformula property, making such systems useful in the design of automated reasoning algorithms. However, the downside of the nested sequent paradigm is that a general theory concerning the automated construction of such calculi (as in the labelled setting) is essentially absent, meaning that the construction of nested systems and the confirmation of their properties is usually done on a case-by-case basis. The refinement method connects both paradigms in a fruitful way, by transforming labelled systems into nested (or, refined labelled) systems with the properties of the former preserved throughout the transformation process. To demonstrate the method of refinement and some of its applications, we consider grammar logics, first-order intuitionistic logics, and deontic STIT logics. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics. Furthermore, we employ our refined labelled calculi for grammar logics to show that every logic in the class possesses the effective Lyndon interpolation property. (shrink)