We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to (...) a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics. (shrink)

We define cut-free display calculi for knowledge logics wherean indiscernibility relation is associated to each set of agents, andwhere agents decide the membership of objects using thisindiscernibility relation. To do so, we first translate the knowledgelogics into polymodal logics axiomatised by primitive axioms and thenuse Kracht's results on properly displayable logics to define thedisplay calculi. Apart from these technical results, we argue thatDisplay Logic is a natural framework to define cut-free calculi for manyother logics with relative accessibility relations.

We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.

ABSTRACT It has become standard to conceive of metalinguistic disagreement as motivated by a form of negotiation, aimed at reaching consensus because of the practical consequences of using a word with one content rather than another. This paper presents an alternative motive for expressing and pursuing metalinguistic disagreement. In using words with given criteria, we betray our location amongst social categories or groups. Because of this, metalinguistic disagreement can be used as a stage upon which to perform a social identity. (...) The ways in which metalinguistic disagreements motivated in this way diverge in character from metalinguistic negotiations are described, as are several consequences of the existence of metalinguistic disagreements motivated in this way. (shrink)

The present monograph is a slightly revised version of my Habilitations schrift Proof-theoretic Aspects of Intensional and Non-Classical Logics, successfully defended at Leipzig University, November 1997. It collects work on proof systems for modal and constructive logics I have done over the last few years. The main concern is display logic, a certain refinement of Gentzen's sequent calculus developed by Nuel D. Belnap. This book is far from offering a comprehensive presentation of generalized sequent systems for modal logics broadly conceived. (...) The proof-theory of non-classical logics is a rapidly developing field, and even the generalizations of the ordinary notion of sequent listed in Chapter 1 can hardly be presented in great detail within a single volume. In addition to further investigating the various approaches toward generalized Gentzen systems, it is important to compare them and to discuss their relative advantages and disadvantages. An initial attempt at bringing together work on different kinds of proof systems for modal logics has been made in [188]. Another step in the same direction is [196]. Since Chapter 1 contains introductory considerations and, moreover, every remaining chapter begins with some surveying or summarizing remarks, in this preface I shall only emphasize a relation to philosophy that is important to me, register the sources of papers that have entered this book in some form or another, and acknowledge advice and support. (shrink)

Many logics in the relevant family can be given a proof theory in the style of Belnap's display logic. However, as originally given, the proof theory is essentially more expressive than the logics they seek to model. In this paper, we consider a modified proof theory which more closely models relevant logics. In addition, we use this proof theory to show decidability for a large range of substructural logics.

We compare several methods of implementing the display (sequent) calculus RA for relation algebra in the logical frameworks Isabelle and Twelf. We aim for an implementation enabling us to formalise within the logical framework proof-theoretic results such as the cut-elimination theorem for RA and any associated increase in proof length. We discuss issues arising from this requirement.

This article contributes to ongoing studies in conversation analysis dealing with the way in which epistemic authority is displayed, claimed, contested and negotiated in social interaction. More particularly, it focuses on the articulation between action format, sequential organization, membership categorization and epistemic authority. The article offers an empirical analysis of the way in which knowledge is distributed and recognized in social gatherings, with a special focus on guided visits. Guided visits are a perspicuous setting for this analysis, since it is (...) an activity in which the guide displays knowledge in comments and explanations and the guided seeks for knowledge in questions. However, this distribution of knowledge is regularly challenged. The article offers a systematic study of a collection of sequences initiated by turns beginning with ‘et là’ and locating a new referent in the environment, either in informings or in questions. While the former are frequently produced by the guide, assuming a knowing status, and the latter by the guided, assuming a not knowing, it is possible to observe informings initiated by the guided, who, by so doing, claims a revision of his or her epistemic authority. Likewise, in second position, questions are generally answered by the guide, but can also be answered by another person, claiming alternative epistemic rights. By examining the details of turn and action design in these environments, the article shows how they either reproduce and confirm the current epistemic status of the participants or challenge, negotiate and transform them. The latter case is particularly revealing of the fact that epistemic status and stance are constantly reflexively elaborated by the participants in social interaction. (shrink)

This article addresses the issue of how team identity is constructed between two people during a series of regular meetings of a work group in Serbia. Using conversation analysis to investigate social actions, this study looks at the recurrent construction of an implicit team identity by focusing on management of speaking rights and co-construction of units, and displays of knowledge and accountability. With its longitudinal perspective, the article contributes to the existing body of research on teams in interaction in (...) general, as it builds upon previous research on interactional parties and conjoined participation. The results are especially relevant for the investigations of teams in meetings, as they provide evidence of how formal features of interaction are recurrently employed to display institutionally relevant epistemics and accountability. (shrink)

In this paper we introduce and compare four different syntactic methods for generating sequent calculi for the main systems of modal logic: the multiple sequents method, the higher-arity sequents method, the tree-hypersequents method and the display method. More precisely we show how the first three methods can all be translated in the fourth one. This result sheds new light on these generalisations of the sequent calculus and raises issues that will be examined in the last section.

This paper is a revised version of a talk given at the Logic and Logical Philosophy conference in Poland in September 1995. In it, I sketch the connections between Nuel Belnap's Display Logic and J. Michael Dunn's Gaggle Theory.

Live streaming shopping, the streaming of real-time videos promoting products that consumers can purchase online, has recently been a booming area of e-commerce, especially during the COVID-19 pandemic. The success of live streaming e-commerce largely relies on the extent to which the broadcaster can get consumers engaged by the live stream. Thus, it is important to discover the antecedents of consumer engagement in such a context. Drawing on consumer engagement and neuroscience literature, this study used electroencephalography inter-subject correlation to explore (...) how broadcasters' entrepreneurial passion during live streaming videos influenced consumers' neural engagement as they watched the live streaming videos. We used the framework of displayed passion and preparedness from the entrepreneurial passion literature to predict consumer engagement. We found significant ISC for strong displayed passion, while preparedness had partially significant effects on the first, second, and summed components of ISC. The interaction effects of these two factors on the first and summed components of ISC were partially significant. Strong displayed passion and preparedness activated the left and right prefrontal regions of the consumers' brains. These findings indicate that broadcasters' displayed passion and preparedness can influence consumer engagement in live streaming e-commerce settings. Our findings suggest that a scientific approach could be used to improve a broadcaster's performance by testing ISC during rehearsals before live streaming. (shrink)

In this essay I give a complete join semi-lattice of possible display-equivalence schemes for Display Logic, using the standard connectives, and leaving fixed only the schemes governing the star. In addition to proving the completeness of this list, I offer a discussion of the basic properties of these schemes.

This study investigates moments in which one participant in an interaction embodies that he is “doing thinking,” a display that is commonly referred to as “thinking face. ” From an interactional perspective, it is assumed that embodied displays of “doing thinking” are a recurring social practice and serve interactive functions. While previous studies have examined thinking faces primarily in word searches and storytelling, the present study focuses on argumentative activities, in which children engage in processes of joint decision-making. The (...) paper has two interrelated aims. The first aim is to describe how multiple modalities—beyond the face—are temporally coordinated to create multimodal gestalts of “doing thinking.” It is shown that thinking displays not only involve dynamic imaginative gaze but also stylized bodily postures. The second aim is to generate knowledge about the functions of thinking displays in children's argumentative activities. The analysis describes how both speakers and recipients use thinking displays in different turn positions and align them with verbal talk or silence. The data for this study comprise video recordings of decision-making processes in groups of older children. Drawing on a multimodal approach to situated interaction, it will be proposed that embodied displays of “doing thinking” provide a resource to shape participation frameworks, mark epistemic stances and create epistemic ecologies for collaborative reasoning. By investigating thinking displays in a particular conversational activity, the study sheds light on the diversity and context-sensitive functionality of thinking displays. It also contributes to recent research on children's collaborative reasoning as an embodied discursive practice. (shrink)

It is shown that the constructive four-valued logic N4 can be faithfully embedded into the modal logic S4. This embedding is used to obtain complete, cut-free display sequent calculi for N4 and C4, the modal logic of consistency over N4. C4 is a natural monotonic base system for semantics-based non-monotonic reasoning.

According to the deductivist view of mathematics which became the rule during the nineteenth century, formal proofs working with symbolic formulas replaced the intuitive knowledge that used to be gained by the step-by-step construction of geometric fgures and diagrams. Twentieth century epistemological refection on symbolic formulas and formal proofs, however, took them to be diagrams respectively exhibiting formal relations and transformations. The claim was also made that, for such diagrams to be proofs, temporal displays of transformations—and of other speech (...) acts—were required. By returning to the signifcant elements of contemporary theories of mathematical proofs, we will here show how these proofs came to be a matter for semiotics and pragmatics as much as for formal logic. Once this is done, we will provide a few arguments against the standard objections to the ability of diagrams to present temporal order or perform speech acts. (shrink)

This paper presents an overview of the methods of hypersequents and display sequents in the proof theory of non-classical logics. In contrast with existing surveys dedicated to hypersequent calculi or to display calculi, our aim is to provide a unified perspective on these two formalisms highlighting their differences and similarities and discussing applications and recent results connecting and comparing them.

It is shown that the constructive four-valued logic N4 can be faithfully embedded into the modal logic S4. This embedding is used to obtain complete, cut-free display sequent calculi for N4 and C4, the modal logic of consistency over N4. C4 is a natural monotonic base system for semantics-based non-monotonic reasoning.

We formulate a unified display calculus proof theory for the four principal varieties of bunched logic by combining display calculi for their component logics. Our calculi satisfy cut-elimination, and are sound and complete with respect to their standard presentations. We show how to constrain applications of display-equivalence in our calculi in such a way that an exhaustive proof search need be only finitely branching, and establish a full deduction theorem for the bunched logics with classical additives, BBI and CBI. We (...) also show that the standard sequent calculus for BI can be seen as a reformulation of its display calculus, and argue that analogous sequent calculi for the other varieties of bunched logic are very unlikely to exist. (shrink)

In the present article, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly (...) beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag–Moss–Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination. (shrink)

Given the prevalence of social media, a nascent but important area of research is the effect of social media posting on one’s own self. It is possible that an individual’s social media posts may have predictive capacity, especially in relation to health behavior. Researchers have long used concepts from the theory of reasoned action to predict health behaviors. The theory does not account for social media, which may influence or predict health behaviors. The purpose of this study was to test (...) a model including Facebook alcohol displays and constructs from the theory of reasoned action to predict binge drinking. Incoming college freshmen from two schools (312 participants between 18 and 19 years old) were interviewed prior to (T1) and 1 year into college (T2), and their Facebook profiles were evaluated for displayed alcohol content. Path modeling was used to evaluate direct and indirect paths predicting binge drinking. Path analysis suggested that Facebook alcohol displays at T1 directly predict binge drinking at T2, while alcohol attitude both directly and indirectly predicts binge drinking. Based on these results, a preliminary model of social media presentation and action is discussed. (shrink)

The actual and potential uses of holograms in museum displays, and the philosophy of knowledge and progress that they represent. Magazine journalists, museum curators, and historians sometimes face similar challenges in making topics or technologies relevant to wider audiences. To varying degrees, they must justify the significance of their subjects of study by identifying a newsworthy slant, a pedagogical role, or an analytical purpose. This chasse au trésor may skew historical story telling itself. In science and technology studies, the (...) problem potentially is worst for those subjects that do not retain an enduring capacity for spectacle or do not readily conform to templates of progress or economic importance. The case of holography is an excellent illustration of these points. An unusually wide-ranging subject, holography has attracted competing interpretations of intellectual novelty, technological application, and cultural significance. This paper examines the history of museum collections and exhibits of holography from the explosion of interest in the technique in 1964 to the end of the twentieth century. I argue that holography presents a particular challenge to museum collections and to popular representations of the history of science and technology. (shrink)

Resumo Neste artigo, tentar-se-á reconstruir e defender a noção de “especificidade média” que se refere ao cinema. Começar-se-á por discutir a ontologia de um certo tipo de exibição visual, geralmente encontrada em conexão com uma vasta gama de obras cinematográficas. Argumentar-se-á que estas exibições têm uma natureza essencial ou real. Obras construídas em torno de tais exibições estão aptas a manifestar certas qualidades e poderes peculiares. Assim, o “meio de cinema” consiste em parte, num tipo particular de meio veicular e, (...) de várias propriedades nem sempre manifestas distintas dele. Ao discutir-se o conceito de “meio”, considera-se também um sentido em que esta noção é negligenciada, a saber, que as competências e habilidades pessoais operam uma mediação entre a concepção de uma exibição e a sua produção. Prosseguir-se-á, argumentando, que apesar dos defeitos da “especificidade média”, proveniente de uma versão da teoria clássica do cinema, o cinema como uma forma de arte ou corpo de obras de arte, é ou tem um “meio especial” dotado de distintas propriedades artísticas. Palavras-chave : essencialismo, medium specificity, medium, obra, ontologia do cinema, valor artísticoIn this paper, I try to reconstruct and defend the notion of medium specificity as it relates to cinema. I begin by discussing the ontology of a certain kind of visual display commonly found in connection with a vast range of candidate cinematic works. These displays, I argue, have an essential or real nature. Works constructed around such displays are apt to manifest certain qualities and powers peculiar to displays of that kind. Thus cinema’s medium consists in part of a particular type of vehicular medium and various not always manifested properties distinctive to it. In discussing the concept of medium, I also consider a neglected sense of this term, namely, personal abilities and skills that mediate between one’s designing a certain display and one’s producing a matching object or result. I go on to argue that, despite the defects of classic film theory’s version of medium specificity, it is true that cinema, as artform or body of artworks, is or has a special medium endowed with distinctive artistic properties. Keywords : artistic value, essentialism, medium specificity, medium, ontology of cinema, work. (shrink)

Post-Fregean theorists use 'quotation' to denote indifferently both colloquially called quotations (repetitions of prior utterances) and what I call 'displays': 'Rot' means red. Colloquially, quotation is a strictly historical property, not semantic or syntactic. Displays are semantically and syntactically distinctive sentential elements. Most displays are not quotations. Pure echo quotations (Cosmological arguments involve "an unnecessary shuffle") aren't displays. Frege-inspired formal languages stipulate that enquotation forms a singular term referring to the enquoted expression (type). Formalist enquotations differ (...) semantically and syntactically from natural language displays. Call them autonomes, and mark them with stars: *Rot* means red. In formal languages, an unenstarred expression has only one meaning, and an autonome has only one meaning viz., a name (or indexical) designating the unenstarred expression (type). Stars have semantic content and can’t disambiguate. Display punctuation only disambiguates; it says only: This material is displayed. Displays have a semantic function; their marks don't.nDisplays are not terms or lexical items. Displays are objects incorporable into utterances. Such incorporation enables them to be linguistically appropriated much as we appropriate speech-external objects by extrasentential supplementation (e.g., gesturing) to identify the extension of a term by ostending the object -- but now without any extrasentential supplement. Displays are always adjunctive to an (implicit or explicit) ostensionable term, a term whose extension is identifiable by ostending an object. The display-ostensionable term extension relations are various. A display may (1) be the term's referent, or (2) represent the term's extension by (a) replicating or (b) instantiating or (c) expressing the term's referent, or (e) instantiating the property the term predicates. (shrink)

Runaway social selection resulting from partner choice may have shaped aspects of human cooperation and complex sociality that are otherwise hard to account for. Social selection is the subtype of natural selection that results from the social behaviors of other individuals. Competition to be chosen as a social partner can, like competition to be chosen as a mate, result in runaway selection that shapes extreme traits. People prefer partners who display valuable resources and bestow them selectively on close partners. The (...) resulting phenotypic covariance between displays and preferences gives fitness advantages to both, creating runaway selection that could shape a whole suite of prosocial traits including altruism, moral capacities, empathy, and theory of mind. Even though they give a net fitness benefit, traits at the endpoint of runaway social selection can have substantial deleterious effects on other traits such as viability, ability to accumulate resources, or vulnerability to mental disorders. Social selection forces arising from self-interested partner choices may be an invisible hand that shaped capacities for commitment, altruism, and other prosocial capacities of the human social brain. (shrink)

Using multimodal conversation analysis, we investigate how novices learning the “inner body” acting technique in the context of a community theater project share their experiences of the bodily exercises through verbal and embodied conduct. We focus on how verbal description and bodily enactment of the experience mutually elaborate each other, and how the experienced sensorimotor and affective qualities are made to be witnessed and recognized by the others. Participants describe their experiences without naming qualities. Instead, a display of the experienced (...) qualities is made accessible to others through coordinating the unfolding talk and bodily conduct. In particular, we show how grammatical and action projection is fulfilled by interconnected verbal and embodied conduct, with body movement and posture giving off ineffable experiential qualities. The moving body appears both as a source of the experience and as a resource for depicting perceived qualities to others; additional resources (non-specific person reference and gaze aversion) contribute to organizing the subjective and intersubjective layers of the reflection of the experiences. The study contributes to and extends recent research on sensoriality in interaction by focusing on phenomena of proprioception and interoception. The data are two cases drawn from 60 h of video-recordings made in the context of a devised community theater project. The data are in Finnish with English translations. (shrink)

The protection of cultural relics has always been an important issue in the field of museums and archaeology. With the development of Internet of Things technology, the security system of the museum is more intelligent and integrated. In order for the museum display system to keep up with the intelligent age, this article mainly studies the research and realization of the museum showcase system based on the Internet of Things technology in a smart environment. Before the start of the experiment, (...) we developed the overall design of the system, including three functional modules: temperature module, illumination module, and monitoring module. The experiment is done mainly for system testing. The performance test of the sensor module needs to sample the temperature and humidity sensor to verify the accuracy of the temperature and humidity signal collected in the instrument circuit. The light information collection test uses the ADC sampling inside the CC2530 to obtain the required data and judges whether these temperature, humidity, and light intensity values exceed the preset values. The serial port needs to be initialized to carry out data communication and transmission normally. After the receiving end finishes receiving, the sending end will clear the data buffer to prepare for the next data transmission. The experimental data show that the error between the predicted value and measured value of the temperature system is about 3°C, which is within the allowable error range of the experiment. The results show that the system has perfect functions, is safe and reliable, meets the expected requirements, and has good practicability. (shrink)

We use a deep embedding of the display calculus for relation algebras ÆRA in the logical framework Isabelle /HOL to formalise a machine-checked proof of cut-admissibility for ÆRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle /HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.

We applaud Domjan et al. for providing an elegant account of Pavlovian feed-forward mechanisms in social behavior that eschews the pitfall of purposivism. However, they seem to imply that they have provided a complete account without provision for operant conditioning. We argue that operant conditioning plays a central role in social behavior, giving examples from fish and infant behavior.

The aim of this paper is to introduce and explain display calculi for a variety of logics. We provide a survey of key results concerning such calculi, though we focus mainly on the global cut elimination theorem. Propositional, first-order, and modal display calculi are considered and their properties detailed.