We show that Pitts' modeling of propositional quantification in intuitionistic logic (as the appropriate interpolants) does not coincide with the topological interpretation. This contrasts with the case of the monadic language and the interpretation over sufficiently regular topological spaces. We also point to the difference between the topological interpretation over sufficiently regular spaces and the interpretation of propositional quantifiers in Kripke models.

The Moral Law is fulfilled iff everything that ought to be the case is the case, and The Good is realised in a possible world w at a time t iff w is deontically accessible from w at t. In this paper, I will introduce a set of temporal modal deontic systems with propositional quantifiers that can be used to prove some interesting theorems about The Moral Law and The Good. First, I will describe a set of systems without any (...) propositional quantifiers. Then, I will show how these systems can be extended by a couple of propositional quantifiers. I will use a kind of TxW semantics to describe the systems semantically and semantic tableaux to describe them syntactically. Every system will include a constant · that stands for The Good. ‘·’ is read as ‘The Good is realised’. All systems that contain the propositional quantifiers will also include a constant '*' that stands for The Moral Law. '*' is read as ‘The Moral Law is fulfilled’. I will prove that all systems (without the propositional quantifiers) are sound and complete with respect to their semantics 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)

In this paper, I will develop a set of boulesic-doxastic tableau systems and prove that they are sound and complete. Boulesic-doxastic logic consists of two main parts: a boulesic part and a doxastic part. By ‘boulesic logic’ I mean ‘the logic of the will’, and by ‘doxastic logic’ I mean ‘the logic of belief’. The first part deals with ‘boulesic’ concepts, expressions, sentences, arguments and theorems. I will concentrate on two types of boulesic expression: ‘individual x wants it to be (...) the case that’ and ‘individual x accepts that it is the case that’. The second part deals with ‘doxastic’ concepts, expressions, sentences, arguments and theorems. I will concentrate on two types of doxastic expression: ‘individual x believes that’ and ‘it is imaginable to individual x that’. Boulesic-doxastic logic investigates how these concepts are related to each other. Boulesic logic is a new kind of logic. Doxastic logic has been around for a while, but the approach to this branch of logic in this paper is new. Each system is combined with modal logic with two kinds of modal operators for historical and absolute necessity and predicate logic with necessary identity and ‘possibilist’ quantifiers. I use a kind of possible world semantics to describe the systems semantically. I also sketch out how our basic language can be extended with propositional quantifiers. All the systems developed in this paper are new. (shrink)

Fine and Kripke extended S5, S4, S4.2 and such to produce propositionally quantified systems , , : given a Kripke frame, the quantifiers range over all the sets of possible worlds. is decidable and, as Fine and Kripke showed, many of the other systems are recursively isomorphic to second-order logic. In the present paper I consider the propositionally quantified system that arises from the topological semantics for S4, rather than from the Kripke semantics. The topological system, which I dub , (...) is strictly weaker than its Kripkean counterpart. I prove here that second-order arithmetic can be recursively embedded in . In the course of the investigation, I also sketch a proof of Fine's and Kripke's results that the Kripkean system is recursively isomorphic to second-order logic. (shrink)

This article concerns the treatment of propositional quantification in a framework of labelled natural deduction for modal logic developed by Basin, Matthews and Viganò. We provide a detailed analysis of a basic calculus that can be used for a proof-theoretic rendering of minimal normal multimodal systems with quantification over stable domains of propositions. Furthermore, we consider variations of the basic calculus obtained via relational theories and domain theories allowing for quantification over possibly unstable domains of propositions. The main result of (...) the article is that fragments of the labelled calculi not exploiting reductio ad absurdum enjoy the Church–Rosser property and the strong normalization property; such result is obtained by combining Girard’s method of reducibility candidates and labelled languages of lambda calculus codifying the structure of modal proofs. (shrink)

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)

Sentences about logic are often used to show that certain embedding expressions are hyperintensional. Yet it is not clear how to regiment “logic talk” in the object language so that it can be compositionally embedded under such expressions. In this paper, I develop a formal system called hyperlogic that is designed to do just that. I provide a hyperintensional semantics for hyperlogic that doesn’t appeal to logically impossible worlds, as traditionally understood, but instead uses a shiftable parameter that determines the (...) interpretation of the logical connectives. I argue this semantics compares favorably to the more common impossible worlds semantics, which faces difficulties interpreting propositionally quantified logic talk. (shrink)

In two of the earliest papers on extending modal logic with propositional quantifiers, R. A. Bull and K. Fine studied a modal logic S5Π extending S5 with axioms and rules for propositional quantification. Surprisingly, there seems to have been no proof in the literature of the completeness of S5Π with respect to its most natural algebraic semantics, with propositional quantifiers interpreted by meets and joins over all elements in a complete Boolean algebra. In this note, we give such a proof. (...) This result raises the question: For which normal modal logics L can one axiomatize the quantified propositional modal logic determined by the complete modal algebras for L? (shrink)

In two of the earliest papers on extending modal logic with propositional quantifiers, R. A. Bull and K. Fine studied a modal logic S5Π extending S5 with axioms and rules for propositional quantification. Surprisingly, there seems to have been no proof in the literature of the completeness of S5Π with respect to its most natural algebraic semantics, with propositional quantifiers interpreted by meets and joins over all elements in a complete Boolean algebra. In this note, we give such a proof. (...) This result raises the question: For which normal modal logics. (shrink)

Predicates are term-to-sentence devices, and operators are sentence-to-sentence devices. What Kaplan and Montague's Paradox of the Knower demonstrates is that necessity and other modalities cannot be treated as predicates, consistent with arithmetic; they must be treated as operators instead. Such is the current wisdom.A number of previous pieces have challenged such a view by showing that a predicative treatment of modalities neednot raise the Paradox of the Knower. This paper attempts to challenge the current wisdom in another way as well: (...) to show that mere appeal to modal operators in the sense of sentence-to-sentence devices is insufficient toescape the Paradox of the Knower. A family of systems is outlined in which closed formulae can encode other formulae and in which the diagonal lemma and Paradox of the Knower are thereby demonstrable for operators in this sense. (shrink)

The Routley-Meyer relational semantics for relevant logics is extended to give a sound and complete model theory for many propositionally quantified relevant logics (and some non-relevant ones). This involves a restriction on which sets of worlds are admissible as propositions, and an interpretation of propositional quantification that makes ∀ pA true when there is some true admissible proposition that entails all p -instantiations of A . It is also shown that without the admissibility qualification many of the systems considered are (...) semantically incomplete, including all those that are sub-logics of the quantified version of Anderson and Belnap’s system E of entailment, extended by the mingle axiom and the Ackermann constant t . The incompleteness proof involves an algebraic semantics based on atomless complete Boolean algebras. (shrink)

Propositional quantifiers are added to a propositional modal language with two modal operators. The resulting language is interpreted over so-called products of Kripke frames whose accessibility relations are equivalence relations, letting propositional quantifiers range over the powerset of the set of worlds of the frame. It is first shown that full second-order logic can be recursively embedded in the resulting logic, which entails that the two logics are recursively isomorphic. The embedding is then extended to all sublogics containing the logic (...) of so-called fusions of frames with equivalence relations. This generalizes a result due to Antonelli and Thomason, who construct such an embedding for the logic of such fusions. (shrink)

Propositional modal logic over relational frames is naturally extended with propositional quantifiers by letting them range over arbitrary sets of worlds of the relevant frame. This is also known as second-order propositional modal logic. The propositionally quantified modal logic of a class of relational frames is often not axiomatizable, although there are known exceptions, most notably the case of frames validating the strong modal logic$\mathrm {S5}$. Here, we develop new general methods with which many of the open questions in this (...) area can be answered. We illustrate the usefulness of these methods by applying them to a range of examples, which provide a detailed picture of which normal modal logics define classes of relational frames whose propositionally quantified modal logic is axiomatizable. We also apply these methods to establish new results in the multimodal case. (shrink)

In this paper I shall present some of the results I have obtained on modal theories which contain quantifiers for propositions. The paper is in two parts: in the first part I consider theories whose non-quantificational part is S5; in the second part I consider theories whose non-quantificational part is weaker than or not contained in S5. Unless otherwise stated, each theory has the same language L. This consists of a countable set V of propositional variables pl, pa, ... , (...) the operators v (or), ~ (not) and □ (necessarily), the universal quantifier (p), p a propositional variable, and brackets ( and ). The formulas of L are then defined in the usual way. (shrink)

This paper is part of a general programme of developing and investigating particular first- order modal theories. In the paper, a modal theory of propositions is constructed under the assumption that there are genuinely singular propositions, ie. ones that contain individuals as constituents. Various results on decidability, axiomatizability and definability are established.

We consider extending the modal logic KD45, commonly taken as the baseline system for belief, with propositional quantifiers that can be used to formalize natural language sentences such as “everything I believe is true” or “there is something that I neither believe nor disbelieve.” Our main results are axiomatizations of the logics with propositional quantifiers of natural classes of complete Boolean algebras with an operator validating KD45. Among them is the class of complete, atomic, and completely multiplicative BAOs validating KD45. (...) Hence, by duality, we also cover the usual method of adding propositional quantifiers to normal modal logics by considering their classes of Kripke frames. In addition, we obtain decidability for all the concrete logics we discuss. (shrink)

We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible.

We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory.

This chapter presents a new semantics for inductive empirical knowledge. The epistemic agent is represented concretely as a learner who processes new inputs through time and who forms new beliefs from those inputs by means of a concrete, computable learning program. The agent’s belief state is represented hyper-intensionally as a set of time-indexed sentences. Knowledge is interpreted as avoidance of error in the limit and as having converged to true belief from the present time onward. Familiar topics are re-examined within (...) the semantics, such as inductive skepticism, the logic of discovery, Duhem’s problem, the articulation of theories by auxiliary hypotheses, the role of serendipity in scientific knowledge, Fitch’s paradox, deductive closure of knowability, whether one can know inductively that one knows inductively, whether one can know inductively that one does not know inductively, and whether expert instruction can spread common inductive knowledge—as opposed to mere, true belief—through a community of gullible pupils. (shrink)

Special issue: "Reflecting on the Legacy of C.I. Lewis: Contemporary and Historical Perspectives on Modal Logic".

The paper sketches an analysis of the notion of a self-fulfilling belief in terms of doxastic modal logic. We point out a connection between self-fulfilling beliefs and Moore’s paradox. Then we look at self-fulfilling beliefs in the context of neighborhood semantics. We argue that the analysis of several interesting self-fulfilling beliefs has to make essential use of propositional quantification.

Given the frequency of human error, it seems rational to believe that some of our own rational beliefs are false. This is the axiom of epistemic modesty. Unfortunately, using standard propositional quantification, and the usual relational semantics, this axiom is semantically inconsistent with a common logic for rational belief, namely KD45. Here we explore two alternative semantics for KD45 and the axiom of epistemic modesty. The first uses the usual relational semantics and bisimulation quantifiers. The second uses a topological semantics (...) and standard propositional quantification. We show the two different semantics validate many of the same formulas, though we do not know whether they validate exactly the same formulas. Along the way we address various philosophical concerns. (shrink)

A logic is called higher order if it allows for quantification over higher order objects, such as functions of individuals, relations between individuals, functions of functions, relations between functions, etc. Higher order logic began with Frege, was formalized in Russell [46] and Whitehead and Russell [52] early in the previous century, and received its canonical formulation in Church [14].1 While classical type theory has since long been overshadowed by set theory as a foundation of mathematics, recent decades have shown remarkable (...) comebacks in the fields of mechanized reasoning (see, e.g., Benzm¨. (shrink)

Scroggs's theorem on the extensions of S5 is an early landmark in the modern mathematical studies of modal logics. From it, we know that the lattice of normal extensions of S5 is isomorphic to the inverse order of the natural numbers with infinity and that all extensions of S5 are in fact normal. In this paper, we consider extending Scroggs's theorem to modal logics with propositional quantifiers governed by the axioms and rules analogous to the usual ones for ordinary quantifiers. (...) We call them Π-logics. Taking S5Π, the smallest normal Π-logic extending S5, as the natural counterpart to S5 in Scroggs's theorem, we show that all normal Π-logics extending S5Π are complete with respect to their complete simple S5 algebras, that they form a lattice that is isomorphic to the lattice of the open sets of the disjoint union of two copies of the one-point compactification of N, that they have arbitrarily high Turing-degrees, and that there are non-normal Π-logics extending S5Π. (shrink)