Ordered from most to least recent.
The modal \(\mu\)-calculus is obtained by adding least and greatest fixed-point operators to modal logic. It's alternation hierarchy classifies the \(\mu\)-formulas by their alternation depth: a measure of the codependence of their least and greatest fixed-point operators. The \(\mu\)-calculus' alternation hierarchy is strict over the class of all Kripke frames: for all \(n\), there is a \(\mu\)-formula with alternation depth \(n+1\) which is not equivalent to any formula with alternation depth \(n\). This does not always happen if we restrict the semantics. For example, every \(\mu\)-formula is equivalent to a formula without fixed-point operators over \(\mathsf{S5}\) frames. We show that the multimodal \(\mu\)-calculus' alternation hierarchy is strict over non-trivial fusions of modal logics. We also comment on two examples of multimodal logics where the \(\mu\)-calculus collapses to modal logic.
Das, van der Giessen, and Marin recently introduced \(\mathsf{IGL}\), an intuitionistic version of Gödel-Löb logic. Their proof systems involves ill-founded proofs with a progressiveness condition. Their completeness proof uses the principle of \(\Sigma^1_1\)-determinacy; which is not provable in \(\mathsf{ZFC}\). We define a cyclic proof system for \(\mathsf{IGL}\) and give a proof of its completeness theorem avoiding \(\Sigma^1_1\)-determinacy.
Feedback Turing machines are Turing machines which can query a halting oracle which has information on the convergence or divergence of feedback computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze? We define \(\alpha\)th order feedback Turing machines for each computable ordinal \(\alpha\). We also describe feedback computable and semi-computable sets using inductive definitions and Gale–Stewart games.
Abstract: It is known that the \(\mu\)-calculus collapses to its alternation-free fragment over transitive frames and to modal logic over equivalence relations. We adapt a proof by D'Agostino and Lenzi to show that the \(\mu\)-calculus collapses to its alternation-free fragment over weakly transitive frames. As a consequence, we show that the \(\mu\)-calculus with derivative topological semantics collapses to its alternation-free fragment. We also study the collapse over frames of \(\mathsf{S4.2}\), \(\mathsf{S4.3}\), \(\mathsf{S4.3.2}\), \(\mathsf{S4.4}\) and \(\mathsf{KD45}\), logics important for Epistemic Logic. At last, we use the \(\mu\)-calculus to define degrees of ignorance on Epistemic Logic and study the implications of \(\mu\)-calculus's collapse over the logics above.
We study a variant of the modal \(\mu\)-calculus based on the constructive modal logic \(\mathsf{CK}\). We define game semantics for the constructive \(\mu\)-calculus and prove its equivalence to the birelational Kripke semantics. We then use the game semantics to prove the soundness and completeness of a fully-labeled non-wellfounded proof system for it. At last, we briefly describe how to adapt the game semantics and proof system to the \(\mu\)-calculus over other non-classical modal logics.
We develop polytopological semantics for various constructive, intuitionistic, and Gödel-Dummett variations of \(\mathsf{K4}\) and \(\mathsf{S4\). In our models, intuitionistic and modal operators are interpreted via various topologies over a single set, equipped with either the closure or derivative operators. We identify regularity conditions to ensure that spaces validate each of our target logics and prove that all the logics considered are sound and strongly complete with respect to their respective semantics.
In this note, we prove that the constructive and intuitionistic variants of the modal logic \(\mathsf{KB}\) coincide. This result contrasts with a recent result by Das and Marin, who showed that the constructive and intuitionistic variants of \(\mathsf{K}\) do not prove the same diamond-free formulas.
We define game semantics for the constructive \(\mu\)-calculus and prove its correctness. We use these game semantics to prove that the \(\mu\)-calculus collapses to modal logic over \(\mathsf{CS5}\) frames. Finally, we prove the completeness of \(\mathsf{\mu CS5}\) over \(\mathsf{CS5}\) frames.
Abstract: It is known that several variations of the axiom of determinacy play important roles in the study of reverse mathematics, and the relation between the hierarchy of determinacy and comprehension are revealed by Tanaka, Nemoto, Montalbán, Shore, and others. We prove variations of a result by Kołodziejczyk and Michalewski relating determinacy of arbitrary boolean combinations of \(\Sigma^0_2\) sets and reflection in second-order arithmetic. Specifically, we prove that: over \(\mathsf{ACA}_0\), \(\Pi^1_2\)-\(\mathsf{Ref}(\mathsf{ACA}_0)\) is equivalent to \(\forall n.(\Sigma^0_1)_n\)-\(\mathsf{Det}^*_0\); \(\Pi^1_3\)-\(\mathsf{Ref}(\Pi^1_1\)-\(\mathsf{CA}_0)\) is equivalent to \(\forall n.(\Sigma^0_1)_n\)-\(\mathsf{Det}\); and \(\Pi^1_3\)-\(\mathsf{Ref}(\Pi^1_2\)-\(\mathsf{CA}_0)\) is equivalent to \(\forall n.(\Sigma^0_2)_n\)-\(\mathsf{Det}\). We also restate results by Montalbán and Shore to show that \(\Pi^1_3\)-\(\mathsf{Ref}(\mathsf{Z}_2)\) is equivalent to \(\forall n.(\Sigma^0_3)_n\)-\(\mathsf{Det}\) over \(\mathsf{ACA}_0\).
Abstract soon.
Abstract soon.
Artemov and Protopopescu defined an intuitionistic epistemic logic IEL to reason about intuitionistic knowledge. While classical knowledge implies classical truth, intuitionistic truth implies intuitionistic knowledge. We describe Artemov and Protopopescu's IEL and its BHK interpretation. We characterize epistemic possibility in IEL.
We survey recent results on reflection in second-order arithmetic. The reflection principles we consider can be roughly divided into two categories: semantic reflection and syntactic reflection.
In this paper, we study one-variable fragments of modal \(\mu\)-calculus and their relations to parity games. We first introduce the weak modal \(\mu\)-calculus as an extension of the one-variable modal \(\mu\)-calculus. We apply weak parity games to show the strictness of the one-variable hierarchy as well as its extension. We also consider games with infinitely many priorities and show that their winning positions can be expressed by both \(\Sigma^\mu_2\) and \(\Pi^\mu_2\) formulas with two variables, but requires a transfinite extension of the \(L_\mu\)-formulas to be expressed with only one variable. At last, we define the \(\mu\)-arithmetic and show that a set of natural numbers is definable by both a \(\Sigma^\mu_2\) and a \(\Pi^\mu_2\) formula of \(\mu\)-arithmetic if and only if it is definable by a formula of the one-variable transfinite \(\mu\)-arithmetic.
Back to main page.