In a manuscript which is being studied here for the first time, al-Samaw'al quotes a paragraph from al-Bīrūnī which shows that the latter knew not only of Brahmagupta's method of quadratic interpolation, but also of another Indian method. Al-Samaw'al examines these methods, as well as linear interpolation, compares them, and evaluates their respective results. He also tries to improve them. In this article the author shows that al-Bīrūnī had used four methods of interpolation, two of which were of Indian origin; (...) and that al-Samaw'al explicitly introduced a new way of evaluating these different methods. He also throws light on the active movement of research on numerical methods that constitutes the background to al-Bīrūmī's and al-Samaw'al's work, and uses modern means to evaluate the different methods and to justify the mathematicians' choices. The author has edited and translated al-Samaw'al's text in order to make it available to historians of Arabic and Indian mathematics. This allows them to follow the history and the mathematical arguments, and deepens our understanding of the importance to the development of mathematics of certain astronomical work. It also highlights the contribution of Indian mathematicians to the development of Arabic mathematics. Dans un texte manuscrit jamais examiné auparavant, al-Samaw'al cite un paragraphe d'un écrit d'al-Bīrīnī qui montre bien que ce dernier connaissait non seulement la méthode d'interpolation quadratique de Brahmagupta, mais également une autre methode indienne. Al-Samaw'al éetudie ces méthodes ainsi que l'interpolation linéaire, les compare les unes aux autres et par conséquent s'interroge sur leurs performances respectives afin d'opter pour la meilleure, et tente de les perfectionner. Dans cet article, l'auteur montre qu'al-Bīrūnī disposait de quatre méthodes d'interpolation, dont deux sont d'origine indienne, et qu'al-Samaw'al a introduit explicitement une nouvelle interrogation pour juger de la performance des différentes méthodes; il restitue les études d'al- Bī;rūnī et d'al-Samaw'al dans le mouvement actif de recherche sur les méthodes numériques, et reprend avec des moyens modernes la comparaison entre les diverses méthodes pour comprendre les choix des différents mathématiciens. L'auteur établit et traduit le texte d'al-Samaw'al afin de le rendre accessible aux historiens des mathématiques arabes et indiennes, et pour permettre aux lecteurs de suivre l'exposé' historique et mathématique qui vise, au-delà de ces résultats, à mieux connaître l'apport de certaines recherches en astronomie au développement des mathématiques, et d'autre part, la contribution des mathématiciens de l'Inde à l'histoire des mathématiques arabes. (shrink)

After spinal cord injury (SCI), motoneuron death occurs at and around the level of injury which induces changes in function and organization throughout the nervous system, including cortical changes. Muscle affected by SCI may consist of both innervated (accessible to voluntary drive) and denervated (inaccessible to voluntary drive) muscle fibers. Voluntary activation measured with transcranial magnetic stimulation (VATMS) can quantify voluntary cortical/subcortical drive to muscle but is limited by technical challenges including suboptimal stimulation of target muscle relative to its antagonist. (...) The motor evoked potential (MEP) in the biceps compared to the triceps (i.e., MEP ratio) may be a key parameter in the measurement of biceps VATMS after SCI. We used paired pulse TMS, which can inhibit or facilitate MEPs, to determine whether the MEP ratio affects VATMS in individuals with tetraplegia. Ten individuals with tetraplegia following cervical SCI and ten non-impaired individuals completed single pulse and paired pulse VATMS protocols. Paired pulse stimulation was delivered at 1.5, 10, and 30 ms inter-stimulus intervals (ISI). In both the SCI and non-impaired groups, the main effect of the stimulation pulse (paired pulse compared to single pulse) on VATMS was not significant in the linear mixed-effects models. In both groups for the stimulation parameters we tested, the MEP ratio was not modulated across all effort levels and did not affect VATMS. Linearity of the voluntary moment and superimposed twitch moment relation was lower in SCI participants compared to non-impaired. Poor linearity in the SCI group limits interpretation of VATMS. Future work is needed to address methodological issues that limit clinical application of VATMS. (shrink)

The subject of Time has a wide intellectual appeal across different dis ciplines. This has shown in the variety of reactions received from readers of the first edition of the present Book. Many have reacted to issues raised in its philosophical discussions, while some have even solved a number of the open technical questions raised in the logical elaboration of the latter. These results will be recorded below, at a more convenient place. In the seven years after the first publication, (...) there have been some noticeable newer developments in the logical study of Time and temporal expressions. As far as Temporal Logic proper is concerned, it seems fair to say that these amount to an increase in coverage and sophistication, rather than further break-through innovation. In fact, perhaps the most significant sources of new activity have been the applied areas of Linguistics and Computer Science (including Artificial Intelligence), where many intriguing new ideas have appeared presenting further challenges to temporal logic. Now, since this Book has a rather tight composition, it would have been difficult to interpolate this new material without endangering intelligibility. (shrink)

Sentences such as "The author started the book" are indeterminate because they do not make explicit what the subject (the author) started doing with the object (the book). In principle, indeterminate sentences allow for an infinite number of interpretations. One theory, however, assumes that these sentences are resolved by semantic coercion, a linguistic process that forces the noun "book" to be interpreted as an activity (e.g., writing the book) or by a process that interpolates this activity information in the resulting (...) enriched semantic composition. An alternative theory, pragmatic, assumes classical semantic composition, whereby meaning arises from the denotation of words and how they are combined syntactically, with enrichment obtained via pragmatic inferences beyond linguistic-semantic processes. Cognitive neuroscience studies investigating the neuroanatomical and functional correlates of indeterminate sentences have shown activations either at the ventromedial pre-frontal cortex or at the left inferior frontal gyrus. These studies have supported the semantic coercion theory assuming that one of these regions is where enriched semantic composition takes place. Employing fMRI, we found that indeterminate sentences activate bilaterally the superior temporal gyrus, the right inferior frontal gyrus, and the anterior cingulate cortex, more so than control sentences ("The author wrote the book"). Activation of indeterminate sentences exceeded that of anomalous sentences ("…drank the book") and engaged more left- and right-hemisphere areas than other sentence types. We suggest that the widespread activations for indeterminate sentences represent the deployment of pragmatic-inferential processes, which seek to enrich sentence content without necessarily resorting to semantic coercion. (shrink)

This article holds that governmental investments in quantum technologies speak to the imaginable futures of digital sovereignty and digital infrastructures, two major areas of change driven by related technologies like AI and Big Data, among other things, in international law today. Under intense development today for future interpolation into digital systems that they may alter, quantum technologies occupy a sort of liminal position, rooted in existing assemblages of computational technologies while pointing to new horizons for them. The possibilities they raise (...) are neither certain nor determinate, but active investments in them (legal, political and material investments) offer perspective on digital technology-driven influences on an international legal imagination. In contributing to visions of the future that are guiding ambitions for digital sovereignty and digital infrastructures, quantum technologies condition digital technology-driven changes to international law and legal imagination in the present. Privileging observation and description, I adapt and utilize a diffractive method with the aim to discern what emerges out of the interference among the several related things assembled for this article, including material technologies and legal institutions. In conclusion, I observe ambivalent changes to an international legal imagination, changes which promise transformation but appear nonetheless to reproduce current distributions of power and resources. (shrink)

This article interprets Jakob von Uexkull’s understanding of different beings’ Innenwelt, Gegenwelt, and umwelt through Deleuzian insights of multiplicity, context, and particularity. This Deleuzian interpolation into Uexkull’s insights acknowledges the absence of a unitary ‘human’ view of nature, recognizing instead that plural viewpoints of cultures, subgroups and individuals understand and interpret natural signs variously not just because of ideology but because of physiology and contrastive fundamental ways of accessing the world. Recent formative research in comparative neurobiology suggests that universal anthropological (...) claims of cross-cultural semiotic similarity are incorrect.Interpreting biosemiotics as the investigation of apprehending the Innenwelt of radically different others (species), such semiotic understandings themselves are not necessarily generalizable between different members of the same species in a group, same-species groups in different natural cultural contexts, or even (as with humans) the same animal at different points of time (based on new understandings, patterns, or events of meaning altering interpretations of self and events). Conjoining Deleuze’s insights of the complexity of multiplicity with Uexkull’s scientific-imaginative system of comprehending other creatures’ ways of understanding their world offers an increased self-reflexivity regarding the simultaneous levels of actual semiotic activity for biosemiotic inquiry. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:diacritics 30.1 (2000) 2-24 [Access article in PDF] Three-Way Misreading Mieke Bal Gayatri Chakravorty Spivak. A Critique of Postcolonial Reason: Toward a History of the Vanishing Present. Cambridge: Harvard UP, 1999. [CPR] Introduction: Reading Other-Wise This openly declared interest makes my reading the kind of "mistake" without which no practice can enable itself. 1 --Gayatri Chakravorty Spivak, Critique of Postcolonial ReasonAs many readers of this journal familiar with her (...) earlier work will surmise, Gayatri Chakravorty Spivak's Critique of Postcolonial Reason (CPR) is not easy to read. Yet reading is what the book is about, what it does, and what it teaches. The book, on more levels than one but beginning with its own accessibility, teaches how to read, other-wise. Indeed, this book is perhaps overreadable, if such a notion makes sense. I mean a form of readerliness based on multiplicity, both of (academic) levels and of lines of argumentation, subjects, and discourses. It can be read in a number of ways, none of which is adequate, all of which are enriching and useful for whatever area of specialization one is working in, as long as one is engaged in (thinking through) culture and the activity of analysis."My aim, to begin with, was...": beginning in the past tense and ending on the word "undone," this is a book with no beginning and no end, just like its subject matter, which can be briefly summarized as a passage from its title to a program of developing "transnational literacy." To pretend that either book or subject matter does have an end is to closet it. 2 But both book and subject matter have many openings that beckon you in yet leave the doors open so you can leave when and how you wish. Thus, it sets itself up to be appropriated, and in full awareness of how that makes me complicitous with much that the author at times rants about, I feel compelled to do just that: to productively misread it. Feeling invited to take the book "home"--to divert it from its many-branched course but confirming its multiple readership--I will offer here three readings of CPR. All three are willful misreadings, for misreading, always inevitable, is particularly indispensable in this encounter. 3 Instead of a review, I offer a pedagogical supplement. I will follow or spin three threads, to which the book is in no way reducible, and which [End Page 2] [Begin Page 4] are even insufficiently complex to account for the part-issue on which they focus. My goal is simply to convey one sense in which this book can be read with enormous productivity. I have selected three issues that appear as misreadings even at first sight, to the extent that they foreground aspects of the book's reasoning and analysis that are paradoxical here. In a study explicitly allied to postcolonial theory and politics, I will discuss aesthetics; in a practice of deconstruction, referentiality; and in a book of intricate and self-reflective writing, orality. These three elements are meant to underscore and remedy the profound misreadings to which those who mistrust, misinterpret, or misjudge the author's triple allegiance to transnational culture studies, deconstructive critique, and teaching have subjected her work.CPR contains four long chapters, simply titled "Philosophy," "Literature," "History," "Culture." Simply, or overambitiously? Neither. Whenever the book appears to spread out, it narrows down in the same move. The enumeration embodies a tight program. The sequence of the chapters is clear and significant. It is justified forwards and backwards as an itinerary and guideline for an interdisciplinary culture study that is responsible to each of its components as well as to the objects that can be confined to none. Moving forwards, "Philosophy" examines the arguments, "Literature" the figurations, "History" the archival material in which arguments and figurations collaborate to determine, and retrospectively leave traces of, what happened. 4 "History" also changes the practice of history by interpolating between positive research and philosophy the need to read and a way to do it, borrowed largely from literature. "Culture" opens up to the politics of a world in... (shrink)

This article is about ‘genogeographic’ maps produced by late-Soviet geneticists and published during post-Soviet time. It focuses on the visual and numerical techniques scientists used to project genetic data onto geographic space. Rather than discussing their representational character, I follow these visuals as ‘folded objects’, describing the layering and realigning of measurements and temporalities as well as the shifts in the practices and meanings of genetics. In the 1970s Soviet biological anthropologists transformed scattered data points by means of spatial statistics (...) into visually coherent maps for a ‘genogeographical atlas’, by interpolating data for the entire USSR territory. Computer-aided modelling rendered ‘populations’ as systemic entities and enacted specific cybernetic versions of population, evolution and difference. Tracing the history of their making helps one in understanding what these folded objects hold in store, in terms of data ranging from Russian imperial and colonial anthropology, through early Soviet traditions, to cold war technologies. Folded into those maps in intricate ways, they have co-shaped post-Soviet human genetics as an ever-active site for possible reinscriptions of difference. (shrink)

Short-term or working memory provides temporary storage of information in the brain after an experience and is associated with conscious awareness. Neurons sensitive to the multiple stimulus attributes comprising an experience are distributed within many brain regions. Such distributed cell assemblies, activated by an event, are the most plausible system to represent the WM of that event. Studies with a variety of imaging technologies have implicated widespread brain regions in the mediation of WM for different categories of information. Each kind (...) of WM may thus be expected to involve many brain regions rather than a local, uniquely dedicated set of cells. Neurons in a distributed “cell assembly” may be self-selected by their temporally coherent activations. The process by which this fragmented representation of the recent past is reassembled to accomplish essentially automatic and reliable recognition of a recurrent event constitutes an important problem. One plausible mechanism to achieve the identification of past with previous events would require that the representational system mediating WM must coexist in spatial extent and somehow overlap in temporal activation with cell ensembles registering input from subsequent events. The detection of such a postulated mechanism required an experimental approach which would focus upon spatial patterns of coherent activation while information about different events was stored in WM and retrieved, rather than focusing upon the temporal sequences of activation in localized regions of interest. For this purpose, the familiar delayed matching from sample task was modified. A series of information-free flashes, or “noncontingent probes,” was presented before an initial series of visual information items, the Priming Sample, which were to be held in WM during a Delay Period. A second series of visual information items were then presented, the Matching Sample. The task required detection of any item in the second series which had beenabsentfrom the initial series. Thirty such trials with a particular category of visual information constituted a single task. Several DMS tasks with this standardized design, but with different categories of visual information, were presented within each test session. The information categories included letters of the alphabet, single digit numbers, or faces from a school yearbook. Event-related potentials , were computed from 21 standardized electrode placements, separately for information-free probes and for information items in each interval of the trials within a task. Because each electrode is particularly sensitive to coherent activation of neurons in the immediately underlying brain regions, topographic maps were constructed and interpolated across the surface of the scalp. The momentary fluctuations of the resulting voltage “landscapes” throughout the task were then subjected to quantitative analysis. Distinctive landscapes sometimes persisted for prolonged periods, implying sustained engagement of very large populations of neurons. “Difference landscapes” were constructed by subtraction of topographic maps evoked by noncontingent probes during the Delay Period from maps of probe ERPs before the presentation of the initial information in the Priming Sample. Such probe difference landscapes displayed recurrent high similarity to momentary landscapes elicited during subsequent presentation of the information items in the Matching Sample. It seemed as if the distributed cell assembly continuously engaged by mediation of WM of the diverse attributes of the initial stimuli was being dynamically compared to the ensembles engaged by registration of the subsequent stimuli. Spatial Principal Component Analysis was applied to the sequences of momentary voltage landscapes observed throughout trials of each task. This method sought a small number of spatial patterns with which these large sets of inhomogeneous spatial distributions of voltage could be reconstructed. This is the spatial analog of the reconstruction of local ERPs by temporal principal components, as often described previously. Five Spatial Principal Components were found which accounted for about 90% of the total variance of voltage across the surface of the scalp throughout every task. Theloadings,or distinguishing topographic features, of these SPCs, were highly similar during every cognitive task for every subject. However,factor scores,or relative average contribution to the overall voltage distributions, of the different SPCs varied substantially among subjects between the tasks and momentarily within successive intervals of each task. These five SPCs may reflect coherent activation of huge distributed ensembles of neurons which comprise independent but interacting functional brain subsystems. These subsystems may correspond to basic resources available to individuals for allocation to mediate conscious evaluation of information during cognitive activity, providing a filter to bind together fractionated representations of the past to evaluate the present. (shrink)

This work examines how the conceptualization of knowledge as both problem and solution reconfigured intelligence and law enforcement after 9/11. The idea was that more information should be collected, and better analyzed. If the intelligence that resulted was shared, then terrorists could be identified, their acts predicted, and ultimately prevented. Law enforcement entered into this scenario in the United States, and internationally. "Policing terrorism" refers to the engagement of state and local law enforcement in intelligence, as well as approaching terrorism (...) as a legal crime, in addition to or as opposed to an act of war. Two venues are explored: fusion centers in the United States and the international organization of police, Interpol. The configuration can be thought of schematically as operating through the set of law, discipline and security. Intelligence is predominantly a security approach. It modulates that within its purview, wielding the techniques and technologies that are here discussed.The dissertation is divided into two sections: Intelligence and Policing Terrorism. In the first, intelligence is taken up as a term, and its changes in referent and concept are examined. The Preface and Chapter One present a general introduction to the contemporary situation and intelligence, via Sherman Kent, as knowledge, organization and activities. Chapter Two traces the development of intelligence in the United States as a craft and profession. Chapter Three discusses some of the issues involving the intersection of intelligence and policy, and how those manifested in the aftermath of 9/11 and the lead up to the 2003 invasion of Iraq. The second section examines the turn to policing terrorism, beginning, in Chapter Four, with how Interpol has dealt with bioterrorism, and an examination of the shifting conceptualization of biological threats in international law. Moving from threats to their consequences, Chapter Five takes up the concept of an event in order to analyze the common comparison of Pearl Harbor and 9/11. Chapters Six and Seven turn to fieldwork done in the United States, with an examination of the suspicious activity reporting system and law enforcement's inclusion in the Information Sharing Environment, focusing on fusion centers and data mining. (shrink)

Given that Lucretius offers a systematic and cohesive explanation of the workings of nature, we should not expect inconsistencies in his poem. The explanation presented by Lucretius emphatically rejects any interventionist divine machinery of the cosmos, offering in its place the eminently regular dynamics of atomic configuration and dissolution, which can explain everything that pertains to natural philosophy without necessitating the activity of any divinity. The reader who understands the basics of Lucretius’ philosophy, therefore, should be surprised that theDRNbegins with (...) an anthropomorphic description of the goddess Venus, whom the poet petitions to intervene actively in human affairs. Lucretius gradually refines this initial presentation of the goddess’ essence throughout the poem, suggesting that the Venus who inaugurates the poem must be nuanced once one has learned the basic principles of Epicurean philosophy. At the end ofDRN4, Venus is presented not as a divine being but as nothing more than the sexual drive shared by all creatures in nature (haec Venus est nobis, 4.1058). Historically scholars have been keen to ‘correct’ perceived inconsistencies such as this, either by arguing that such imperfections derive from later interpolators or by appealing to the incomplete nature of the text as we possess it. Of course, no one has suggested that Lucretius would have changed or removed the proem, so the Venus problem remains an issue. One major aim of this article is to show that the process we witness with Lucretius’ Venus is not inconsistent but programmatic, a point grasped by many with regard to Venus herself but not in respect to theDRNas a whole. In other words, this article extends this insight about Lucretius’ Venus, whose providential attributes are only provisionally attached to her at the outset of the poem and, in due course, are completely removed. In fact, I will argue that the technique of gradually redefining initial propositions—a process I will refer to as provisional argumentation—fundamentally informs Lucretius’ famous metaphor of the honeyed cup, and I will suggest that we ought to recognize this technique as a major aspect of Lucretius’ discursive method throughout theDRN. (shrink)

Literary criticism is neither more nor less important today than it has been since the becoming an accepted activity in the Renaissance. The humanists of the sixteenth and seventeenth centuries created the institution of criticism as we know it: the recovery and analysis of works of art. They printed, edited, and interpreted texts that dated from antiquity and which had been lost or disheveled. Evangelical in their fervor, avid in their search for lost or buried riches, they also put into (...) circulation certain influential ideas. Perhaps the most important of these was that the authoritative version of a book is the original version, freed from interpolation and accretion. A correlative idea was that, similarly, one could rely on an original or natural light in the interpreter, an intuitive good sense that helped him to a true understanding of a text if it was a genuine text. . . . There are signs that we are now nearing the end of this Renaissance humanism. Not because of a determinist or providential march of history, but ideas eventually exhaust what influence they may have. Today, after all, there is no dearth of ancient texts, or of new ones. Editing, moreover, has become only too conscious of the difficulty of recovering an "original" version or edition: in Wordsworth scholarship, for example, the authority of the 1850 Prelude, the text approved by the poet shortly before his death, was challenged by the 1805-6 Prelude printed by de Sélincourt in the 1920s; and the authority of this is in turn being eroded by antecedent manuscripts, the so-called "Five-Books Prelude" and "Two-Part Prelude." It is equally precarious to establish the text of Emily Dickinson's poems—which of the variants are to be chosen as definitive? Or, from another angle, Melville's Billy Budd has become a mine for genetic speculation. Even when no editorial problem exists, a philosophical issue arises as to the concept of originality itself.1 · 1. For the time being, it is enough to quote Hegel's provocative attack on all "Ur-Metaphysics": "What comes later is more concrete and richer; the first is abstract, and least differentiated." Geoffrey Hartman, professor of English and comparative literature at Yale University, is the author of The Unmediated Vision, Andre Malraux, Wordsworth's Poetry, Beyond Formalism, and most recently The Fate of Reading. He is currently working on a book to be published in late 1977, Criticism in the Wilderness. (shrink)

Ioulios Polydeukes, more commonly known as Pollux, was a Greek sophist and lexicographer active in the closing decades of the second century a.d. His Onomasticon is one of the most important lexicographical texts of the Imperial period. It is essentially a set of word lists dedicated to collecting clusters of related words on topics from a vast range of different areas of intellectual activity and everyday life. The text survives only in epitomized form, and shows signs of interpolation as well (...) as abridgement. Nevertheless, the consensus is that the bulk of what survives is Pollux’ own work, and that reading it in Eric Bethe's Teubner edition gives an accurate cumulative impression of Pollux’ standard procedures and preoccupations, even if we cannot be entirely confident that any particular cluster of words had exactly the same form within the text's original design. It is divided into ten books, each with its own dedicatory preface addressed to the Emperor Commodus. Each book has its own distinctive focus on certain key themes, although the ordering principles are much clearer in some than in others. (shrink)

In this paper we draw attention that there have been significant increases in activity relating to child sexual abuse and exploitation on both the surface web and dark web during the COVID-19 lockdown period. This paper aim is an analyse about how the COVID-19 pandemic is presently modifying the trends and threats of child sexual exploitation and abuse offences, which were already at high levels prior to the pandemic. This article highlights the trends and threats in the current COVID-19 context (...) compared to pre-pandemic measures, what impact these are having in the short-term, and what changes we have seen when COVID-19 measures are reduced. It contributes to the space of the dark web during lockdown by manifestation on the ongoing organised business model that has evolved as technology expands and the level of threat that it poses to children. The objective is to share these trends across the global law enforcement community and science in order to improve the monitoring and detection of child sexual exploitation and abuse online, further investigations and global police response. (shrink)

This chapter examines global policing as it takes shape through the work of Interpol, the International Criminal Police Organization. Global policing emerges in the legal, political and technological amalgam through which transnational police cooperation is carried out, and includes the police practices inflected and made possible by this phenomenon. Interpol’s role is predominantly in the circulation of information, through which it enters into relationships and provides services that affect aspects of governance, from the local to national, regional and global. The (...) chapter describes this assemblage as a noteworthy experiment in developing what McKeon called a frame for common action. Drawing on Interpol publications, news stories, interviews with staff, and fieldwork at the General Secretariat in Lyon, France, the history, institutional structure, and daily practices are described. Three cases are analyzed, concerning Red Notices, national sovereignty, and terrorism, in order to explore some of the problems arising in Interpol’s political and technical operating arrangements. In conclusion, international and global policing are compared schematically, together with Interpol’s attempts to give institutional and procedural direction to the still-evolving form of global policing. (shrink)

We discuss the interpolation property on some important families of non classical logics, such as intuitionistic, modal, fuzzy, and linear logics. A special paragraph is devoted to a generalization of the interpolation property, uniform interpolation.

In this article we show that bi-intuitionistic predicate logic lacks the Craig Interpolation Property. We proceed by adapting the counterexample given by Mints, Olkhovikov and Urquhart for intuitionistic predicate logic with constant domains [13]. More precisely, we show that there is a valid implication $\phi \rightarrow \psi $ with no interpolant. Importantly, this result does not contradict the unfortunately named ‘Craig interpolation’ theorem established by Rauszer in [24] since that article is about the property more correctly named ‘deductive interpolation’ (see (...) Galatos, Jipsen, Kowalski and Ono’s use of this term in [5]) for global consequence. Given that the deduction theorem fails for bi-intuitionistic logic with global consequence, the two formulations of the property are not equivalent. (shrink)

We analyse the structure of propositional proofs in the sequent calculus focusing on the well-known procedures of Interpolation and Cut Elimination. We are motivated in part by the desire to understand why a tautology might be ‘hard to prove’. Given a proof we associate to it a logical graph tracing the flow of formulas in it . We show some general facts about logical graphs such as acyclicity of cut-free proofs and acyclicity of contraction-free proofs , and we give a (...) proof of a strengthened version of the Craig Interpolation Theorem based on flows of formulas. We show that tautologies having minimal interpolants of non-linear size must have proofs with certain precise structural properties. We then show that given a proof Π and a cut-free form Π′ associated to it , certain subgraphs of Π′ which are logical graphs correspond to subgraphs of Π which are logical graphs for the same sequent. This locality property of cut elimination leads to new results on the complexity of interpolants, which cannot follow from the known constructions proving the Craig Interpolation Theorem. (shrink)

Preservation and interpolation results are obtained for L ∞ω and sublogics $\mathscr{L} \subseteq L_{\infty\omega}$ such that equivalence in L can be characterized by suitable back-and-forth conditions on sets of partial isomorphisms.

Interpolation has become one of the standard properties that logicians investigate when designing a logic. In this paper, we provide strong evidence that the presence of interpolants is not only cogent for scientific reasoning but has also important practical implications in computer science. We illustrate that interpolation in general, and uniform splitting interpolants, in particular, play an important role in applications where formality and modularity are invoked. In recognition of the fact that common logical formalisms often lack uniform interpolants, we (...) advocate the need for developing general methods to engineer a specification logic so that some critical uniform interpolants become available. (shrink)

A new technique is presented for proving that a consequence system enjoys Craig interpolation or Maehara interpolation based on the fact that these properties hold in another consequence system. This technique is based on the existence of a back and forth translation satisfying some properties between the consequence systems. Some examples of translations satisfying those properties are described. Namely a translation between the global/local consequence systems induced by fragments of linear logic, a Kolmogorov-Gentzen-Gödel style translation, and a new translation between (...) the global consequence systems induced by full Lambek calculus and linear logic, mixing features of a Kiriyama-Ono style translation with features of a Kolmogorov-Gentzen-Gödel style translation. These translations establish a strong relationship between the logics involved and are used to obtain new results about whether Craig interpolation and Maehara interpolation hold in that logics . (shrink)

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.

Preservation and interpolation results are obtained for L ∞ω and sublogics $\mathscr{L} \subseteq L_{\infty\omega}$ such that equivalence in L can be characterized by suitable back-and-forth conditions on sets of partial isomorphisms.

We investigate interpolation properties of many-valued propositional logics related to continuous t-norms. In case of failure of interpolation, we characterize the minimal interpolating extensions of the languages. For finite-valued logics, we count the number of interpolating extensions by Fibonacci sequences.

Several extensions of the basic modal language are characterized in terms of interpolation. Our main results are of the following form: Language ℒ' is the least expressive extension of ℒ with interpolation. For instance, let ℳ be the extension of the basic modal language with a difference operator [7]. First-order logic is the least expressive extension of ℳ with interpolation. These characterizations are subsequently used to derive new results about hybrid logic, relation algebra and the guarded fragment.

Arrow and turnstile interpolations are investigated in UCL [introduced by Sernadas et al. ], a logic that is a complete extension of classical propositional logic for reasoning about connectives that only behave as expected with a given probability. Arrow interpolation is shown to hold in general and turnstile interpolation is established under some provisos.

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. (shrink)