Hybrid languages are expansions of propositional modal languages which can refer to worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work has focussed on a more constrained system called $\mathscr{H}$. We show in detail that $\mathscr{H}$ is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations and a syntactic characterization. The key result to emerge is that $\mathscr{H}$ corresponds to the fragment of first-order logic which is invariant for generated (...) submodels. We then show that $\mathscr{H}$ enjoys interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for the sublanguage $\mathscr{H}$. Finally, we provide complexity results for $\mathscr{H}$ and other fragments and variants, and sharpen known undecidability results for $\mathscr{H}$. (shrink)

We show that basic hybridization makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$@_i$\end{document} in propositional and first-order hybrid logic. This means: interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$@_i\alpha _a$\end{document}, where \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} (...) \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\alpha _a$\end{document} is an expression of any type \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$a$\end{document}, as an expression of type \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$a$\end{document} that rigidly returns the value that \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\alpha_a$\end{document} receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic. (shrink)

Quantified hybrid logic is quantified modal logic extended with apparatus for naming states and asserting that a formula is true at a named state. While interpolation and Beth's definability theorem fail in a number of well-known quantified modal logics , their counterparts in quantified hybrid logic have these properties. These are special cases of the main result of the paper: the quantified hybrid logic of any class of frames definable in the bounded fragment of first-order logic has the interpolation property, (...) irrespective of whether varying, constant, expanding, or contracting domains are assumed. (shrink)

We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret $@_i$ in propositional and first-order hybrid logic. This means: interpret $@_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of type $a$ that (...) rigidly returns the value that $\alpha_a$ receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual inhybrid logic) we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic. (shrink)

We investigate dynamic operations acting over a knowing how logic. Our approach makes use of a recently introduced semantics for the knowing how operator, based on an indistinguishability relation between plans. This semantics is arguably closer to the standard presentation of knowing that modalities in classic epistemic logic. Here, we discuss how the semantics enables us to define dynamic modalities representing different ways in which an agent can learn how to achieve a goal. In this regard, we study two types (...) of updates: ontic updates (for which we provide axiomatizations over a particular class of models), and epistemic updates (for which we investigate some semantic properties). (shrink)

We investigate the expressive power of memory logics. These are modal logics extended with the possibility to store (or remove) the current node of evaluation in (or from) a memory, and to perform membership tests on the current memory. From this perspective, the hybrid logic (↓), for example, can be thought of as a particular case of a memory logic where the memory is an indexed list of elements of the domain.

Este artigo canta uma canção — uma canção criada ao unir o trabalho de quatro grandes nomes na história da lógica: Hans Reichenbach, Arthur Prior, Richard Montague, e Leon Henkin. Embora a obra dos primeiros três desses autores tenha sido previamente combinada, acrescentar as ideias de Leon Henkin é o acréscimo requerido para fazer com que essa combinação funcione no nível lógico. Mas o presente trabalho não se concentra nas tecnicalidades subjacentes (que podem ser encontradas em Areces, Blackburn, Huertas, (...) e Manzano [no prelo]), e sim nos instrumentos subjacentes e no modo como trabalham em conjunto. Esperamos que o leitor fique tentado a cantar junto. DOI:10.5007/1808-1711.2011v15n2p225. (shrink)

Even though residuation is at the core of Categorial Grammar (Lambek, 1958), it is not always immediate to realize how standard logical systems like Multi-modal Categorial Type Logics (MCTL) (Moortgat, 1997) actually embody this property. In this paper, we focus on the basic system NL (Lambek, 1961) and its extension with unary modalities NL() (Moortgat, 1996), and we spell things out by means of Display Calculi (DC) (Belnap, 1982; Goré, 1998). The use of structural operators in DC permits a sharp (...) distinction between the core properties we want to impose on the logical system and the way these properties are projected into the logical operators. We will show how we can obtain Lambek residuated triple \, / and of binary operators, and how the operators and introduced by Moortgat (1996) are indeed their unary counterpart.In the second part of the paper we turn to other important algebraic properties which are usually investigated in conjunction with residuation (Birkhoff, 1967): Galois and dual Galois connections. Again, DC let us readily define logical calculi capturing them. We also provide preliminary ideas on how to use these new operators when modeling linguistic phenomena. (shrink)

In this article, we present a modal logic that extends the basic modal logic with two dynamic operators: copy ( ), which replicates the current model, labelling each copy with a different propositional symbol and respecting accessibility relations even between distinct copies; and remove ( ), which deletes paths in the model that satisfy certain intermediate conditions. We call the resulting logic. We study its computational complexity, and its relative expressivity with respect to (static) modal logics and, and the dynamic (...) epistemic Action Model Logic,. (shrink)

In this article, we present a modal logic that extends the basic modal logic ML with two dynamic operators: copy, which replicates the current model, labelling each copy with a different prop...

En este artículo se sintetiza una visión moderna de las lógicas modales y temporales. En vez de dar una motivación histórica, el paper presenta estas lógicas en relación con ciertos fragmentos de la lógica de primer orden que poseen propiedades interesantes. Esta visión de la lógica es seductora porque nos permite diseñar lenguajes a medida, es decir, optimizados para una tarea específica.

In this paper we develop the theoretical foundations to exploit symmetries in modal logics. We generalize the notion of symmetries of propositional formulas in conjunctive normal form to modal formulas using the framework provided by coinductive modal models introduced in [5]. Hence, the results apply to a wide class of modal logics including, for example, hybrid logics. We present two graph constructions that enable the reduction of symmetry detection in modal formulas to the graph automorphism detection problem, and we evaluate (...) the graph constructions on modal benchmarks. (shrink)

In this article, we formally define and investigate the computational complexity of the definability problem for open first-order formulas with equality. Given a logic $\boldsymbol{\mathcal{L}}$, the $\boldsymbol{\mathcal{L}}$-definability problem for finite structures takes as an input a finite structure $\boldsymbol{A}$ and a target relation $T$ over the domain of $\boldsymbol{A}$ and determines whether there is a formula of $\boldsymbol{\mathcal{L}}$ whose interpretation in $\boldsymbol{A}$ coincides with $T$. We show that the complexity of this problem for open first-order formulas is coNP-complete. We also (...) investigate the parametric complexity of the problem and prove that if the size and the arity of the target relation $T$ are taken as parameters, then open definability is $\textrm{coW}[1]$-complete for every vocabulary $\tau $ with at least one, at least binary, relation. (shrink)

This paper sings a song — a song created by bringing together the work of four great names in the history of logic: Hans Reichenbach, Arthur Prior, Richard Montague, and Leon Henkin. Although the work of the first three of these authors have previously been combined, adding the ideas of Leon Henkin is the addition required to make the combination work at the logical level. But the present paper does not focus on the underlying technicalities rather it focusses on the (...) underlying instruments, and the way they work together. We hope the reader will be tempted to sing a long. (shrink)

Luke Ong, Carlos Areces, Santiago Figueira and Ruy de Queiroz The Bulletin of Symbolic Logic, Volume 19, Issue 3, Page 425-426, September 2013.

We investigate transfer of interpolation in such combinations of modal logic which lead to interaction of the modalities. Combining logics by taking products often blocks transfer of interpolation. The same holds for combinations by taking unions, a generalization of Humberstone's inaccessibility logic. Viewing first-order logic as a product of modal logics, we derive a strong counterexample for failure of interpolation in the finite variable fragments of first-order logic. We provide a simple condition stated only in terms of frames and bisimulations (...) which implies failure of interpolation. Its use is exemplified in a wide range of cases. (shrink)

This book constitutes revised selected papers from the refereed proceedings of the 4th International Workshop on Dynamic Logic, DaLí 2022, held in Haifa, Israel, in July/August 2022. The 8 full papers presented in this volume were carefully reviewed and selected from 22 submissions. They deal with new trends and applications in the area of Dynamic Logic.

Effective vaccines for COVID‐19 are already available to humankind. In Peru, 86 million doses were administered to cover the demand for 33 million Peruvian people. Hence, vaccination has been prioritized in groups: health personnel, subjects with pre‐existing health conditions and those over 65 years of age. However, given the social problems and the public health situation in Peru, this work defends that the priority of vaccination should be focused on the population living in extreme poverty. The method used was an (...) ethical argumentation on the distribution of scarce antiSARS‐CoV2 vaccine in Peru. This argument is based on the analysis of the Peruvian population living in extreme poverty, which presents different layers of vulnerability, and that, in the face of an eventual SARS‐CoV2 infection, these would be exacerbated one after the other, through a cascade effect. This scenario would give rise to new vulnerabilities to those already existing, causing greater damage. Vaccination efforts on this key population would give them the opportunity to continue to find ways to bring food to their homes, significantly reducing the risk of contagion in their environment and mitigating the devastating effect of the local diseases to which they are already exposed. Four objections related to this argument are raised with their corresponding responses. Priority access to the vaccine would significantly reduce the humanitarian harm to people living in extreme poverty, prevailing the principles of justice and equity. (shrink)

La humanidad ya dispone de vacunas eficaces contra el COVID‐19. En Perú se administraron 86 millones de dosis para cubrir la demanda de 33 millones de peruanos. Para ello, se ha priorizado la vacunación en grupos clave: personal de salud, sujetos con condiciones de salud preexistentes y mayores de 65 años. Sin embargo, dada la problemática social y la situación de la salud pública en Perú, este trabajo defiende que la prioridad de la vacunación debe centrarse en la población que (...) vive en extrema pobreza. El método utilizado fue una argumentación ética sobre la distribución de la vacuna contra el COVID‐19 en Perú. Esta argumentación se basa en el análisis de la población peruana que vive en extrema pobreza, la cual presenta diferentes estratos de vulnerabilidad, y que, ante una eventual infección por SARS‐CoV‐2, se irían agravando uno tras otro, a través de un efecto en cascada. Este escenario daría lugar a nuevas vulnerabilidades de las ya existentes, causando mayores daños. Los esfuerzos de vacunación en esta población clave les brindaría oportunidad de seguir encontrando formas de llevar alimentos a sus hogares, reduciendo significativamente el riesgo de contagio en su entorno y mitigando el efecto devastador de las enfermedades locales a las que ya está expuesta. Se plantean cuatro objeciones relacionadas con este argumento, con sus correspondientes respuestas. El acceso prioritario a la vacuna reduciría significativamente el daño a las personas que viven en la extrema pobreza, haciendo prevalecer los principios de justicia y equidad. (shrink)

In their simplest form, hybrid languages are propositional modal languages which can refer to states. They were introduced by Arthur Prior, the inventor of tense logic, and played an important role in his work: because they make reference to specific times possible, they remove the most serious obstacle to developing modal approaches to temporal representation and reasoning. However very little is known about the computational complexity of hybrid temporal logics.In this paper we analyze the complexity of the satisfiability problem of (...) a number of hybrid temporal logics: the basic hybrid language over transitive trees; nominal Until logic; and referential interval logic. We discuss the effects of including nominals, the @ operator, the somewhere modality E, and the difference operator D. Adding nominals to tense logic leads for several frame-classes to an increase in complexity of the satisfiability problem from PSPACE to EXPTIME. On transitive trees, however, the satisfiability problem for this language can be decided in PSPACE. Along the way we make a detour through hybrid propositional dynamic logic: we establish upper bounds for a number of temporal logics by generalizing results due to Passy and Tinchev [29] and De Giacomo [16]. We conclude with some remarks on the relevance of our results to description logic, and draw attention to the utility of the spypoint technique for proving upper and lower bounds. (shrink)

Many of the computing systems programmed using Machine Learning are opaque: it is difficult to know why they do what they do or how they work. Explainable Artificial Intelligence aims to develop analytic techniques that render opaque computing systems transparent, but lacks a normative framework with which to evaluate these techniques’ explanatory successes. The aim of the present discussion is to develop such a framework, paying particular attention to different stakeholders’ distinct explanatory requirements. Building on an analysis of “opacity” from (...) philosophy of science, this framework is modeled after accounts of explanation in cognitive science. The framework distinguishes between the explanation-seeking questions that are likely to be asked by different stakeholders, and specifies the general ways in which these questions should be answered so as to allow these stakeholders to perform their roles in the Machine Learning ecosystem. By applying the normative framework to recently developed techniques such as input heatmapping, feature-detector visualization, and diagnostic classification, it is possible to determine whether and to what extent techniques from Explainable Artificial Intelligence can be used to render opaque computing systems transparent and, thus, whether they can be used to solve the Black Box Problem. (shrink)

The received view of dynamical explanation is that dynamical cognitive science seeks to provide covering law explanations of cognitive phenomena. By analyzing three prominent examples of dynamicist research, I show that the received view is misleading: some dynamical explanations are mechanistic explanations, and in this way resemble computational and connectionist explanations. Interestingly, these dynamical explanations invoke the mathematical framework of dynamical systems theory to describe mechanisms far more complex and distributed than the ones typically considered by philosophers. Therefore, contemporary dynamicist (...) research reveals the need for a more sophisticated account of mechanistic explanation. (shrink)

Models developed using machine learning are increasingly prevalent in scientific research. At the same time, these models are notoriously opaque. Explainable AI aims to mitigate the impact of opacity by rendering opaque models transparent. More than being just the solution to a problem, however, Explainable AI can also play an invaluable role in scientific exploration. This paper describes how post-hoc analytic techniques from Explainable AI can be used to refine target phenomena in medical science, to identify starting points for future (...) investigations of causal relationships, and to generate possible explanations of target phenomena in cognitive science. In this way, this paper describes how Explainable AI—over and above machine learning itself—contributes to the efficiency and scope of data-driven scientific research. (shrink)

In a context of pervasive digitalization of the social world, both before and during the COVID-19 pandemic, the field of education has undergone major changes with the development of digital practices and settings. However, the physical presence of the subjects and the body remain something primordial and irreplaceable in traditional educational processes. Thus, it is often assumed that virtuality is opposed to the corporeal reality of the subjects involved in teaching, learning and studying. In this paper we aim to critically (...) challenge this assumption by addressing the phenomenon of virtuality in a more original sense: as a fundamental dimension of corporeality itself. Drawing on Merleau-Ponty’s phenomenological insights, we argue that the experience of the virtual is inherently embodied and fully real. We understand corporeality and virtuality as entangled and multidimensional phenomena. At the same time, this leads us to rethink the digital as only one possible medium in which virtuality can appear as inherent to embodied experience. We develop our phenomenological approach in three instances. First, we question and bracket two common assumptions about corporeality. From our critical perspective, assumptions about a disembodied digitality and a devirtualized corporeality represent extremes within which educational discourses currently move. Second, we address the inherent virtuality of embodied experience. We outline the heuristic concept of the virtual body to describe corporeality and virtuality as entangled and multidimensional phenomena that encompass extension, intercorporeality and intermediality. Finally, we make some remarks on the relationships of corporeality and virtuality considering the challenges of digital education. (shrink)

Bayesian reverse-engineering is a research strategy for developing three-level explanations of behavior and cognition. Starting from a computational-level analysis of behavior and cognition as optimal probabilistic inference, Bayesian reverse-engineers apply numerous tweaks and heuristics to formulate testable hypotheses at the algorithmic and implementational levels. In so doing, they exploit recent technological advances in Bayesian artificial intelligence, machine learning, and statistics, but also consider established principles from cognitive psychology and neuroscience. Although these tweaks and heuristics are highly pragmatic in character and (...) are often deployed unsystematically, Bayesian reverse-engineering avoids several important worries that have been raised about the explanatory credentials of Bayesian cognitive science: the worry that the lower levels of analysis are being ignored altogether; the challenge that the mathematical models being developed are unfalsifiable; and the charge that the terms ‘optimal’ and ‘rational’ have lost their customary normative force. But while Bayesian reverse-engineering is therefore a viable and productive research strategy, it is also no fool-proof recipe for explanatory success. (shrink)

The philosophical conception of mechanistic explanation is grounded on a limited number of canonical examples. These examples provide an overly narrow view of contemporary scientific practice, because they do not reflect the extent to which the heuristic strategies and descriptive practices that contribute to mechanistic explanation have evolved beyond the well-known methods of decomposition, localization, and pictorial representation. Recent examples from evolutionary robotics and network approaches to biology and neuroscience demonstrate the increasingly important role played by computer simulations and mathematical (...) representations in the epistemic practices of mechanism discovery and mechanism description. These examples also indicate that the scope of mechanistic explanation must be re-examined: With new and increasingly powerful methods of discovery and description comes the possibility of describing mechanisms far more complex than traditionally assumed. (shrink)