Modal Logic

A brief overview of the system S5 in modal logic as defined by Brian F. Chellas, author of "Modal Logic: An Introduction." The history and usage of modal logic are given mention, along with some applications. Very much a draft. Written for PhileInSophia on July 5, 2021.

Possibility semantics offers an elegant framework for a semantic analysis of modal logic that does not recruit fully determinate entities such as possible worlds. The present papers considers the application of possibility semantics to the modeling of the indeterminacy of the future. Interesting theoretical problems arise in connection to the addition of object-language determinacy operator. We argue that adding a two-dimensional layer to possibility semantics can help solve these problems. The resulting system assigns to the two-dimensional determinacy operator a well-known (...) logic (coinciding with the logic of universal modalities under global consequence). The paper concludes with some preliminary inroads into the question of how to distinguish two-dimensional possibility semantics from the more established branching framework. (shrink)

This essay aims to provide a modal logic for rational intuition. Similarly to treatments of the property of knowledge in epistemic logic, I argue that rational intuition can be codified by a modal operator governed by the modal $\mu$-calculus. Via correspondence results between fixed point modal propositional logic and the bisimulation-invariant fragment of monadic second-order logic, a precise translation can then be provided between the notion of 'intuition-of', i.e., the cognitive phenomenal properties of thoughts, and the modal operators regimenting the (...) notion of 'intuition-that'. I argue that intuition-that can further be shown to entrain conceptual elucidation, by way of figuring as a dynamic-interpretational modality which induces the reinterpretation of both domains of quantification and the intensions and hyperintensions of mathematical concepts that are formalizable in monadic first- and second-order formal languages. Hyperintensionality is countenanced via a topic-sensitive epistemic two-dimensional truthmaker semantics. (shrink)

Cathoristic logic is a multi-modal logic where negation is replaced by a novel operator allowing the expression of incompatible sentences. We present the syntax and semantics of the logic including complete proof rules, and establish a number of results such as compactness, a semantic characterisa- tion of elementary equivalence, the existence of a quadratic-time decision pro- cedure, and Brandom’s incompatibility semantics property. We demonstrate the usefulness of the logic as a language for knowledge representation.

It is often assumed that pluralities are rigid, in the sense of having all and only their actual members necessarily. This assumption is operative in standard approaches to modal plural logic. I argue that a sceptical approach towards the assumption is warranted.

Ontological arguments like those of Gödel (1995) and Pruss (2009; 2012) rely on premises that initially seem plausible, but on closer scrutiny are not. The premises have modal import that is required for the arguments but is not immediately grasped on inspection, and which ultimately undermines the simpler logical intuitions that make the premises seem plausible. Furthermore, the notion of necessity that they involve goes unspecified, and yet must go beyond standard varieties of logical necessity. This leaves us little reason (...) to believe the premises, while their implausible existential import gives us good reason not to. (shrink)

The dogma that the propositional logic of metaphysical modality is S5 is rebutted in related installments (previously published and unpublished essays).

Two definitions of deduction are offered. The first is that deduction is an inference type that is both possibly valid and possibly invalid. No inference can satisfy this definition, because valid inferences are not possibly invalid and invalid inferences are not possibly valid. In the second definition, deduction is understood as an inference that aims for validity. This definition also has unwanted consequences, including the fact that invalid inferences are only deductive when they are thought to be possibly valid. If (...) the only genuine deductions are the valid ones, then our talk about deduction is an indirect and thoughtless way of referring to valid inferences rather than to an inference type. There is simply no deduction to speak off. Only valid inferences. (shrink)

Possible worlds are commonly seen as an interpretation of modal operators such as "possible" and "necessary". Here, we develop possible world semantics (PWS) which can be expressed in basic set theory and first-order logic, thus offering a reductionist account of modality. Specifically, worlds are understood as complete sets of statements and possible worlds are sets whose statements are consistent with a set of conceptual laws. We introduce the construction calculus (CC), a set of axioms and rules for truth, possibility, worldness (...) and consistency. We show that CC allows to prove fundamental theorems about necessity, possibility, impossibility and contigency, thus demonstrating prima-facie plausibility of PWS. Finally, we discuss the explanatory power of our approach and draw connections between our account and established philosophical conceptions of possible worlds. (shrink)

Some central epistemological notions are expressed by sentential operators O that entail the possibility of knowledge in the sense that 'Op' entails 'It is possible to know that p'. We call these modal-epistemological notions. Using apriority and being in a position to know as case studies, we argue that the logics of modal epistemological notions are extremely weak. In particular, their logics are not normal and do not include any closure principles.

This paper is a study of a distinctively chemical notion of possibility. This is the notion of possibility that occurs in chemical discourses when chemists speak of the possibility or impossibility of achieving a given result through chemical means. This notion pertains to the possibility of processes, not of compounds, so it differs from the kind of chemical possibility mentioned in Wittgenstein's Philosophical Investigations or the kinds discussed in the literature on Putnam's Twin Earth argument. I argue that this process-oriented (...) notion of possibility cannot be reduced in a simple way to physical possibility, and that standard possible worlds semantics does not allow a natural analysis of this notion. I suggest an extension of possible worlds semantics that may overcome this limitation. I finish by pointing out some open questions about chemical possibility. (shrink)

Fragmentalism allows incompatible facts to constitute reality in an absolute manner, provided that they fail to obtain together. In recent years, the view has been extensively discussed, with a focus on its formalisation in model-theoretic terms. This paper focuses on three formalisations: Lipman’s approach, the subvaluationist interpretation, and a novel view that has been so far overlooked. The aim of the paper is to explore the application of these formalisations to the alethic modal case. This logical exploration will allow us (...) to study (i) cases of metaphysical incompatibility between modal facts and (ii) cases of modal dialetheias. In turn, this will enrich our understanding of the role of impossibility in the fragmentalist framework. (shrink)

This paper draws attention to a proof of the necessity of identity given by Arthur Prior. In its simplicity, it is comparable to a proof of Quine's, popularised by Kripke, but it is slightly different. Prior's Polish notation is transcribed into a more familiar idiom. Prior's proof is followed by a proof of the necessity of difference, possibly the first such proof in the literature, which is also repeated here and transcribed. The paper concludes with a brief discussion of Prior's (...) views on identity and difference over time. (shrink)

In artificial intelligence (AI), responses generated by machine-learning models (most often large language models) may be unfactual information presented as a fact. For example, a chatbot might state that the Mona Lisa was painted in 1815. Such phenomenon is called AI hallucinations, seeking inspiration from human psychology, with a great difference of AI ones being connected to unjustified beliefs (that is, AI “beliefs”) rather than perceptual failures). -/- AI hallucinations may have their source in the data itself, that is, the (...) source content, or in the training procedure, i.e. the way the knowledge was encoded in the model’s parameters, so that errors in encoding and decoding textual and non-textual representations can cause hallucinations. In this paper, we will observe how such errors come to life and how they might be mitigated. For this purpose, we will analyze the usability of justification logics, to behave as a proof checker for validating the correctness of large language models’ (LLM) responses. Justification logic was developed by S. Artemov, and later on mostly by Artemov and M. Fitting, deriving its main idea from the logic of proofs (LP): knowledge and belief modalities are seen as justification terms, i.e. t:X stands for t is a (proper) justification for X. Justification logic originated from attempts to create semantics for intuitionistic logic where proofs were the most proper justifications, but in further development, justification logic could be applied to different kinds of justifications). With the recent attempts to mitigate incorrect LLM responses, we will analyze various guardrails that are currently used for LLM responses, and see how the logic of justification may provide its benefits as an AI safety layer against false data. (shrink)

In her recent book, Russell (2023) examines various so-called “barriers to entailment,” including Hume’s law, roughly the thesis that an ‘ought’ cannot be derived from an ‘is.’ Hume’s law bears an obvious resemblance to the proscription on fallacies of modality in relevance logic, which has traditionally formally been captured by the so-called Ackermann property. In the context of relevant modal logic, this property might be articulated thus: no conditional whose antecedent is box-free and whose consequent is box-prefixed is valid (for (...) the connection, interpret box deontically). While the deontic significance of Ackermann-like properties has been observed before, Russell’s new book suggests a more broad-scoped formal investigation of the relationship between barrier theses of various kinds and corresponding Ackermann-like properties. In this paper, I undertake such an investigation by elaborating a general relevant bimodal logical framework in which several of the barriers Russell examines can be given formal expression. I then consider various Ackermann-like properties corresponding to these barriers and prove that certain systems satisfy them. Finally, I respond to some objections Russell makes against the use of relevance logic to formulate Hume’s law and related barriers. (shrink)

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency program. Similar efforts continue, but have been (...) expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages. (shrink)

We investigate a recently devised polyhedral semantics for intermediate logics, in which formulas are interpreted in n-dimensional polyhedra. An intermediate logic is polyhedrally complete if it is complete with respect to some class of polyhedra. The first main result of this paper is a necessary and sufficient condition for the polyhedral completeness of a logic. This condition, which we call the Nerve Criterion, is expressed in terms of Alexandrov’s notion of the nerve of a poset. It affords a purely combinatorial (...) characterisation of polyhedrally complete logics. Using the Nerve Criterion we show, easily, that there are continuum many intermediate logics that are not polyhedrally complete but which have the finite model property. We also provide, at considerable combinatorial labour, a countably infinite class of logics axiomatised by the Jankov–Fine formulas of ‘starlike trees’ all of which are polyhedrally complete. The polyhedral completeness theorem for these ‘starlike logics’ is the second main result of this paper. (shrink)

Prior to Kripke’s seminal work on the semantics of modal logic, McKinsey offered an alternative interpretation of the necessity operator, inspired by the Bolzano–Tarski notion of logical truth. According to this interpretation, ‘it is necessary that A’ is true just in case every sentence with the same logical form as A is true. In our paper, we investigate this interpretation of the modal operator, resolving some technical questions, and relating it to the logical interpretation of modality and some views in (...) modal metaphysics. In particular, we present an hitherto unpublished solution to problems 41 and 42 from Friedman’s 102 problems, which uses a different method of proof from the solution presented in the paper of Tadeusz Prucnal. (shrink)

Some philosophers advance the claim that the phenomena of logical omniscience and of the indiscernibility of metaphysical statements, which arise in (certain) interpretations of normal modal logic, provide strong reasons in favour of impossible world approaches. These two specific lines of argument will be presented and discussed in this paper. Contrary to the recent much-held view that the characteristics of these two phenomena provide us with strong reasons to adopt impossible world approaches, the view defended here is that no such (...) ‘knock-down arguments’ do emanate on those grounds. This is not to rule out that there cannot be any other good reasons for assuming impossible world semantics. However, the discussion of a further argument for impossible worlds will suggest that different attempts to argue for them likely present intertwined problems. (shrink)

Rumfitt has given two arguments that in unilateralist verificationist theories of meaning, truth collapses into correct assertibility. In the present paper I give similar arguments that show that in unilateral falsificationist theories of meaning, falsehood collapses into correct deniability. According to bilateralism, meanings are determined by assertion and denial conditions, so the question arises whether it succumbs to similar arguments. I show that this is not the case. The final section considers the question whether a principle central to Rumfitt's first (...) argument, ‘It is assertible that if and only if it is assertible that it is assertible that ’, is one that bilateralists can reject, and concludes that they cannot. It follows that the logic of assertibility and deniability, according to a result by Williamson, is the little known modal logic K4 studied by Sobociński. The paper ends with a plaidoyer for bilateralists to adopt this logic. (shrink)

A consequence relation is strongly classical if it has all the theorems and entailments of classical logic as well as the usual meta-rules (such as Conditional Proof). A consequence relation is weakly classical if it has all the theorems and entailments of classical logic but lacks the usual meta-rules. The most familiar example of a weakly classical consequence relation comes from a simple supervaluational approach to modelling vague language. This approach is formally equivalent to an account of logical consequence according (...) to which α1, ..., αn entails β just in case □α1, ..., □αn entails □β in the modal logic S5. This raises a natural question: If we start with a different underlying modal logic, can we generate a strongly classical logic? This paper explores this question. In particular, it discusses four related technical issues: (1) Which base modal logics generate strongly classical logics and which generate weakly classical logics? (2) Which base logics generate themselves? (3) How can we directly characterize the logic generated from a given base logic? (4) Given a logic that can be generated, which base logics generate it? The answers to these questions have philosophical interest. They can help us to determine whether there is a plausible supervaluational approach to modelling vague language that yields the usual meta-rules. They can also help us to determine the feasibility of other philosophical projects that rely on an analogous formalism, such as the project of defining logical consequence in terms of the preservation of an epistemic status. (shrink)

Este artigo explora o uso de metodologias lúdicas, como gamificação e narrativas, para tornar o ensino de Lógica mais dinâmico e acessível no Ensino Médio. Através de enigmas como os do tipo Cavaleiros e Patifes, abordam-se tanto a lógica proposicional clássica quanto as não-clássicas (notadamente, as lógicas paraconsistentes e modal),proporcionando um aprendizado ativo e colaborativo. O artigo oferece ferramentas práticas para educadores, com ênfase no desenvolvimento de competências críticas e na criação de um ambiente inclusivo, acessível a todos os alunos.

A fundamental question asked in modal logic is whether a given theory is consistent. But consistent with what? A typical way to address this question identifies a choice of background knowledge axioms (say, S4, D, etc.) and then shows the assumptions codified by the theory in question to be consistent with those background axioms. But determining the specific choice and division of background axioms is, at least sometimes, little more than tradition. This paper introduces generic theories for propositional modal logic (...) to address consistency results in a more robust way. As building blocks for background knowledge, generic theories provide a standard for categorical determinations of consistency. We argue that the results and methods of this paper help to elucidate problems in epistemology and enjoy sufficient scope and power to have purchase on problems bearing on modalities in judgement, inference, and decision making. (shrink)

Havstad (2022) argues that the argument from inductive risk for the claim that non-epistemic values have a legitimate role to play in the internal stages of science is deductively valid. She also defends its premises and thus soundness. This is, as far as we are aware, the best reconstruction of the argument from inductive risk in the existing literature. However, there is a small flaw in this reconstruction of the argument from inductive risk which appears to render the argument invalid. (...) This flaw is superficial, and a small amendment to it rescues the claim of validity. (shrink)

O problema lógico do mal é a alegação de que a existência de Deus e a existência de mal no mundo são logicamente inconsistentes. Neste artigo, descrevemos o sistema N3, baseado em partes na contribuição de Nieznański (2007, 2008), que oferece uma resposta ao problema lógico do mal através da refutação de uma versão do determinismo religioso. Argumentamos especificamente que, dados os resultados de N3, a existência de Deus não é contraditória com a do mal, e portanto, o teísmo clássico (...) não pode ser considerado irracional com base no problema lógico do mal. Nossa abordagem pode ser considerada um caso de lógica da religião, ou seja, de lógica aplicada ao discurso religioso. (shrink)

El presente trabajo pretende explicitar que los operadores modales, como construcciones lógicas, insertos en las interpretaciones modales (MI) de la mecánica cuántica son usados de manera informal sin una semántica modal adecuada. Primero se estudiarán en detalle los motivos por los que ninguna lógica cuántica puede ofrecer una base apropiada para formalizar estos operadores en contextos mecánico-cuánticos. A continuación, se presentará el enfoque de las historias cuánticas como una nueva lógica cuántica (NQL) intrínsecamente booleana como posible herramienta para formalizar operadores (...) modales en el contexto de las MI. Tras comentar brevemente las principales MI, se propondrá abordar un estudio de las modalidades presentes en ellas desde esta NQL prestando siempre especial atención al problema de la medida como hilo conductor. Finalmente, se pretende señalar cuáles han de ser los primeros pasos necesarios para ofrecer una exposición lógicamente consistente de las modalidades en contextos cuánticos relevantes con NQL como herramienta, así como señalar las ventajas que esta perspectiva podría llegar a ofrecer. (shrink)

A solid foundation of modal logic requires a clear conception of the notion of modality. Modern modal logic treats modality as a propositional operator. I shall present an alternative according to which modality applies primarily to illocutionary force, that is, to the force, or mood, of a speech act. By a first step of internalization, modality applied at this level is pushed to the level of speech-act content. By a second step of internalization, we reach a propositional operator validating the (...) modal logic S4. After a brief discussion of problematic modality and possibility, the article concludes with an extension of the account that identifies modality with illocutionary force. Throughout, close attention is paid to the intended interpretation of the formalism. All of the rules stipulated will be justified on the basis of this interpretation. (shrink)

In recent years, there has been a growing interest in truthmaker semantics as a framework for understanding a range of phenomena in philosophy and linguistics. Despite this interest, there has been limited study of the various logics that arise from the semantics. This paper aims to address this gap by exploring numerous ‘truthmaker logics’ and proving their compactness and decidability. This is in continuation with the inquiry of Fine and Jago (2019), who proved compactness and decidability for a particular kind (...) of truthmaker logic. The key results going into this are (1) ‘standard translations’ into first-order logic; (2) a truthmaker analogue of the finite model property; and (3) a proof showing that truthmaker consequence on semilattices coincides with truthmaker consequence on complete lattices. Finally, the connection with modal logic is examined. Specifically, it is illustrated how endowing truthmaker semantics with classical negation results in modal information logics. (shrink)

We present a new puzzle about logical truth, necessity, and moral responsibility. We defend one solution to the puzzle. A corollary of our preferred solution is that prominent arguments for the incompatibility of determinism and moral responsibility are invalid.

Sorensen (1992) has provided two modal-logical schemas to reconstruct the logical structure of two types of destructive thought experiments: the Necessity Refuter and the Possibility Refuter. The schemas consist of five propositions which Sorensen claims but does not prove to be inconsistent.We show that the five propositions, as presented by Sorensen, are not inconsistent, but by adding a premise (and a logical truth), we prove that the resulting sextet of premises is inconsistent. Häggqvist (2009) has provided a different modal-logical schema (...) (Counterfactual Refuter), which is equivalent to four premises, again claimed to be inconsistent. We show that this schema also is not inconsistent, for similar reasons. Again, we add another premise to achieve inconsistency. The conclusion is that all three modal-logical reconstructions of the arguments that accompany thought experiments, two by Sorensen and one by Häggqvist, have now been made rigorously correct. This may inaugurate new avenues to respond to destructive thought experiments. (shrink)

This essay considers Kant’s theory of modality in light of a debate in contemporary modal metaphysics and modal logic concerning the Barcan formulas. The comparison provides a new and fruitful perspective on Kant’s complex and sometimes confusing claims about possibility and necessity. Two central Kantian principles provide the starting point for the comparison: that the possible must be grounded in the actual and that existence is not a real predicate. Both are shown to be intimately connected to the Barcan formulas, (...) and Kant’s views on what he distinguishes as three different kinds of modality are then considered in light of this connection. (shrink)

We develop a theory of necessity operators within a version of higher-order logic that is neutral about how fine-grained reality is. The theory is axiomatized in terms of the primitive of *being a necessity*, and we show how the central notions in the philosophy of modality can be recovered from it. Various questions are formulated and settled within the framework, including questions about the ordering of necessities under strength, the existence of broadest necessities satisfying various logical conditions, and questions about (...) their logical behaviour. We also wield the framework to probe the conditions under which a logicist account of necessities is possible, in which the theory is completely reducible to logic. (shrink)

Upward monotonic semantics for necessity modals give rise to Ross’s Puzzle: they predict that □φ entails □(φ ∨ ψ), but common intuitions about arguments of this form suggest they are invalid. It is widely assumed that the intuitive judgments involved in Ross’s Puzzle can be explained in terms of the licensing of ‘Diversity’ inferences: from □(φ ∨ ψ), interpreters infer that the truth of each disjunct (φ, ψ) is compatible with the relevant set of worlds. I introduce two pieces of (...) data that this analysis fails to explain. Analyzing this data, I argue, suggests that necessity modals with embedded disjunctions license ‘Independence’ inferences: from the truth of □(φ ∨ ψ), interpreters infer that φ-without-ψ and ψ-without-φ are each compatible with the relevant set of worlds. I outline a bilateral inquisitive semantics for necessity modals that predicts the validity of the Independence inferences. I then argue that the resulting theory should be understood as one on which disjunctions denote pluralities of propositions, and necessity modals behave like collective predicates applied to these pluralities. (shrink)

One of the most expected properties of a logical system is that it can be algebraizable, in the sense that an algebraic counterpart of the deductive machinery could be found. Since the inception of da Costa's paraconsistent calculi, an algebraic equivalent for such systems have been searched. It is known that these systems are non self-extensional (i.e., they do not satisfy the replacement property). More than this, they are not algebraizable in the sense of Blok-Pigozzi. The same negative results hold (...) for several systems of the hierarchy of paraconsistent logics known as Logics of Formal Inconsistency (LFIs). Because of this, these logics are uniquely characterized by semantics of non-deterministic kind. This paper offers a solution for two open problems in the domain of paraconsistency, in particular connected to algebraization of LFIs, by obtaining several LFIs weaker than C1, each of one is algebraizable in the standard Lindenbaum-Tarski's sense by a suitable variety of Boolean algebras extended with operators. This means that such LFIs satisfy the replacement property. The weakest LFI satisfying replacement presented here is called RmbC, which is obtained from the basic LFI called mbC. Some axiomatic extensions of RmbC are also studied, and in addition a neighborhood semantics is defined for such systems. It is shown that RmbC can be defined within the minimal bimodal non-normal logic E+E defined by the fusion of the non-normal modal logic E with itself. Finally, the framework is extended to first-order languages. RQmbC, the quantified extension of RmbC, is shown to be sound and complete w.r.t. BALFI semantics. (shrink)

Jaakko Hintikka proposed treating objectual perception sentences, such as “Alice sees Bob,” as de re propositional perception sentences. Esa Saarinen extended Hintikka’s idea to eventive perception sentences, such as “Alice sees Bob smile.” These approaches, elegant as they may be, are not philosophically neutral, for they presuppose, controversially, that the content of all perceptual experiences is propositional in nature. The aim of this paper is to propose a formal treatment of objectual and eventive perception sentences that builds on Hintikka’s modal (...) approach to propositional attitude ascriptions while avoiding controversial assumptions on the nature of perceptual experiences. Despite being simple and theoretically frugal, our approach is powerful enough to express a variety of interesting philosophical views about propositional, objectual, and eventive perception sentences, thus enabling the study of their inferential relationships. (shrink)

We present epistemic multilateral logic, a general logical framework for reasoning involving epistemic modality. Standard bilateral systems use propositional formulae marked with signs for assertion and rejection. Epistemic multilateral logic extends standard bilateral systems with a sign for the speech act of weak assertion (Incurvati and Schlöder 2019) and an operator for epistemic modality. We prove that epistemic multilateral logic is sound and complete with respect to the modal logic S5 modulo an appropriate translation. The logical framework developed provides the (...) basis for a novel, proof-theoretic approach to the study of epistemic modality. To demonstrate the fruitfulness of the approach, we show how the framework allows us to reconcile classical logic with the contradictoriness of so-called Yalcin sentences and to distinguish between various inference patterns on the basis of the epistemic properties they preserve. (shrink)

This paper investigates and develops generalizations of two-dimensional modal logics to any finite dimension. These logics are natural extensions of multidimensional systems known from the literature on logics for a priori knowledge. We prove a completeness theorem for propositional n-dimensional modal logics and show them to be decidable by means of a systematic tableau construction.

It is a widely held principle that no one is able to do something that would require the past to have been different from how it actually is. This principle of the fixity of the past has been presented in numerous ways, playing a crucial role in arguments for logical and theological fatalism, and for the incompatibility of causal determinism and the ability to do otherwise. I will argue that, assuming bivalence, this principle is in conflict with standard views about (...) knowledge and the semantics for ‘actually’. I also consider many possible responses to the argument. (shrink)

Rosenkranz (2021) devised two bimodal epistemic logics: an idealized one and a realistic one. The former is shown to be sound with respect to a class of neighborhood frames called i-frames. Rosenkranz designed a specific i-frame able to invalidate a series of undesired formulas, proving that these are not theorems of the idealized logic. Nonetheless, an unwanted formula and an unwanted rule of inference are not invalidated. Invalidating the former guarantees the distinction between the two modal operators characteristic of the (...) logic, while invalidating the latter is crucial in order to deal with the problem of logical omniscience. In this paper, I present an i-frame able to invalidate all the undesired formulas already invalidated by Rosenkranz, together with the missing formula and rule of inference. (shrink)

This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell, but the system, based on a different choice of axioms, is better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only primitive logical (...) connectives and necessity as the only primitive modal operator. The full source code is available online and has been typechecked with Lean 3.4.2. (shrink)

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)

This paper looks at dialectical inferences as they relate to Hegel’s modal metaphysics, closely examining the Actuality section of Hegel’s Science of Logic and positing a reading of Hegel’s modal actualism that engages with two strains of secondary commentary. Responding to commentators, we make the case that Hegel’s ‘das Logische’ avoids presupposing possibility’s being prior to actuality insofar as actuality and the derivation of possibility is considered as the in-itselfness of actuality, an implicit inner moment whereby actuality further determines itself. (...) Actuality is immediate yet derived as an identity from the logic of inner and outer. If actuality as immediacy is explicit/outer, then its opposition, its implicitness/innerness, has to be possibility in the logic of modality. In order to conceive of actuality as existence, and particularly as an emerging process, we must already conceive the problem of presupposing an alien form within the logic of actuality. (shrink)

En este artículo presentamos una posible vía para interpretar las nociones de posibilidad y necesidad desarrolladas en el seno de la lógica megárico-estoica como operadores modales aléticos. Se introducirá la semántica megárico-estoica como trasfondo metafísico de las definiciones de necesidad y posibilidad y se ofrecerán argumentos para abandonar las interpretaciones predominantes que incluyen variables temporales ad hoc. Tras proponer la lectura de las definiciones diodóricas desde una semántica modal relacional se señalará una serie de temas que merecen ser revisitados desde (...) esta óptica. (shrink)

This paper and its sequel “look under the hood” of the usual sorts of proof-theoretic systems for certain well-known intuitionistic and classical propositional modal logics. Section 1 is preliminary. Of most importance: a marked formula will be the result of prefixing a formula in a propositional modal language with a step-marker, for this paper either 0 or 1. Think of 1 as indicating the taking of “one step away from 0.” Deductions will be constructed using marked formulas. Section 2 presents (...) the model-theoretic concepts, based on those in [7], that guide the rest of this paper. Section 3 presents Natural Deduction systems IK and CK, formalizations of intuitionistic and classical one-step versions of K. In these systems, occurrences of step-markers allow deductions to display deductive structure that is covered over in familiar “no step” proof-theoretic systems for such logics. Box and Diamond are governed by Introduction and Elimination rules; the familiar K rule and Necessitation are derived (i.e. admissible) rules. CK will be the result of adding the 0-version of the Rule of Excluded Middle to the rules which generate IK. Note: IK is the result of merely dropping that rule from those generating CK, without addition of further rules or axioms (as was needed in [7]). These proof-theoretic systems yield intuitionistic and classical consequence relations by the obvious definition. Section 4 provides some examples of what can be deduced in IK. Section 5 defines some proof-theoretic concepts that are used in Section 6 to prove the soundness of the consequence relation for IK (relative to the class of models defined in Section 2.) Section 7 proves its completeness (relative to that class). Section 8 extends these results to the consequence relation for CK. (Looking ahead: Part 2 will investigate one-step proof-theoretic systems formalizing intuitionistic and classical one-step versions of some familiar logics stronger than K.). (shrink)

Many classically valid meta-inferences fail in a standard supervaluationist framework. This allegedly prevents supervaluationism from offering an account of good deductive reasoning. We provide a proof system for supervaluationist logic which includes supervaluationistically acceptable versions of the classical meta-inferences. The proof system emerges naturally by thinking of truth as licensing assertion, falsity as licensing negative assertion and lack of truth-value as licensing rejection and weak assertion. Moreover, the proof system respects well-known criteria for the admissibility of inference rules. Thus, supervaluationists (...) can provide an account of good deductive reasoning. Our proof system moreover brings to light how one can revise the standard supervaluationist framework to make room for higher-order vagueness. We prove that the resulting logic is sound and complete with respect to the consequence relation that preserves truth in a model of the non-normal modal logic _NT_. Finally, we extend our approach to a first-order setting and show that supervaluationism can treat vagueness in the same way at every order. The failure of conditional proof and other meta-inferences is a crucial ingredient in this treatment and hence should be embraced, not lamented. (shrink)

Hardcore actualism (HA) grounds all modal truths in the concrete constituents of the actual world (see, e.g., Borghini and Williams (2008), Jacobs (2010), Vetter (2015)). I bolster HA, and elucidate the very nature of possibility (and necessity) according to HA, by considering if it can validate S5 modal logic. Interestingly, different considerations pull in different directions on this issue. To resolve the tension, we are forced to think hard about the nature of the hardcore actualist's modal reality and how radically (...) this departs from possible worlds orthodoxy. Once we achieve this departure, the prospects of a hardcore actualist validation of S5 look considerably brighter. This paper thus strengthens hardcore actualism by arguing that it can indeed validate S5–arguably the most popular logic of metaphysical modality–and, in the process, it elucidates the very nature of modality according to this revisionary, but very attractive, modal metaphysics. (shrink)

We employ a recently developed methodology -- called "structural refinement" -- to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are parameterized with formal grammars, (...) and which encode certain frame conditions expressible as first-order Horn formulae that correspond to a subclass of the Scott-Lemmon axioms. We show that our nested systems are sound, cut-free complete, and admit hp-admissibility of typical structural rules. (shrink)

This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates the (...) semantics of the associated logic, and such systems typically violate the subformula property to a high degree. By contrast, nested sequent calculi employ a simpler syntax and adhere to a strict reading of the subformula property, making such systems useful in the design of automated reasoning algorithms. However, the downside of the nested sequent paradigm is that a general theory concerning the automated construction of such calculi (as in the labelled setting) is essentially absent, meaning that the construction of nested systems and the confirmation of their properties is usually done on a case-by-case basis. The refinement method connects both paradigms in a fruitful way, by transforming labelled systems into nested (or, refined labelled) systems with the properties of the former preserved throughout the transformation process. To demonstrate the method of refinement and some of its applications, we consider grammar logics, first-order intuitionistic logics, and deontic STIT logics. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics. Furthermore, we employ our refined labelled calculi for grammar logics to show that every logic in the class possesses the effective Lyndon interpolation property. (shrink)