We present a cut-admissible system for the modal logic S5 in a formalism that makes explicit and intensive use of deep inference. Deep inference is induced by the methods applied so far in conceptually pure systems for this logic. The system enjoys systematicity and modularity, two important properties that should be satisfied by modal systems. Furthermore, it enjoys a simple and direct design: the rules are few and the modal rules are in exact correspondence to the modal axioms.

There are logics where necessity is defined by means of a given identity connective: \ is a tautology). On the other hand, in many standard modal logics the concept of propositional identity \ can be defined by strict equivalence \}\). All these approaches to modality involve a principle that we call the Collapse Axiom : “There is only one necessary proposition.” In this paper, we consider a notion of PI which relies on the identity axioms of Suszko’s non-Fregean logic SCI. (...) Then S3 proves to be the smallest Lewis modal system where PI can be defined as SE. We extend S3 to a non-Fregean logic with propositional quantifiers such that necessity and PI are integrated as non-interdefinable concepts. CA is not valid and PI refines SE. Models are expansions of SCI-models. We show that SCI-models are Boolean prealgebras, and vice-versa. This associates non-Fregean logic with research on Hyperintensional Semantics. PI equals SE iff models are Boolean algebras and CA holds. A representation result establishes a connection to Fine’s approach to propositional quantifiers and shows that our theories are conservative extensions of S3–S5, respectively. If we exclude the Barcan formula and a related axiom, then the resulting systems are still complete w.r.t. a simpler denotational semantics. (shrink)

It is known that a theory in S5‐epistemic logic with several agents may have numerous models. This is because each such model specifies also what an agent knows about infinite intersections of events, while the expressive power of the logic is limited to finite conjunctions of formulas. We show that this asymmetry between syntax and semantics persists also when infinite conjunctions (up to some given cardinality) are permitted in the language. We develop a strengthened S5‐axiomatic system for such infinitary (...) logics, and prove a strong completeness theorem for them. Then we show that in every such logic there is always a theory with more than one model. (shrink)

Il s’agit d’une methode qui permet d’associer à chaque formule bien formée du système S5 de logique modale un nombre naturel invariant pour toutes les formules qui appartiennent a la même classe d’equivalence que la première.En particulier, étant donné que la méthode associe à toutes les tautologies du système le nombre o et a toutes les contradictions du système un certain nombre Φ, il suffit de calculer le nombre qui, en vertu des associations fondamentales, reste associé à n’importe quelle formule (...) pour décider si cette dernière est tautologique, contradictoire ou contingente.Les relations logiques reliant deux formules du systeme -par exemple, des implications, des incompatibilités, des oppositions contradictaires, etc.- sont révéciés par un simpIe examen oculaire des nombres assoc iés aux formules données et une rapide vérification manuelle ou informatique fondée sur la comparaison des chiffres du même rang de ces nombres, écrits en hexadécimal.Finalement, l’analyse de la composition binaire du nombre associé a une formule donnée permet d’obtenir l’expression de la première sous sa forme normale conjonctive.La méthode décrite constitue donc une nouvelle méthode arithmétique de décision pour le système modal indiqué. (shrink)

In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). -/- The sequent derivations and proofnets are both simple extensions of sequents and proofnets for classical propositional logic, in which the new machinery—to take account of the modal vocabulary—is directly (...) motivated in terms of the simple, universal Kripke semantics for S5. The sequent system is cut-free and the circuit proofs are normalising. (shrink)

The numerous modal systems between S4 and S5 are investigated from an epistemological point of view by interpreting necessity either as knowledge or as (strong) belief. It is shown that-granted some assumptions about epistemic logic for which the author has argued elsewhere-the system S4.4 may be interpreted as the logic of true belief, while S4.3.2 and S4.2 may be taken to represent epistemic logic systems for individuals who accept the scheme knowledge = true belief only for certain special instances. (...) There is strong evidence in favor of the assumption that S4.2 is the logic of knowledge. (shrink)

Abstract: I argue that the solution to the Red Hat Problem, a puzzle derived from interactive epistemic logic, requires S5. Interactive epis- temic logic is set out in formal terms, and an attempt to solve the red hat puzzle is made in K, K, and K, each of which fails, showing that a stronger system, K is required.

Natural deduction systems for classical, intuitionistic and modal logics were deeply investigated by Prawitz [D. Prawitz, Natural Deduction: A Proof-theoretical Study, in: Stockholm Studies in Philosophy, vol. 3, Almqvist and Wiksell, Stockholm, 1965. Reprinted at: Dover Publications, Dover Books on Mathematics, 2006] from a proof-theoretical perspective. Prawitz proved weak normalization for classical logic only for a language without logical or, there exists and with a restricted application of reduction ad absurdum. Reduction steps related to logical or, there exists and classical (...) negation bring about many problems solved only rather recently. For classical S5 modal logic, Prawitz defined a normalizable system, but for a language without logical or, there exists, ◊ and, for a propositional language without ◊, Medeiros [M.da P.N. Medeiros, A new S4 classical modal logic in natural deduction, Journal of Symbolic Logic 71 799–809] presented a normalizable system for classical S4. We can mention many cut-free Gentzen systems for S4, S5 and K45/K45D, some normalizable natural deduction systems for intuitionistic modal logics and one more for full classical S4, but not for full classical S5. Here our focus is on the definition of a classical and normalizable natural deduction system for S5, taking not only □ and ◊ as primitive symbols, but also all connectives and quantifiers, including classical negation, disjunction and the existential quantifier. The normalization procedure is based on the strategy proposed by Massi [C.D.B. Massi, Provas de normalizaçaõ para a lógica clássica, Ph.D. Thesis, Departamento de Filosofia, UNICAMP, Campinas, 1990] and Pereira and Massi [L.C. Pereira, C.D.B. Massi, Normalização para a lógica clássica, in: O que nos faz pensar, Cadernos de Filosofia da PUC-RJ, vol. 2, 1990, pp. 49–53] for first-order classical logic to cope with the combined use of classical negation, disjunction and the existential quantifier. Here we extend such results to deal with □ and ◊ too. The elimination rule for ◊ uses the notions of connection and of essentially modal formulas already proposed by Prawitz for the introduction of □. Beyond weak normalization, we also prove the subformula property for full S5. (shrink)

This paper is mostly about the role of modal system S5 in conceivability arguments against, as well as in the defense of, different versions of physicalism. Jonathon VandenHombergh argued in a recent article that “[s]o far as the modal epistemology of reduction is concerned, therefore, it pays to go intrinsic.” His reasoning is that while the weaker, extrinsic version of reductive physicalism is vulnerable to conceivability arguments, the stronger, intrinsic, version is uniquely resistant to this type of challenge. To (...) get to this surprising conclusion, VandenHombergh claims that the standard strategies of preempting the Dualist’s reasoning rely on some premise(s) that the Dualist can do without: one such premise is axiom-scheme S5. I will argue that the use of S5 is legitimate in countering the Dualist, as she herself relies on it, not to secure the _validity_ of her arguments as VandenHombergh assumes, but rather, its _soundness_. I will also argue that this axiom-scheme is tacitly present in the auxiliary premises the stronger, intrinsic version of physicalism relies on: Kripke’s postulates about identity and non-identity statements. Indeed, this paper will forge an interesting and potentially important connection between Kripke’s postulates and modal system S5. (shrink)

The topological semantics for modal logic interprets a standard modal propositional language in topological spaces rather than Kripke frames: the most general logic of topological spaces becomes S4. But other modal logics can be given a topological semantics by restricting attention to subclasses of topological spaces: in particular, S5 is logic of the class of almost discrete topological spaces, and also of trivial topological spaces. Dynamic Topological Logic interprets a modal language enriched with two unary temporal connectives, next and henceforth. (...) DTL interprets the extended language in dynamic topological systems: a DTS is a topological space together with a continuous function used to interpret the temporal connectives. In this paper, we axiomatize four conservative extensions of S5, and show them to be the logic of continuous functions on almost discrete spaces, of homeomorphisms on almost discrete spaces, of continuous functions on trivial spaces and of homeomorphisms on trivial spaces. (shrink)

In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC (...) but with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form. (shrink)

Falsification-aware (hyper)sequent calculi and Kripke semantics for normal modal logics including S4 and S5 are introduced and investigated in this study. These calculi and semantics are constructed based on the idea of a falsification-aware framework for Nelson’s constructive three-valued logic. The cut-elimination and completeness theorems for the proposed calculi and semantics are proved.

In this paper, we present a simple sequent calculus for the modal propositional logic S5. We prove that this sequent calculus is theoremwise equivalent to the Hilbert-style system S5, that it is contraction-free and cut-free, and finally that it is decidable. All results are proved in a purely syntactic way.

This paper studies proof systems for the logics of super-strict implication ST2–ST5, which correspond to C.I. Lewis’ systems S2–S5 freed of paradoxes of strict implication. First, Hilbert-style axiomatic systems are introduced and shown to be sound and complete by simulating STn in Sn and backsimulating Sn in STn, respectively(for n=2,...,5). Next, G3-style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are distinctive of G3-style calculi, that they are sound and complete, and (...) it is shown that the proof search for G3. ST2 is terminating and therefore the logic is decidable. (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 recapitulate (Section 1) some basic details of the system of implicative BCSK logic, which has two primitive binary implicational connectives, and which can be viewed as a certain fragment of the modal logic S5. From this modal perspective we review (Section 2) some results according to which the pure sublogic in either of these connectives (i.e., each considered without the other) is an exact replica of the material implication fragment of classical propositional logic. In Sections 3 and 5 (...) we show that for the pure logic of one of these implicational connectives two – in general distinct – consequence relations (global and local) definable in the Kripke semantics for modal logic turn out to coincide, though this is not so for the pure logic of the other connective, and that there is an intimate relation between formulas constructed by means of the former connective and the local consequence relation. (Corollary 5.8. This, as we show in an Appendix, is connected to the fact that the ‘propositional operations’ associated with both of our implicational connectives are close to being what R. Quackenbush has called pattern functions.) Between these discussions Section 4 examines some of the replacement-of-equivalents properties of the two connectives, relative to these consequence relations, and Section 6 closes with some observations about the metaphor of identical twins as applied to such pairs of connectives. (shrink)

This paper studies proof systems for the logics of super-strict implication \(\textsf{ST2}\) – \(\textsf{ST5}\), which correspond to C.I. Lewis’ systems \(\textsf{S2}\) – \(\textsf{S5}\) freed of paradoxes of strict implication. First, Hilbert-style axiomatic systems are introduced and shown to be sound and complete by simulating \(\textsf{STn}\) in \(\textsf{Sn}\) and backsimulating \(\textsf{Sn}\) in \(\textsf{STn}\), respectively (for \({\textsf{n}} =2, \ldots, 5\) ). Next, \(\textsf{G3}\) -style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are distinctive (...) of \(\textsf{G3}\) -style calculi, that they are sound and complete, and it is shown that the proof search for \(\mathsf {G3.ST2}\) is terminating and therefore the logic is decidable. (shrink)

We prove that every normal extension of the bi-modal system S52 is finitely axiomatizable and that every proper normal extension has NP-complete satisfiability problem.

We show that every proper normal extension of the bi-modal system S5 2 has the poly-size model property. In fact, to every proper normal extension L of S5 2 corresponds a natural number b(L) - the bound of L. For every L, there exists a polynomial P(·) of degree b(L) + 1 such that every L-consistent formula is satisfiable on an L-frame whose universe is bounded by P(||), where || denotes the number of subformulas of . It is shown (...) that this bound is optimal. (shrink)

We prove that every normal extension of the bi-modal system S52 is finitely axiomatizable and that every proper normal extension has NP-complete satisfiability problem.

The sentential calculus SC of Kalish and Montague is extended to modal sentences. Rules of inference and a derivation procedure are added. The resultant natural deduction system SMC is like a system for S4 due to Fitch, but SMC is for S5 and the restriction on necessity derivation concerns.terminations of such derivations whereas the restriction on strict subordinate proof in Fitch's system concerns the line-by-line development of such proofs. An axiomatic system AxMC for S5 founded on (...) SC is presented and it is shown that SMC and AxMC are equivalent : what ever is derivable in one system is derivable in the other. (shrink)

The purpose of this work is to present Gentzen-style formulations of S5 and S4 based on sequents of higher levels. Sequents of level 1 are like ordinary sequents, sequents of level 1 have collections of sequents of level 1 on the left and right of the turnstile, etc. Rules for modal constants involve sequents of level 2, whereas rules for customary logical constants of first-order logic with identity involve only sequents of level 1. A restriction on Thinning on the right (...) of level 2, which when applied to Thinning on the right of level 1 produces intuitionistic out of classical logic (without changing anything else), produces S4 out of S5 (without changing anything else). This characterization of modal constants with sequents of level 2 is unique in the following sense. If constants which differ only graphically are given a formally identical characterization, they can be shown inter-replaceable (not only uniformly) with the original constants salva provability. Customary characterizations of modal constants with sequents of level 1, as well as characterizations in Hilbert-style axiomatizations, are not unique in this sense. This parallels the case with implication, which is not uniquely characterized in Hilbert-style axiomatizations, but can be uniquely characterized with sequents of level 1. These results bear upon theories of philosophical logic which attempt to characterize logical constants syntactically. They also provide an illustration of how alternative logics differ only in their structural rules, whereas their rules for logical constants are identical. (shrink)

We show that every proper normal extension of the bi-modal system S52 has the poly-size model property. In fact, to every proper normal extension L of S52 corresponds a natural number b(L) - the bound of L. For every L, there exists a polynomial P(·) of degree b(L) + 1 such that every L-consistent formula ϕ is satisfiable on an L-frame whose universe is bounded by P(|ϕ|), where |ϕ| denotes the number of subformulas of ϕ. It is shown that (...) this bound is optimal. (shrink)

1. It is a fact that developing a good proof theory for modal logics is a difficult task. The problem is not in having deductive systems. In fact, all the main modal logics enjoy an axiomatic prese...

Sentences about logic are often used to show that certain embedding expressions, including attitude verbs, conditionals, and epistemic modals, are hyperintensional. Yet it not clear how to regiment “logic talk” in the object language so that it can be compositionally embedded under such expressions. This paper does two things. First, it argues against a standard account of logic talk, viz., the impossible worlds semantics. It is shown that this semantics does not easily extend to a language with propositional quantifiers, which (...) are necessary for regimenting some logic talk. Second, it develops an alternative framework based on logical expressivism, which explains logic talk using shifting conventions. When combined with the standard S5π+ semantics for propositional quantifiers, this framework results in a well-behaved system that does not face the problems of the impossible worlds semantics. It can also be naturally extended with hybrid operators to regiment a broader range of logic talk, e.g., claims about what laws hold according to other logics. The resulting system, called hyperlogic, is therefore a better framework for modeling logic talk than previous accounts. (shrink)

Trying to overcome Dugundji’s result on uncharacterisability of modal logics by finite logical matrices, Kearns and Ivlev proposed, independently, a characterisation of some modal systems by means of four-valued multivalued truth-functions , as an alternative to Kripke semantics. This constitutes an antecedent of the non-deterministic matrices introduced by Avron and Lev . In this paper we propose a reconstruction of Kearns’s and Ivlev’s results in a uniform way, obtaining an extension to another modal systems. The first part of the paper (...) is devoted to four-valued Nmatrices, including Kearns’s and Ivlev’s. Besides proving with full details Kearns’s results for T, S4 and S5, we also obtain a characterisation of the system B by four-valued Nmatrices with level valuations. Concerning Ivlev’s results, two new modal systems are introduced and char.. (shrink)

In the late forties, Stanisław Jaśkowski published two papers onthe discursive sentential calculus, D2. He provided a definition of it by an interpretation in the language of S5 of Lewis. The knownaxiomatization of D2 with discursive connectives as primitives was introduced by da Costa, Dubikajtis and Kotas in 1977. It turns out, however,that one of the axioms they used is not a thesis of the real Jaśkowski’s calculus. In fact, they built a new system, D∗2 for short, that differs (...) from D2 inmany respects. The aim of this paper is to introduce a direct Kripke-type semantics for the system, axiomatize it in a new way and prove soundness andcompleteness theorems. Additionally, we present labelled tableaux for D∗2.1. (shrink)

In [2] we have presented sequent formulations of the modal logics S5 and S4 based on sequents of higher levels: sequents of level 1 are like ordinary sequents, sequents of level 2 have collections of sequents of level 1 on the left and right of the turnstile, etc. The rules we gave for modal constants involved sequents of level 2, whereas rules for other customary logical constants of first–order logic involved only sequents of level 1. Here we show starting from (...) the same sequent rules of higher level we can obtain sequent formulations of intuitionistic analogues of S5 and S4. We presuppose for this paper an acquaintance with [2]. (shrink)

In Symbolic Logic (1932), C. I. Lewis developed five modal systems S1 − S5. S4 and S5 are so-called normal modal systems. Since Lewis and Langford’s pioneering work many other systems of this kind have been investigated, among them the 32 systems that can be generated by the five axioms T, D, B, 4 and 5. Lewis also discusses how his systems can be augmented by propositional quantifiers and how these augmented logics allow us to express some interesting ideas that (...) cannot be expressed in the corresponding quantifier-free logics. In this paper, I will develop 64 normal modal semantic tableau systems that can be extended by propositional quantifiers yielding 64 extended systems. All in all, we will investigate 128 different systems. I will show how these systems can be used to prove some interesting theorems and I will discuss Lewis’s so-called existence postulate and some of its consequences. Finally, I will prove that all normal modal systems are sound and complete and that all systems (including the extended systems) are sound with respect to their semantics. It is left as an open question whether or not the extended systems are complete. (shrink)

The system obtained by adding full propositional quantification to S5 is known to be decidable, while that obtained by doing so for T is known to be recursively intertranslatable with full second-order logic. Recently it was shown that the system with two S5 operators and full propositional quantification is also recursively intertranslatable with second-order logic. This note establishes that the map assigning [1][2]p to \squarep provides a validity and satisfaction preserving translation between the T system and the (...) double S5 system, thus providing an easier proof of the recent result. (shrink)

In his "Access Denied to Zombies", Gualtiero Piccinini argues that the possibility of zombies does not entail the falsity of physicalism, since the accessibility relation can be understood so that even in S5 system for modal logic worlds inaccessible from our world are allowed (in the case in which the accessibility relation is understood as an equivalence rather than as universal accessibility). According to Piccinini, whether the zombie world is accessible from our world depends on whether physicalism is true (...) in our world, which is something that cannot be answered in a non-question-begging way. In order to show this, he recalls a well known strategy of making a parody of the zombie argument. After pointing out that Piccinini's strategy of parodying the zombie argument renders his former strategy, based on the distinguishing between the two notions of accessibility, redundant, I recall the two ways of handling parodies of the zombie argument. In addition, I argue that persisting on the distinction between accessibility understood as an equivalence and universal accessibility in dealing with the zombie argument relies upon accepting modal dualism (a view that there are two spaces of possibilities rather than one), which is something usually dismissed for methodological reasons (simplicity in particular). Given that Piccinini has not provided new arguments neither in favour of modal dualism nor in favour of parodying the zombie argument, the conclusion he infers remains unsupported by the premises he uses. (shrink)

This article is a presentation of Plantinga’s ontological argument in its historical and systematical frames. Criticisms of the argument are presented as well. Philosophical claims underlying the defense of the argument are described as minimalist, but their connection with a strong logical system is noted.

Monoidal t-norm based logic $\mathbf {MTL}$ is the weakest t-norm based residuated fuzzy logic, which is a $[0,1]$ -valued propositional logical system having a t-norm and its residuum as truth function for conjunction and implication. Monadic fuzzy predicate logic $\mathbf {mMTL\forall }$ that consists of the formulas with unary predicates and just one object variable, is the monadic fragment of fuzzy predicate logic $\mathbf {MTL\forall }$, which is indeed the predicate version of monoidal t-norm based logic $\mathbf {MTL}$. The (...) main aim of this paper is to give an algebraic proof of the completeness theorem for monadic fuzzy predicate logic $\mathbf {mMTL\forall }$ and some of its axiomatic extensions. Firstly, we survey the axiomatic system of monadic algebras for t-norm based residuated fuzzy logic and amend some of them, thus showing that the relationships for these monadic algebras completely inherit those for corresponding algebras. Subsequently, using the equivalence between monadic fuzzy predicate logic $\mathbf {mMTL\forall }$ and S5-like fuzzy modal logic $\mathbf {S5(MTL)}$, we prove that the variety of monadic MTL-algebras is actually the equivalent algebraic semantics of the logic $\mathbf {mMTL\forall }$, giving an algebraic proof of the completeness theorem for this logic via functional monadic MTL-algebras. Finally, we further obtain the completeness theorem of some axiomatic extensions for the logic $\mathbf {mMTL\forall }$, and thus give a major application, namely, proving the strong completeness theorem for monadic fuzzy predicate logic based on involutive monoidal t-norm logic $\mathbf {mIMTL\forall }$ via functional representation of finitely subdirectly irreducible monadic IMTL-algebras. (shrink)

Formal systems seem to come in two general kinds: useful and useless. This is painting things starkly, but the point is important. Formal structures can either be used in interesting and important ways, or they can languish unused and irrelevant. Lewis' modal logics are good examples. The systems S4 and S5 are useful in many different ways. They map out structures that are relevant to a number of different applications. S1, S2 and S3 however, are not so lucky. They are (...) little studied, and used even less. It has become dear that the structures described by S4 and S5 are important in different ways, while the structures described by S1 to S3 are not so important. In this paper, we will see another formal system with a number of different uses. We will examine a substructural logic which is important in a number of different ways. The logic of Peirce monoids, inspired by the logic of relations, is useful in the independent areas of linguistic types and information flow.In what follows I will describe the logic of Peirce monoids in its various guises, sketch out its main properties, and indicate why it is important. As proofs of theorems are readily available elsewhere in the literature, I simply sketch the relevant proofs here, and point the interested reader to where complete proofs can be found. (shrink)

What formulas are tense-logically valid depends on the structure of time, for example on whether it has a beginning. Logicians have investigated what formulas correspond to what physical hypotheses about time. Analogously, we can investigate what formulas of modal logic correspond to what metaphysical hypotheses about necessity. It is widely held that physical hypotheses about time may be contingent. If so, tense-logical validity may be contingent. In contrast, validity in modal logic is typically taken to be non-contingent, as reflected by (...) the general acceptance of the so-called “rule of necessitation.” But as has been argued by various authors in recent years, metaphysical hypotheses may likewise be contingent. If, in particular, hypotheses about the extent of possibility are contingent, we should expect modal-logical validity to be contingent too. Let “contingentism” be the view that everything that is not ruled out by logic is possible. I shall investigate what the right system of modal logic is, if contingentism is true. Given plausible assumptions, the system contains the McKinsey principle, and is thus not even contained in S5. It also contains simple and elegant iteration principles for the contingency operator: something is contingent if and only if it is contingently contingent. (shrink)

Arthur Norman Prior (1914 – 1969) and Georg Henrik von Wright (1916 – 2003) both attended a conference in England sometime in the spring of 1956, after which they corresponded on Anselm’s ontological argument. Prior had at the conference presented a formal treatment of the ontological argument. Based upon notes from the Prior archive at the Bodleian Library, and correspondence with von Wright, we here presents Prior’s and von Wrights’ discussion of Anselm’s argument in light of Prior’s published, as well (...) as unpublished writings on the ontological argument. Three versions of the ontological argument from Prior’s unpublished as well as published papers is presented: a non-modal, an argument from possible existence and finally a modal version. While Prior dismissed the first on the basis of a meta-theorem for proof in argumentation, the second on the basis of a fallacious commutation of operators, he argued that a valid version of the ontological argument can be proven from the distinctive S5 thesis of Lewis modal logic. While Prior gave reasons for a rejection of those distinct S5 thesis, in favour of Lewis S4 system, he also provided a novel argument in favour of accepting the S5 thesis for necessity and possibility. Finally we relate Prior’s work to Plantinga (1974) and consider objections raised by Oppy (2012) and Gale (2007) toward the modal versions of the ontological argument. (shrink)

In [1] Béziau developed the paraconsistent logic Z, which is definitionally equivalent to the modal logic S5, and gave an axiomatization of the logic Z: the system HZ. In the present paper, we prove that some axioms of HZ are not independent and then propose another axiomatization of Z. We also discuss a new perspective on the relation between S5 and classical propositional logic with the help of the new axiomatization of Z. Then we conclude the paper by making (...) a remark on the paraconsistency of HZ. (shrink)

In Kantian philosophy, the term “condition of possibility” is central, but carries the following ambiguity. According to one reading, “condition of possibility” merely means “necessary condition”. However, it is demonstrated that a deeper interpretation of the term “possibility” proves to be more fruitful. This reading allows us to reconstruct an important background assumption of Kant: Every condition of the possibility of experience holds necessarily, provided that experience is possible. Or more generally: All conditions of the possibility hold necessarily as long (...) as the conditioned is actually possible. -/- This conclusion is understood through the axiomatic system S5. Therefore I argue by referencing the schematism chapter that Kant’s notion of modal terms can be formalized through S5. (shrink)

R. Suszko’s Sentential Calculus with Identity \( SCI \) results from classical propositional calculus \( CPC \) by adding a new connective \(\equiv \) and axioms for identity \(\varphi \equiv \psi \) (which we interpret here as ‘propositional identity’). We reformulate the original semantics of \( SCI \) using Boolean prealgebras which, introduced in different ways, are known in the literature as structures for the modeling of (hyper-) intensional semantics. We regard intensionality here as a measure for the discernibility of (...) propositions (and hyperintensionality as a high degree of intensionality). As concrete examples of \( SCI \) -based intensional modeling, we review and study algebraic semantics of some Lewis-style modal logics in the vicinity of \( S3 \) and present conditions under which those modal systems can be restored, in a precise sense, as certain axiomatic extensions of \( SCI \). This generalizes work of Suszko which is focused on the modal systems \( S4 \) and \( S5 \). Our approach is particularly intended as a proposal to consider and to further study \( SCI \) (and its extensions) as a general framework for the modeling of (hyper-) intensional semantics. (shrink)

A propositional system of modal logic is second-order if it contains quantifiers ∀p and ∃p, which, in the standard interpretation, are construed as ranging over sets of possible worlds (propositions). Most second-order systems of modal logic are highly intractable; for instance, when augmented with propositional quantifiers, K, B, T, K4 and S4 all become effectively equivalent to full second-order logic. An exception is S5, which, being interpretable in monadic second-order logic, is decidable.

The article studies knowledge in multiagent systems where data available to the agents may have small errors. To reason about such uncertain knowledge, a formal semantics is introduced in which indistinguishability relations, commonly used in the semantics for epistemic logic S5, are replaced with metrics to capture how much two epistemic worlds are different from an agent’s point of view. The main result is a logical system sound and complete with respect to the proposed semantics.