I formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. The formalization precisely details the structure of this proof method.
This paper aims to tackle some of the basic (a-)symmetries of presupposition projection in a pragmatic, bivalent, and incrementally-oriented framework. The main data point that we are trying to capture is that projection from the first conjunct of a conjunction is asymmetric, while projection from the first disjunct of a disjunction can be symmetric. We argue that a solution where there are effectively two filtering mechanisms, one symmetric and one asymmetric, [11], is not tenable given recent experimental evidence, [4, 7]. Instead, we propose a bivalent system, where at each point during the incremental interpretation of a sentence S, the comprehender is trying to compute the sets of worlds in the context where the truth value of S has already been determined. This computation plays out differently in the case of conjunction vs the case of disjunction, and coupled with appropriate definitions of the incremental interpretation process and of what it means for a presupposition to project in the current system, it leads to asymmetric conjunction, but symmetric disjunction.
Declarative Distributed Systems (DDSs) are data-centric distributed systems grounded in logic programming. Enjoying a close correspondence between the distributed programs and their formal semantics, they configure as an interesting model for studying formal verification of distributed systems. Unfortunately, recent studies proved that the DDS model-checking problem is undecidable, unless boundedness conditions are imposed on the various DDS data-sources. Nevertheless, to check boundedness is, again, undecidable. Thus, we investigate whether it is possible to lift it in favor of syntactic, decidable conditions on the expressiveness of the data-sources. Considering the available decidability results, in this paper we study the impact of weak message expressiveness in place of channel-boundedness and obtain flexible decidability results on DDS verification. Those indicate that boundedness can sometimes be lifted in favor of decidable constraints, while retaining the decidability of the verification problem.
In this study, we provide a new empirical generalization of the meaning contribution of the Mandarin sentence-final particle de from an information maximizer perspective. Based on the cross-entropy model, we quantify the informativity associated with the prejacent that de attaches to. We further explore the plausibility of applying cross-entropy methods (as well as related Kullback-Leibler divergence-based methods) across languages, as a precise model of understanding the subtle pragmatic meanings of sentence-final particles in general.
In this paper, we report a qualitative and quantitative evaluation of a hand-crafted set of discourse features and their interaction with different text types. To be more specific, we compared two distinct text types—scientific abstracts and their accompanying full texts—in terms of linguistic properties, which include, among others, sentence length, coreference information, noun density, self-mentions, noun phrase count, and noun phrase complexity. Our findings suggest that abstracts and full texts differ in three mechanisms which are size and purpose bound. In abstracts, nouns tend to be more densely distributed, which indicates that there is a smaller distance between noun occurrences to be observed because of the compact size of abstracts. Furthermore, in abstracts we find a higher frequency of personal and possessive pronouns which authors use to make references to themselves. In contrast, in full texts we observe a higher frequency of noun phrases. These findings are our first attempt to identify text type motivated linguistic features that can help us draw clearer text type boundaries. These features could be used as parameters during the construction of systems for writing evaluation that could assist both tutors and students in text analysis, or as guides in linguistically-controllable neural text generation systems.
As the counterpart to kinds of entities or objects [5], event kinds are used to account for a variety of linguistic facts in the event domain. The modification of event kinds is usually considered to be restricted, and temporal modifiers are claimed to be hardly acceptable [18]. In this paper I focus on verbal gerunds in English, which have been analyzed as event kind descriptions [15], and demonstrate that they accept temporal modification but remain kind-referring. I extend the analysis of frequency adjectives [13] to interpret both temporal and frequency modifiers in verbal gerunds, showing that the modification of event kinds is less restricted than commonly assumed.
In this paper, we introduce an extension of the Lambek calculus by optional divisions ( L_opt ). Namely, the right optional division A ∠ B is defined as A ∧ (A/B) , and the left one is defined as A ∧ (B \ A) . A possible linguistic motivation to consider the new operations is describing verbs with optional arguments, e.g. reads in Tim reads the book. L_opt is a fragment of the multiplicative-additive Lambek calculus, so it would be interesting to compare the two calculi. The main part of the paper is devoted to the following grammar result: finite intersections of context-free languages can be generated by grammars over the calculus L_opt . The proof involves introducing a useful normal form for Lambek grammars, namely, the notion of an interpretable grammar.
Fox (2014) argues that cancelling the Maxim of Quantity can minimally dissociate between the pragmatic (primarily neo-Gricean) and grammatical approaches to scalar implicature. Under the pragmatic approach, scalar implicatures only arise as a result of adherence to the maxim of Quantity. The grammatical approach can predict that scalar implicatures remain available, in principle, when Quantity is not a conversational requirement as they arise from mechanisms independent of the maxim of Quantity. The present study operationalizes Fox’s game-show scenario into an experiment in which participants are tasked with determining which items are associated with money. The host, who is reticent about their knowledge, provides partial information (disjunctions and numerals) as hints to help the contestants. Experimental results demonstrated that participants can strengthen the meaning of disjunctions and numerals to help them make judgments about the relevant alternatives. The present work provides experimental evidence for the availability of scalar implicatures in a conversational context where the speaker does not obey the maxim of Quantity.
Certain propositional anaphora, like the Polarity Particles and Polar Additives discussed in this paper, are sensitive to the polarity of their antecedent clause. The paper establishes that discourse polarity—the polarity of the antecedent clause for the purposes of licensing subsequent anaphora—is influenced by complex factors, some of them syntactic, semantic, and pragmatic in nature. The hyperintensional dynamic framework presented here gives a formal foundation to a distinction of polarity for propositional discourse referents and captures some of the central generalizations. It uses discourse referents for hyperintensional propositions, providing a level of representation that connects information from the discourse context, the proposition’s semantic content, and the information about the polarity of the antecedent clause. Therefore, it constitutes a step towards an analysis capturing the heterogeneous factors influencing discourse polarity.
In this paper, we study a new epistemic modal operator, termed hope, which has been introduced recently in the context of a novel epistemic reasoning framework for distributed multi-agent systems with arbitrarily ("byzantine") faulty agents. It has been proved that both preconditions of actions used in agent protocols, as well as assertions about the epistemic states of agents obtained for analysis purposes, need to be restricted in a particular way for such systems. Hope has been proposed as the most promising candidate for analysis purposes, and defined in terms of the standard knowledge operator. To support the challenging next step of defining the semantics of common hope and eventual common hope, which are crucial for the analysis of fault-tolerant distributed agreement algorithms, we provide a suitable axiomatization of individual hope that avoids knowledge altogether, and prove its (strong) soundness and (strong) completeness.
Epistemic logic pays barely any attention to the notion of understanding, which stands in total contrast to the current situation in epistemology and in philosophy of science. This paper studies understanding why in an epistemic-logic-style. It is generally acknowledged that understanding why moves beyond knowing why. Inspired by philosophical ideas, we consider whereas knowing why requires knowing horizontal explanations, understanding why additionally requires vertical explanations. Based on justification logic and existing logical work for knowing why, we build up a framework by introducing vertical explanations, and show it could accommodate different philosophical viewpoints via adding conditions to the models. A sound and complete axiomatization for the most general case is given.
In a certain picture of cooperative conversation, ‘silence gives assent’. However, in adversarial contexts, structured by power dynamics, silence may be a powerful expression of dissent. To reconcile these opposite interpretations, I propose an analysis of silence as the expression of a default attitude. Given pragmatic cues, participants infer the cooperativeness of conversational settings. Depending on cooperativeness, they assign a default attitude (of assent, of suspension of judgment, of dissent) to other participants, that they take intentional silence to express. This analysis takes the main effect of speech acts to be proposals to update the conversational Common Ground, and highlights the necessity of assent in conversational updates.
Ciardelli et al. (2018b) adopt the framework of inquisitive semantics to provide a novel semantics for counterfactuals. They argue in favour of adopting inquisitive semantics based on experimental evidence that De Morgan’s law, which fails in inquisitive semantics, is invalid in counterfactual antecedents. We show that a unique feature of inquisitive semantics—the fact that its meanings are downward closed—leads to difficulties for Ciardelli et al.’s semantic account of their data. The scenarios we consider suggest either adopting a semantic framework other than inquisitive semantics, or developing a non-semantic explanation of the phenomena Ciardelli et al. (2018b) seek to explain.
The multimodal Lambek calculus is an extension of the Lambek calculus that includes several product operations (some of them being commutative or/and associative), unary modalities, and corresponding residual implications. In this work, we relate this calculus to the hypergraph Lambek calculus HL. The latter is a general pure logic of residuation defined in a sequent form; antecedents of its sequents are hypergraphs, and the rules of HL involve hypergraph transformation. Our main result is the embedding of the multimodal Lambek calculus (with at most one associative product) in HL. It justifies that HL is a very general Lambek-style logic and also provides a novel syntactic interface for the multimodal Lambek calculus: antecedents of sequents of the multimodal Lambek calculus are represented as tree-like hypergraphs in HL, and they are derived from each other by means of hyperedge replacement. The advantage of this embedding is that commutativity and associativity are incorporated in the sequent structure rather than added as separate rules. Besides, modalities of the multimodal Lambek calculus are represented in HL using the product and the division of HL, which explicitizes their residual nature.
In this paper, we consider the full Lambek calculus enriched with subexponential modalities in a distributive setting. We show that the distributive Lambek calculus with subexponentials is complete with respect to its Kripke frames via canonical extensions. In this approach, we consider subexponentials as S4-like modalities and each modality is interpreted with a reflexive and transitive relation similarly to usual Kripke semantics.
We demonstrate how to parse Geach's Donkey sentences in a compositional distributional model of meaning. We build on previous work on the DisCoCat (Distributional Compositional Categorical) framework, including extensions that model discourse, determiners, and relative pronouns. We present a type-logical syntax for parsing donkey sentences, for which we define both relational and vector space semantics.
We provide a generalisation of Kripke semantics for Petr Hajek's Basic Logic and prove soundness and completeness of the same with respect to our semantics. We find this semantics easily specialises to the linearly-ordered Kripke frames for Godel-Dummett logic, which BL properly contains. Our soundness, deduction theorem and completeness arguments further strengthen this analogy. This paper extends the insights of our previous paper, "A Kripke Semantics for Intuitionistic Lukasiewicz logic," to the case of Hajeks' BL.
Linear logical frameworks with subexponentials have been used for the specification of, among other systems, proof systems, concurrent programming languages and linear authorisation logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organised as sets and multisets of formulae not being possible to organise formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with the local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.
DisCoCirc is a newly proposed framework for representing the grammar and semantics of texts using compositional, generative circuits. While it constitutes a development of the Categorical Distributional Compositional (DisCoCat) framework, it exposes radically new features. In particular, [14] suggested that DisCoCirc goes some way toward eliminating grammatical differences between languages. In this paper we provide a sketch that this is indeed the case for restricted fragments of English and Urdu. We first develop DisCoCirc for a fragment of Urdu, as it was done for English in [14]. There is a simple translation from English grammar to Urdu grammar, and vice versa. We then show that differences in grammatical structure between English and Urdu - primarily relating to the ordering of words and phrases - vanish when passing to DisCoCirc circuits.
We show that both an LSTM and a unitary-evolution recurrent neural network (URN) can achieve encouraging accuracy on two types of syntactic patterns: context-free long distance agreement, and mildly context-sensitive cross serial dependencies.This work extends recent experiments on deeply nested context-free long distance dependencies, with similar results.URNs differ from LSTMs in that they avoid non-linear activation functions, and they apply matrix multiplication to word embeddings encoded as unitary matrices.This permits them to retain all information in the processing of an input string over arbitrary distances.It also causes them to satisfy strict compositionality.URNs constitute a significant advance in the search for explainable models in deep learning applied to NLP.
