Abstract A propositional system of modal logic issecond-orderif it contains quantifiers ∀pand ∃pwhich, 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. In this paper we generalize this framework by allowing multiple modalities. While this does not affect the undecidability of K, B, T, K4 and S4, poly-modal second-order S5 is dramatically more expressive than its mono-modal counterpart. As an example, we establish the definability of the transitive closure of finitely many modal operators. We also take up the decidability issue, and, using a novel encoding of sets of unordered pairs by partitions of the leaves of certain graphs, we show that the second-order propositional logic of two S5 modalitities is also equivalent to full second-order logic.

Abstract In this paper we introduce the notion of a set algebra satisfying a system E of equations. After defining a notion of freeness for such algebras, we show that, for any system E of equations, set algebras that are free in the class of structures satisfying E exist and are unique up to a bisimulation. Along the way, analogues of classical set-theoretic and algebraic properties are investigated.

Quine's “New Foundations” (NF) was first presented in Quine [10] and later on in Quine [11]. Ernst Specker [15, 13], building upon a previous result of Ehrenfeucht and Mostowski [5], showed that NF is consistent if and only if there is a model of the Theory of Negative (and positive) Types (TNT) with full extensionality that admits of a “shifting automorphism,” but the existence of such a model remains an open problem. In his [8], Ronald Jensen gave a partial solution to the problem of the consistency of Quine's NF. Jensen considered a version of NF—referred to as NFU—in which the axiom of extensionality is weakened to allow forUrelementeor “atoms.” He showed, modifying Specker's theorem, that the existence of a model of TNT with atoms admitting of a “shifting automorphism” implies the consistency of NFU, proceeding then to exhibit such a model. This paper presents a reduction of the consistency problem for NF to the existence of a model of TNT with atoms containing certain “large” (unstratified) sets and admitting a shifting automorphism. In particular we show that such a model can be “collapsed” to a model ofpureTNT in such a way as to preserve the shifting automorphism. By the above-mentioned result of Specker's, this implies the consistency of NF. Let us take the time to explain the main ideas behind the construction. Suppose we have a certain universeUof sets, built up from certain individuals or “atoms.” In such a universe we have only a weak version of the axiom of extensionality: two objects are the same if and only if they are both sets having the same members. We would like to obtain a universeU′that is as close toUas possible, but in which there are no atoms (i.e., the only memberless object is the empty set). One way of doing this is to assign to each atom ξ, aset a(perhaps the empty set), inductively identifying sets that have members that we are already committed to considering “the same.” In doing this we obtain an equivalence relation ≃ overUthat interacts nicely with the membership relation (provided we have accounted for multiplicity of members, i.e., we have allowed sets to contain “multiple copies” of the same object). Then we can takeU′=U/≃, the quotient ofUwith respect to ≃. It is then possible to define a “membership” relation overU′in such a way as to have full extensionality. Relations such as ≃ are referred to as “contractions” by Hinnion and “bisimulations” by Aczel.

In this paper, we are going to present a new notion of “extension” for defeasible inheritance networks that allows us to deal with cyclic nets. Horty has shown that cyclic nets need not have extensions in the sense of Touretzky. This paper presents a generalization of that notion of extension that can be applied to cyclic nets. The present proposal is inspired by a somewhat unexpected analogy between cyclic nets and “semantically closed” languages, i.e., languages containing their own truth predicate. Accordingly, this approach to defeasible inheritance networks with cycles shows similarities to the solution of semantic paradoxes put forth by Kripke.