Abstract In this article we define a logical system called Hybrid Partial Type Theory ( $\mathcal {HPTT}$ ). The system is obtained by combining William Farmer’s partial type theory with a strong form of hybrid logic. William Farmer’s system is a version of Church’s theory of types which allows terms to be non-denoting; hybrid logic is a version of modal logic in which it is possible to name worlds and evaluate expressions with respect to particular worlds. We motivate this combination of ideas in the introduction, and devote the rest of the article to defining, axiomatising, and proving a completeness result for $\mathcal {HPTT}$ .

Abstract We present an axiom system for what we call Prior’s Ideal Language and prove its completeness and pure completeness with respect to general models. With this is done, we explain, with examples, why this system provides a useful setting for exploring Arthur Prior’s work.

In this paper we present the results of a manual classification of all ethical consideration sections for ACL 2021.We also compare how many papers had an ethics consideration section per track and per world region in ACL 2021.We classified papers according to the ethical issues covered (research benefits, potential harms, and vulnerable groups affected) and whether the paper was marked as requiring ethics review by at least one reviewer.Moreover, we discuss recurring obstacles we have observed (highlighting some interesting texts we found along the way) and conclude with three suggestions.We think that this paper may be useful for anyone who needs to write -or review -an ethics section and would like to get an overview of what others have done.

Collaborative grounding is a fundamental aspect of human-human dialog which allows people to negotiate meaning.In this paper we argue that it is missing from current deep learning approaches to dialog and interactive systems.Our central point is that making mistakes and being able to recover from them collaboratively is a key ingredient in grounding meaning.We illustrate the pitfalls of being unable to ground collaboratively, discuss what can be learned from the language acquisition and dialog systems literature, and reflect on how to move forward.

In order to interpret the communicative intents of an utterance, it needs to be grounded in something that is outside of language; that is, grounded in world modalities.In this paper we argue that dialogue clarification mechanisms make explicit the process of interpreting the communicative intents of the speaker's utterances by grounding them in the various modalities in which the dialogue is situated.This paper frames dialogue clarification mechanisms as an understudied research problem and a key missing piece in the giant jigsaw puzzle of natural language understanding.We discuss both the theoretical background and practical challenges posed by this problem, and propose a recipe for obtaining grounding annotations.We conclude by highlighting ethical issues that need to be addressed in future work.

Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labelling approach lies at the heart of the best known hybrid resolution, natural deduction and tableau systems. But there is another approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in natural deduction and sequent calculus in the 1990s. The purpose of this article is to introduce a Seligman-style tableau system, to prove its completeness, and to show how it can be made to terminate. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just statements prefixed by @-operators. They do so by introducing machinery for switching to other proof contexts. We capture this idea in the setting of tableaus by introducing a rule called GoTo, which allows us to ‘jump to a named world’ on a tableau branch. We first develop a Seligman-style tableau system for basic hybrid logic and prove its completeness. We then prove termination of a restricted version of the system without resorting to loop checking, and show that the restrictions do not effect completeness. Both completeness and termination results are proved by explicit translations that transform tableaus in a standard labelled system into Seligman-style tableaus and vice-versa.

This article extends and improves work on tableau-based decision methods for hybrid logic by Bolander and Braüner. Their paper gives tableau-based decision procedures for basic hybrid logic (with unary modalities) and the basic logic extended with the global modality. All their proof procedures make use of loop-checks to ensure termination. Here we take a closer look at termination for hybrid tableaus. We cover both types of system used in hybrid logic: prefixed tableaus and internalized tableaus. We first treat prefixed tableaus. We prove a termination result for the basic language (with n-ary operators) that does not involve loop-checks. We then successively add the global modality and n-ary inverse modalities, show why various different types of loop-check are required in these cases, and then re-prove termination. Following this we consider internalized tableaus. At first sight, such systems seem to be more complex. However, we define a internalized system which terminates without loop-checks. It is simpler than previously known internalized systems (all of which require loop-checks to terminate) and simpler than our prefix systems (no non-local side conditions on rules are required).

Abstract Craig's interpolation lemma (if φ → ψ is valid, then φ → θ and θ → ψ are valid, for θ a formula constructed using only primitive symbols which occur both in φ and ψ) fails for many propositional and first order modal logics. The interpolation property is often regarded as a sign of well-matched syntax and semantics. Hybrid logicians claim that modal logic is missing important syntactic machinery, namely tools for referring to worlds, and that adding such machinery solves many technical problems. The paper presents strong evidence for this claim by defining interpolation algorithms for both propositional and first order hybrid logic. These algorithms produce interpolants for the hybrid logic of every elementary class of frames satisfying the property that a frame is in the class if and only if all its point-generated subframes are in the class. In addition, on the class of all frames, the basic algorithm is conservative: on purely modal input it computes interpolants in which the hybrid syntactic machinery does not occur.

We introduce hybrid Ockhamist temporal logic, which combines the mechanisms of hybrid logic with Ockhamist semantics by employing nominals, satisfaction operators, binders, and quantifiers over branches. We provide a complete (with respect to bundled trees semantics) axiomatic system for the basic hybrid Ockhamist temporal logic (HOT) and for some of its extensions including the full hybrid Ockhamist temporal logic. The fill system is expressively equivalent to the first-order logic over trees extended with branch quantifiers which was proved decidable previously.

Abstract Hybrid languages are expansions of propositional modal languages which can refer to (or even quantify over) worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work (for example [BS98, BT98a, BT99]) has focussed on a more constrained system called H(↓, @). We show in detail that (↓, @) is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations (via a restricted notion of Ehrenfeucht-Fraïssé game, and an enriched notion of bisimulation) and a syntactic characterization (in terms of bounded formulas). The key result to emerge is that (↓, @) corresponds to the fragment of first-order logic which is invariant for generated submodels. We then show that (↓, @) enjoys (strong) interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for the sublanguage (@). Finally, we provide complexity results for (@) and other fragments and variants, and sharpen known undecidability results for (↓, @).

1 ILLC, University of Amsterdam, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands. E-mail: [email protected] 2 INRIA, Lorraine, 615, rue du Jardin Botanique, 54602 Villers lès Nancy Cedex, France. E-mail: [email protected]

This paper shows how to internalize the Kripke satisfaction definition using the basic hybrid language, and explores the proof theoretic consequences of doing so. The basic hybrid language enables the transfer of classic Gabbay-style labelled deduction methods from the metalanguage to the object language, and the logical handling of labelling discipline. This internalized approach to labelled deduction links neatly with the Gabbay-style rules now widely used in modal Hilbert-systems, enables completeness results for a wide range of first-order definable frame classes to be obtained automatically, and extends to many richer languages. The paper discusses related work by Jerry Seligman and Miroslava Tzakova and concludes with some reflections on the status of labelling in modal logic.