Mathematical Logic at the Institute of Science Tokyo
I'm a postdoctoral researcher at the Institute of Science Tokyo working with Ryo Kashima. My research is focused on non-classical modal logics, with focus on fixed-point and provability logics.
We study \(\mu\mathsf{CK}\), a variant of the modal μ-calculus based on the constructive modal logic \(\mathsf{CK}\). We define game semantics for the constructive μ-calculus and use it to prove the soundness and completeness of a non-wellfounded proof system. We also describe how to adapt the game semantics and proof system to the \(\mu\)-calculus over other non-classical modal logics.
We develop bi-relational and real valued semantics for a Gödel--Dummett--Gödel--Löb Logic \(\mathsf{GGL}\). We study a fully labeled proof system for it in order to obtain its finite model property and decidability. We use the finite model property to show that both semantics have the same validities.
Artemov and Protopopescu introduced IEL, a modal extension of intuitionistic propositional logic with a modal operator K, standing for knowledge. The K operator is governed by two characteristic axioms: P -> KP and KP -> ~~P. We define and study an alternative semantics for IEL where K is evaluated as a constructive diamond. We show completeness and FMP for our semantics. For applications, we have the following: we separate intuitionistic knowledge and intuitionistic belief; we discuss the relation between Glivenko's Theorem and ignorance; we show that in some sense IEL is indeed intuitionistic, but in another sense it is not. (This is joint work with Igor Sedlár, Czech Academy of Science)
\(\mathsf{IGL}\) is an intuitionistic version of the provability logic \(\mathsf{GL}\) using both box and diamond modalities. It was first studied by Das, van der Giessen, and Marin, who provided two ill-founded proof systems and two semantics for this logic. Later, Aguilera and P. defined a cyclic proof system \(\mathsf{cm\ell IGL}\) for \(\mathsf{IGL}\); they also proved that the set of theorems of \(\mathsf{IGL}\) is recursively enumerable.
We define a well-founded labeled proof system \(\mathsf{\omega m\ell IGL}\) for \(\mathsf{IGL}\) characterized by the following \(\omega\)-rule: \[ \frac{x:\Box^n\bot, \mathbf{R}, \Gamma \vdash \Delta \; (\forall n\in\omega)}{\mathbf{R},\Gamma \vdash \Delta}, \] where \(x\) is a label variable. To prove that all valid formulas of \(\mathsf{IGL}\) can be proved using the \(\omega\)-rule, we use a proof search game argument. To show the soundness of the \(\omega\)-rule are valid, we closely analyze the completeness of \(\mathsf{cm\ell IGL}\). Note that an \(\omega\)-rule for classical \(\mathsf{GL}\) was studied by Tanaka.
We comment on behavior of constructive diamonds in three settings. First, we review a result of Das and Marin showing that the diamond-free fragment constructive and intuitionistic variants of the modal logic K do not coincide. Second, we show that the constructive and intuitionistic variants of S5 coincide. Last, we show that diamonds are equivalent to double negation in Artemov and Protopopescu's intuitionistic epistemic logic.
We prove that the constructive and intuitionistic variants of the modal logic \(\mathsf{𝖪𝖡}\) coincide. This result contrasts with a recent result by Das and Marin, who showed that the constructive and intuitionistic variants of \(\mathsf{𝖪}\) do not prove the same diamond-free formulas.
Das, van der Giessen and Marin recently defined an intuitionistic version of the provability logic \(\mathsf{GL}\). They define birelational and predicate semantics and two non-wellfounded proof systems \(\ell\mathsf{IGL}\) and \(m\ell\mathsf{IGL}\). They prove the completeness and soundness of the two proof systems with respect to both semantics. In the proof of the completeness of \(m\ell\mathsf{IGL}\) with respect to the predicate semantics, they use \(\Sigma^1_1\)-determinacy; a statement not provable in \(\mathsf{ZFC}\). We define a cyclic proof system \(c\ell\mathsf{IGL}\) for IGL and prove its completeness with respect to predicate semantics using open determinacy. In particular, this implies that the completeness of \(m\ell\mathsf{IGL}\) does not need \(\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.
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.
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 define a constructive version of the \(\mu\)-calculus by adding least and greatest fixed-point operators to constructive modal logic. We define game semantics for the constructive \(\mu\)-calculus and prove its equivalence to bi-relational Kripke semantics. For applications, we study the logic \(\mu\mathsf{CS5}\), a constructive variation of \(\mathsf{S5}\) with fixed-points operators.
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. This is joint work with Kazuyuki Tanaka. Slides.
It is well-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 (especially the level of \(\Sigma^0_2\) and \(\Sigma^0_3\)) and comprehension axioms are revealed by Tanaka, Nemoto, Montalbán, Shore, and others. In this talk, we show variations of a result by Kołodziejczyk and Michalewski relating determinacy and reflection in second-order arithmetic based on a model-theoretic characterization of the reflection principles. Slides. Video.
More presentations here.
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.
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.
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.
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.
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.
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: 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.
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: 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.
Abstract: 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.
Available here.
Short abstract: In this thesis, we study two problems related to difference hierarchies. The difference hierarchy for a point class \(\Gamma\) classifies the Boolean combinations of sets in \(\Gamma\) by their complexity. Gale–Stewart games play essential roles in both problems.
In the first part of this thesis, we study the \(\mu\)-calculus' alternation hierarchy over various semantics. The \(\mu\)-calculus' alternation hierarchy classifies its formulas by how many interdependent fixed-point operators appear in a given formula. Bradfield showed that the alternation hierarchy is strict over arbitrary frames. This may not happen if we modify the semantics.
We refine Alberucci and Facchini's proof of the collapse to modal logic over equivalence relations to show that the alternation hierarchy collapses to modal logic in bigger classes of frames. We use this characterization to study degrees of ignorance in various epistemic logics. Afterwards, we show that, on graded semantics, constructive semantics and modal logic with impossible worlds, the alternation hierarchy collapses to modal logic over equivalence relations. On the other hand, the alternation hierarchy is strict on multimodal \(\mu\)-calculus over equivalence relations. We also show that current proofs of the collapse do not work on the non-monotone \(\mu\)-calculus. Furthermore, we show that the alternation hierarchy collapses to its alternation-free fragment over weakly transitive frames.
In the second part of this thesis, we study the connection between Gale–Stewart games and reflection principles in second-order arithmetic. Gale–Stewart games have been studied in reverse mathematics since its beginning and are central to descriptive set theory. Sets definable by the \(\mu\)-calculus are exactly the winning regions of Gale–Stewart games whose payoffs are Boolean combinations of \(\Sigma^0_2\) sets.
Kołodziejczyk and Michalewski proved that the determinacy of Boolean combinations of \(\Sigma^0_2\) sets is equivalent to the reflection principle \(\Pi^1_3\)-\(\mathrm{Ref}(\Pi^1_2\)-\(\mathsf{CA}_0)\). We use finite sequences of coded \(\beta\)-models to prove that the determinacy of Boolean combinations of \(\Sigma^0_1\) sets is equivalent to the reflection principle \(\Pi^1_3\)-\(\mathrm{Ref}(\Pi^1_1\)-\(\mathsf{CA}_0)\). We also use the same method to give a new proof of Kołodziejczyk and Michalewski's result. At last, we use a modified version of the method to prove that the determinacy of Boolean combinations of \(\Sigma^0_1\) sets of Cantor space is equivalent to the reflection principle \(\Pi^1_2\)-\(\mathrm{Ref}(\mathsf{ACA}_0)\).
Available here.
In this thesis we present the weak \(\mu\)-calculus and weak \(\mu\)-arithmetic and their alternations hierarchies. We also prove a refinement of a result in Reverse Mathematics related to the \(\mu\)-arithmetic and the determinacy of the finite levels of the difference hierarchy of \(\Sigma^0_2\).
Mail: leonardovpacheco [at] gmail [dot] com
CV: available here
Mastodon: @leonardopacheco@mathstodon.xyz
Blog: https://leonardopacheco.xyz/blog
This is a picture of me:
