The goal of this paper is to introduce a new Gentzen formulation of the modal logic S5. The history of this problem goes back to the fifties where a counter-example to cut-elimination was given for an otherwise natural and straightforward formulation of S5. Since then, several cut-free Gentzen style formulations of S5 have been given. However, all these systems are technically involved, and furthermore, they differ considerably from Gentzen's original formulation of classical logic. In this paper we give a new (...) sequent system for S5 which is a straightforward and technically simple extension of Gentzen's original sequent system for classical logic. A characteristic feature is the notion of a connection in a proof. The new system satisfies cut-elimination as well as the subformula property. Cut-elimination is proved by giving an algorithm for eliminating cuts. The fact that we give an algorithm for eliminating cuts makes it clear that our system is susceptible to a formulae-as-types computational interpretation. (shrink)

This is the first book-length treatment of hybrid logic and its proof-theory. Hybrid logic is an extension of ordinary modal logic which allows explicit reference to individual points in a model. This is useful for many applications, for example when reasoning about time one often wants to formulate a series of statements about what happens at specific times. There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and the relationships between proof systems (...) for different modal logics are often unclear. In the present book we demonstrate that hybrid-logical proof-theory remedies these deficiencies by giving a spectrum of well-behaved proof systems for a spectrum of different hybrid logics. (shrink)

Hybrid logics are a principled generalization of both modal logics and description logics, a standard formalism for knowledge representation. In this paper we give the first constructive version of hybrid logic, thereby showing that it is possible to hybridize constructive modal logics. Alternative systems are discussed, but we fix on a reasonable and well-motivated version of intuitionistic hybrid logic and prove essential proof-theoretical results for a natural deduction formulation of it. Our natural deduction system is also extended with additional inference (...) rules corresponding to conditions on the accessibility relations expressed by so-called geometric theories. Thus, we give natural deduction systems in a uniform way for a wide class of constructive hybrid logics. This shows that constructive hybrid logics are a viable enterprise and opens up the way for future applications. (shrink)

Braüner, Blackburn and Polyanskaya relate children’s being deceived to their theory of mind skills. Second‐order false‐belief tasks are often used to test children’s second‐order theory of mind development. The article gives a logical analysis of the reasoning needed to solve four types of second‐order false belief tasks, distinguished on whether a story character is deceived, and on whether the story hinges on facts in the world changing. The principle of inertia plays an important role. [74].

This paper demonstrates the practical and philosophical strengths of adopting Luciano Floridi’s “general definition of information” (GDI) for use in the information sciences (IS). Many definitions of information have been proposed, but little work has been done to determine which definitions are most coherent or useful. Consequently, doubts have been cast on the necessity and possibility of finding a definition. In response to these doubts, the paper shows how items and events central to IS are adequately described by Floridi’s conception (...) of information, and demonstrates how it helps clarify the muddy theoretical framework resulting from the many previous definitions. To this end, it analyzes definitions, popular in IS, that conceive of information as energy, processes, knowledge, and physical objects. The paper finds that each of these definitions produces problematic or counterintuitive implications that the GDI suitably accounts for. It discusses the role of truth in IS, notes why the GDI is preferable to its truth-requiring variant, and ends with comments about the import of such a theory for IS research and practice. (shrink)

This is a companion paper to Braüner where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an axiom system first-order hybrid logic.

The main aim of the present paper is to use a proof system for hybrid modal logic to formalize what are called false-belief tasks in cognitive psychology, thereby investigating the interplay between cognition and logical reasoning about belief. We consider two different versions of the Smarties task, involving respectively a shift of perspective to another person and to another time. Our formalizations disclose that despite this difference, the two versions of the Smarties task have exactly the same underlying logical structure. (...) We also consider the Sally-Anne task, having a more complicated logical structure, presupposing a “principle of inertia” saying that a belief is preserved over time, unless there is belief to the contrary. (shrink)

In the paper (Braüner, 2001) we gave a minimal condition for the existence of a homophonic theory of truth for a modal or tense logic. In the present paper we generalise this result to arbitrary modal logics and we also show that a modal logic permits the existence of a homophonic theory of truth if and only if it permits the definition of a socalled master modality. Moreover, we explore a connection between the master modality and hybrid logic: We show (...) that if attention is restricted to bidirectional frames, then the expressive power of the master modality is exactly what is needed to translate the bounded fragment of first-order logic into hybrid logic in a truth preserving way. We believe that this throws new light on Arthur Prior's fourth grade tense logic. (shrink)

The standard medical case report often reduces patients and caregivers to complexes of medical facts and clinical decisions. Restructuring the genre itself to acknowledge the human dimensions of both patients and physicians allows questions of human values to regain their stature as integral components of the discourse.

In this short paper, we show that a popular view in information science, information-as-thing, fails to account for a common example of information that seems physical. We then demonstrate how the distinction between types and tokens, recently used to analyse Shannon information, can account for this same example by viewing information as abstract, and discuss existing definitions of information that are consistent with this approach. -/- Dans ce court article nous montrons qu'une vision populaire en sciences de l'information, l'information en (...) tant qu’une chose, échoue à rendre compte d'un exemple commun d'information qui semble physique. Nous démontrons ensuite comment la distinction type/token, utilisée récemment pour analyser l'information de Shannon, peut rendre compte de ce même exemple en considérant l'information comme abstraite, et nous discutons des définitions existantes de l’information qui sont compatibles avec cette approche. (shrink)

The medical record, as a managerial, historic, and legal document, serves many purposes. Although its form may be well established and many of the cases documented in it routine in medical experience, what is written in the medical record nevertheless records decisions and actions of individuals. Viewed as an interpretive text, it can itself become the object of interpretation. This essay applies literary theory and methodology to the structure, content, and writing style(s) of an actual medical record for the purpose (...) of exploring the relationship between the forms and language of medical discourse and the daily decisions surrounding medical treatment. The medical record is shown to document not only the absence of a consistent treatment plan for the patient studied but also a breakdown in communication between different health professionals caring for that patient. The paper raises questions about the kind of education being given to house staff in this instance. The essay concludes with a consideration of how such situations might be more generally avoided. (shrink)

In this paper we give axiom systems for classical and intuitionistic hybrid logic. Our axiom systems can be extended with additional rules corresponding to conditions on the accessibility relation expressed by so-called geometric theories. In the classical case other axiomatisations than ours can be found in the literature but in the intuitionistic case no axiomatisations have been published. We consider plain intuitionistic hybrid logic as well as a hybridized version of the constructive and paraconsistent logic N4.

In this paper various branching time semantics are compared with the aim of clarifying the role of true futures of counterfactual moments, that is, true futures of moments outside the true chronicle. First we give an account of Arthur Prior’s Ockhamistic semantics where truth of a formula is relative to a moment and a chronicle. We prove that this is equivalent to a version of a semantics put forward by Thomason and Gupta where truth is relative to a moment and (...) what is called a chronicle function which assigns a chronicle to each moment. Later we discuss how a semantic theory considered by Belnap and Green may be formalised. It comes about by assuming a chronicle function to be given once and for all. However, this semantics invalidates an intuitively valid formula, so we present an alternative semantics where the formula in question is valid. Furthermore, we shall exhibit an intuitively invalid formula which is invalid in our alternative semantics, but which is valid in Prior’s Ockhamistic semantics. So we can conclude that Prior’s Ockhamistic validity does not imply validity in the alternative semantics. On the other hand, the converse implication does hold, as we shall prove. Summary of mathematical results: We have proved that Prior’s Ockhamistic semantics has the same valid formulas as Thomason and Gupta’s semantics, and we have proved that Prior’s Ockhamistic semantics has strictly more valid formulas than the alternative semantics. (shrink)

BackgroundUndocumented immigrants can donate their organs, but lack access to organ transplantation. This challenges foundational principles of organ donation: fairness and informed consent. Little is known about undocumented immigrants’ knowledge of barriers to their access to organ transplantation or how this might affect their decision to donate their organs.MethodsThe study was performed in an urban, university-affiliated, safety-net hospital. We interviewed hospitalized patients who selfidentified as undocumented immigrants and were unaware of having any contraindication to organ donation (for example, cancer). We (...) first recorded their demographic characteristics and knowledge and attitudes regarding organ donation. We then assessed the effects of informing participants about limits to their access to organ transplants on their willingness to donate.ResultsThis group of 59 uninsured Hispanic immigrants had adequate knowledge about organ donation. Participants were suspicious about inequality within the medical system, but most were willing to donate their organs (74 percent). Most participants (74 percent) were aware that they would have to pay to receive an organ, but they dramatically underestimated the out-of-pocket expenses. Yet willingness to donate their organs was unaffected by participants being explicitly informed of the low likelihood that they would be able to afford to receive an organ transplant.ConclusionsDespite being well informed about the organ donation system, undocumented Hispanic immigrants underestimate the costs and overestimate their likelihood of receiving an organ. Even when they are given this information, they remain willing to donate their own organs. (shrink)

We present an axiom system for basic hybrid logic extended with propositional quantifiers (a second-order extension of basic hybrid logic) and prove its (basic and pure) strong completeness with respect to general models.

In a study involving 62 Danish children with autism spectrum disorder, we obtained results showing that the mastery of linguistic recursion is a significant predictor of success in second-order false belief tasks. The same study also showed that the mastery of linguistic recursion was not significantly correlated with success in a task involving three heavily used Danish discourse particles. This calls for further explanation, as the reasoning involved in both types of tasks seems similar. In this paper, we discuss second-order (...) false belief reasoning, the reasoning underlying the use of the three Danish discourse particles, say what we know about them experimentally, and discuss what they do have in common. (shrink)

This paper is about non-labelled proof-systems for hybrid logic, that is, proofsystems where arbitrary formulas can occur, not just satisfaction statements. We give an overview of such proof-systems, focusing on analytic systems: Natural deduction systems, Gentzen sequent systems and tableau systems. We point out major results and we discuss a couple of striking facts, in particular that nonlabelled hybrid-logical natural deduction systems are analytic, but this is not proved in the usual way via step-by-step normalization of derivations.

A hybrid logic is obtained by adding to an ordinary modal logic further expressive power in the form of a second sort of propositional symbols called nominals and by adding so-called satisfaction operators. In this paper we consider hybridized versions of S5 (“the logic of everywhere”) and the modal logic of inequality (“the logic of elsewhere”). We give natural deduction systems for the logics and we prove functional completeness results.

This is primarily a conceptual paper. The goal of the paper is to put into perspective the proof-theory of hybrid logic and in particular, try to give an answer to the following question: Why does the proof-theory of hybrid logic work so well compared to the proof-theory of ordinary modal logic?Roughly, there are two different kinds of proof systems for modal logic: Systems where the formulas involved in the rules are formulas of the object language, that is, ordinary modal-logical formulas, (...) and systems where the formulas involved in the rules are metalingustic formulas obtained by attaching labels representing possible worlds to ordinary modal-logical formulas. Systems of the second kind often also involve an explicit representation of the accessibility relation. From a proof-theoretic point of view, modal-logical systems of the first kind are less well-behaved than systems of the second kind.It turns out that this can be remedied by hybridization, that is, hybridization of modal logics enables the formulation of well-behaved proof systems without involving metalinguistic machinery. What has happened is that the metalinguistic machinery has been internalized in the object language. This gives an answer to the initial question, which is that the proof-theory of hybrid logic works so well because the metalinguistic semantic machinery has been internalized in the object language. (shrink)

In this paper we define a family of many-valued semantics for hybrid logic, where each semantics is based on a finite Heyting algebra of truth-values. We provide sound and complete tableau systems for these semantics. Moreover, we show how the tableau systems can be made terminating and thereby give rise to decision procedures for the logics in question. Our many-valued hybrid logics turn out to be "intermediate" logics between intuitionistic hybrid logic and classical hybrid logic in a specific sense explained (...) in the paper. Our results show that many-valued hybrid logic is indeed a natural enterprise. (shrink)

In this paper we define a family of many-valued semantics for hybrid logic, where each semantics is based on a finite Heyting algebra of truth-values. We provide sound and complete tableau systems for these semantics. Moreover, we show how the tableau systems can be made terminating and thereby give rise to decision procedures for the logics in question. Our many-valued hybrid logics turn out to be "intermediate" logics between intuitionistic hybrid logic and classical hybrid logic in a specific sense explained (...) in the paper. Our results show that many-valued hybrid logic is indeed a natural enterprise. (shrink)

Each time patients and their families are asked to make a decision about resuscitation, they are also asked to engage the political, social, and cultural concerns that have shaped its history. That history is exemplified in the career of Claude S. Beck, arguably the most influential researcher and teacher of resuscitation in the twentieth century. Careful review of Beck’s work discloses that the development and popularization of the techniques of resuscitation proceeded through a multiplication of definitions of death. CPR consequently (...) remains unique among medical treatments, because it is indicated precisely when a person dies, depending always on how each event of death becomes defined practically by patients, families, and medical professionals present at the time. It is therefore as an occasion to manage a surplus of definitions of death, and not as an occasion to determine the physiological efficacy of resuscitation, that one should approach analysis of contemporary challenges in decision-making about resuscitation. (shrink)